Home
last modified time | relevance | path

Searched refs:canonMultConstConst (Results 1 – 8 of 8) sorted by relevance

/dports/math/cvc3/cvc3-2.4.1/src/theory_arith/
H A Darith_proof_rules.h109 virtual Theorem canonMultConstConst(const Expr& c1, const Expr& c2) = 0;
H A Darith_theorem_producer.h170 virtual Theorem canonMultConstConst(const Expr& c1, const Expr& c2);
H A Darith_theorem_producer_old.h169 virtual Theorem canonMultConstConst(const Expr& c1, const Expr& c2);
H A Darith_theorem_producer3.h169 virtual Theorem canonMultConstConst(const Expr& c1, const Expr& c2);
H A Dtheory_arith_new.cpp3695 Theorem canonLeft = d_rules->canonMultConstConst(thm.getExpr()[0][0], thm.getExpr()[0][1]); in getLowerBoundExplanation()
3713 Theorem canonLeft = d_rules->canonMultConstConst(thm.getExpr()[0][0], thm.getExpr()[0][1]); in getLowerBoundExplanation()
3787 Theorem canonLeft = d_rules->canonMultConstConst(thm.getExpr()[0][0], thm.getExpr()[0][1]); in getUpperBoundExplanation()
3808 Theorem canonLeft = d_rules->canonMultConstConst(thm.getExpr()[0][0], thm.getExpr()[0][1]); in getUpperBoundExplanation()
H A Darith_theorem_producer.cpp605 return canonMultConstConst(e1,e2); in canonMultMtermMterm()
983 ArithTheoremProducer::canonMultConstConst(const Expr& c1, const Expr& c2) { in canonMultConstConst() function in ArithTheoremProducer
H A Darith_theorem_producer3.cpp576 return canonMultConstConst(e1,e2); in canonMultMtermMterm()
969 ArithTheoremProducer3::canonMultConstConst(const Expr& c1, const Expr& c2) { in canonMultConstConst() function in ArithTheoremProducer3
H A Darith_theorem_producer_old.cpp577 return canonMultConstConst(e1,e2); in canonMultMtermMterm()
1019 ArithTheoremProducerOld::canonMultConstConst(const Expr& c1, const Expr& c2) { in canonMultConstConst() function in ArithTheoremProducerOld