Home
last modified time | relevance | path

Searched refs:normKind (Results 1 – 1 of 1) sorted by relevance

/dports/math/cvc4/CVC4-1.7/src/theory/arith/
H A Dtheory_arith_private.cpp5542 Kind normKind = negated ? negateKind(atomKind) : atomKind; in decomposeLiteral() local
5544 if(normKind == GEQ || normKind == GT){ in decomposeLiteral()
5546 normKind = (normKind == GEQ) ? LEQ : LT; in decomposeLiteral()
5552 << lit << "(" << normKind << "*" << dir << ")"<< endl in decomposeLiteral()
5564 if(normKind == LT){ in decomposeLiteral()
5569 k = normKind; in decomposeLiteral()