Home
last modified time | relevance | path

Searched refs:canonInvert (Results 1 – 7 of 7) sorted by relevance

/dports/math/cvc3/cvc3-2.4.1/src/theory_arith/
H A Darith_proof_rules.h96 virtual Theorem canonInvert(const Expr & e) = 0;
H A Darith_theorem_producer.h144 virtual Theorem canonInvert(const Expr & e);
H A Darith_theorem_producer_old.h143 virtual Theorem canonInvert(const Expr & e);
H A Darith_theorem_producer3.h143 virtual Theorem canonInvert(const Expr & e);
H A Darith_theorem_producer.cpp873 Expr result = canonInvert(e[0]).getRHS(); in canonInvertMult()
876 canonMultMtermMterm(result * canonInvert(e[i]).getRHS()).getRHS(); in canonInvertMult()
885 ArithTheoremProducer::canonInvert(const Expr& e) in canonInvert() function in ArithTheoremProducer
921 Theorem thm = newRWTheorem(e, e[0]*(canonInvert(e[1]).getRHS()), Assumptions::emptyAssump(), pf); in canonDivide()
H A Darith_theorem_producer3.cpp827 Expr result = canonInvert(e[0]).getRHS(); in canonInvertMult()
830 canonMultMtermMterm(result * canonInvert(e[i]).getRHS()).getRHS(); in canonInvertMult()
839 ArithTheoremProducer3::canonInvert(const Expr& e) in canonInvert() function in ArithTheoremProducer3
916 Theorem thm = newRWTheorem(e, e[0]*(canonInvert(e[1]).getRHS()), Assumptions::emptyAssump(), pf); in canonDivide()
H A Darith_theorem_producer_old.cpp877 Expr result = canonInvert(e[0]).getRHS(); in canonInvertMult()
880 canonMultMtermMterm(result * canonInvert(e[i]).getRHS()).getRHS(); in canonInvertMult()
889 ArithTheoremProducerOld::canonInvert(const Expr& e) in canonInvert() function in ArithTheoremProducerOld
966 Theorem thm = newRWTheorem(e, e[0]*(canonInvert(e[1]).getRHS()), Assumptions::emptyAssump(), pf); in canonDivide()