Home
last modified time | relevance | path

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

/dports/math/cvc3/cvc3-2.4.1/src/theory_arith/
H A Darith_theorem_producer.cpp1642 const Expr& isIntaExpr = isInta.getExpr(); in finiteInterval() local
1644 CHECK_SOUND(isIntPred(isIntaExpr) && isIntaExpr[0] == e1[0], in finiteInterval()
1646 +e1.toString()+"\n isInta = "+isIntaExpr.toString()); in finiteInterval()
H A Darith_theorem_producer3.cpp1599 const Expr& isIntaExpr = isInta.getExpr(); in finiteInterval() local
1601 CHECK_SOUND(isIntPred(isIntaExpr) && isIntaExpr[0] == e1[0], in finiteInterval()
1603 +e1.toString()+"\n isInta = "+isIntaExpr.toString()); in finiteInterval()
H A Darith_theorem_producer_old.cpp1797 const Expr& isIntaExpr = isInta.getExpr(); in finiteInterval() local
1799 CHECK_SOUND(isIntPred(isIntaExpr) && isIntaExpr[0] == e1[0], in finiteInterval()
1801 +e1.toString()+"\n isInta = "+isIntaExpr.toString()); in finiteInterval()