Home
last modified time | relevance | path

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

/dports/math/cvc3/cvc3-2.4.1/src/theory_arith/
H A Dtheory_arith3.cpp1151 bool& isolatedVarOnRHS) in isolateVariable() argument
1198 isolatedVarOnRHS = true; in isolateVariable()
1201 isolatedVarOnRHS = in isolateVariable()
1347 bool isolatedVarOnRHS) in projectInequalities() argument
1368 !isolatedVarOnRHS); in projectInequalities()
1373 isolatedVarOnRHS ? theIneq[1] : theIneq[0]; in projectInequalities()
1380 updateSubsumptionDB(theIneq, isolatedVarOnRHS, subsumed); in projectInequalities()
1399 isolatedVarOnRHS ? d_inequalitiesRightDB : d_inequalitiesLeftDB; in projectInequalities()
1403 list->push_back(Ineq(theIneqThm, isolatedVarOnRHS, bestConst)); in projectInequalities()
1423 betaLTt = isolatedVarOnRHS ? theIneqThm : ineqThm; in projectInequalities()
[all …]
H A Dtheory_arith_old.cpp1500 bool& isolatedVarOnRHS) in isolateVariable() argument
1555 isolatedVarOnRHS = true; in isolateVariable()
1558 isolatedVarOnRHS = in isolateVariable()
1711 bool isolatedVarOnRHS) in projectInequalities() argument
1715 ", isolatedVarOnRHS="+string(isolatedVarOnRHS? "true" : "false") in projectInequalities()
1739 Expr isolatedMonomial = isolatedVarOnRHS ? theIneq[1] : theIneq[0]; in projectInequalities()
1745 const FreeConst& bestConst = updateSubsumptionDB(theIneq, isolatedVarOnRHS, subsumed); 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()
[all …]
/dports/math/cvc3/cvc3-2.4.1/src/include/
H A Dtheory_arith3.h246 void projectInequalities(const Theorem& theInequality,bool isolatedVarOnRHS);
H A Dtheory_arith_new.h196 void projectInequalities(const Theorem& theInequality,bool isolatedVarOnRHS);
H A Dtheory_arith_old.h273 void projectInequalities(const Theorem& theInequality,bool isolatedVarOnRHS);