Searched refs:theIneqThm (Results 1 – 2 of 2) sorted by relevance
| /dports/math/cvc3/cvc3-2.4.1/src/theory_arith/ |
| H A D | theory_arith3.cpp | 1359 Theorem theIneqThm(theInequality); in projectInequalities() local
1360 Expr theIneq = theIneqThm.getExpr(); in projectInequalities()
1369 theIneqThm = canonPred(iffMP(theIneqThm, thm)); in projectInequalities()
1370 theIneq = theIneqThm.getExpr(); in projectInequalities()
1395 theoryCore()->setupTerm(theIneq[0], this, theIneqThm); in projectInequalities()
1396 theoryCore()->setupTerm(theIneq[1], this, theIneqThm); in projectInequalities()
1403 list->push_back(Ineq(theIneqThm, isolatedVarOnRHS, bestConst)); in projectInequalities()
1407 ((*it1).second)->push_back(Ineq(theIneqThm, isolatedVarOnRHS, bestConst)); in projectInequalities()
1423 betaLTt = isolatedVarOnRHS ? theIneqThm : ineqThm; in projectInequalities()
1424 tLTalpha = isolatedVarOnRHS ? ineqThm : theIneqThm; in projectInequalities()
|
| H A D | theory_arith_old.cpp | 1725 Theorem theIneqThm(theInequality); in projectInequalities() local
1726 Expr theIneq = theIneqThm.getExpr(); in projectInequalities()
1734 theIneqThm = canonPred(iffMP(theIneqThm, thm)); in projectInequalities()
1735 theIneq = theIneqThm.getExpr(); in projectInequalities()
1760 theoryCore()->setupTerm(theIneq[0], this, theIneqThm); in projectInequalities()
1761 theoryCore()->setupTerm(theIneq[1], this, theIneqThm); in projectInequalities()
1767 list->push_back(Ineq(theIneqThm, isolatedVarOnRHS, bestConst)); in projectInequalities()
1771 ((*it1).second)->push_back(Ineq(theIneqThm, isolatedVarOnRHS, bestConst)); in projectInequalities()
1789 betaLTt = isolatedVarOnRHS ? theIneqThm : ineqThm; in projectInequalities()
1790 tLTalpha = isolatedVarOnRHS ? ineqThm : theIneqThm; in projectInequalities()
|