Home
last modified time | relevance | path

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

/dports/math/cvc3/cvc3-2.4.1/src/include/
H A Dtheory_arith3.h58 Ineq(const Theorem& ineq, bool varOnRHS, const FreeConst& c): in Ineq() argument
59 d_ineq(ineq), d_rhs(varOnRHS), d_const(&c) { } in Ineq()
65 bool varOnRHS() const { return d_rhs; } in varOnRHS() function
144 const Rational& freeConstIneq(const Expr& ineq, bool varOnRHS);
152 const FreeConst& updateSubsumptionDB(const Expr& ineq, bool varOnRHS,
H A Dtheory_arith_old.h61 Ineq(const Theorem& ineq, bool varOnRHS, const FreeConst& c): in Ineq() argument
62 d_ineq(ineq), d_rhs(varOnRHS), d_const(&c) { } in Ineq()
68 bool varOnRHS() const { return d_rhs; } in varOnRHS() function
168 const Rational& freeConstIneq(const Expr& ineq, bool varOnRHS);
176 const FreeConst& updateSubsumptionDB(const Expr& ineq, bool varOnRHS,
H A Dtheory_arith_new.h73 Ineq(const Theorem& ineq, bool varOnRHS, const FreeConst& c): in Ineq() argument
74 d_ineq(ineq), d_rhs(varOnRHS), d_const(&c) { } in Ineq()
80 bool varOnRHS() const { return d_rhs; } in varOnRHS() function
/dports/math/cvc3/cvc3-2.4.1/src/theory_arith/
H A Dtheory_arith3.cpp56 << (ineq.varOnRHS()? "RHS" : "LHS") << ", const = " in operator <<()
95 const Expr& e = varOnRHS? ineq[0] : ineq[1]; in freeConstIneq()
114 ", var isolated on "+string(varOnRHS? "RHS" : "LHS")+")"); in updateSubsumptionDB()
119 const Expr& t = varOnRHS? ineq[0] : ineq[1]; in updateSubsumptionDB()
137 if(varOnRHS) in updateSubsumptionDB()
143 if(varOnRHS) in updateSubsumptionDB()
164 if(varOnRHS) { in updateSubsumptionDB()
1062 bool varOnRHS; in processBuffer() local
1069 Theorem thm1 = isolateVariable(ineqThm, varOnRHS); in processBuffer()
1079 projectInequalities(thm1, varOnRHS); in processBuffer()
[all …]
H A Dtheory_arith_old.cpp58 << (ineq.varOnRHS()? "RHS" : "LHS") << ", const = " in operator <<()
100 const Expr& e = varOnRHS? ineq[0] : ineq[1]; in freeConstIneq()
116 TheoryArithOld::updateSubsumptionDB(const Expr& ineq, bool varOnRHS, in updateSubsumptionDB() argument
119 ", var isolated on "+string(varOnRHS? "RHS" : "LHS")+")"); in updateSubsumptionDB()
124 const Expr& t = varOnRHS? ineq[0] : ineq[1]; in updateSubsumptionDB()
143 if(varOnRHS) in updateSubsumptionDB()
149 if(varOnRHS) in updateSubsumptionDB()
170 if(varOnRHS) { in updateSubsumptionDB()
1040 bool varOnRHS; in processBuffer() local
1137 projectInequalities(thm1, varOnRHS); in processBuffer()
[all …]
H A Dtheory_arith_new.cpp56 << (ineq.varOnRHS()? "RHS" : "LHS") << ", const = " in operator <<()
1359 DebugAssert((*ratsLTe)[i].varOnRHS(), "variable on wrong side!"); in findBounds()