Home
last modified time | relevance | path

Searched refs:itePos (Results 1 – 3 of 3) sorted by relevance

/dports/math/cvc3/cvc3-2.4.1/src/sat/
H A Dcnf_theorem_producer.cpp208 Theorem CNF_TheoremProducer::ifLiftRule(const Expr& e, int itePos) { in ifLiftRule() argument
213 CHECK_SOUND(itePos >= 0, "itePos negative"+int2string(itePos)); in ifLiftRule()
214 CHECK_SOUND(e.arity() > itePos && e[itePos].isITE(), in ifLiftRule()
218 const Expr& ite = e[itePos]; in ifLiftRule()
232 k1[itePos] = t1; in ifLiftRule()
235 k1[itePos] = t2; in ifLiftRule()
242 pf = newPf("if_lift_rule", e, resultITE, d_em->newRatExpr(itePos)); in ifLiftRule()
H A Dcnf_rules.h57 virtual Theorem ifLiftRule(const Expr& e, int itePos) = 0;
H A Dcnf_theorem_producer.h49 Theorem ifLiftRule(const Expr& e, int itePos);