Searched refs:inequalityFind (Results 1 – 1 of 1) sorted by relevance
| /dports/math/cvc3/cvc3-2.4.1/src/theory_arith/ |
| H A D | theory_arith_old.cpp | 1071 Expr inequalityFind = inequalityFindThm.getExpr(); in processBuffer() local
1076 TRACE("arith buffer", "with find : ", inequalityFind, ""); in processBuffer()
1078 if (!isIneq(inequalityFind)) { in processBuffer()
1083 if (alreadyProjected.find(inequalityFind) != alreadyProjected.end()) { in processBuffer()
1094 if (inequality != inequalityFind) { in processBuffer()
1096 alreadyProjected[inequalityFind] = dummy; in processBuffer()
1098 Expr rhs = inequalityFind[1]; in processBuffer()
1116 extractTermsFromInequality(inequalityFind, c1, t1, c2, t2); in processBuffer()
1118 …TRACE("arith ineq", "skipping because stronger bounds asserted ", inequalityFind.toString(), ":" +… in processBuffer()
|