Home
last modified time | relevance | path

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

/dports/math/cvc3/cvc3-2.4.1/src/include/
H A Dtheory_arith3.h162 Theorem canonSimplify(const Expr& e);
167 Theorem canonSimplify(const Theorem& thm) { in canonSimplify() function
168 return transitivityRule(thm, canonSimplify(thm.getRHS())); in canonSimplify()
H A Dtheory_arith_new.h151 Theorem canonSimplify(const Expr& e);
155 Theorem canonSimplify(const Theorem& thm) { in canonSimplify() function
156 return transitivityRule(thm, canonSimplify(thm.getRHS())); in canonSimplify()
H A Dtheory_arith_old.h186 Theorem canonSimplify(const Expr& e);
191 Theorem canonSimplify(const Theorem& thm) { in canonSimplify() function
192 return transitivityRule(thm, canonSimplify(thm.getRHS())); in canonSimplify()
/dports/math/cvc3/cvc3-2.4.1/src/theory_arith/
H A Dtheory_arith3.cpp360 TheoryArith3::canonSimplify(const Expr& e) { in canonSimplify() function in TheoryArith3
395 thms.push_back(canonSimplify(e[0])); in canonPred()
396 thms.push_back(canonSimplify(e[1])); in canonPred()
409 thms.push_back(canonSimplify(e[0])); in canonPredEquiv()
410 thms.push_back(canonSimplify(e[1])); in canonPredEquiv()
H A Dtheory_arith_new.cpp246 Theorem TheoryArithNew::canonSimplify(const Expr& e) { in canonSimplify() function in TheoryArithNew
284 thms.push_back(canonSimplify(e[0])); in canonPred()
285 thms.push_back(canonSimplify(e[1])); in canonPred()
306 thms.push_back(canonSimplify(e[0])); in canonPredEquiv()
307 thms.push_back(canonSimplify(e[1])); in canonPredEquiv()
H A Dtheory_arith_old.cpp144 index = leExpr(rat(0), canonSimplify(ineq[1] - newT).getRHS()); in updateSubsumptionDB()
146 index = leExpr(canonSimplify(ineq[0]-newT).getRHS(), rat(0)); in updateSubsumptionDB()
371 TheoryArithOld::canonSimplify(const Expr& e) { in canonSimplify() function in TheoryArithOld
406 thms.push_back(canonSimplify(e[0])); in canonPred()
407 thms.push_back(canonSimplify(e[1])); in canonPred()
422 thms.push_back(canonSimplify(e[0])); in canonPredEquiv()
423 thms.push_back(canonSimplify(e[1])); in canonPredEquiv()