30 #define _CVC3_TRUSTED_
52 #define CLASS_NAME "ArithTheoremProducer"
57 if(withProof()) pf = newPf(
"var_to_mult", e);
58 return newRWTheorem(e, (rat(1) * e), Assumptions::emptyAssump(), pf);
67 if(withProof()) pf = newPf(
"uminus_to_mult", e);
70 return newRWTheorem((-e), (rat(-1) * e), Assumptions::emptyAssump(), pf);
80 if (withProof()) pf = newPf(
"minus_to_plus", x, y);
83 return newRWTheorem((x-y), (x + (rat(-1) * y)), Assumptions::emptyAssump(), pf);
89 Theorem ArithTheoremProducer::canonUMinusToDivide(
const Expr& e) {
91 if(withProof()) pf = newPf(
"canon_uminus", e);
92 return newRWTheorem((-e), (e / rat(-1)), Assumptions::emptyAssump(), pf);
103 CLASS_NAME "::canonDivideConst:\n c not a constant: "
106 CLASS_NAME "::canonDivideConst:\n d not a constant: "
111 pf = newPf(
"canon_divide_const", c, d, d_hole);
113 return newRWTheorem((c/d), (rat(dr==0? 0 : (c.
getRational()/dr))), Assumptions::emptyAssump(), pf);
123 "Not a (c * x) expression: "
127 "d is not a constant: " + d.
toString());
130 Rational cdr(dr==0? 0 : (cx[0].getRational()/dr));
134 pf = newPf(
"canon_divide_mult", cx[0], cx[1], d);
137 return newRWTheorem((cx/d), (cx[1]), Assumptions::emptyAssump(), pf);
139 return newRWTheorem((cx/d), cd, Assumptions::emptyAssump(), pf);
141 return newRWTheorem((cx/d), (cd*cx[1]), Assumptions::emptyAssump(), pf);
149 "Expr is not a canonical sum: "
153 "d is not a const: " + d.
toString());
158 pf = newPf(
"canon_divide_plus", rat(sum.
arity()),
160 vector<Expr> newKids;
162 newKids.push_back((*i)/d);
164 return newRWTheorem((sum/d), (
plusExpr(newKids)), Assumptions::emptyAssump(), pf);
172 "d is not a const: " + d.
toString());
177 pf = newPf(
"canon_divide_var", e);
181 return newRWTheorem(e/d, e, Assumptions::emptyAssump(), pf);
183 return newRWTheorem(e/d, d, Assumptions::emptyAssump(), pf);
185 return newRWTheorem(e/d, rat(1/dr) * e, Assumptions::emptyAssump(), pf);
203 Expr ArithTheoremProducer::simplifiedMultExpr(std::vector<Expr> & mulKids) {
206 DebugAssert(mulKids.size() >= 1 && mulKids[0].isRational(),
"");
209 if (mulKids.size() == 1)
return mulKids[0];
214 Expr ArithTheoremProducer::canonMultConstMult(
const Expr & c,
const Expr & e) {
220 DebugAssert ((e.
arity() > 1) && (e[0].
isRational()),
"arith_theorem_producer::canonMultConstMult: a canonized MULT expression must have \
221 arity greater than 1: and first child must be rational " + e.
toString());
224 std::vector<Expr> mulKids;
228 mulKids.push_back(rat(c.
getRational() * (*i).getRational()));
230 for(i ++; i != e.
end(); i ++)
231 mulKids.push_back(*i);
234 return simplifiedMultExpr(mulKids);
237 Expr ArithTheoremProducer::canonMultConstPlus(
const Expr & e1,
const Expr & e2) {
243 std::vector<Theorem> thmPlusVector;
247 thmPlusVector.push_back(canonMultMtermMterm(e1*(*i)));
250 Theorem thmPlus1 = d_theoryArith->substitutivityRule(e2.
getOp(), thmPlusVector);
256 Expr ArithTheoremProducer::canonMultPowPow(
const Expr & e1,
264 if (leaf1 == leaf2) {
269 else if (rsum == 1) {
274 return powExpr(rat(rsum), leaf1);
279 std::vector<Expr> mulKids;
280 mulKids.push_back(rat(1));
283 mulKids.push_back(e2);
284 mulKids.push_back(e1);
288 mulKids.push_back(e1);
289 mulKids.push_back(e2);
292 return simplifiedMultExpr(mulKids);
296 Expr ArithTheoremProducer::canonMultPowLeaf(
const Expr & e1,
304 if (leaf1 == leaf2) {
309 else if (rsum == 1) {
314 return powExpr(rat(rsum), leaf1);
319 std::vector<Expr> mulKids;
320 mulKids.push_back(rat(1));
323 mulKids.push_back(e2);
324 mulKids.push_back(e1);
328 mulKids.push_back(e1);
329 mulKids.push_back(e2);
331 return simplifiedMultExpr(mulKids);
335 Expr ArithTheoremProducer::canonMultLeafLeaf(
const Expr & e1,
342 if (leaf1 == leaf2) {
347 std::vector<Expr> mulKids;
348 mulKids.push_back(rat(1));
351 mulKids.push_back(e2);
352 mulKids.push_back(e1);
356 mulKids.push_back(e1);
357 mulKids.push_back(e2);
359 return simplifiedMultExpr(mulKids);
363 Expr ArithTheoremProducer::canonMultLeafOrPowMult(
const Expr & e1,
372 std::vector<Expr> mulKids;
376 mulKids.push_back(*i);
379 for(; i != e2.
end(); ++i) {
380 Expr leaf2 = ((*i).getKind() ==
POW) ? (*i)[1] : (*i);
381 if (leaf1 == leaf2) {
384 ((*i).getKind() ==
POW ? (*i)[0].getRational() : 1);
389 mulKids.push_back(leaf1);
393 mulKids.push_back(
powExpr(rat(r1 + r2), leaf1));
402 else if (leaf2 < leaf1) {
403 mulKids.push_back(e1);
404 mulKids.push_back(*i);
408 mulKids.push_back(*i);
411 mulKids.push_back(e1);
416 for (++i; i != e2.
end(); ++i) {
417 mulKids.push_back(*i);
420 return simplifiedMultExpr(mulKids);
428 return ArithTheoremProducer::greaterthan(e1,e2);
434 Expr ArithTheoremProducer::canonCombineLikeTerms(
const std::vector<Expr> & sumExprs) {
438 vector<Expr> sumKids;
441 std::vector<Expr>::const_iterator i = sumExprs.begin();
442 std::vector<Expr>::const_iterator i_end = sumExprs.end();
443 for (; i != i_end; i++) {
458 DebugAssert(mul.
arity() > 1 && mul[0].
isRational(),
"If sum term is multiplication it must have the first term a rational, and at least another one");
464 vector<Expr> newKids;
473 MonomMap::iterator i = sumHashMap.find(newMul);
476 if (i == sumHashMap.end()) sumHashMap[newMul] = r;
478 else (*i).second += r;
487 MonomMap::iterator i = sumHashMap.find(
multExpr(rat(1), mul));
490 if (i == sumHashMap.end()) sumHashMap[
multExpr(rat(1), mul)] = 1;
491 else (*i).second += 1;
501 if (constant != 0) sumKids.push_back(rat(constant));
504 MonomMap::iterator j = sumHashMap.begin(), jend=sumHashMap.end();
505 for(; j != jend; j++) {
507 if ((*j).second != 0) {
509 vector<Expr> newKids;
511 for(
Expr::iterator m = (*j).first.begin(); m != (*j).first.end(); m ++) newKids.push_back(*m);
513 newKids[0] = rat((*j).second);
515 sumKids.push_back(
multExpr(newKids));
520 if (constant != 0 && sumKids.size() == 1)
return sumKids[0];
523 if (constant == 0 && sumKids.size() == 1)
return sumKids[0];
526 if (constant == 0 && sumKids.size() == 0)
return rat(0);
532 Expr ArithTheoremProducer::canonMultLeafOrPowOrMultPlus(
const Expr & e1,
542 std::vector<Expr> sumExprs;
545 for (; i != e2.
end(); ++i) {
546 sumExprs.push_back(canonMultMtermMterm(e1 * (*i)).getRHS());
548 return canonCombineLikeTerms(sumExprs);
551 Expr ArithTheoremProducer::canonMultPlusPlus(
const Expr & e1,
558 std::vector<Expr> sumExprs;
561 for (; i != e1.
end(); ++i) {
563 for (; j != e2.
end(); ++j) {
564 sumExprs.push_back(canonMultMtermMterm((*i) * (*j)).getRHS());
567 return canonCombineLikeTerms(sumExprs);
574 Theorem ArithTheoremProducer::canonMultMtermMterm(
const Expr& e) {
588 const Expr& e1 = e[0];
589 const Expr& e2 = e[1];
592 string cmmm =
"canon_mult_mterm_mterm";
598 return canonMultZero(e2);
600 return canonMultOne(e2);
605 return canonMultConstConst(e1,e2);
611 return d_theoryArith->reflexivityRule (e);
615 rhs = canonMultConstMult(e1,e2);
616 if(withProof()) pf = newPf(cmmm,e,rhs);
617 return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
620 rhs = canonMultConstPlus(e1,e2);
621 if(withProof()) pf = newPf(cmmm,e,rhs);
622 return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
627 return d_theoryArith->reflexivityRule(e);
636 return canonMultMtermMterm(e2 * e1);
639 rhs = canonMultPowPow(e1,e2);
640 if(withProof()) pf = newPf(cmmm,e,rhs);
641 return newRWTheorem(e,rhs, Assumptions::emptyAssump(), pf);
644 rhs = canonMultLeafOrPowMult(e1,e2);
645 if(withProof()) pf = newPf(cmmm,e,rhs);
646 return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
649 rhs = canonMultLeafOrPowOrMultPlus(e1,e2);
650 if(withProof()) pf = newPf(cmmm,e,rhs);
651 return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
654 rhs = canonMultPowLeaf(e1,e2);
655 if(withProof()) pf = newPf(cmmm,e,rhs);
656 return newRWTheorem(e,rhs, Assumptions::emptyAssump(), pf);
665 return canonMultMtermMterm(e2 * e1);
672 for (; i != e1.end(); ++i) {
673 result = canonMultMtermMterm((*i) * result).getRHS();
675 if(withProof()) pf = newPf(cmmm,e,result);
676 return newRWTheorem(e, result, Assumptions::emptyAssump(), pf);
680 rhs = canonMultLeafOrPowOrMultPlus(e1,e2);
681 if(withProof()) pf = newPf(cmmm,e,rhs);
682 return newRWTheorem(e,rhs, Assumptions::emptyAssump(), pf);
687 return canonMultMtermMterm(e2 * e1);
697 return canonMultMtermMterm(e2 * e1);
700 rhs = canonMultPlusPlus(e1,e2);
701 if(withProof()) pf = newPf(cmmm,e,rhs);
702 return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
707 return canonMultMtermMterm(e2 * e1);
716 return canonMultMtermMterm(e2 * e1);
719 rhs = canonMultPowLeaf(e2,e1);
720 if(withProof()) pf = newPf(cmmm,e,rhs);
721 return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
724 rhs = canonMultLeafOrPowMult(e1,e2);;
725 if(withProof()) pf = newPf(cmmm,e,rhs);
726 return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
729 rhs = canonMultLeafOrPowOrMultPlus(e1,e2);
730 if(withProof()) pf = newPf(cmmm,e,rhs);
731 return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
735 rhs = canonMultLeafLeaf(e1,e2);
736 if(withProof()) pf = newPf(cmmm,e,rhs);
737 return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
742 return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
755 std::vector<Expr> sumKids;
757 for(; i != e.
end(); ++i) {
758 if ((*i).getKind() !=
PLUS)
759 sumKids.push_back(*i);
763 for(; j != (*i).end(); ++j)
764 sumKids.push_back(*j);
769 Expr val = canonCombineLikeTerms(sumKids);
773 pf = newPf(
"canon_plus", e, val);
777 return newRWTheorem(e, val, Assumptions::emptyAssump(), pf);
799 for (; i != e.
end(); ++i) {
801 result = canonMultMtermMterm(result * (*i)).getRHS();
806 pf = newPf(
"canon_mult", e,result);
810 return newRWTheorem(e, result, Assumptions::emptyAssump(), pf);
815 ArithTheoremProducer::canonInvertConst(
const Expr& e)
823 pf = newPf(
"canon_invert_const", e);
826 return newRWTheorem((rat(1)/e), rat(er==0? 0 : (1/er)), Assumptions::emptyAssump(), pf);
831 ArithTheoremProducer::canonInvertLeaf(
const Expr& e)
836 pf = newPf(
"canon_invert_leaf", e);
838 return newRWTheorem((rat(1)/e),
powExpr(rat(-1), e), Assumptions::emptyAssump(), pf);
843 ArithTheoremProducer::canonInvertPow(
const Expr& e)
850 pf = newPf(
"canon_invert_pow", e);
852 if (e[0].getRational() == -1)
853 return newRWTheorem((rat(1)/e), e[1], Assumptions::emptyAssump(), pf);
855 return newRWTheorem((rat(1)/e),
856 powExpr(rat(-e[0].getRational()), e),
857 Assumptions::emptyAssump(),
862 ArithTheoremProducer::canonInvertMult(
const Expr& e)
869 pf = newPf(
"canon_invert_mult", e);
873 Expr result = canonInvert(e[0]).getRHS();
874 for (
int i = 1; i < e.
arity(); ++i) {
876 canonMultMtermMterm(result * canonInvert(e[i]).getRHS()).getRHS();
878 return newRWTheorem((rat(1)/e), result, Assumptions::emptyAssump(), pf);
885 ArithTheoremProducer::canonInvert(
const Expr& e)
888 "Cannot do inverse on a PLUS"+e.
toString());
891 return canonInvertConst(e);
894 return canonInvertPow(e);
897 return canonInvertMult(e);
901 return canonInvertLeaf(e);
917 pf = newPf(
"canon_invert_divide", e);
921 Theorem thm = newRWTheorem(e, e[0]*(canonInvert(e[1]).getRHS()), Assumptions::emptyAssump(), pf);
924 return d_theoryArith->transitivityRule(thm, canonMult(thm.
getRHS()));
931 ArithTheoremProducer::canonMultTermConst(
const Expr& c,
const Expr& t) {
936 "c is not a constant: " + c.
toString());
938 if(withProof()) pf = newPf(
"canon_mult_term_const", c, t);
939 return newRWTheorem((t*c), (c*t), Assumptions::emptyAssump(), pf);
945 ArithTheoremProducer::canonMultTerm1Term2(
const Expr& t1,
const Expr& t2) {
949 CHECK_SOUND(
false,
"Fatal Error: We don't support multiplication"
950 "of two non constant terms at this time "
960 if(withProof()) pf = newPf(
"canon_mult_zero", e);
961 return newRWTheorem((rat(0)*e), rat(0), Assumptions::emptyAssump(), pf);
971 if(withProof()) pf = newPf(
"canon_mult_one", e);
974 if (d_theoryArith->isLeaf(e))
return d_theoryArith->reflexivityRule (rat(1)*e);
977 return newRWTheorem((rat(1)*e), e, Assumptions::emptyAssump(), pf);
983 ArithTheoremProducer::canonMultConstConst(
const Expr& c1,
const Expr& c2) {
988 "c1 is not a constant: " + c1.
toString());
991 "c2 is not a constant: " + c2.
toString());
993 if(withProof()) pf = newPf(
"canon_mult_const_const", c1, c2);
995 newRWTheorem((c1*c2), rat(c1.
getRational()*c2.getRational()), Assumptions::emptyAssump(), pf);
1001 ArithTheoremProducer::canonMultConstTerm(
const Expr& c1,
1007 "c1 is not a constant: " + c1.
toString());
1010 "c2 is not a constant: " + c2.
toString());
1013 if(withProof()) pf = newPf(
"canon_mult_const_term", c1, c2, t);
1021 ArithTheoremProducer::canonMultConstSum(
const Expr& c1,
const Expr& sum) {
1023 std::vector<Expr> sumKids;
1028 "c1 is not a constant: " + c1.
toString());
1031 "the kind must be a PLUS: " + sum.
toString());
1034 for(; i != sum.
end(); ++i)
1035 sumKids.push_back(c1*(*i));
1037 if(withProof()) pf = newPf(
"canon_mult_const_sum", c1, sum, ret);
1038 return newRWTheorem((c1*sum),ret , Assumptions::emptyAssump(), pf);
1047 "ArithTheoremProducer::canonPowConst("+e.
toString()+
")");
1053 "ArithTheoremProducer::canonPowConst("+e.
toString()+
")");
1056 if (base == 0 && p < 0) {
1059 else res = rat(
pow(p, base));
1062 pf = newPf(
"canon_pow_const", e);
1063 return newRWTheorem(e, res, Assumptions::emptyAssump(), pf);
1070 ArithTheoremProducer::canonFlattenSum(
const Expr& e) {
1072 std::vector<Expr> sumKids;
1076 "input must be a PLUS:" + e.
toString());
1080 for(; i != e.
end(); ++i){
1081 if (
PLUS != (*i).getKind())
1082 sumKids.push_back(*i);
1085 for(; j != (*i).end(); ++j)
1086 sumKids.push_back(*j);
1090 if(withProof()) pf = newPf(
"canon_flatten_sum", e,ret);
1091 return newRWTheorem(e,ret, Assumptions::emptyAssump(), pf);
1097 ArithTheoremProducer::canonComboLikeTerms(
const Expr& e) {
1099 std::vector<Expr> sumKids;
1105 for(; k != e.
end(); ++k)
1108 "input must be a flattened PLUS:" + k->
toString());
1111 for(; i != e.
end(); ++i){
1116 if(0 == sumHashMap.
count((*i)))
1119 sumHashMap[*i] += 1;
1122 if(0 == sumHashMap.
count((*i)[1]))
1123 sumHashMap[(*i)[1]] = (*i)[0].getRational();
1125 sumHashMap[(*i)[1]] = sumHashMap[(*i)[1]] + (*i)[0].getRational();
1130 sumKids.push_back(rat(constant));
1132 for(; j != sumHashMap.
end(); ++j) {
1133 if(0 == (*j).second)
1135 else if (1 == (*j).second)
1136 sumKids.push_back((*j).first);
1138 sumKids.push_back(rat((*j).second) * (*j).first);
1145 if(2 == sumKids.size() && 0 == constant) ret = sumKids[1];
1146 else if (1 == sumKids.size()) ret = sumKids[0];
1149 if(withProof()) pf = newPf(
"canon_combo_like_terms",e,ret);
1150 return newRWTheorem(e, ret, Assumptions::emptyAssump(), pf);
1161 "multEqZero invariant violated"+expr.
toString());
1166 for (; i != iend; ++i) {
1167 kids.push_back(rat(0).eqExpr(*i));
1170 pf = newPf(
"multEqZero", expr);
1172 return newRWTheorem(expr,
Expr(
OR, kids), Assumptions::emptyAssump(), pf);
1185 "powEqZero invariant violated"+expr.
toString());
1189 pf = newPf(
"powEqZero", expr);
1194 res = d_em->falseExpr();
1197 res = rat(0).
eqExpr(expr[1][1]);
1199 return newRWTheorem(expr, res, Assumptions::emptyAssump(), pf);
1212 expr[0][0] == expr[1][0],
1213 "elimPower invariant violated"+expr.
toString());
1217 pf = newPf(
"elimPower", expr);
1222 res = res.
orExpr(expr[0][1].eqExpr(-expr[1][1]));
1224 return newRWTheorem(expr, res, Assumptions::emptyAssump(), pf);
1238 "elimPowerConst invariant violated"+expr.
toString());
1242 pf = newPf(
"elimPowerConst", expr, rat(root));
1247 res = res.
orExpr(expr[0][1].eqExpr(rat(-root)));
1249 return newRWTheorem(expr, res, Assumptions::emptyAssump(), pf);
1262 "evenPowerEqNegConst invariant violated"+expr.
toString());
1266 pf = newPf(
"evenPowerEqNegConst", expr);
1268 return newRWTheorem(expr, d_em->falseExpr(), Assumptions::emptyAssump(), pf);
1281 ratRoot(expr[1].getRational(), expr[0][0].getRational().getUnsigned()) == 0,
1282 "intEqIrrational invariant violated"+expr.
toString());
1284 "ArithTheoremProducerOld::intEqIrrational:\n "
1285 "wrong integrality constraint:\n expr = "
1292 pf = newPf(
"int_eq_irr", expr, isIntx.
getProof());
1294 return newRWTheorem(expr, d_em->falseExpr(), assump, pf);
1304 "non-const parameters: " + e.
toString());
1312 result = (r1 == r2)?
true :
false;
1315 result = (r1 < r2)?
true :
false;
1318 result = (r1 <= r2)?
true :
false;
1321 result = (r1 > r2)?
true :
false;
1324 result = (r1 >= r2)?
true :
false;
1329 "ArithTheoremProducer::constPredicate: wrong kind");
1333 Expr ret = (result) ? d_em->trueExpr() : d_em->falseExpr();
1334 if(withProof()) pf = newPf(
"const_predicate", e,ret);
1335 return newRWTheorem(e, ret, Assumptions::emptyAssump(), pf);
1350 "ArithTheoremProduder::rightMinusLeft: wrong kind");
1352 if(withProof()) pf = newPf(
"right_minus_left",e);
1353 return newRWTheorem(e,
Expr(e.
getOp(), rat(0), e[1] - e[0]), Assumptions::emptyAssump(), pf);
1367 "ArithTheoremProduder::rightMinusLeft: wrong kind");
1369 if(withProof()) pf = newPf(
"left_minus_right",e);
1370 return newRWTheorem(e,
Expr(e.
getOp(), e[0] - e[1], rat(0)), Assumptions::emptyAssump(), pf);
1378 const Expr& z,
int kind) {
1385 "ArithTheoremProduder::plusPredicate: wrong kind");
1390 if(withProof()) pf = newPf(
"plus_predicate",left,right);
1391 return newRWTheorem(left, right, Assumptions::emptyAssump(), pf);
1401 "ArithTheoremProducer::multEqn(): multiplying equation by 0");
1402 if(withProof()) pf = newPf(
"mult_eqn", x, y, z);
1403 return newRWTheorem(x.
eqExpr(y), (x * z).eqExpr(y * z), Assumptions::emptyAssump(), pf);
1412 if(withProof()) pf = newPf(
"mult_eqn_nonconst", x, y, z);
1414 Assumptions::emptyAssump(), pf);
1435 ret =
Expr(op, e[0]*z, e[1]*z);
1439 case LE: ret =
geExpr(e[0]*z, e[1]*z);
break;
1440 case LT: ret =
gtExpr(e[0]*z, e[1]*z);
break;
1441 case GE: ret =
leExpr(e[0]*z, e[1]*z);
break;
1442 case GT: ret =
ltExpr(e[0]*z, e[1]*z);
break;
1450 if(withProof()) pf = newPf(
"mult_ineqn", e, ret);
1453 return newRWTheorem(e, ret, Assumptions::emptyAssump(), pf);
1503 "ArithTheoremProducer::flipInequality: wrong kind: " +
1509 if(withProof()) pf = newPf(
"flip_inequality", e,ret);
1510 return newRWTheorem(e,ret, Assumptions::emptyAssump(), pf);
1520 const Expr& ineq = e[0];
1523 "ArithTheoremProducer::negatedInequality: wrong kind: " +
1526 "ArithTheoremProducer::negatedInequality: wrong kind: " +
1530 if(withProof()) pf = newPf(
"negated_inequality", e);
1542 return newRWTheorem(e,
Expr(kind, ineq[0], ineq[1]), Assumptions::emptyAssump(), pf);
1555 "ArithTheoremProducer::realShadow: Wrong Kind: " +
1559 "ArithTheoremProducer::realShadow:"
1560 " t must be same for both inputs: " +
1561 expr1[1].toString() +
" , " + expr2[0].toString());
1564 int firstKind = expr1.
getKind();
1565 int secondKind = expr2.
getKind();
1566 int kind = (firstKind == secondKind) ? firstKind :
LT;
1570 pfs.push_back(alphaLTt.
getProof());
1572 pf = newPf(
"real_shadow",expr1, expr2, pfs);
1574 return newTheorem(
Expr(kind, expr1[0], expr2[1]), a, pf);
1589 "ArithTheoremProducer::realShadowLTLE: Wrong Kind: " +
1593 "ArithTheoremProducer::realShadowLTLE:"
1594 " t must be same for both inputs: " +
1598 "ArithTheoremProducer::realShadowLTLE:"
1599 " alpha must be same for both inputs: " +
1606 pfs.push_back(alphaLEt.
getProof());
1607 pfs.push_back(tLEalpha.
getProof());
1608 pf = newPf(
"real_shadow_eq", alphaLEt.
getExpr(), tLEalpha.
getExpr(), pfs);
1610 return newRWTheorem(expr1[0], expr1[1], a, pf);
1614 ArithTheoremProducer::finiteInterval(
const Theorem& aLEt,
1622 "ArithTheoremProducer::finiteInterval:\n e1 = "
1626 "ArithTheoremProducer::finiteInterval:\n e1 = "
1630 "ArithTheoremProducer::finiteInterval:\n e1 = "
1634 "ArithTheoremProducer::finiteInterval:\n e1 = "
1638 && e2[1][1].getRational() >= 1,
1639 "ArithTheoremProducer::finiteInterval:\n e1 = "
1645 "Wrong integrality constraint:\n e1 = "
1646 +e1.
toString()+
"\n isInta = "+isIntaExpr.toString());
1648 "Wrong integrality constraint:\n e1 = "
1651 vector<Theorem> thms;
1652 thms.push_back(aLEt);
1653 thms.push_back(tLEac);
1654 thms.push_back(isInta);
1655 thms.push_back(isIntt);
1663 es.push_back(isInta.
getExpr());
1664 es.push_back(isIntt.
getExpr());
1669 pf = newPf(
"finite_interval", es, pfs);
1672 Expr g(grayShadow(e1[1], e1[0], 0, e2[1][1].getRational()));
1673 return newTheorem(g, a, pf);
1685 const Expr& isIntAlphaExpr = isIntAlpha.
getExpr();
1691 "ArithTheoremProducer::darkGrayShadow2ab: Wrong Kind: " +
1695 const Expr& beta = expr1[0];
1696 const Expr& bx = expr1[1];
1697 const Expr& ax = expr2[0];
1698 const Expr& alpha = expr2[1];
1706 "ArithTheoremProducer::darkGrayShadow2ab:\n "
1707 "wrong integrality constraint:\n alpha = "
1708 +alpha.
toString()+
"\n isIntAlpha = "
1711 "ArithTheoremProducer::darkGrayShadow2ab:\n "
1712 "wrong integrality constraint:\n beta = "
1716 "ArithTheoremProducer::darkGrayShadow2ab:\n "
1717 "wrong integrality constraint:\n x = "
1722 "ArithTheoremProducer::darkGrayShadow2ab:\n ax<=alpha: " +
1725 "ArithTheoremProducer::darkGrayShadow2ab:\n beta<=bx: "
1727 +
"\n ax<=alpha: "+ axLEalpha.
toString());
1729 "ArithTheoremProducer::darkGrayShadow2ab:\n beta<=bx: "
1731 +
"\n ax<=alpha: "+ axLEalpha.
toString());
1733 vector<Theorem> thms;
1734 thms.push_back(betaLEbx);
1735 thms.push_back(axLEalpha);
1736 thms.push_back(isIntAlpha);
1737 thms.push_back(isIntBeta);
1738 thms.push_back(isIntx);
1744 Expr d = darkShadow(rat(a*b-1), t);
1745 Expr g = grayShadow(ax, alpha, -a+1, 0);
1750 exprs.push_back(expr1);
1751 exprs.push_back(expr2);
1756 pfs.push_back(betaLEbx.
getProof());
1757 pfs.push_back(axLEalpha.
getProof());
1758 pfs.push_back(isIntAlpha.
getProof());
1759 pfs.push_back(isIntBeta.
getProof());
1762 pf = newPf(
"dark_grayshadow_2ab", exprs, pfs);
1765 return newTheorem((d || g) && (!d || !g), A, pf);
1776 const Expr& isIntAlphaExpr = isIntAlpha.
getExpr();
1782 "ArithTheoremProducer::darkGrayShadow2ba: Wrong Kind: " +
1786 const Expr& beta = expr1[0];
1787 const Expr& bx = expr1[1];
1788 const Expr& ax = expr2[0];
1789 const Expr& alpha = expr2[1];
1797 "ArithTheoremProducer::darkGrayShadow2ab:\n "
1798 "wrong integrality constraint:\n alpha = "
1799 +alpha.
toString()+
"\n isIntAlpha = "
1802 "ArithTheoremProducer::darkGrayShadow2ab:\n "
1803 "wrong integrality constraint:\n beta = "
1807 "ArithTheoremProducer::darkGrayShadow2ab:\n "
1808 "wrong integrality constraint:\n x = "
1813 "ArithTheoremProducer::darkGrayShadow2ba:\n ax<=alpha: " +
1816 "ArithTheoremProducer::darkGrayShadow2ba:\n beta<=bx: "
1818 +
"\n ax<=alpha: "+ axLEalpha.
toString());
1820 "ArithTheoremProducer::darkGrayShadow2ba:\n beta<=bx: "
1822 +
"\n ax<=alpha: "+ axLEalpha.
toString());
1824 vector<Theorem> thms;
1825 thms.push_back(betaLEbx);
1826 thms.push_back(axLEalpha);
1827 thms.push_back(isIntAlpha);
1828 thms.push_back(isIntBeta);
1829 thms.push_back(isIntx);
1834 pfs.push_back(betaLEbx.
getProof());
1835 pfs.push_back(axLEalpha.
getProof());
1836 pfs.push_back(isIntAlpha.
getProof());
1837 pfs.push_back(isIntBeta.
getProof());
1840 pf = newPf(
"dark_grayshadow_2ba", betaLEbx.
getExpr(),
1847 Expr d = darkShadow(rat(a*b-1), t);
1848 Expr g = grayShadow(bx, beta, 0, b-1);
1849 return newTheorem((d || g) && (!d || !g), A, pf);
1858 "ArithTheoremProducer::expandDarkShadow: not DARK_SHADOW: " +
1863 pf = newPf(
"expand_dark_shadow", theShadow, darkShadow.
getProof());
1873 "ArithTheoremProducer::expandGrayShadowConst0:"
1874 " not GRAY_SHADOW: " +
1877 "ArithTheoremProducer::expandGrayShadow0: c1!=c2: " +
1881 if(withProof()) pf = newPf(
"expand_gray_shadowconst0", theShadow,
1883 const Expr& v = theShadow[0];
1884 const Expr& e = theShadow[1];
1898 "ArithTheoremProducer::expandGrayShadowConst: not a shadow" +
1907 "ArithTheoremProducer::expandGrayShadow: " +
1911 const Expr& v = theShadow[0];
1912 const Expr& e = theShadow[1];
1916 Expr g1(grayShadow(v, e, c1, c));
1917 Expr g2(grayShadow(v, e, c+1, c2));
1921 exprs.push_back(theShadow);
1922 exprs.push_back(g1);
1923 exprs.push_back(g2);
1924 pf = newPf(
"split_gray_shadow", exprs, gThm.
getProof());
1935 "ArithTheoremProducer::expandGrayShadowConst: not a shadow" +
1944 "ArithTheoremProducer::expandGrayShadow: " +
1948 const Expr& v = theShadow[0];
1949 const Expr& e = theShadow[1];
1953 pf = newPf(
"expand_gray_shadow", theShadow, gThm.
getProof());
1962 ArithTheoremProducer::expandGrayShadowConst(
const Theorem& gThm) {
1964 const Expr& ax = theShadow[0];
1965 const Expr& cExpr = theShadow[1];
1966 const Expr& bExpr = theShadow[2];
1970 "ArithTheoremProducer::expandGrayShadowConst: "
1971 "'a' in a*x is not a const: " +theShadow.
toString());
1978 "ArithTheoremProducer::expandGrayShadowConst: "
1979 "not a GRAY_SHADOW: " +theShadow.
toString());
1981 "ArithTheoremProducer::expandGrayShadowConst: "
1982 "'a' is not integer: " +theShadow.
toString());
1984 "ArithTheoremProducer::expandGrayShadowConst: "
1985 "'c' is not rational" +theShadow.
toString());
1987 "ArithTheoremProducer::expandGrayShadowConst: b not integer: "
1993 Rational j = constRHSGrayShadow(c,b,a);
2005 pf = newPf(
"expand_gray_shadow_const_0", theShadow,
2007 conc = newTheorem(d_em->falseExpr(), assump, pf);
2008 }
else if(bAbs < a+j) {
2010 pf = newPf(
"expand_gray_shadow_const_1", theShadow,
2012 conc = newRWTheorem(ax, rat(c+b-signB*j), assump, pf);
2015 pf = newPf(
"expand_gray_shadow_const", theShadow,
2018 conc = newTheorem(ax.
eqExpr(rat(c+b-signB*j)).
orExpr(newGrayShadow),
2027 ArithTheoremProducer::grayShadowConst(
const Theorem& gThm) {
2035 const Expr& ax = g[0];
2036 const Expr& e = g[1];
2040 d_theoryArith->separateMonomial(ax, aExpr, x);
2044 "ArithTheoremProducer::grayShadowConst("+g.
toString()+
")");
2046 "ArithTheoremProducer::grayShadowConst("+g.
toString()+
")");
2054 "ArithTheoremProducer::grayShadowConst("+g.
toString()+
")");
2057 Rational newC1 = ceil((c1+c)/a), newC2 = floor((c2+c)/a);
2058 Expr newG((newC1 > newC2)? d_em->falseExpr()
2059 : grayShadow(x, rat(0), newC1, newC2));
2062 pf = newPf(
"gray_shadow_const", g, newG, gThm.
getProof());
2074 "ArithTheoremProducer::constRHSGrayShadow: a, b, c must be ints");
2078 return mod(a-(c+b), a);
2095 "ArithTheoremProducer::LTtoLE: ineq must be <");
2098 "ArithTheoremProducer::lessThanToLE: bad integrality check:\n"
2099 " ineq = "+ineq.
toString()+
"\n isIntLHS = "
2102 "ArithTheoremProducer::lessThanToLE: bad integrality check:\n"
2103 " ineq = "+ineq.
toString()+
"\n isIntRHS = "
2106 vector<Theorem> thms;
2107 thms.push_back(less);
2108 thms.push_back(isIntLHS);
2109 thms.push_back(isIntRHS);
2112 Expr le = changeRight?
2113 leExpr(ineq[0], ineq[1] + rat(-1))
2114 :
leExpr(ineq[0] + rat(1), ineq[1]);
2119 pfs.push_back(isIntLHS.
getProof());
2120 pfs.push_back(isIntRHS.
getProof());
2121 pf = newPf(changeRight?
"lessThan_To_LE_rhs" :
"lessThan_To_LE_lhs",
2125 return newRWTheorem(ineq, le, a, pf);
2138 ArithTheoremProducer::intVarEqnConst(
const Expr& eqn,
2149 "ArithTheoremProducer::intVarEqnConst: "
2150 "rhs has a wrong format: " + right.
toString());
2152 "ArithTheoremProducer:intVarEqnConst:left is not a zero: " +
2160 d_theoryArith->separateMonomial(right, aExpr, x);
2165 d_theoryArith->separateMonomial(right[1], aExpr, x);
2170 "ArithTheoremProducer:intVarEqnConst: "
2171 "bad integrality constraint:\n right = " +
2172 right.
toString()+
"\n isIntx = "+isIntxexpr.toString());
2173 CHECK_SOUND(a!=0,
"ArithTheoremProducer:intVarEqnConst: eqn = "
2179 pf = newPf(
"int_const_eq", eqn, isIntx.
getProof());
2185 return newRWTheorem(eqn, x.
eqExpr(rat(r)), assump, pf);
2187 return newRWTheorem(eqn, d_em->falseExpr(), assump, pf);
2192 ArithTheoremProducer::create_t(
const Expr& eqn) {
2193 const Expr& lhs = eqn[0];
2197 const Expr& x = lhs[1];
2202 sumModM(kids, eqn[1], m, m);
2204 kids.push_back(monomialModM(eqn[1], m, m));
2206 kids.push_back(
multExpr(rat(1/m), x));
2211 ArithTheoremProducer::create_t2(
const Expr& lhs,
const Expr& rhs,
2212 const Expr& sigma) {
2217 sumModM(kids, rhs, m, -1);
2219 kids.push_back(rat(0));
2220 Expr monom = monomialModM(rhs, m, -1);
2222 kids.push_back(monom);
2226 kids.push_back(rat(m)*sigma);
2231 ArithTheoremProducer::create_t3(
const Expr& lhs,
const Expr& rhs,
2232 const Expr& sigma) {
2238 sumMulF(kids, rhs, m, 1);
2240 kids.push_back(rat(0));
2241 Expr monom = monomialMulF(rhs, m, 1);
2243 kids.push_back(monom);
2247 kids.push_back(rat(-a)*sigma);
2255 Rational res((i - m*(floor((i/m) + half))));
2264 return (floor(i/m + half)+modEq(i,m));
2268 ArithTheoremProducer::sumModM(vector<Expr>& summands,
const Expr& sum,
2270 DebugAssert(divisor != 0,
"ArithTheoremProducer::sumModM: divisor = "
2275 C = modEq(C,m)/divisor;
2276 summands.push_back(rat(C));
2279 Expr monom = monomialModM(*i, m, divisor);
2281 summands.push_back(monom);
2288 ArithTheoremProducer::monomialModM(
const Expr& i,
2291 DebugAssert(divisor != 0,
"ArithTheoremProducer::monomialModM: divisor = "
2296 ai = modEq(ai,m)/divisor;
2297 if(0 == ai) res = rat(0);
2298 else if(1 == ai && i.
arity() == 2) res = i[1];
2300 vector<Expr> kids = i.
getKids();
2306 if(1 == ai) res = i;
2307 else res = rat(ai)*i;
2309 DebugAssert(!res.isNull(),
"ArithTheoremProducer::monomialModM()");
2311 +
", div="+divisor.
toString()+
") = ", res,
"");
2316 ArithTheoremProducer::sumMulF(vector<Expr>& summands,
const Expr& sum,
2318 DebugAssert(divisor != 0,
"ArithTheoremProducer::sumMulF: divisor = "
2324 summands.push_back(rat(C));
2327 Expr monom = monomialMulF(*i, m, divisor);
2329 summands.push_back(monom);
2336 ArithTheoremProducer::monomialMulF(
const Expr& i,
2339 DebugAssert(divisor != 0,
"ArithTheoremProducer::monomialMulF: divisor = "
2343 ai = f(ai,m)/divisor;
2344 if(0 == ai)
return rat(0);
2345 if(1 == ai)
return xi;
2357 i = eMap.
find(term);
2363 i = eMap.
find(term[1]);
2365 return term[0]*(*i).second;
2371 vector<Expr> output;
2373 output.push_back(substitute(*j, eMap));
2379 bool ArithTheoremProducer::greaterthan(
const Expr & l,
const Expr & r)
2382 if (l==r)
return false;
2401 ((r[1]==l[1]) && (r[0].getRational() < l[0].
getRational())));
2407 if (r[1] == l)
return false;
2408 return greaterthan(l, r[1]);
2416 return ((r < l[1]) || ((r == l[1]) && l[0].getRational() > 1));
2431 return ((l[1] == r) || greaterthan(l[1], r));
2441 for (; i != l.
end() && j != r.
end(); ++i, ++j) {
2444 return greaterthan(*i,*j);
2465 return ((l[1] == r) || greaterthan(l[1], r));
2480 return ((r[1] < l) || ((r[1] == l) && (r[0].getRational() < 1)));
2485 if (l == r[1])
return false;
2486 return greaterthan(l,r[1]);
2510 "Expected IS_INTEGER predicate");
2513 DebugAssert(!d_theoryArith->isInteger(expr),
"Expected non-integer");
2520 pf = newPf(
"isIntElim", isIntx.
getProof());
2523 Expr newVar = d_em->newBoundVarExpr(d_theoryArith->intType());
2526 return newTheorem(res, a, pf);
2532 const vector<Theorem>& isIntVars) {
2533 TRACE(
"arith eq",
"eqElimIntRule(", eqn.
getExpr(),
") {");
2538 "ArithTheoremProducer::eqElimInt: input must be an equation" +
2544 d_theoryArith->separateMonomial(lhs, a, x);
2550 "ArithTheoremProducer::eqElimInt\n eqn = "
2552 +
"\n isIntx = "+isIntxe.
toString());
2555 "ArithTheoremProducer::eqElimInt:\n lhs = "+lhs.
toString());
2559 "ArithTheoremProducer::eqElimInt:\n rhs = "+rhs.
toString());
2563 d_theoryArith->separateMonomial(rhs, c, v);
2566 && isIntVars[0].getExpr()[0] == v
2568 "ArithTheoremProducer::eqElimInt:\n rhs = "+rhs.
toString()
2569 +
"isIntVars.size = "+
int2string(isIntVars.size()));
2572 "ArithTheoremProducer::eqElimInt: rhs = "+rhs.
toString());
2575 "ArithTheoremProducer::eqElimInt: rhs = "+rhs.
toString());
2577 for(
size_t i=0, iend=isIntVars.size(); i<iend; ++i) {
2579 d_theoryArith->separateMonomial(rhs[i+1], c, v);
2580 const Expr&
isInt(isIntVars[i].getExpr());
2583 "ArithTheoremProducer::eqElimInt:\n rhs["+
int2string(i+1)
2591 static int varCount(0);
2592 Expr newVar = d_em->newBoundVarExpr(
"_int_var",
int2string(varCount++));
2594 Expr t2 = create_t2(lhs, rhs, newVar);
2595 Expr t3 = create_t3(lhs, rhs, newVar);
2597 vars.push_back(newVar);
2598 Expr res = d_em->newClosureExpr(
EXISTS, vars,
2601 vector<Theorem> thms(isIntVars);
2602 thms.push_back(isIntx);
2603 thms.push_back(eqn);
2610 vector<Theorem>::const_iterator i=isIntVars.begin(), iend=isIntVars.end();
2612 pfs.push_back(i->getProof());
2613 pf = newPf(
"eq_elim_int", eqn.
getExpr(), res , pfs);
2616 Theorem thm(newTheorem(res, assump, pf));
2617 TRACE(
"arith eq",
"eqElimIntRule => ", thm.
getExpr(),
" }");
2623 ArithTheoremProducer::isIntConst(
const Expr& e) {
2628 "ArithTheoremProducer::isIntConst(e = "
2632 pf = newPf(
"is_int_const", e);
2634 return newRWTheorem(e, isInt? d_em->trueExpr() : d_em->falseExpr(), Assumptions::emptyAssump(), pf);
2639 ArithTheoremProducer::equalLeaves1(
const Theorem& thm)
2646 e[1].getRational() ==
Rational(0) &&
2647 e[0].getKind() ==
PLUS &&
2648 e[0].arity() == 3 &&
2650 e[0][0].getRational() ==
Rational(0) &&
2651 e[0][1].getKind() ==
MULT &&
2652 e[0][1].arity() == 2 &&
2654 e[0][1][0].getRational() ==
Rational(-1),
2661 pf = newPf(
"equalLeaves1", e, pfs);
2663 return newRWTheorem(e, e[0][1][1].eqExpr(e[0][2]), thm.
getAssumptionsRef(), pf);
2668 ArithTheoremProducer::equalLeaves2(
const Theorem& thm)
2675 e[0].getRational() ==
Rational(0) &&
2676 e[1].getKind() ==
PLUS &&
2677 e[1].arity() == 3 &&
2679 e[1][0].getRational() ==
Rational(0) &&
2680 e[1][1].getKind() ==
MULT &&
2681 e[1][1].arity() == 2 &&
2683 e[1][1][0].getRational() ==
Rational(-1),
2690 pf = newPf(
"equalLeaves2", e, pfs);
2692 return newRWTheorem(e, e[1][1][1].eqExpr(e[1][2]), thm.
getAssumptionsRef(), pf);
2697 ArithTheoremProducer::equalLeaves3(
const Theorem& thm)
2704 e[1].getRational() ==
Rational(0) &&
2705 e[0].getKind() ==
PLUS &&
2706 e[0].arity() == 3 &&
2708 e[0][0].getRational() ==
Rational(0) &&
2709 e[0][2].getKind() ==
MULT &&
2710 e[0][2].arity() == 2 &&
2712 e[0][2][0].getRational() ==
Rational(-1),
2719 pf = newPf(
"equalLeaves3", e, pfs);
2721 return newRWTheorem(e, e[0][2][1].eqExpr(e[0][1]), thm.
getAssumptionsRef(), pf);
2726 ArithTheoremProducer::equalLeaves4(
const Theorem& thm)
2733 e[0].getRational() ==
Rational(0) &&
2734 e[1].getKind() ==
PLUS &&
2735 e[1].arity() == 3 &&
2737 e[1][0].getRational() ==
Rational(0) &&
2738 e[1][2].getKind() ==
MULT &&
2739 e[1][2].arity() == 2 &&
2741 e[1][2][0].getRational() ==
Rational(-1),
2748 pf = newPf(
"equalLeaves4", e, pfs);
2750 return newRWTheorem(e, e[1][2][1].eqExpr(e[1][1]), thm.
getAssumptionsRef(), pf);
2754 ArithTheoremProducer::diseqToIneq(
const Theorem& diseq) {
2761 "ArithTheoremProducer::diseqToIneq: expected disequality:\n"
2765 const Expr& x = e[0][0];
2766 const Expr& y = e[0][1];
2789 vector<Expr> sumTerms;
2795 if ((*it).isRational()) r = r + (*it).getRational();
2797 else sumTerms.push_back((*it));
2802 if (sumTerms.size() > 1)
2807 transformed =
Expr(e.
getKind(), sumTerms[0], rat(-r));
2812 if (withProof()) pf = newPf(
"arithm_sum_constant_right", e);
2815 return newRWTheorem(e, transformed, Assumptions::emptyAssump(), pf);
2828 const Expr& x = e[0];
2829 const Expr& y = e[1];
2833 pf = newPf(
"eqToIneq", e);
2841 return newRWTheorem(e, d_em->trueExpr(), Assumptions::emptyAssump(), pf);
2852 "oneElimination: input must be a multiplication by one" + e.
toString());
2859 pf = newPf(
"oneElimination", e);
2862 return newRWTheorem(e, e[1], Assumptions::emptyAssump(), pf);
2868 const Expr& lowerBoundExpr = lowerBound.
getExpr();
2869 const Expr& upperBoundExpr = upperBound.
getExpr();
2873 CHECK_SOUND(
isLE(lowerBoundExpr) ||
isLT(lowerBoundExpr),
"clashingBounds: lowerBound should be >= or > " + lowerBoundExpr.
toString());
2874 CHECK_SOUND(
isGE(upperBoundExpr) ||
isGT(upperBoundExpr),
"clashingBounds: upperBound should be <= or < " + upperBoundExpr.
toString());
2877 CHECK_SOUND(lowerBoundExpr[1] == upperBoundExpr[1],
"clashingBounds: bounds not on the same term " + lowerBoundExpr.
toString() +
", " + upperBoundExpr.
toString());
2883 if (
isLE(lowerBoundExpr) &&
isGE(upperBoundExpr)) {
2884 CHECK_SOUND(upperBoundR < lowerBoundR,
"clashingBounds: bounds are satisfiable");
2886 CHECK_SOUND(upperBoundR <= lowerBoundR,
"clashingBounds: bounds are satisfiable");
2894 pf = newPf(
"clashingBounds", lowerBoundExpr, upperBoundExpr);
2898 assumptions.
add(lowerBound);
2899 assumptions.
add(upperBound);
2902 return newTheorem(d_em->falseExpr(), assumptions, pf);
2931 int kind = (kind1 == kind2) ? kind1 : ((kind1 ==
LT) || (kind2 ==
LT))?
LT :
GT;
2939 pf = newPf(
"addInequalities", expr1, expr2, pfs);
2947 return newTheorem(
Expr(kind, leftSide, rightSide), a, pf);
2950 Theorem ArithTheoremProducer::implyWeakerInequality(
const Expr& expr1,
const Expr& expr2) {
2959 bool type_less_than =
true;
2966 type_less_than =
false;
2974 CHECK_SOUND(expr1[1] == expr2[1],
"implyWeakerInequality: the expression must be the same" + expr1.
toString() +
" and " + expr2.
toString());
2981 if (type_less_than) {
2983 CHECK_SOUND(expr2rat < expr1rat,
"implyWeakerInequality: the implication doesn't apply" + expr1.
toString() +
" and " + expr2.
toString());
2985 CHECK_SOUND(expr2rat <= expr1rat,
"implyWeakerInequality: the implication doesn't apply" + expr1.
toString() +
" and " + expr2.
toString());
2989 CHECK_SOUND(expr2rat > expr1rat,
"implyWeakerInequality: the implication doesn't apply" + expr1.
toString() +
" and " + expr2.
toString());
2991 CHECK_SOUND(expr2rat >= expr1rat,
"implyWeakerInequality: the implication doesn't apply" + expr1.
toString() +
" and " + expr2.
toString());
2998 if(withProof()) pf = newPf(
"implyWeakerInequality", expr1, expr2);
3001 return newTheorem(expr1.
impExpr(expr2), Assumptions::emptyAssump(), pf);
3004 Theorem ArithTheoremProducer::implyNegatedInequality(
const Expr& expr1,
const Expr& expr2) {
3012 CHECK_SOUND(expr1[1] == expr2[1],
"implyNegatedInequality: bounds not on the same term " + expr1.
toString() +
", " + expr2.
toString());
3019 CHECK_SOUND(upperBoundR < lowerBoundR,
"implyNegatedInequality: cant imply negation" + expr1.
toString() +
", " + expr2.
toString());
3021 CHECK_SOUND(upperBoundR <= lowerBoundR,
"implyNegatedInequality: cant imply negation" + expr1.
toString() +
", " + expr2.
toString());
3023 CHECK_SOUND(upperBoundR > lowerBoundR,
"implyNegatedInequality: cant imply negation" + expr1.
toString() +
", " + expr2.
toString());
3025 CHECK_SOUND(upperBoundR >= lowerBoundR,
"implyNegatedInequality: cant imply negation" + expr1.
toString() +
", " + expr2.
toString());
3030 if (withProof()) pf = newPf(
"implyNegatedInequality", expr1, expr2);
3033 return newTheorem(expr1.
impExpr(expr2.
negate()), Assumptions::emptyAssump(), pf);
3042 if (withProof()) pf = newPf(
"trustedRewrite", expr1, expr2);
3045 return newRWTheorem(expr1, expr2, Assumptions::emptyAssump(), pf);
3061 if (withProof()) pf = newPf(
"integerSplit", intVar, rat(intPoint));
3064 return newTheorem(split, Assumptions::emptyAssump(), pf);
3075 CHECK_SOUND(isIntConstrThm.
getExpr()[0] == constr[1],
"rafineStrictInteger: proof of intger doesn't correspond to the constarint right side");
3076 CHECK_SOUND(constr[0].
isRational(),
"rafineStrictInteger: right side of the constraint muts be a rational");
3090 else bound = ceil(bound);
3094 if (!bound.
isInteger()) bound = ceil(bound);
3099 else bound = floor(bound);
3103 if (!bound.
isInteger()) bound = floor(bound);
3108 Expr newConstr(kind, rat(bound), constr[1]);
3115 if (withProof()) pf = newPf(
"rafineStrictInteger", constr, newConstr,isIntConstrThm.
getProof());
3118 return newRWTheorem(constr, newConstr, assump, pf);
3133 Theorem ArithTheoremProducer::intEqualityRationalConstant(
const Theorem& isIntConstrThm,
const Expr& constr) {
3138 Theorem ArithTheoremProducer::cycleConflict(
const vector<Theorem>& inequalitites) {
3143 Theorem ArithTheoremProducer::implyEqualities(
const vector<Theorem>& inequalitites) {
3161 CHECK_SOUND(
isLT(ineq),
"ArithTheoremProducerOld::LTtoLE: ineq must be <");
3164 "ArithTheoremProducerOld::lessThanToLE: bad integrality check:\n"
3165 " ineq = "+ineq.
toString()+
"\n isIntLHS = "
3168 "ArithTheoremProducerOld::lessThanToLE: bad integrality check:\n"
3169 " ineq = "+ineq.
toString()+
"\n isIntRHS = "
3173 vector<Theorem> thms;
3174 thms.push_back(isIntLHS);
3175 thms.push_back(isIntRHS);
3178 Expr le = changeRight?
leExpr(ineq[0], ineq[1] + rat(-1)) :
leExpr(ineq[0] + rat(1), ineq[1]);
3181 pfs.push_back(isIntLHS.
getProof());
3182 pfs.push_back(isIntRHS.
getProof());
3183 pf = newPf(changeRight?
"lessThan_To_LE_rhs_rwr" :
"lessThan_To_LE_lhs_rwr", ineq, le, pfs);
3186 return newRWTheorem(ineq, le, a, pf);
3195 Theorem ArithTheoremProducer::implyWeakerInequalityDiffLogic(
const std::vector<Theorem>& antecedentThms,
const Expr& implied) {
3200 Theorem ArithTheoremProducer::implyNegatedInequalityDiffLogic(
const std::vector<Theorem>& antecedentThms,
const Expr& implied) {
3205 Theorem ArithTheoremProducer::expandGrayShadowRewrite(
const Expr& theShadow) {
3210 Theorem ArithTheoremProducer::compactNonLinearTerm(
const Expr& nonLinear) {
3221 std::vector<Theorem>& c1_le_x,
Rational c1,
3222 std::vector<Theorem>& x_le_c2,
Rational c2) {
3227 Theorem ArithTheoremProducer::addInequalities(
const vector<Theorem>& thms) {