Searched defs:isIntRHS (Results 1 – 6 of 6) sorted by relevance
2087 const Theorem& isIntRHS, in lessThanToLE()3123 Theorem ArithTheoremProducer::simpleIneqInt(const Expr& ineq, const Theorem& isIntRHS) in simpleIneqInt()3154 const Theorem& isIntRHS, in lessThanToLERewrite()
2045 const Theorem& isIntRHS, in lessThanToLE()3073 Theorem ArithTheoremProducer3::simpleIneqInt(const Expr& ineq, const Theorem& isIntRHS) in simpleIneqInt()3105 const Theorem& isIntRHS, in lessThanToLERewrite()
819 vector<Theorem> isIntRHS; in processSimpleIntEq() local1731 Theorem isIntRHS(isIntegerThm(theIneq[1])); in projectInequalities() local3277 Theorem isIntRHS(isIntegerThm(theIneq[1])); in rewrite() local3315 Theorem isIntRHS(isIntegerThm(theIneq[1])); in rewrite() local
839 vector<Theorem> isIntRHS; in processSimpleIntEq() local1363 Theorem isIntRHS(isIntegerThm(theIneq[1])); in projectInequalities() local
1508 Theorem ArithTheoremProducerOld::simpleIneqInt(const Expr& ineq, const Theorem& isIntRHS) in simpleIneqInt()2247 const Theorem& isIntRHS, in lessThanToLE()3418 const Theorem& isIntRHS, in lessThanToLERewrite()
595 vector<Theorem> isIntRHS; in processSimpleIntEq() local