Home
last modified time | relevance | path

Searched refs:multEqZero (Results 1 – 9 of 9) sorted by relevance

/dports/math/cvc3/cvc3-2.4.1/src/theory_arith/
H A Darith_proof_rules.h126 virtual Theorem multEqZero(const Expr& expr) = 0;
H A Darith_theorem_producer.h188 virtual Theorem multEqZero(const Expr& expr);
H A Darith_theorem_producer_old.h187 virtual Theorem multEqZero(const Expr& expr);
H A Darith_theorem_producer3.h187 virtual Theorem multEqZero(const Expr& expr);
H A Dtheory_arith3.cpp470 enqueueFact(iffMP(eqnThm, d_rules->multEqZero(eqnThm.getExpr()))); in doSolve()
480 enqueueFact(iffMP(eqnThm, d_rules->multEqZero(eqnThm.getExpr()))); in doSolve()
H A Dtheory_arith_old.cpp487 enqueueFact(iffMP(eqnThm, d_rules->multEqZero(eqnThm.getExpr()))); in doSolve()
497 enqueueFact(iffMP(eqnThm, d_rules->multEqZero(eqnThm.getExpr()))); in doSolve()
3162 Theorem eq_thm = d_rules->multEqZero(nonlinearEq); in rewrite()
H A Darith_theorem_producer.cpp1155 Theorem ArithTheoremProducer::multEqZero(const Expr& expr) in multEqZero() function in ArithTheoremProducer
H A Darith_theorem_producer3.cpp1142 Theorem ArithTheoremProducer3::multEqZero(const Expr& expr) in multEqZero() function in ArithTheoremProducer3
H A Darith_theorem_producer_old.cpp1192 Theorem ArithTheoremProducerOld::multEqZero(const Expr& expr) in multEqZero() function in ArithTheoremProducerOld