Home
last modified time | relevance | path

Searched refs:rewriteIteElse (Results 1 – 4 of 4) sorted by relevance

/dports/math/cvc3/cvc3-2.4.1/src/theory_core/
H A Dcore_theorem_producer.h57 Theorem rewriteIteElse(const Expr& e, const Theorem& elseThm);
H A Dcore_proof_rules.h60 virtual Theorem rewriteIteElse(const Expr& e, const Theorem& elseThm) = 0;
H A Dexpr_transform.cpp398 thm = d_commonRules->transitivityRule(thm, d_rules->rewriteIteElse(newExpr, thm2)); in newPPrec()
H A Dcore_theorem_producer.cpp161 CoreTheoremProducer::rewriteIteElse(const Expr& e, const Theorem& elseThm) { in rewriteIteElse() function in CoreTheoremProducer