30 #define _CVC3_TRUSTED_
52 #define CLASS_NAME "ArithTheoremProducer3"
58 if(withProof()) pf = newPf(
"var_to_mult", e);
59 return newRWTheorem(e, (rat(1) * e), Assumptions::emptyAssump(), pf);
66 if(withProof()) pf = newPf(
"uminus_to_mult", e);
67 return newRWTheorem((-e), (rat(-1) * e), Assumptions::emptyAssump(), pf);
75 if(withProof()) pf = newPf(
"minus_to_plus", x, y);
76 return newRWTheorem((x-y), (x + (rat(-1) * y)), Assumptions::emptyAssump(), pf);
82 Theorem ArithTheoremProducer3::canonUMinusToDivide(
const Expr& e) {
84 if(withProof()) pf = newPf(
"canon_uminus", e);
85 return newRWTheorem((-e), (e / rat(-1)), Assumptions::emptyAssump(), pf);
91 Theorem ArithTheoremProducer3::canonDivideConst(
const Expr& c,
96 CLASS_NAME "::canonDivideConst:\n c not a constant: "
99 CLASS_NAME "::canonDivideConst:\n d not a constant: "
104 pf = newPf(
"canon_divide_const", c, d, d_hole);
106 return newRWTheorem((c/d), (rat(dr==0? 0 : (c.
getRational()/dr))), Assumptions::emptyAssump(), pf);
116 "Not a (c * x) expression: "
120 "d is not a constant: " + d.
toString());
123 Rational cdr(dr==0? 0 : (cx[0].getRational()/dr));
127 pf = newPf(
"canon_divide_mult", cx[0], cx[1], d);
130 return newRWTheorem((cx/d), (cx[1]), Assumptions::emptyAssump(), pf);
132 return newRWTheorem((cx/d), cd, Assumptions::emptyAssump(), pf);
134 return newRWTheorem((cx/d), (cd*cx[1]), Assumptions::emptyAssump(), pf);
142 "Expr is not a canonical sum: "
146 "d is not a const: " + d.
toString());
151 pf = newPf(
"canon_divide_plus", rat(sum.
arity()),
153 vector<Expr> newKids;
155 newKids.push_back((*i)/d);
157 return newRWTheorem((sum/d), (
plusExpr(newKids)), Assumptions::emptyAssump(), pf);
165 "d is not a const: " + d.
toString());
170 pf = newPf(
"canon_divide_var", e);
174 return newRWTheorem(e/d, e, Assumptions::emptyAssump(), pf);
176 return newRWTheorem(e/d, d, Assumptions::emptyAssump(), pf);
178 return newRWTheorem(e/d, rat(1/dr) * e, Assumptions::emptyAssump(), pf);
196 Expr ArithTheoremProducer3::simplifiedMultExpr(std::vector<Expr> & mulKids)
198 DebugAssert(mulKids.size() >= 1 && mulKids[0].isRational(),
"");
199 if (mulKids.size() == 1) {
202 if ((mulKids[0] == rat(1)) && mulKids.size() == 2) {
209 Expr ArithTheoremProducer3::canonMultConstMult(
const Expr & c,
216 std::vector<Expr> mulKids;
218 "ArithTheoremProducer3::canonMultConstMult: "
219 "a canonized MULT expression must have arity "
220 "greater than 1: and first child must be "
223 mulKids.push_back(rat(c.
getRational() * (*i).getRational()));
225 for(; i != e.
end(); ++i) {
226 mulKids.push_back(*i);
228 return simplifiedMultExpr(mulKids);
231 Expr ArithTheoremProducer3::canonMultConstPlus(
const Expr & e1,
239 std::vector<Theorem> thmPlusVector;
241 for(; i!= e2.
end(); ++i) {
242 thmPlusVector.push_back(canonMultMtermMterm(e1*(*i)));
246 d_theoryArith->substitutivityRule(e2.
getOp(), thmPlusVector);
250 Expr ArithTheoremProducer3::canonMultPowPow(
const Expr & e1,
258 if (leaf1 == leaf2) {
263 else if (rsum == 1) {
268 return powExpr(rat(rsum), leaf1);
273 std::vector<Expr> mulKids;
274 mulKids.push_back(rat(1));
277 mulKids.push_back(e2);
278 mulKids.push_back(e1);
282 mulKids.push_back(e1);
283 mulKids.push_back(e2);
286 return simplifiedMultExpr(mulKids);
290 Expr ArithTheoremProducer3::canonMultPowLeaf(
const Expr & e1,
298 if (leaf1 == leaf2) {
303 else if (rsum == 1) {
308 return powExpr(rat(rsum), leaf1);
313 std::vector<Expr> mulKids;
314 mulKids.push_back(rat(1));
317 mulKids.push_back(e2);
318 mulKids.push_back(e1);
322 mulKids.push_back(e1);
323 mulKids.push_back(e2);
325 return simplifiedMultExpr(mulKids);
329 Expr ArithTheoremProducer3::canonMultLeafLeaf(
const Expr & e1,
336 if (leaf1 == leaf2) {
341 std::vector<Expr> mulKids;
342 mulKids.push_back(rat(1));
345 mulKids.push_back(e2);
346 mulKids.push_back(e1);
350 mulKids.push_back(e1);
351 mulKids.push_back(e2);
353 return simplifiedMultExpr(mulKids);
357 Expr ArithTheoremProducer3::canonMultLeafOrPowMult(
const Expr & e1,
366 std::vector<Expr> mulKids;
370 mulKids.push_back(*i);
373 for(; i != e2.
end(); ++i) {
374 Expr leaf2 = ((*i).getKind() ==
POW) ? (*i)[1] : (*i);
375 if (leaf1 == leaf2) {
378 ((*i).getKind() ==
POW ? (*i)[0].getRational() : 1);
383 mulKids.push_back(leaf1);
387 mulKids.push_back(
powExpr(rat(r1 + r2), leaf1));
396 else if (leaf2 < leaf1) {
397 mulKids.push_back(e1);
398 mulKids.push_back(*i);
402 mulKids.push_back(*i);
405 mulKids.push_back(e1);
410 for (++i; i != e2.
end(); ++i) {
411 mulKids.push_back(*i);
414 return simplifiedMultExpr(mulKids);
422 return ArithTheoremProducer3::greaterthan(e1,e2);
429 ArithTheoremProducer3::canonCombineLikeTerms(
const std::vector<Expr> & sumExprs)
433 vector<Expr> sumKids;
437 std::vector<Expr>::const_iterator i = sumExprs.begin();
438 for (; i != sumExprs.end(); ++i) {
446 std::vector<Expr> mulKids;
448 mulKids.push_back(rat(1));
451 for (; j!= mul.
end(); ++j) {
452 mulKids.push_back(*j);
456 Expr tempExpr = mulKids.size() > 2 ?
multExpr(mulKids): mulKids[1];
457 MonomMap::iterator i=sumHashMap.find(tempExpr);
458 if (i == sumHashMap.end()) {
467 MonomMap::iterator i=sumHashMap.find(mul);
469 if (i == sumHashMap.end()) {
481 sumKids.push_back(rat(constant));
482 MonomMap::iterator j = sumHashMap.begin(), jend=sumHashMap.end();
483 for(; j != jend; ++j) {
484 if ((*j).second != 0)
486 (canonMultMtermMterm(rat((*j).second) * (*j).first).getRHS());
500 if ((constant == 0) && (sumKids.size() == 2)) {
503 else if (sumKids.size() == 1) {
510 Expr ArithTheoremProducer3::canonMultLeafOrPowOrMultPlus(
const Expr & e1,
520 std::vector<Expr> sumExprs;
523 for (; i != e2.
end(); ++i) {
524 sumExprs.push_back(canonMultMtermMterm(e1 * (*i)).getRHS());
526 return canonCombineLikeTerms(sumExprs);
529 Expr ArithTheoremProducer3::canonMultPlusPlus(
const Expr & e1,
536 std::vector<Expr> sumExprs;
539 for (; i != e1.
end(); ++i) {
541 for (; j != e2.
end(); ++j) {
542 sumExprs.push_back(canonMultMtermMterm((*i) * (*j)).getRHS());
545 return canonCombineLikeTerms(sumExprs);
553 ArithTheoremProducer3::canonMultMtermMterm(
const Expr& e)
557 "canonMultMtermMterm: e = "+e.
toString());
561 const Expr& e1 = e[0];
562 const Expr& e2 = e[1];
563 string cmmm =
"canon_mult_mterm_mterm";
569 return canonMultZero(e2);
571 return canonMultOne(e2);
576 return canonMultConstConst(e1,e2);
582 return d_theoryArith->reflexivityRule (e);
586 rhs = canonMultConstMult(e1,e2);
587 if(withProof()) pf = newPf(cmmm,e,rhs);
588 return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
591 rhs = canonMultConstPlus(e1,e2);
592 if(withProof()) pf = newPf(cmmm,e,rhs);
593 return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
598 return d_theoryArith->reflexivityRule(e);
607 return canonMultMtermMterm(e2 * e1);
610 rhs = canonMultPowPow(e1,e2);
611 if(withProof()) pf = newPf(cmmm,e,rhs);
612 return newRWTheorem(e,rhs, Assumptions::emptyAssump(), pf);
615 rhs = canonMultLeafOrPowMult(e1,e2);
616 if(withProof()) pf = newPf(cmmm,e,rhs);
617 return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
620 rhs = canonMultLeafOrPowOrMultPlus(e1,e2);
621 if(withProof()) pf = newPf(cmmm,e,rhs);
622 return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
625 rhs = canonMultPowLeaf(e1,e2);
626 if(withProof()) pf = newPf(cmmm,e,rhs);
627 return newRWTheorem(e,rhs, Assumptions::emptyAssump(), pf);
636 return canonMultMtermMterm(e2 * e1);
643 for (; i != e1.end(); ++i) {
644 result = canonMultMtermMterm((*i) * result).getRHS();
646 if(withProof()) pf = newPf(cmmm,e,result);
647 return newRWTheorem(e, result, Assumptions::emptyAssump(), pf);
651 rhs = canonMultLeafOrPowOrMultPlus(e1,e2);
652 if(withProof()) pf = newPf(cmmm,e,rhs);
653 return newRWTheorem(e,rhs, Assumptions::emptyAssump(), pf);
658 return canonMultMtermMterm(e2 * e1);
668 return canonMultMtermMterm(e2 * e1);
671 rhs = canonMultPlusPlus(e1,e2);
672 if(withProof()) pf = newPf(cmmm,e,rhs);
673 return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
678 return canonMultMtermMterm(e2 * e1);
687 return canonMultMtermMterm(e2 * e1);
690 rhs = canonMultPowLeaf(e2,e1);
691 if(withProof()) pf = newPf(cmmm,e,rhs);
692 return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
695 rhs = canonMultLeafOrPowMult(e1,e2);;
696 if(withProof()) pf = newPf(cmmm,e,rhs);
697 return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
700 rhs = canonMultLeafOrPowOrMultPlus(e1,e2);
701 if(withProof()) pf = newPf(cmmm,e,rhs);
702 return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
706 rhs = canonMultLeafLeaf(e1,e2);
707 if(withProof()) pf = newPf(cmmm,e,rhs);
708 return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
713 return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
718 ArithTheoremProducer3::canonPlus(
const Expr& e)
723 pf = newPf(
"canon_plus", e);
729 std::vector<Expr> sumKids;
731 for(; i != e.
end(); ++i) {
732 if ((*i).getKind() !=
PLUS) {
733 sumKids.push_back(*i);
738 for(; j != (*i).end(); ++j)
739 sumKids.push_back(*j);
742 Expr val = canonCombineLikeTerms(sumKids);
744 pf = newPf(
"canon_plus", e, val);
746 return newRWTheorem(e, val, Assumptions::emptyAssump(), pf);
751 ArithTheoremProducer3::canonMult(
const Expr& e)
758 for (; i != e.
end(); ++i) {
759 result = canonMultMtermMterm(result * (*i)).getRHS();
762 pf = newPf(
"canon_mult", e,result);
764 return newRWTheorem(e, result, Assumptions::emptyAssump(), pf);
769 ArithTheoremProducer3::canonInvertConst(
const Expr& e)
777 pf = newPf(
"canon_invert_const", e);
780 return newRWTheorem((rat(1)/e), rat(er==0? 0 : (1/er)), Assumptions::emptyAssump(), pf);
785 ArithTheoremProducer3::canonInvertLeaf(
const Expr& e)
790 pf = newPf(
"canon_invert_leaf", e);
792 return newRWTheorem((rat(1)/e),
powExpr(rat(-1), e), Assumptions::emptyAssump(), pf);
797 ArithTheoremProducer3::canonInvertPow(
const Expr& e)
804 pf = newPf(
"canon_invert_pow", e);
806 if (e[0].getRational() == -1)
807 return newRWTheorem((rat(1)/e), e[1], Assumptions::emptyAssump(), pf);
809 return newRWTheorem((rat(1)/e),
810 powExpr(rat(-e[0].getRational()), e),
811 Assumptions::emptyAssump(),
816 ArithTheoremProducer3::canonInvertMult(
const Expr& e)
823 pf = newPf(
"canon_invert_mult", e);
827 Expr result = canonInvert(e[0]).getRHS();
828 for (
int i = 1; i < e.
arity(); ++i) {
830 canonMultMtermMterm(result * canonInvert(e[i]).getRHS()).getRHS();
832 return newRWTheorem((rat(1)/e), result, Assumptions::emptyAssump(), pf);
839 ArithTheoremProducer3::canonInvert(
const Expr& e)
842 "Cannot do inverse on a PLUS"+e.
toString());
845 return canonInvertConst(e);
848 return canonInvertPow(e);
851 return canonInvertMult(e);
855 return canonInvertLeaf(e);
861 Theorem ArithTheoremProducer3::moveSumConstantRight(
const Expr& e) {
877 vector<Expr> sumTerms;
883 if ((*it).isRational()) r = r + (*it).getRational();
885 else sumTerms.push_back((*it));
890 if (sumTerms.size() > 1)
895 transformed =
Expr(e.
getKind(), sumTerms[0], rat(-r));
900 if (withProof()) pf = newPf(
"arithm_sum_constant_right", e);
903 return newRWTheorem(e, transformed, Assumptions::emptyAssump(), pf);
907 ArithTheoremProducer3::canonDivide(
const Expr& e)
913 pf = newPf(
"canon_invert_divide", e);
916 Theorem thm = newRWTheorem(e, e[0]*(canonInvert(e[1]).getRHS()), Assumptions::emptyAssump(), pf);
918 return d_theoryArith->transitivityRule(thm, canonMult(thm.
getRHS()));
925 ArithTheoremProducer3::canonMultTermConst(
const Expr& c,
const Expr& t) {
930 "c is not a constant: " + c.
toString());
932 if(withProof()) pf = newPf(
"canon_mult_term_const", c, t);
933 return newRWTheorem((t*c), (c*t), Assumptions::emptyAssump(), pf);
939 ArithTheoremProducer3::canonMultTerm1Term2(
const Expr& t1,
const Expr& t2) {
943 CHECK_SOUND(
false,
"Fatal Error: We don't support multiplication"
944 "of two non constant terms at this time "
954 if(withProof()) pf = newPf(
"canon_mult_zero", e);
955 return newRWTheorem((rat(0)*e), rat(0), Assumptions::emptyAssump(), pf);
962 if(withProof()) pf = newPf(
"canon_mult_one", e);
963 return newRWTheorem((rat(1)*e), e, Assumptions::emptyAssump(), pf);
969 ArithTheoremProducer3::canonMultConstConst(
const Expr& c1,
const Expr& c2) {
974 "c1 is not a constant: " + c1.
toString());
977 "c2 is not a constant: " + c2.
toString());
979 if(withProof()) pf = newPf(
"canon_mult_const_const", c1, c2);
981 newRWTheorem((c1*c2), rat(c1.
getRational()*c2.getRational()), Assumptions::emptyAssump(), pf);
987 ArithTheoremProducer3::canonMultConstTerm(
const Expr& c1,
993 "c1 is not a constant: " + c1.
toString());
996 "c2 is not a constant: " + c2.
toString());
999 if(withProof()) pf = newPf(
"canon_mult_const_term", c1, c2, t);
1007 ArithTheoremProducer3::canonMultConstSum(
const Expr& c1,
const Expr& sum) {
1009 std::vector<Expr> sumKids;
1014 "c1 is not a constant: " + c1.
toString());
1017 "the kind must be a PLUS: " + sum.
toString());
1020 for(; i != sum.
end(); ++i)
1021 sumKids.push_back(c1*(*i));
1023 if(withProof()) pf = newPf(
"canon_mult_const_sum", c1, sum, ret);
1024 return newRWTheorem((c1*sum),ret , Assumptions::emptyAssump(), pf);
1030 ArithTheoremProducer3::canonPowConst(
const Expr& e) {
1034 "ArithTheoremProducer3::canonPowConst("+e.
toString()+
")");
1040 "ArithTheoremProducer3::canonPowConst("+e.
toString()+
")");
1043 if (base == 0 && p < 0) {
1046 else res = rat(
pow(p, base));
1049 pf = newPf(
"canon_pow_const", e);
1050 return newRWTheorem(e, res, Assumptions::emptyAssump(), pf);
1057 ArithTheoremProducer3::canonFlattenSum(
const Expr& e) {
1059 std::vector<Expr> sumKids;
1063 "input must be a PLUS:" + e.
toString());
1067 for(; i != e.
end(); ++i){
1068 if (
PLUS != (*i).getKind())
1069 sumKids.push_back(*i);
1072 for(; j != (*i).end(); ++j)
1073 sumKids.push_back(*j);
1077 if(withProof()) pf = newPf(
"canon_flatten_sum", e,ret);
1078 return newRWTheorem(e,ret, Assumptions::emptyAssump(), pf);
1084 ArithTheoremProducer3::canonComboLikeTerms(
const Expr& e) {
1086 std::vector<Expr> sumKids;
1092 for(; k != e.
end(); ++k)
1095 "input must be a flattened PLUS:" + k->
toString());
1098 for(; i != e.
end(); ++i){
1103 if(0 == sumHashMap.
count((*i)))
1106 sumHashMap[*i] += 1;
1109 if(0 == sumHashMap.
count((*i)[1]))
1110 sumHashMap[(*i)[1]] = (*i)[0].getRational();
1112 sumHashMap[(*i)[1]] = sumHashMap[(*i)[1]] + (*i)[0].getRational();
1117 sumKids.push_back(rat(constant));
1119 for(; j != sumHashMap.
end(); ++j) {
1120 if(0 == (*j).second)
1122 else if (1 == (*j).second)
1123 sumKids.push_back((*j).first);
1125 sumKids.push_back(rat((*j).second) * (*j).first);
1132 if(2 == sumKids.size() && 0 == constant) ret = sumKids[1];
1133 else if (1 == sumKids.size()) ret = sumKids[0];
1136 if(withProof()) pf = newPf(
"canon_combo_like_terms",e,ret);
1137 return newRWTheorem(e, ret, Assumptions::emptyAssump(), pf);
1148 "multEqZero invariant violated"+expr.
toString());
1153 for (; i != iend; ++i) {
1154 kids.push_back(rat(0).eqExpr(*i));
1157 pf = newPf(
"multEqZero", expr);
1159 return newRWTheorem(expr,
Expr(
OR, kids), Assumptions::emptyAssump(), pf);
1172 "powEqZero invariant violated"+expr.
toString());
1176 pf = newPf(
"powEqZero", expr);
1181 res = d_em->falseExpr();
1184 res = rat(0).
eqExpr(expr[1][1]);
1186 return newRWTheorem(expr, res, Assumptions::emptyAssump(), pf);
1199 expr[0][0] == expr[1][0],
1200 "elimPower invariant violated"+expr.
toString());
1204 pf = newPf(
"elimPower", expr);
1209 res = res.
orExpr(expr[0][1].eqExpr(-expr[1][1]));
1211 return newRWTheorem(expr, res, Assumptions::emptyAssump(), pf);
1225 "elimPowerConst invariant violated"+expr.
toString());
1229 pf = newPf(
"elimPowerConst", expr, rat(root));
1234 res = res.
orExpr(expr[0][1].eqExpr(rat(-root)));
1236 return newRWTheorem(expr, res, Assumptions::emptyAssump(), pf);
1249 "evenPowerEqNegConst invariant violated"+expr.
toString());
1253 pf = newPf(
"evenPowerEqNegConst", expr);
1255 return newRWTheorem(expr, d_em->falseExpr(), Assumptions::emptyAssump(), pf);
1268 ratRoot(expr[1].getRational(), expr[0][0].getRational().getUnsigned()) == 0,
1269 "intEqIrrational invariant violated"+expr.
toString());
1271 "ArithTheoremProducer3::intEqIrrational:\n "
1272 "wrong integrality constraint:\n expr = "
1279 pf = newPf(
"int_eq_irr", expr, isIntx.
getProof());
1281 return newRWTheorem(expr, d_em->falseExpr(), assump, pf);
1291 "non-const parameters: " + e.
toString());
1299 result = (r1 == r2)?
true :
false;
1302 result = (r1 < r2)?
true :
false;
1305 result = (r1 <= r2)?
true :
false;
1308 result = (r1 > r2)?
true :
false;
1311 result = (r1 >= r2)?
true :
false;
1316 "ArithTheoremProducer3::constPredicate: wrong kind");
1320 Expr ret = (result) ? d_em->trueExpr() : d_em->falseExpr();
1321 if(withProof()) pf = newPf(
"const_predicate", e,ret);
1322 return newRWTheorem(e, ret, Assumptions::emptyAssump(), pf);
1336 "ArithTheoremProducer3::rightMinusLeft: wrong kind");
1338 if(withProof()) pf = newPf(
"right_minus_left",e);
1339 return newRWTheorem(e,
Expr(e.
getOp(), rat(0), e[1] - e[0]), Assumptions::emptyAssump(), pf);
1354 "ArithTheoremProducer3::rightMinusLeft: wrong kind");
1356 if(withProof()) pf = newPf(
"left_minus_right",e);
1357 return newRWTheorem(e,
Expr(e.
getOp(), e[0] - e[1], rat(0)), Assumptions::emptyAssump(), pf);
1364 const Expr& z,
int kind) {
1371 "ArithTheoremProducer3::plusPredicate: wrong kind");
1376 if(withProof()) pf = newPf(
"plus_predicate",left,right);
1377 return newRWTheorem(left, right, Assumptions::emptyAssump(), pf);
1387 "ArithTheoremProducer3::multEqn(): multiplying equation by 0");
1388 if(withProof()) pf = newPf(
"mult_eqn", x, y, z);
1389 return newRWTheorem(x.
eqExpr(y), (x * z).eqExpr(y * z), Assumptions::emptyAssump(), pf);
1398 if(withProof()) pf = newPf(
"mult_eqn_nonconst", x, y, z);
1400 Assumptions::emptyAssump(), pf);
1415 "ArithTheoremProducer3::multIneqn: wrong kind");
1417 "ArithTheoremProducer3::multIneqn: "
1418 "z must be non-zero rational: " + z.
toString());
1425 ret =
Expr(op, e[0]*z, e[1]*z);
1427 ret =
Expr(op, e[1]*z, e[0]*z);
1428 if(withProof()) pf = newPf(
"mult_ineqn", e, ret);
1429 return newRWTheorem(e, ret, Assumptions::emptyAssump(), pf);
1443 const Expr& x = e[0];
1444 const Expr& y = e[1];
1448 pf = newPf(
"eqToIneq", e);
1460 "ArithTheoremProducer3::flipInequality: wrong kind: " +
1466 if(withProof()) pf = newPf(
"flip_inequality", e,ret);
1467 return newRWTheorem(e,ret, Assumptions::emptyAssump(), pf);
1477 const Expr& ineq = e[0];
1480 "ArithTheoremProducer3::negatedInequality: wrong kind: " +
1483 "ArithTheoremProducer3::negatedInequality: wrong kind: " +
1487 if(withProof()) pf = newPf(
"negated_inequality", e);
1499 return newRWTheorem(e,
Expr(kind, ineq[0], ineq[1]), Assumptions::emptyAssump(), pf);
1512 "ArithTheoremProducer3::realShadow: Wrong Kind: " +
1516 "ArithTheoremProducer3::realShadow:"
1517 " t must be same for both inputs: " +
1518 expr1[1].toString() +
" , " + expr2[0].toString());
1521 int firstKind = expr1.
getKind();
1522 int secondKind = expr2.
getKind();
1523 int kind = (firstKind == secondKind) ? firstKind :
LT;
1527 pfs.push_back(alphaLTt.
getProof());
1529 pf = newPf(
"real_shadow",expr1, expr2, pfs);
1531 return newTheorem(
Expr(kind, expr1[0], expr2[1]), a, pf);
1546 "ArithTheoremProducer3::realShadowLTLE: Wrong Kind: " +
1550 "ArithTheoremProducer3::realShadowLTLE:"
1551 " t must be same for both inputs: " +
1555 "ArithTheoremProducer3::realShadowLTLE:"
1556 " alpha must be same for both inputs: " +
1563 pfs.push_back(alphaLEt.
getProof());
1564 pfs.push_back(tLEalpha.
getProof());
1565 pf = newPf(
"real_shadow_eq", alphaLEt.
getExpr(), tLEalpha.
getExpr(), pfs);
1567 return newRWTheorem(expr1[0], expr1[1], a, pf);
1571 ArithTheoremProducer3::finiteInterval(
const Theorem& aLEt,
1579 "ArithTheoremProducer3::finiteInterval:\n e1 = "
1583 "ArithTheoremProducer3::finiteInterval:\n e1 = "
1587 "ArithTheoremProducer3::finiteInterval:\n e1 = "
1591 "ArithTheoremProducer3::finiteInterval:\n e1 = "
1595 && e2[1][1].getRational() >= 1,
1596 "ArithTheoremProducer3::finiteInterval:\n e1 = "
1602 "Wrong integrality constraint:\n e1 = "
1603 +e1.
toString()+
"\n isInta = "+isIntaExpr.toString());
1605 "Wrong integrality constraint:\n e1 = "
1608 vector<Theorem> thms;
1609 thms.push_back(aLEt);
1610 thms.push_back(tLEac);
1611 thms.push_back(isInta);
1612 thms.push_back(isIntt);
1620 es.push_back(isInta.
getExpr());
1621 es.push_back(isIntt.
getExpr());
1626 pf = newPf(
"finite_interval", es, pfs);
1629 Expr g(grayShadow(e1[1], e1[0], 0, e2[1][1].getRational()));
1630 return newTheorem(g, a, pf);
1642 const Expr& isIntAlphaExpr = isIntAlpha.
getExpr();
1648 "ArithTheoremProducer3::darkGrayShadow2ab: Wrong Kind: " +
1652 const Expr& beta = expr1[0];
1653 const Expr& bx = expr1[1];
1654 const Expr& ax = expr2[0];
1655 const Expr& alpha = expr2[1];
1663 "ArithTheoremProducer3::darkGrayShadow2ab:\n "
1664 "wrong integrality constraint:\n alpha = "
1665 +alpha.
toString()+
"\n isIntAlpha = "
1668 "ArithTheoremProducer3::darkGrayShadow2ab:\n "
1669 "wrong integrality constraint:\n beta = "
1673 "ArithTheoremProducer3::darkGrayShadow2ab:\n "
1674 "wrong integrality constraint:\n x = "
1679 "ArithTheoremProducer3::darkGrayShadow2ab:\n ax<=alpha: " +
1682 "ArithTheoremProducer3::darkGrayShadow2ab:\n beta<=bx: "
1684 +
"\n ax<=alpha: "+ axLEalpha.
toString());
1686 "ArithTheoremProducer3::darkGrayShadow2ab:\n beta<=bx: "
1688 +
"\n ax<=alpha: "+ axLEalpha.
toString());
1690 vector<Theorem> thms;
1691 thms.push_back(betaLEbx);
1692 thms.push_back(axLEalpha);
1693 thms.push_back(isIntAlpha);
1694 thms.push_back(isIntBeta);
1695 thms.push_back(isIntx);
1701 Expr d = darkShadow(rat(a*b-1), t);
1702 Expr g = grayShadow(ax, alpha, -a+1, 0);
1707 exprs.push_back(expr1);
1708 exprs.push_back(expr2);
1713 pfs.push_back(betaLEbx.
getProof());
1714 pfs.push_back(axLEalpha.
getProof());
1715 pfs.push_back(isIntAlpha.
getProof());
1716 pfs.push_back(isIntBeta.
getProof());
1719 pf = newPf(
"dark_grayshadow_2ab", exprs, pfs);
1722 return newTheorem((d || g), A, pf);
1733 const Expr& isIntAlphaExpr = isIntAlpha.
getExpr();
1739 "ArithTheoremProducer3::darkGrayShadow2ba: Wrong Kind: " +
1743 const Expr& beta = expr1[0];
1744 const Expr& bx = expr1[1];
1745 const Expr& ax = expr2[0];
1746 const Expr& alpha = expr2[1];
1754 "ArithTheoremProducer3::darkGrayShadow2ab:\n "
1755 "wrong integrality constraint:\n alpha = "
1756 +alpha.
toString()+
"\n isIntAlpha = "
1759 "ArithTheoremProducer3::darkGrayShadow2ab:\n "
1760 "wrong integrality constraint:\n beta = "
1764 "ArithTheoremProducer3::darkGrayShadow2ab:\n "
1765 "wrong integrality constraint:\n x = "
1770 "ArithTheoremProducer3::darkGrayShadow2ba:\n ax<=alpha: " +
1773 "ArithTheoremProducer3::darkGrayShadow2ba:\n beta<=bx: "
1775 +
"\n ax<=alpha: "+ axLEalpha.
toString());
1777 "ArithTheoremProducer3::darkGrayShadow2ba:\n beta<=bx: "
1779 +
"\n ax<=alpha: "+ axLEalpha.
toString());
1781 vector<Theorem> thms;
1782 thms.push_back(betaLEbx);
1783 thms.push_back(axLEalpha);
1784 thms.push_back(isIntAlpha);
1785 thms.push_back(isIntBeta);
1786 thms.push_back(isIntx);
1791 pfs.push_back(betaLEbx.
getProof());
1792 pfs.push_back(axLEalpha.
getProof());
1793 pfs.push_back(isIntAlpha.
getProof());
1794 pfs.push_back(isIntBeta.
getProof());
1797 pf = newPf(
"dark_grayshadow_2ba", betaLEbx.
getExpr(),
1804 Expr d = darkShadow(rat(a*b-1), t);
1805 Expr g = grayShadow(bx, beta, 0, b-1);
1806 return newTheorem((d || g), A, pf);
1815 "ArithTheoremProducer3::expandDarkShadow: not DARK_SHADOW: " +
1820 pf = newPf(
"expand_dark_shadow", theShadow, darkShadow.
getProof());
1830 "ArithTheoremProducer3::expandGrayShadowConst0:"
1831 " not GRAY_SHADOW: " +
1834 "ArithTheoremProducer3::expandGrayShadow0: c1!=c2: " +
1838 if(withProof()) pf = newPf(
"expand_gray_shadowconst0", theShadow,
1840 const Expr& v = theShadow[0];
1841 const Expr& e = theShadow[1];
1856 "ArithTheoremProducer3::expandGrayShadowConst: not a shadow" +
1865 "ArithTheoremProducer3::expandGrayShadow: " +
1869 const Expr& v = theShadow[0];
1870 const Expr& e = theShadow[1];
1874 Expr g1(grayShadow(v, e, c1, c));
1875 Expr g2(grayShadow(v, e, c+1, c2));
1879 exprs.push_back(theShadow);
1880 exprs.push_back(g1);
1881 exprs.push_back(g2);
1882 pf = newPf(
"split_gray_shadow", exprs, gThm.
getProof());
1893 "ArithTheoremProducer3::expandGrayShadowConst: not a shadow" +
1902 "ArithTheoremProducer3::expandGrayShadow: " +
1906 const Expr& v = theShadow[0];
1907 const Expr& e = theShadow[1];
1911 pf = newPf(
"expand_gray_shadow", theShadow, gThm.
getProof());
1920 ArithTheoremProducer3::expandGrayShadowConst(
const Theorem& gThm) {
1922 const Expr& ax = theShadow[0];
1923 const Expr& cExpr = theShadow[1];
1924 const Expr& bExpr = theShadow[2];
1928 "ArithTheoremProducer3::expandGrayShadowConst: "
1929 "'a' in a*x is not a const: " +theShadow.
toString());
1936 "ArithTheoremProducer3::expandGrayShadowConst: "
1937 "not a GRAY_SHADOW: " +theShadow.
toString());
1939 "ArithTheoremProducer3::expandGrayShadowConst: "
1940 "'a' is not integer: " +theShadow.
toString());
1942 "ArithTheoremProducer3::expandGrayShadowConst: "
1943 "'c' is not rational" +theShadow.
toString());
1945 "ArithTheoremProducer3::expandGrayShadowConst: b not integer: "
1951 Rational j = constRHSGrayShadow(c,b,a);
1963 pf = newPf(
"expand_gray_shadow_const_0", theShadow,
1965 conc = newTheorem(d_em->falseExpr(), assump, pf);
1966 }
else if(bAbs < a+j) {
1968 pf = newPf(
"expand_gray_shadow_const_1", theShadow,
1970 conc = newRWTheorem(ax, rat(c+b-signB*j), assump, pf);
1973 pf = newPf(
"expand_gray_shadow_const", theShadow,
1976 conc = newTheorem(ax.
eqExpr(rat(c+b-signB*j)).
orExpr(newGrayShadow),
1985 ArithTheoremProducer3::grayShadowConst(
const Theorem& gThm) {
1993 const Expr& ax = g[0];
1994 const Expr& e = g[1];
1998 d_theoryArith->separateMonomial(ax, aExpr, x);
2002 "ArithTheoremProducer3::grayShadowConst("+g.
toString()+
")");
2004 "ArithTheoremProducer3::grayShadowConst("+g.
toString()+
")");
2012 "ArithTheoremProducer3::grayShadowConst("+g.
toString()+
")");
2015 Rational newC1 = ceil((c1+c)/a), newC2 = floor((c2+c)/a);
2016 Expr newG((newC1 > newC2)? d_em->falseExpr()
2017 : grayShadow(x, rat(0), newC1, newC2));
2020 pf = newPf(
"gray_shadow_const", g, newG, gThm.
getProof());
2032 "ArithTheoremProducer3::constRHSGrayShadow: a, b, c must be ints");
2036 return mod(a-(c+b), a);
2053 "ArithTheoremProducer3::LTtoLE: ineq must be <");
2056 "ArithTheoremProducer3::lessThanToLE: bad integrality check:\n"
2057 " ineq = "+ineq.
toString()+
"\n isIntLHS = "
2060 "ArithTheoremProducer3::lessThanToLE: bad integrality check:\n"
2061 " ineq = "+ineq.
toString()+
"\n isIntRHS = "
2064 vector<Theorem> thms;
2065 thms.push_back(less);
2066 thms.push_back(isIntLHS);
2067 thms.push_back(isIntRHS);
2070 Expr le = changeRight?
2071 leExpr(ineq[0], ineq[1] + rat(-1))
2072 :
leExpr(ineq[0] + rat(1), ineq[1]);
2076 pfs.push_back(isIntLHS.
getProof());
2077 pfs.push_back(isIntRHS.
getProof());
2078 pf = newPf(changeRight?
"lessThan_To_LE_rhs" :
"lessThan_To_LE_lhs",
2082 return newRWTheorem(ineq, le, a, pf);
2095 ArithTheoremProducer3::intVarEqnConst(
const Expr& eqn,
2106 "ArithTheoremProducer3::intVarEqnConst: "
2107 "rhs has a wrong format: " + right.
toString());
2109 "ArithTheoremProducer3:intVarEqnConst:left is not a zero: " +
2117 d_theoryArith->separateMonomial(right, aExpr, x);
2122 d_theoryArith->separateMonomial(right[1], aExpr, x);
2127 "ArithTheoremProducer3:intVarEqnConst: "
2128 "bad integrality constraint:\n right = " +
2129 right.
toString()+
"\n isIntx = "+isIntxexpr.toString());
2130 CHECK_SOUND(a!=0,
"ArithTheoremProducer3:intVarEqnConst: eqn = "
2155 pf = newPf(
"int_const_eq", eqn, x.
eqExpr(rat(r)),isIntx.
getProof());
2156 return newRWTheorem(eqn, x.
eqExpr(rat(r)), assump, pf);
2160 pf = newPf(
"int_const_eq", eqn, d_em->falseExpr(),isIntx.
getProof());
2161 return newRWTheorem(eqn, d_em->falseExpr(), assump, pf);
2167 ArithTheoremProducer3::create_t(
const Expr& eqn) {
2168 const Expr& lhs = eqn[0];
2172 const Expr& x = lhs[1];
2177 sumModM(kids, eqn[1], m, m);
2179 kids.push_back(monomialModM(eqn[1], m, m));
2181 kids.push_back(
multExpr(rat(1/m), x));
2186 ArithTheoremProducer3::create_t2(
const Expr& lhs,
const Expr& rhs,
2187 const Expr& sigma) {
2192 sumModM(kids, rhs, m, -1);
2194 kids.push_back(rat(0));
2195 Expr monom = monomialModM(rhs, m, -1);
2197 kids.push_back(monom);
2201 kids.push_back(rat(m)*sigma);
2206 ArithTheoremProducer3::create_t3(
const Expr& lhs,
const Expr& rhs,
2207 const Expr& sigma) {
2213 sumMulF(kids, rhs, m, 1);
2215 kids.push_back(rat(0));
2216 Expr monom = monomialMulF(rhs, m, 1);
2218 kids.push_back(monom);
2222 kids.push_back(rat(-a)*sigma);
2230 Rational res((i - m*(floor((i/m) + half))));
2239 return (floor(i/m + half)+modEq(i,m));
2243 ArithTheoremProducer3::sumModM(vector<Expr>& summands,
const Expr& sum,
2245 DebugAssert(divisor != 0,
"ArithTheoremProducer3::sumModM: divisor = "
2250 C = modEq(C,m)/divisor;
2251 summands.push_back(rat(C));
2254 Expr monom = monomialModM(*i, m, divisor);
2256 summands.push_back(monom);
2263 ArithTheoremProducer3::monomialModM(
const Expr& i,
2266 DebugAssert(divisor != 0,
"ArithTheoremProducer3::monomialModM: divisor = "
2271 ai = modEq(ai,m)/divisor;
2272 if(0 == ai) res = rat(0);
2273 else if(1 == ai && i.
arity() == 2) res = i[1];
2275 vector<Expr> kids = i.
getKids();
2281 if(1 == ai) res = i;
2282 else res = rat(ai)*i;
2284 DebugAssert(!res.isNull(),
"ArithTheoremProducer3::monomialModM()");
2286 +
", div="+divisor.
toString()+
") = ", res,
"");
2291 ArithTheoremProducer3::sumMulF(vector<Expr>& summands,
const Expr& sum,
2293 DebugAssert(divisor != 0,
"ArithTheoremProducer3::sumMulF: divisor = "
2299 summands.push_back(rat(C));
2302 Expr monom = monomialMulF(*i, m, divisor);
2304 summands.push_back(monom);
2311 ArithTheoremProducer3::monomialMulF(
const Expr& i,
2314 DebugAssert(divisor != 0,
"ArithTheoremProducer3::monomialMulF: divisor = "
2318 ai = f(ai,m)/divisor;
2319 if(0 == ai)
return rat(0);
2320 if(1 == ai)
return xi;
2332 i = eMap.
find(term);
2338 i = eMap.
find(term[1]);
2340 return term[0]*(*i).second;
2346 vector<Expr> output;
2348 output.push_back(substitute(*j, eMap));
2354 bool ArithTheoremProducer3::greaterthan(
const Expr & l,
const Expr & r)
2357 if (l==r)
return false;
2376 ((r[1]==l[1]) && (r[0].getRational() < l[0].
getRational())));
2382 if (r[1] == l)
return false;
2383 return greaterthan(l, r[1]);
2391 return ((r < l[1]) || ((r == l[1]) && l[0].getRational() > 1));
2406 return ((l[1] == r) || greaterthan(l[1], r));
2416 for (; i != l.
end() && j != r.
end(); ++i, ++j) {
2419 return greaterthan(*i,*j);
2440 return ((l[1] == r) || greaterthan(l[1], r));
2455 return ((r[1] < l) || ((r[1] == l) && (r[0].getRational() < 1)));
2460 if (l == r[1])
return false;
2461 return greaterthan(l,r[1]);
2485 "Expected IS_INTEGER predicate");
2488 DebugAssert(!d_theoryArith->isInteger(expr),
"Expected non-integer");
2495 pf = newPf(
"isIntElim", isIntx.
getProof());
2498 Expr newVar = d_em->newBoundVarExpr(d_theoryArith->intType());
2501 return newTheorem(res, a, pf);
2507 const vector<Theorem>& isIntVars) {
2508 TRACE(
"arith eq",
"eqElimIntRule(", eqn.
getExpr(),
") {");
2513 "ArithTheoremProducer3::eqElimInt: input must be an equation" +
2519 d_theoryArith->separateMonomial(lhs, a, x);
2525 "ArithTheoremProducer3::eqElimInt\n eqn = "
2527 +
"\n isIntx = "+isIntxe.
toString());
2530 "ArithTheoremProducer3::eqElimInt:\n lhs = "+lhs.
toString());
2534 "ArithTheoremProducer3::eqElimInt:\n rhs = "+rhs.
toString());
2538 d_theoryArith->separateMonomial(rhs, c, v);
2541 && isIntVars[0].getExpr()[0] == v
2543 "ArithTheoremProducer3::eqElimInt:\n rhs = "+rhs.
toString()
2544 +
"isIntVars.size = "+
int2string(isIntVars.size()));
2547 "ArithTheoremProducer3::eqElimInt: rhs = "+rhs.
toString());
2550 "ArithTheoremProducer3::eqElimInt: rhs = "+rhs.
toString());
2552 for(
size_t i=0, iend=isIntVars.size(); i<iend; ++i) {
2554 d_theoryArith->separateMonomial(rhs[i+1], c, v);
2555 const Expr&
isInt(isIntVars[i].getExpr());
2558 "ArithTheoremProducer3::eqElimInt:\n rhs["+
int2string(i+1)
2566 static int varCount(0);
2567 Expr newVar = d_em->newBoundVarExpr(
"_int_var",
int2string(varCount++));
2569 Expr t2 = create_t2(lhs, rhs, newVar);
2570 Expr t3 = create_t3(lhs, rhs, newVar);
2572 vars.push_back(newVar);
2573 Expr res = d_em->newClosureExpr(
EXISTS, vars,
2576 vector<Theorem> thms(isIntVars);
2577 thms.push_back(isIntx);
2578 thms.push_back(eqn);
2585 vector<Theorem>::const_iterator i=isIntVars.begin(), iend=isIntVars.end();
2587 pfs.push_back(i->getProof());
2588 pf = newPf(
"eq_elim_int", eqn.
getExpr(), res, pfs);
2591 Theorem thm(newTheorem(res, assump, pf));
2592 TRACE(
"arith eq",
"eqElimIntRule => ", thm.
getExpr(),
" }");
2598 ArithTheoremProducer3::isIntConst(
const Expr& e) {
2603 "ArithTheoremProducer3::isIntConst(e = "
2607 pf = newPf(
"is_int_const", e);
2609 return newRWTheorem(e, isInt? d_em->trueExpr() : d_em->falseExpr(), Assumptions::emptyAssump(), pf);
2614 ArithTheoremProducer3::equalLeaves1(
const Theorem& thm)
2621 e[1].getRational() ==
Rational(0) &&
2622 e[0].getKind() ==
PLUS &&
2623 e[0].arity() == 3 &&
2625 e[0][0].getRational() ==
Rational(0) &&
2626 e[0][1].getKind() ==
MULT &&
2627 e[0][1].arity() == 2 &&
2629 e[0][1][0].getRational() ==
Rational(-1),
2636 pf = newPf(
"equalLeaves1", e, pfs);
2638 return newRWTheorem(e, e[0][1][1].eqExpr(e[0][2]), thm.
getAssumptionsRef(), pf);
2643 ArithTheoremProducer3::equalLeaves2(
const Theorem& thm)
2650 e[0].getRational() ==
Rational(0) &&
2651 e[1].getKind() ==
PLUS &&
2652 e[1].arity() == 3 &&
2654 e[1][0].getRational() ==
Rational(0) &&
2655 e[1][1].getKind() ==
MULT &&
2656 e[1][1].arity() == 2 &&
2658 e[1][1][0].getRational() ==
Rational(-1),
2665 pf = newPf(
"equalLeaves2", e, pfs);
2667 return newRWTheorem(e, e[1][1][1].eqExpr(e[1][2]), thm.
getAssumptionsRef(), pf);
2672 ArithTheoremProducer3::equalLeaves3(
const Theorem& thm)
2679 e[1].getRational() ==
Rational(0) &&
2680 e[0].getKind() ==
PLUS &&
2681 e[0].arity() == 3 &&
2683 e[0][0].getRational() ==
Rational(0) &&
2684 e[0][2].getKind() ==
MULT &&
2685 e[0][2].arity() == 2 &&
2687 e[0][2][0].getRational() ==
Rational(-1),
2694 pf = newPf(
"equalLeaves3", e, pfs);
2696 return newRWTheorem(e, e[0][2][1].eqExpr(e[0][1]), thm.
getAssumptionsRef(), pf);
2701 ArithTheoremProducer3::equalLeaves4(
const Theorem& thm)
2708 e[0].getRational() ==
Rational(0) &&
2709 e[1].getKind() ==
PLUS &&
2710 e[1].arity() == 3 &&
2712 e[1][0].getRational() ==
Rational(0) &&
2713 e[1][2].getKind() ==
MULT &&
2714 e[1][2].arity() == 2 &&
2716 e[1][2][0].getRational() ==
Rational(-1),
2723 pf = newPf(
"equalLeaves4", e, pfs);
2725 return newRWTheorem(e, e[1][2][1].eqExpr(e[1][1]), thm.
getAssumptionsRef(), pf);
2729 ArithTheoremProducer3::diseqToIneq(
const Theorem& diseq) {
2736 "ArithTheoremProducer3::diseqToIneq: expected disequality:\n"
2740 const Expr& x = e[0][0];
2741 const Expr& y = e[0][1];
2750 return newRWTheorem(e, d_em->trueExpr(), Assumptions::emptyAssump(), pf);
2761 "oneElimination: input must be a multiplication by one" + e.
toString());
2768 pf = newPf(
"oneElimination", e);
2771 return newRWTheorem(e, e[1], Assumptions::emptyAssump(), pf);
2777 const Expr& lowerBoundExpr = lowerBound.
getExpr();
2778 const Expr& upperBoundExpr = upperBound.
getExpr();
2782 CHECK_SOUND(
isLE(lowerBoundExpr) ||
isLT(lowerBoundExpr),
"clashingBounds: lowerBound should be >= or > " + lowerBoundExpr.
toString());
2783 CHECK_SOUND(
isGE(upperBoundExpr) ||
isGT(upperBoundExpr),
"clashingBounds: upperBound should be <= or < " + upperBoundExpr.
toString());
2786 CHECK_SOUND(lowerBoundExpr[1] == upperBoundExpr[1],
"clashingBounds: bounds not on the same term " + lowerBoundExpr.
toString() +
", " + upperBoundExpr.
toString());
2792 if (
isLE(lowerBoundExpr) &&
isGE(upperBoundExpr)) {
2793 CHECK_SOUND(upperBoundR < lowerBoundR,
"clashingBounds: bounds are satisfiable");
2795 CHECK_SOUND(upperBoundR <= lowerBoundR,
"clashingBounds: bounds are satisfiable");
2803 pf = newPf(
"clashingBounds", lowerBoundExpr, upperBoundExpr);
2807 assumptions.
add(lowerBound);
2808 assumptions.
add(upperBound);
2811 return newTheorem(d_em->falseExpr(), assumptions, pf);
2840 int kind = (kind1 == kind2) ? kind1 : ((kind1 ==
LT) || (kind2 ==
LT))?
LT :
GT;
2848 pf = newPf(
"addInequalities", expr1, expr2, pfs);
2856 return newTheorem(
Expr(kind, leftSide, rightSide), a, pf);
2859 Theorem ArithTheoremProducer3::implyWeakerInequality(
const Expr& expr1,
const Expr& expr2) {
2879 CHECK_SOUND(expr1[1] == expr2[1],
"implyWeakerInequality: the expression must be the same" + expr1.
toString() +
" and " + expr2.
toString());
2887 CHECK_SOUND(expr2rat < expr1rat,
"implyWeakerInequality: the implication doesn't apply" + expr1.
toString() +
" and " + expr2.
toString());
2889 CHECK_SOUND(expr2rat <= expr1rat,
"implyWeakerInequality: the implication doesn't apply" + expr1.
toString() +
" and " + expr2.
toString());
2892 CHECK_SOUND(expr2rat > expr1rat,
"implyWeakerInequality: the implication doesn't apply" + expr1.
toString() +
" and " + expr2.
toString());
2894 CHECK_SOUND(expr2rat >= expr1rat,
"implyWeakerInequality: the implication doesn't apply" + expr1.
toString() +
" and " + expr2.
toString());
2900 if(withProof()) pf = newPf(
"implyWeakerInequality", expr1, expr2);
2903 return newTheorem(expr1.
impExpr(expr2), Assumptions::emptyAssump(), pf);
2906 Theorem ArithTheoremProducer3::implyNegatedInequality(
const Expr& expr1,
const Expr& expr2) {
2914 CHECK_SOUND(expr1[1] == expr2[1],
"implyNegatedInequality: bounds not on the same term " + expr1.
toString() +
", " + expr2.
toString());
2921 CHECK_SOUND(upperBoundR < lowerBoundR,
"implyNegatedInequality: cant imply negation" + expr1.
toString() +
", " + expr2.
toString());
2923 CHECK_SOUND(upperBoundR <= lowerBoundR,
"implyNegatedInequality: cant imply negation" + expr1.
toString() +
", " + expr2.
toString());
2925 CHECK_SOUND(upperBoundR > lowerBoundR,
"implyNegatedInequality: cant imply negation" + expr1.
toString() +
", " + expr2.
toString());
2927 CHECK_SOUND(upperBoundR >= lowerBoundR,
"implyNegatedInequality: cant imply negation" + expr1.
toString() +
", " + expr2.
toString());
2932 if (withProof()) pf = newPf(
"implyNegatedInequality", expr1, expr2);
2935 return newTheorem(expr1.
impExpr(expr2.
negate()), Assumptions::emptyAssump(), pf);
2944 if (withProof()) pf = newPf(
"trustedRewrite", expr1, expr2);
2947 return newRWTheorem(expr1, expr2, Assumptions::emptyAssump(), pf);
2963 if (withProof()) pf = newPf(
"integerSplit", intVar, rat(intPoint));
2966 return newTheorem(split, Assumptions::emptyAssump(), pf);
2977 CHECK_SOUND(isIntConstrThm.
getExpr()[0] == constr[1],
"rafineStrictInteger: proof of intger doesn't correspond to the constarint right side");
2978 CHECK_SOUND(constr[0].
isRational(),
"rafineStrictInteger: right side of the constraint muts be a rational");
2992 else bound = ceil(bound);
2996 if (!bound.
isInteger()) bound = ceil(bound);
3001 else bound = floor(bound);
3005 if (!bound.
isInteger()) bound = floor(bound);
3010 Expr newConstr(kind, rat(bound), constr[1]);
3017 if (withProof()) pf = newPf(
"rafineStrictInteger", constr, isIntConstrThm.
getProof());
3020 return newRWTheorem(constr, newConstr, assump, pf);
3029 Theorem ArithTheoremProducer3::implyWeakerInequalityDiffLogic(
const std::vector<Theorem>& antecedentThms,
const Expr& implied) {
3034 Theorem ArithTheoremProducer3::implyNegatedInequalityDiffLogic(
const std::vector<Theorem>& antecedentThms,
const Expr& implied) {
3039 Theorem ArithTheoremProducer3::expandGrayShadowRewrite(
const Expr& theShadow) {
3044 Theorem ArithTheoremProducer3::compactNonLinearTerm(
const Expr& nonLinear) {
3054 Theorem ArithTheoremProducer3::implyDiffLogicBothBounds(
const Expr& x,
3055 std::vector<Theorem>& c1_le_x,
Rational c1,
3056 std::vector<Theorem>& x_le_c2,
Rational c2) {
3061 Theorem ArithTheoremProducer3::addInequalities(
const vector<Theorem>& thms) {
3083 Theorem ArithTheoremProducer3::intEqualityRationalConstant(
const Theorem& isIntConstrThm,
const Expr& constr) {
3088 Theorem ArithTheoremProducer3::cycleConflict(
const vector<Theorem>& inequalitites) {
3093 Theorem ArithTheoremProducer3::implyEqualities(
const vector<Theorem>& inequalitites) {
3112 CHECK_SOUND(
isLT(ineq),
"ArithTheoremProducerOld::LTtoLE: ineq must be <");
3115 "ArithTheoremProducerOld::lessThanToLE: bad integrality check:\n"
3116 " ineq = "+ineq.
toString()+
"\n isIntLHS = "
3119 "ArithTheoremProducerOld::lessThanToLE: bad integrality check:\n"
3120 " ineq = "+ineq.
toString()+
"\n isIntRHS = "
3124 vector<Theorem> thms;
3125 thms.push_back(isIntLHS);
3126 thms.push_back(isIntRHS);
3129 Expr le = changeRight?
leExpr(ineq[0], ineq[1] + rat(-1)) :
leExpr(ineq[0] + rat(1), ineq[1]);
3132 pfs.push_back(isIntLHS.
getProof());
3133 pfs.push_back(isIntRHS.
getProof());
3134 pf = newPf(changeRight?
"lessThan_To_LE_rhs" :
"lessThan_To_LE_lhs", le, pfs);
3137 return newRWTheorem(ineq, le, a, pf);
Expr minusExpr(const Expr &left, const Expr &right)
iterator begin() const
Begin iterator.
Expr ltExpr(const Expr &left, const Expr &right)
Data structure of expressions in CVC3.
bool isIntPred(const Expr &e)
const Rational & getRational() const
Get the Rational value out of RATIONAL_EXPR.
iterator find(const Expr &e)
void add(const std::vector< Theorem > &thms)
Expr eqExpr(const Expr &right) const
std::string toString(int base=10) const
Expr gtExpr(const Expr &left, const Expr &right)
#define DebugAssert(cond, str)
#define CHECK_SOUND(cond, msg)
bool isIntx(const Expr &e, const Rational &x)
bool isPlus(const Expr &e)
const std::vector< Expr > & getKids() const
bool isRational(const Expr &e)
Expr orExpr(const std::vector< Expr > &children)
Expr impExpr(const Expr &right) const
Op getOp() const
Get operator from expression.
size_t count(const Expr &e) const
#define FatalAssert(cond, msg)
If something goes horribly wrong, print a message and abort immediately with exit(1).
std::string toString() const
std::string toString() const
Print the expression to a string.
std::string int2string(int n)
const Expr & getRHS() const
Expr powExpr(const Expr &pow, const Expr &base)
Power (x^n, or base^{pow}) expressions.
const Assumptions & getAssumptionsRef() const
bool isIntegerConst(const Expr &e)
bool isIneq(const Expr &e)
Expr orExpr(const Expr &right) const
map< Expr, Rational, MonomialLess > MonomMap
TRUSTED implementation of arithmetic proof rules.
bool operator()(const Expr &e1, const Expr &e2) const
bool isDarkShadow(const Expr &e)
void setType(const Type &t) const
Set the cached type.
map< Expr, Rational, MonomialLess > MonomMap
bool isDivide(const Expr &e)
Expr plusExpr(const Expr &left, const Expr &right)
bool isGrayShadow(const Expr &e)
const Expr & getLHS() const
Expr geExpr(const Expr &left, const Expr &right)
Rational pow(Rational pow, const Rational &base)
Raise 'base' into the power of 'pow' (pow must be an integer)
bool isPow(const Expr &e)
Expr leExpr(const Expr &left, const Expr &right)
bool isMult(const Expr &e)
Expr andExpr(const std::vector< Expr > &children)
Rational ratRoot(const Rational &base, unsigned long int n)
take nth root of base, return result if it is exact, 0 otherwise
Expr multExpr(const Expr &left, const Expr &right)
iterator end() const
End iterator.