| /dports/math/cvc3/cvc3-2.4.1/src/theory_arith/ |
| H A D | arith_proof_rules.h | 278 const Theorem& isIntLHS,
282 virtual Theorem lessThanToLERewrite(const Expr& ineq, const Theorem& isIntLHS,
|
| H A D | arith_theorem_producer.h | 278 Theorem lessThanToLE(const Theorem& less, const Theorem& isIntLHS,
281 Theorem lessThanToLERewrite(const Expr& ineq, const Theorem& isIntLHS,
|
| H A D | arith_theorem_producer_old.h | 277 Theorem lessThanToLE(const Theorem& less, const Theorem& isIntLHS,
280 Theorem lessThanToLERewrite(const Expr& ineq, const Theorem& isIntLHS,
|
| H A D | arith_theorem_producer3.h | 277 Theorem lessThanToLE(const Theorem& less, const Theorem& isIntLHS,
280 Theorem lessThanToLERewrite(const Expr& ineq, const Theorem& isIntLHS,
|
| H A D | arith_theorem_producer.cpp | 2086 const Theorem& isIntLHS, in lessThanToLE() argument
2090 const Expr& isIntLHSexpr = isIntLHS.getExpr(); in lessThanToLE()
2108 thms.push_back(isIntLHS); in lessThanToLE()
2119 pfs.push_back(isIntLHS.getProof()); in lessThanToLE()
3153 const Theorem& isIntLHS, in lessThanToLERewrite() argument
3157 const Expr& isIntLHSexpr = isIntLHS.getExpr(); in lessThanToLERewrite()
3174 thms.push_back(isIntLHS); in lessThanToLERewrite()
3181 pfs.push_back(isIntLHS.getProof()); in lessThanToLERewrite()
|
| H A D | arith_theorem_producer3.cpp | 2044 const Theorem& isIntLHS, in lessThanToLE() argument
2048 const Expr& isIntLHSexpr = isIntLHS.getExpr(); in lessThanToLE()
2066 thms.push_back(isIntLHS); in lessThanToLE()
2076 pfs.push_back(isIntLHS.getProof()); in lessThanToLE()
3104 const Theorem& isIntLHS, in lessThanToLERewrite() argument
3108 const Expr& isIntLHSexpr = isIntLHS.getExpr(); in lessThanToLERewrite()
3125 thms.push_back(isIntLHS); in lessThanToLERewrite()
3132 pfs.push_back(isIntLHS.getProof()); in lessThanToLERewrite()
|
| H A D | theory_arith_old.cpp | 818 Theorem isIntLHS = isIntegerThm(x); in processSimpleIntEq() local
838 result = d_rules->eqElimIntRule(result, isIntLHS, isIntRHS); in processSimpleIntEq()
1730 Theorem isIntLHS(isIntegerThm(theIneq[0])); in projectInequalities() local
1732 if ((!isIntLHS.isNull() && !isIntRHS.isNull())) { in projectInequalities()
1733 Theorem thm = d_rules->lessThanToLE(theInequality, isIntLHS, isIntRHS, !isolatedVarOnRHS); in projectInequalities()
3276 Theorem isIntLHS(isIntegerThm(theIneq[0])); in rewrite() local
3278 bool isInt = (!isIntLHS.isNull() && !isIntRHS.isNull()); in rewrite()
3281 transitivityRule(thm, d_rules->lessThanToLERewrite(theIneq, isIntLHS, isIntRHS, true))); in rewrite()
3314 Theorem isIntLHS(isIntegerThm(theIneq[0])); in rewrite() local
3316 bool isInt = (!isIntLHS.isNull() && !isIntRHS.isNull()); in rewrite()
[all …]
|
| H A D | arith_theorem_producer_old.cpp | 2246 const Theorem& isIntLHS, in lessThanToLE() argument
2250 const Expr& isIntLHSexpr = isIntLHS.getExpr(); in lessThanToLE()
2268 thms.push_back(isIntLHS); in lessThanToLE()
2278 pfs.push_back(isIntLHS.getProof()); in lessThanToLE()
3417 const Theorem& isIntLHS, in lessThanToLERewrite() argument
3421 const Expr& isIntLHSexpr = isIntLHS.getExpr(); in lessThanToLERewrite()
3438 thms.push_back(isIntLHS); in lessThanToLERewrite()
3445 pfs.push_back(isIntLHS.getProof()); in lessThanToLERewrite()
|
| H A D | theory_arith3.cpp | 838 Theorem isIntLHS = isIntegerThm(x); in processSimpleIntEq() local
858 result = d_rules->eqElimIntRule(result, isIntLHS, isIntRHS); in processSimpleIntEq()
1362 Theorem isIntLHS(isIntegerThm(theIneq[0])); in projectInequalities() local
1364 bool isInt = (!isIntLHS.isNull() && !isIntRHS.isNull()); in projectInequalities()
1367 Theorem thm = d_rules->lessThanToLE(theInequality, isIntLHS, isIntRHS, in projectInequalities()
|
| H A D | theory_arith_new.cpp | 594 Theorem isIntLHS = isIntegerThm(x); in processSimpleIntEq() local
614 result = d_rules->eqElimIntRule(result, isIntLHS, isIntRHS); in processSimpleIntEq()
|