Searched refs:resultITE (Results 1 – 2 of 2) sorted by relevance
| /dports/math/cvc3/cvc3-2.4.1/src/sat/ |
| H A D | cnf_theorem_producer.cpp | 238 Expr resultITE = cond.iteExpr(pred1, pred2); in ifLiftRule() local
242 pf = newPf("if_lift_rule", e, resultITE, d_em->newRatExpr(itePos)); in ifLiftRule()
243 return newRWTheorem(e, resultITE, Assumptions::emptyAssump(), pf); in ifLiftRule()
|
| /dports/math/cvc3/cvc3-2.4.1/src/theory_core/ |
| H A D | core_theorem_producer.cpp | 609 Expr resultITE = cond.iteExpr(e1, e2); in ifLiftUnaryRule() local
614 return newRWTheorem(e, resultITE, Assumptions::emptyAssump(), pf); in ifLiftUnaryRule()
|