30 #define _CVC3_TRUSTED_
53 #define CLASS_NAME "ArithTheoremProducerOld"
59 if(withProof()) pf = newPf(
"var_to_mult", e);
60 return newRWTheorem(e, (rat(1) * e), Assumptions::emptyAssump(), pf);
65 Theorem ArithTheoremProducerOld::uMinusToMult(
const Expr& e) {
67 if(withProof()) pf = newPf(
"uminus_to_mult", e);
68 return newRWTheorem((-e), (rat(-1) * e), Assumptions::emptyAssump(), pf);
76 if(withProof()) pf = newPf(
"minus_to_plus", x, y);
77 return newRWTheorem((x-y), (x + (rat(-1) * y)), Assumptions::emptyAssump(), pf);
83 Theorem ArithTheoremProducerOld::canonUMinusToDivide(
const Expr& e) {
85 if(withProof()) pf = newPf(
"canon_uminus", e);
86 return newRWTheorem((-e), (e / rat(-1)), Assumptions::emptyAssump(), pf);
92 Theorem ArithTheoremProducerOld::canonDivideConst(
const Expr& c,
97 CLASS_NAME "::canonDivideConst:\n c not a constant: "
100 CLASS_NAME "::canonDivideConst:\n d not a constant: "
105 pf = newPf(
"canon_divide_const", c, d, d_hole);
107 return newRWTheorem((c/d), (rat(dr==0? 0 : (c.
getRational()/dr))), Assumptions::emptyAssump(), pf);
117 "Not a (c * x) expression: "
121 "d is not a constant: " + d.
toString());
124 Rational cdr(dr==0? 0 : (cx[0].getRational()/dr));
128 pf = newPf(
"canon_divide_mult", cx[0], cx[1], d);
131 return newRWTheorem((cx/d), (cx[1]), Assumptions::emptyAssump(), pf);
133 return newRWTheorem((cx/d), cd, Assumptions::emptyAssump(), pf);
135 return newRWTheorem((cx/d), (cd*cx[1]), Assumptions::emptyAssump(), pf);
143 "Expr is not a canonical sum: "
147 "d is not a const: " + d.
toString());
152 pf = newPf(
"canon_divide_plus", rat(sum.
arity()),
154 vector<Expr> newKids;
156 newKids.push_back((*i)/d);
158 return newRWTheorem((sum/d), (
plusExpr(newKids)), Assumptions::emptyAssump(), pf);
166 "d is not a const: " + d.
toString());
171 pf = newPf(
"canon_divide_var", e);
175 return newRWTheorem(e/d, e, Assumptions::emptyAssump(), pf);
177 return newRWTheorem(e/d, d, Assumptions::emptyAssump(), pf);
179 return newRWTheorem(e/d, rat(1/dr) * e, Assumptions::emptyAssump(), pf);
197 Expr ArithTheoremProducerOld::simplifiedMultExpr(std::vector<Expr> & mulKids)
199 DebugAssert(mulKids.size() >= 1 && mulKids[0].isRational(),
"");
200 if (mulKids.size() == 1) {
203 if ((mulKids[0] == rat(1)) && mulKids.size() == 2) {
210 Expr ArithTheoremProducerOld::canonMultConstMult(
const Expr & c,
217 std::vector<Expr> mulKids;
219 "ArithTheoremProducerOld::canonMultConstMult: "
220 "a canonized MULT expression must have arity "
221 "greater than 1: and first child must be "
224 mulKids.push_back(rat(c.
getRational() * (*i).getRational()));
226 for(; i != e.
end(); ++i) {
227 mulKids.push_back(*i);
229 return simplifiedMultExpr(mulKids);
232 Expr ArithTheoremProducerOld::canonMultConstPlus(
const Expr & e1,
240 std::vector<Theorem> thmPlusVector;
242 for(; i!= e2.
end(); ++i) {
243 thmPlusVector.push_back(canonMultMtermMterm(e1*(*i)));
247 d_theoryArith->substitutivityRule(e2.
getOp(), thmPlusVector);
251 Expr ArithTheoremProducerOld::canonMultPowPow(
const Expr & e1,
259 if (leaf1 == leaf2) {
264 else if (rsum == 1) {
269 return powExpr(rat(rsum), leaf1);
274 std::vector<Expr> mulKids;
275 mulKids.push_back(rat(1));
278 mulKids.push_back(e2);
279 mulKids.push_back(e1);
283 mulKids.push_back(e1);
284 mulKids.push_back(e2);
287 return simplifiedMultExpr(mulKids);
291 Expr ArithTheoremProducerOld::canonMultPowLeaf(
const Expr & e1,
299 if (leaf1 == leaf2) {
304 else if (rsum == 1) {
309 return powExpr(rat(rsum), leaf1);
314 std::vector<Expr> mulKids;
315 mulKids.push_back(rat(1));
318 mulKids.push_back(e2);
319 mulKids.push_back(e1);
323 mulKids.push_back(e1);
324 mulKids.push_back(e2);
326 return simplifiedMultExpr(mulKids);
330 Expr ArithTheoremProducerOld::canonMultLeafLeaf(
const Expr & e1,
337 if (leaf1 == leaf2) {
342 std::vector<Expr> mulKids;
343 mulKids.push_back(rat(1));
346 mulKids.push_back(e2);
347 mulKids.push_back(e1);
351 mulKids.push_back(e1);
352 mulKids.push_back(e2);
354 return simplifiedMultExpr(mulKids);
358 Expr ArithTheoremProducerOld::canonMultLeafOrPowMult(
const Expr & e1,
367 std::vector<Expr> mulKids;
371 mulKids.push_back(*i);
374 for(; i != e2.
end(); ++i) {
375 Expr leaf2 = ((*i).getKind() ==
POW) ? (*i)[1] : (*i);
376 if (leaf1 == leaf2) {
379 ((*i).getKind() ==
POW ? (*i)[0].getRational() : 1);
384 mulKids.push_back(leaf1);
388 mulKids.push_back(
powExpr(rat(r1 + r2), leaf1));
397 else if (leaf2 < leaf1) {
398 mulKids.push_back(e1);
399 mulKids.push_back(*i);
403 mulKids.push_back(*i);
406 mulKids.push_back(e1);
411 for (++i; i != e2.
end(); ++i) {
412 mulKids.push_back(*i);
415 return simplifiedMultExpr(mulKids);
423 return ArithTheoremProducerOld::greaterthan(e1,e2);
430 ArithTheoremProducerOld::canonCombineLikeTerms(
const std::vector<Expr> & sumExprs)
434 vector<Expr> sumKids;
438 std::vector<Expr>::const_iterator i = sumExprs.begin();
439 for (; i != sumExprs.end(); ++i) {
447 std::vector<Expr> mulKids;
449 mulKids.push_back(rat(1));
452 for (; j!= mul.
end(); ++j) {
453 mulKids.push_back(*j);
457 Expr tempExpr = mulKids.size() > 2 ?
multExpr(mulKids): mulKids[1];
458 MonomMap::iterator i=sumHashMap.find(tempExpr);
459 if (i == sumHashMap.end()) {
468 MonomMap::iterator i=sumHashMap.find(mul);
470 if (i == sumHashMap.end()) {
482 sumKids.push_back(rat(constant));
483 MonomMap::iterator j = sumHashMap.begin(), jend=sumHashMap.end();
484 for(; j != jend; ++j) {
485 if ((*j).second != 0)
487 (canonMultMtermMterm(rat((*j).second) * (*j).first).getRHS());
501 if ((constant == 0) && (sumKids.size() == 2)) {
504 else if (sumKids.size() == 1) {
511 Expr ArithTheoremProducerOld::canonMultLeafOrPowOrMultPlus(
const Expr & e1,
521 std::vector<Expr> sumExprs;
524 for (; i != e2.
end(); ++i) {
525 sumExprs.push_back(canonMultMtermMterm(e1 * (*i)).getRHS());
527 return canonCombineLikeTerms(sumExprs);
530 Expr ArithTheoremProducerOld::canonMultPlusPlus(
const Expr & e1,
537 std::vector<Expr> sumExprs;
540 for (; i != e1.
end(); ++i) {
542 for (; j != e2.
end(); ++j) {
543 sumExprs.push_back(canonMultMtermMterm((*i) * (*j)).getRHS());
546 return canonCombineLikeTerms(sumExprs);
554 ArithTheoremProducerOld::canonMultMtermMterm(
const Expr& e)
558 "canonMultMtermMterm: e = "+e.
toString());
562 const Expr& e1 = e[0];
563 const Expr& e2 = e[1];
564 string cmmm =
"canon_mult_mterm_mterm";
570 return canonMultZero(e2);
572 return canonMultOne(e2);
577 return canonMultConstConst(e1,e2);
583 return d_theoryArith->reflexivityRule (e);
587 rhs = canonMultConstMult(e1,e2);
588 if(withProof()) pf = newPf(cmmm,e,rhs);
589 return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
592 rhs = canonMultConstPlus(e1,e2);
593 if(withProof()) pf = newPf(cmmm,e,rhs);
594 return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
599 return d_theoryArith->reflexivityRule(e);
608 return canonMultMtermMterm(e2 * e1);
611 rhs = canonMultPowPow(e1,e2);
612 if(withProof()) pf = newPf(cmmm,e,rhs);
613 return newRWTheorem(e,rhs, Assumptions::emptyAssump(), pf);
616 rhs = canonMultLeafOrPowMult(e1,e2);
617 if(withProof()) pf = newPf(cmmm,e,rhs);
618 return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
621 rhs = canonMultLeafOrPowOrMultPlus(e1,e2);
622 if(withProof()) pf = newPf(cmmm,e,rhs);
623 return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
626 rhs = canonMultPowLeaf(e1,e2);
627 if(withProof()) pf = newPf(cmmm,e,rhs);
628 return newRWTheorem(e,rhs, Assumptions::emptyAssump(), pf);
637 return canonMultMtermMterm(e2 * e1);
644 for (; i != e1.end(); ++i) {
645 result = canonMultMtermMterm((*i) * result).getRHS();
647 if(withProof()) pf = newPf(cmmm,e,result);
648 return newRWTheorem(e, result, Assumptions::emptyAssump(), pf);
652 rhs = canonMultLeafOrPowOrMultPlus(e1,e2);
653 if(withProof()) pf = newPf(cmmm,e,rhs);
654 return newRWTheorem(e,rhs, Assumptions::emptyAssump(), pf);
659 return canonMultMtermMterm(e2 * e1);
669 return canonMultMtermMterm(e2 * e1);
672 rhs = canonMultPlusPlus(e1,e2);
673 if(withProof()) pf = newPf(cmmm,e,rhs);
674 return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
679 return canonMultMtermMterm(e2 * e1);
688 return canonMultMtermMterm(e2 * e1);
691 rhs = canonMultPowLeaf(e2,e1);
692 if(withProof()) pf = newPf(cmmm,e,rhs);
693 return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
696 rhs = canonMultLeafOrPowMult(e1,e2);;
697 if(withProof()) pf = newPf(cmmm,e,rhs);
698 return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
701 rhs = canonMultLeafOrPowOrMultPlus(e1,e2);
702 if(withProof()) pf = newPf(cmmm,e,rhs);
703 return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
707 rhs = canonMultLeafLeaf(e1,e2);
708 if(withProof()) pf = newPf(cmmm,e,rhs);
709 return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
714 return newRWTheorem(e, rhs, Assumptions::emptyAssump(), pf);
719 ArithTheoremProducerOld::canonPlus(
const Expr& e)
724 pf = newPf(
"canon_plus", e);
730 std::vector<Expr> sumKids;
732 for(; i != e.
end(); ++i) {
733 if ((*i).getKind() !=
PLUS) {
734 sumKids.push_back(*i);
739 for(; j != (*i).end(); ++j)
740 sumKids.push_back(*j);
743 Expr val = canonCombineLikeTerms(sumKids);
745 pf = newPf(
"canon_plus", e, val);
747 return newRWTheorem(e, val, Assumptions::emptyAssump(), pf);
752 ArithTheoremProducerOld::canonMult(
const Expr& e)
760 for (; i != e.
end(); ++i) {
761 result = canonMultMtermMterm(result * (*i)).getRHS();
764 pf = newPf(
"canon_mult", e,result);
768 if (d_theoryArith->nonlinearSignSplit()) {
771 Expr positive = d_em->trueExpr();
772 Expr negative = d_em->falseExpr();
776 int count_non_trivial = 0;
777 int count_constants = 0;
781 for (i = e.
begin(); i != e.
end(); ++i) {
784 if (
isPlus(current)) count_non_trivial ++;
788 count_non_trivial = 0;
792 zero.push_back(current.
eqExpr(rat(0)));
797 if (count_non_trivial > 0 && !count_constants == (e.
arity() - 1)) {
805 if (withProof()) split_pf = newPf(
"multiplicative_sign_split", e, lemma);
806 Theorem case_split_thm = newTheorem(lemma, Assumptions::emptyAssump(), split_pf);
808 TRACE(
"arith nonlinear",
"adding sign split: ", lemma,
"");
810 d_theoryArith->addMultiplicativeSignSplit(case_split_thm);
814 return newRWTheorem(e, result, Assumptions::emptyAssump(), pf);
819 ArithTheoremProducerOld::canonInvertConst(
const Expr& e)
827 pf = newPf(
"canon_invert_const", e);
830 return newRWTheorem((rat(1)/e), rat(er==0? 0 : (1/er)), Assumptions::emptyAssump(), pf);
835 ArithTheoremProducerOld::canonInvertLeaf(
const Expr& e)
840 pf = newPf(
"canon_invert_leaf", e);
842 return newRWTheorem((rat(1)/e),
powExpr(rat(-1), e), Assumptions::emptyAssump(), pf);
847 ArithTheoremProducerOld::canonInvertPow(
const Expr& e)
854 pf = newPf(
"canon_invert_pow", e);
856 if (e[0].getRational() == -1)
857 return newRWTheorem((rat(1)/e), e[1], Assumptions::emptyAssump(), pf);
859 return newRWTheorem((rat(1)/e),
860 powExpr(rat(-e[0].getRational()), e[1]),
861 Assumptions::emptyAssump(),
866 ArithTheoremProducerOld::canonInvertMult(
const Expr& e)
873 pf = newPf(
"canon_invert_mult", e);
877 Expr result = canonInvert(e[0]).getRHS();
878 for (
int i = 1; i < e.
arity(); ++i) {
880 canonMultMtermMterm(result * canonInvert(e[i]).getRHS()).getRHS();
882 return newRWTheorem((rat(1)/e), result, Assumptions::emptyAssump(), pf);
889 ArithTheoremProducerOld::canonInvert(
const Expr& e)
892 "Cannot do inverse on a PLUS"+e.
toString());
895 return canonInvertConst(e);
898 return canonInvertPow(e);
901 return canonInvertMult(e);
905 return canonInvertLeaf(e);
911 Theorem ArithTheoremProducerOld::moveSumConstantRight(
const Expr& e) {
927 vector<Expr> sumTerms;
933 if ((*it).isRational()) r = r + (*it).getRational();
935 else sumTerms.push_back((*it));
940 if (sumTerms.size() > 1)
945 transformed =
Expr(e.
getKind(), sumTerms[0], rat(-r));
950 if (withProof()) pf = newPf(
"arithm_sum_constant_right", e);
953 return newRWTheorem(e, transformed, Assumptions::emptyAssump(), pf);
957 ArithTheoremProducerOld::canonDivide(
const Expr& e)
963 pf = newPf(
"canon_invert_divide", e);
966 Theorem thm = newRWTheorem(e, e[0]*(canonInvert(e[1]).getRHS()), Assumptions::emptyAssump(), pf);
968 return d_theoryArith->transitivityRule(thm, canonMult(thm.
getRHS()));
975 ArithTheoremProducerOld::canonMultTermConst(
const Expr& c,
const Expr& t) {
980 "c is not a constant: " + c.
toString());
982 if(withProof()) pf = newPf(
"canon_mult_term_const", c, t);
983 return newRWTheorem((t*c), (c*t), Assumptions::emptyAssump(), pf);
989 ArithTheoremProducerOld::canonMultTerm1Term2(
const Expr& t1,
const Expr& t2) {
993 CHECK_SOUND(
false,
"Fatal Error: We don't support multiplication"
994 "of two non constant terms at this time "
1004 if(withProof()) pf = newPf(
"canon_mult_zero", e);
1005 return newRWTheorem((rat(0)*e), rat(0), Assumptions::emptyAssump(), pf);
1012 if(withProof()) pf = newPf(
"canon_mult_one", e);
1013 return newRWTheorem((rat(1)*e), e, Assumptions::emptyAssump(), pf);
1019 ArithTheoremProducerOld::canonMultConstConst(
const Expr& c1,
const Expr& c2) {
1024 "c1 is not a constant: " + c1.
toString());
1027 "c2 is not a constant: " + c2.
toString());
1029 if(withProof()) pf = newPf(
"canon_mult_const_const", c1, c2);
1031 newRWTheorem((c1*c2), rat(c1.
getRational()*c2.getRational()), Assumptions::emptyAssump(), pf);
1037 ArithTheoremProducerOld::canonMultConstTerm(
const Expr& c1,
1043 "c1 is not a constant: " + c1.
toString());
1046 "c2 is not a constant: " + c2.
toString());
1049 if(withProof()) pf = newPf(
"canon_mult_const_term", c1, c2, t);
1057 ArithTheoremProducerOld::canonMultConstSum(
const Expr& c1,
const Expr& sum) {
1059 std::vector<Expr> sumKids;
1064 "c1 is not a constant: " + c1.
toString());
1067 "the kind must be a PLUS: " + sum.
toString());
1070 for(; i != sum.
end(); ++i)
1071 sumKids.push_back(c1*(*i));
1073 if(withProof()) pf = newPf(
"canon_mult_const_sum", c1, sum, ret);
1074 return newRWTheorem((c1*sum),ret , Assumptions::emptyAssump(), pf);
1080 ArithTheoremProducerOld::canonPowConst(
const Expr& e) {
1084 "ArithTheoremProducerOld::canonPowConst("+e.
toString()+
")");
1090 "ArithTheoremProducerOld::canonPowConst("+e.
toString()+
")");
1093 if (base == 0 && p < 0) {
1096 else res = rat(
pow(p, base));
1099 pf = newPf(
"canon_pow_const", e, res);
1100 return newRWTheorem(e, res, Assumptions::emptyAssump(), pf);
1107 ArithTheoremProducerOld::canonFlattenSum(
const Expr& e) {
1109 std::vector<Expr> sumKids;
1113 "input must be a PLUS:" + e.
toString());
1117 for(; i != e.
end(); ++i){
1118 if (
PLUS != (*i).getKind())
1119 sumKids.push_back(*i);
1122 for(; j != (*i).end(); ++j)
1123 sumKids.push_back(*j);
1127 if(withProof()) pf = newPf(
"canon_flatten_sum", e,ret);
1128 return newRWTheorem(e,ret, Assumptions::emptyAssump(), pf);
1134 ArithTheoremProducerOld::canonComboLikeTerms(
const Expr& e) {
1136 std::vector<Expr> sumKids;
1142 for(; k != e.
end(); ++k)
1145 "input must be a flattened PLUS:" + k->
toString());
1148 for(; i != e.
end(); ++i){
1153 if(0 == sumHashMap.
count((*i)))
1156 sumHashMap[*i] += 1;
1159 if(0 == sumHashMap.
count((*i)[1]))
1160 sumHashMap[(*i)[1]] = (*i)[0].getRational();
1162 sumHashMap[(*i)[1]] = sumHashMap[(*i)[1]] + (*i)[0].getRational();
1167 sumKids.push_back(rat(constant));
1169 for(; j != sumHashMap.
end(); ++j) {
1170 if(0 == (*j).second)
1172 else if (1 == (*j).second)
1173 sumKids.push_back((*j).first);
1175 sumKids.push_back(rat((*j).second) * (*j).first);
1182 if(2 == sumKids.size() && 0 == constant) ret = sumKids[1];
1183 else if (1 == sumKids.size()) ret = sumKids[0];
1186 if(withProof()) pf = newPf(
"canon_combo_like_terms",e,ret);
1187 return newRWTheorem(e, ret, Assumptions::emptyAssump(), pf);
1199 vector<Expr> non_zero;
1202 for (; i != iend; ++i) {
1220 kids.push_back(leaf.
eqExpr(rat(0)));
1222 kids.push_back(rat(0).eqExpr(leaf));
1226 if (kids.size() == 1) newExpr = kids[0];
1227 else newExpr =
Expr(
OR, kids);
1229 pf = newPf(
"multEqZero", expr);
1232 return newRWTheorem(expr, newExpr, Assumptions::emptyAssump(), pf);
1246 "powEqZero invariant violated"+expr.
toString());
1250 pf = newPf(
"powEqZero", expr);
1255 res = d_em->falseExpr();
1258 res = rat(0).
eqExpr(expr[1][1]);
1260 return newRWTheorem(expr, res, Assumptions::emptyAssump(), pf);
1268 Expr power1, power2;
1269 bool ok = d_theoryArith->isPowersEquality(expr, power1, power2);
1274 pf = newPf(
"elimPower", expr);
1278 res = res.
orExpr(power1[1].eqExpr(-power2[1]));
1279 return newRWTheorem(expr, res, Assumptions::emptyAssump(), pf);
1291 bool ok = d_theoryArith->isPowerEquality(expr, constant, power);
1294 CHECK_SOUND(
pow(power[0].getRational(), root) == constant,
"elimPowerConst invariant violated" + expr.
toString());
1299 pf = newPf(
"elimPowerConst", expr, rat(root));
1303 res = res.
orExpr(power[1].eqExpr(rat(-root)));
1305 return newRWTheorem(expr, res, Assumptions::emptyAssump(), pf);
1310 Theorem ArithTheoremProducerOld::evenPowerEqNegConst(
const Expr& expr)
1316 bool ok = d_theoryArith->isPowerEquality(expr, constant, power);
1320 CHECK_SOUND(power[0].getRational().isInteger() && power[0].getRational() % 2 == 0,
"evenPowerEqNegConst invariant violated" + expr.
toString());
1324 pf = newPf(
"evenPowerEqNegConst", expr);
1325 return newRWTheorem(expr, d_em->falseExpr(), Assumptions::emptyAssump(), pf);
1336 bool ok = d_theoryArith->isPowerEquality(expr, constant, power);
1340 CHECK_SOUND(power[0].getRational() > 0,
"intEqIrrational invariant violated" + expr.
toString());
1341 CHECK_SOUND(
ratRoot(constant, power[0].getRational().getUnsigned()) == 0,
"intEqIrrational invariant violated" + expr.
toString());
1348 pf = newPf(
"int_eq_irr", expr, isIntx.
getProof());
1349 return newRWTheorem(expr, d_em->falseExpr(), assump, pf);
1359 "non-const parameters: " + e.
toString());
1367 result = (r1 == r2)?
true :
false;
1370 result = (r1 < r2)?
true :
false;
1373 result = (r1 <= r2)?
true :
false;
1376 result = (r1 > r2)?
true :
false;
1379 result = (r1 >= r2)?
true :
false;
1384 "ArithTheoremProducerOld::constPredicate: wrong kind");
1388 Expr ret = (result) ? d_em->trueExpr() : d_em->falseExpr();
1389 if(withProof()) pf = newPf(
"const_predicate", e,ret);
1390 return newRWTheorem(e, ret, Assumptions::emptyAssump(), pf);
1404 "ArithTheoremProducerOld::rightMinusLeft: wrong kind");
1406 if(withProof()) pf = newPf(
"right_minus_left",e);
1407 return newRWTheorem(e,
Expr(e.
getOp(), rat(0), e[1] - e[0]), Assumptions::emptyAssump(), pf);
1422 "ArithTheoremProducerOld::rightMinusLeft: wrong kind");
1424 if(withProof()) pf = newPf(
"left_minus_right",e);
1425 return newRWTheorem(e,
Expr(e.
getOp(), e[0] - e[1], rat(0)), Assumptions::emptyAssump(), pf);
1432 const Expr& z,
int kind) {
1439 "ArithTheoremProducerOld::plusPredicate: wrong kind");
1444 if(withProof()) pf = newPf(
"plus_predicate",left,right);
1445 return newRWTheorem(left, right, Assumptions::emptyAssump(), pf);
1455 "ArithTheoremProducerOld::multEqn(): multiplying equation by 0");
1456 if(withProof()) pf = newPf(
"mult_eqn", x, y, z);
1457 return newRWTheorem(x.
eqExpr(y), (x * z).eqExpr(y * z), Assumptions::emptyAssump(), pf);
1466 if(withProof()) pf = newPf(
"mult_eqn_nonconst", x, y, z);
1468 Assumptions::emptyAssump(), pf);
1483 "ArithTheoremProducerOld::multIneqn: wrong kind");
1485 "ArithTheoremProducerOld::multIneqn: "
1486 "z must be non-zero rational: " + z.
toString());
1493 ret =
Expr(op, e[0]*z, e[1]*z);
1495 ret =
Expr(op, e[1]*z, e[0]*z);
1496 if(withProof()) pf = newPf(
"mult_ineqn", e, ret);
1497 return newRWTheorem(e, ret, Assumptions::emptyAssump(), pf);
1521 CHECK_SOUND(
isIntPred(isIntRHSExpr) && isIntRHSExpr[0] == rhs,
"ArithTheoremProducerOld::multSimpleIneqnInt: not an integer proof of rhs");
1524 CHECK_SOUND((
LT == kind) || (
LE==kind) || (
GE==kind) || (
GT==kind),
"ArithTheoremProducerOld::multSimpleIneqnInt: wrong kind");
1530 CHECK_SOUND(
isPlus(rhs),
"ArithTheoremProducerOld::multSimpleIneqnInt: right-hand side must be a plus");
1531 CHECK_SOUND(rhs.
arity() == 2,
"ArithTheoremProducerOld::multSimpleIneqnInt: right-hand side a simple plus");
1537 CHECK_SOUND(a.isRational() && a.getRational().isInteger(),
"ArithTheoremProducerOld::multSimpleIneqnInt: right-hand side a simple plus of a constant");
1540 CHECK_SOUND(
isMult(bx) && bx.
arity() == 2,
"ArithTheoremProducerOld::multSimpleIneqnInt: right-hand side a simple plus of and a multiplication");
1545 CHECK_SOUND(b.isRational() && b.getRational().isInteger(),
"ArithTheoremProducerOld::multSimpleIneqnInt: right-hand side a simple plus of and a multiplication of a constant");
1547 CHECK_SOUND(x.
isVar(),
"ArithTheoremProducerOld::multSimpleIneqnInt: right-hand side a simple plus of and a multiplication of a constant and a leaf");
1556 pfs.push_back(isIntRHS.
getProof());
1557 pf = newPf(
"simpleineqint", ineq, pf);
1569 new_const = floor(a/b);
1571 ret =
Expr(kind, rat(0), rat(new_const) + x);
1573 ret =
Expr(kind, rat(0), x);
1576 new_const = ceil(a/b);
1579 ret =
Expr(kind, rat(0), rat(-new_const) + rat(-1)*x);
1581 ret =
Expr(kind, rat(0), rat(-1)*x);
1587 new_const = floor(a/b);
1589 ret =
Expr(kind, rat(0), rat(new_const) + x);
1591 ret =
Expr(kind, rat(0), x);
1594 new_const = ceil(a/b);
1597 ret =
Expr(kind, rat(0), rat(-new_const) + rat(-1)*x);
1599 ret =
Expr(kind, rat(0), rat(-1)*x);
1605 if (kind ==
GT) kind =
LT;
1609 new_const = ceil(a/b);
1612 ret =
Expr(kind, rat(0), rat(-new_const) + rat(-1)*x);
1614 ret =
Expr(kind, rat(0), rat(-1)*x);
1617 new_const = floor(a/b);
1619 ret =
Expr(kind, rat(0), rat(new_const) + x);
1621 ret =
Expr(kind, rat(0), x);
1627 return newRWTheorem(ineq, ret, Assumptions::emptyAssump(), pf);
1641 const Expr& x = e[0];
1642 const Expr& y = e[1];
1646 pf = newPf(
"eqToIneq", e);
1658 "ArithTheoremProducerOld::flipInequality: wrong kind: " +
1664 if(withProof()) pf = newPf(
"flip_inequality", e,ret);
1665 return newRWTheorem(e,ret, Assumptions::emptyAssump(), pf);
1675 const Expr& ineq = e[0];
1678 "ArithTheoremProducerOld::negatedInequality: wrong kind: " +
1681 "ArithTheoremProducerOld::negatedInequality: wrong kind: " +
1685 if(withProof()) pf = newPf(
"negated_inequality", e);
1697 return newRWTheorem(e,
Expr(kind, ineq[0], ineq[1]), Assumptions::emptyAssump(), pf);
1710 "ArithTheoremProducerOld::realShadow: Wrong Kind: " +
1714 "ArithTheoremProducerOld::realShadow:"
1715 " t must be same for both inputs: " +
1716 expr1[1].toString() +
" , " + expr2[0].toString());
1719 int firstKind = expr1.
getKind();
1720 int secondKind = expr2.
getKind();
1721 int kind = (firstKind == secondKind) ? firstKind :
LT;
1725 pfs.push_back(alphaLTt.
getProof());
1727 pf = newPf(
"real_shadow",expr1, expr2, pfs);
1729 return newTheorem(
Expr(kind, expr1[0], expr2[1]), a, pf);
1744 "ArithTheoremProducerOld::realShadowLTLE: Wrong Kind: " +
1748 "ArithTheoremProducerOld::realShadowLTLE:"
1749 " t must be same for both inputs: " +
1753 "ArithTheoremProducerOld::realShadowLTLE:"
1754 " alpha must be same for both inputs: " +
1761 pfs.push_back(alphaLEt.
getProof());
1762 pfs.push_back(tLEalpha.
getProof());
1763 pf = newPf(
"real_shadow_eq", alphaLEt.
getExpr(), tLEalpha.
getExpr(), pfs);
1765 return newRWTheorem(expr1[0], expr1[1], a, pf);
1769 ArithTheoremProducerOld::finiteInterval(
const Theorem& aLEt,
1777 "ArithTheoremProducerOld::finiteInterval:\n e1 = "
1781 "ArithTheoremProducerOld::finiteInterval:\n e1 = "
1785 "ArithTheoremProducerOld::finiteInterval:\n e1 = "
1789 "ArithTheoremProducerOld::finiteInterval:\n e1 = "
1793 && e2[1][1].getRational() >= 1,
1794 "ArithTheoremProducerOld::finiteInterval:\n e1 = "
1800 "Wrong integrality constraint:\n e1 = "
1801 +e1.
toString()+
"\n isInta = "+isIntaExpr.toString());
1803 "Wrong integrality constraint:\n e1 = "
1806 vector<Theorem> thms;
1807 thms.push_back(aLEt);
1808 thms.push_back(tLEac);
1809 thms.push_back(isInta);
1810 thms.push_back(isIntt);
1818 es.push_back(isInta.
getExpr());
1819 es.push_back(isIntt.
getExpr());
1824 pf = newPf(
"finite_interval", es, pfs);
1827 Expr g(grayShadow(e1[1], e1[0], 0, e2[1][1].getRational()));
1828 return newTheorem(g, a, pf);
1840 const Expr& isIntAlphaExpr = isIntAlpha.
getExpr();
1846 "ArithTheoremProducerOld::darkGrayShadow2ab: Wrong Kind: " +
1850 const Expr& beta = expr1[0];
1851 const Expr& bx = expr1[1];
1852 const Expr& ax = expr2[0];
1853 const Expr& alpha = expr2[1];
1854 Expr a_expr, b_expr, x;
1855 d_theoryArith->separateMonomial(ax, a_expr, x);
1856 d_theoryArith->separateMonomial(bx, b_expr, x);
1863 "ArithTheoremProducerOld::darkGrayShadow2ab:\n "
1864 "wrong integrality constraint:\n alpha = "
1865 +alpha.
toString()+
"\n isIntAlpha = "
1868 "ArithTheoremProducerOld::darkGrayShadow2ab:\n "
1869 "wrong integrality constraint:\n beta = "
1873 "ArithTheoremProducerOld::darkGrayShadow2ab:\n "
1874 "wrong integrality constraint:\n x = "
1886 "ArithTheoremProducerOld::darkGrayShadow2ab:\n beta<=bx: "
1888 +
"\n ax<=alpha: "+ axLEalpha.
toString());
1890 vector<Theorem> thms;
1891 thms.push_back(betaLEbx);
1892 thms.push_back(axLEalpha);
1893 thms.push_back(isIntAlpha);
1894 thms.push_back(isIntBeta);
1895 thms.push_back(isIntx);
1902 Expr g = grayShadow(ax, alpha, -a+1, 0);
1907 exprs.push_back(expr1);
1908 exprs.push_back(expr2);
1913 pfs.push_back(betaLEbx.
getProof());
1914 pfs.push_back(axLEalpha.
getProof());
1915 pfs.push_back(isIntAlpha.
getProof());
1916 pfs.push_back(isIntBeta.
getProof());
1919 pf = newPf(
"dark_grayshadow_2ab", exprs, pfs);
1922 return newTheorem((d || g), A, pf);
1933 const Expr& isIntAlphaExpr = isIntAlpha.
getExpr();
1939 "ArithTheoremProducerOld::darkGrayShadow2ba: Wrong Kind: " +
1943 const Expr& beta = expr1[0];
1944 const Expr& bx = expr1[1];
1945 const Expr& ax = expr2[0];
1946 const Expr& alpha = expr2[1];
1948 Expr a_expr, b_expr, x;
1949 d_theoryArith->separateMonomial(ax, a_expr, x);
1950 d_theoryArith->separateMonomial(bx, b_expr, x);
1957 "ArithTheoremProducerOld::darkGrayShadow2ab:\n "
1958 "wrong integrality constraint:\n alpha = "
1959 +alpha.
toString()+
"\n isIntAlpha = "
1962 "ArithTheoremProducerOld::darkGrayShadow2ab:\n "
1963 "wrong integrality constraint:\n beta = "
1967 "ArithTheoremProducerOld::darkGrayShadow2ab:\n "
1968 "wrong integrality constraint:\n x = "
1980 "ArithTheoremProducerOld::darkGrayShadow2ba:\n beta<=bx: "
1982 +
"\n ax<=alpha: "+ axLEalpha.
toString());
1984 vector<Theorem> thms;
1985 thms.push_back(betaLEbx);
1986 thms.push_back(axLEalpha);
1987 thms.push_back(isIntAlpha);
1988 thms.push_back(isIntBeta);
1989 thms.push_back(isIntx);
1994 pfs.push_back(betaLEbx.
getProof());
1995 pfs.push_back(axLEalpha.
getProof());
1996 pfs.push_back(isIntAlpha.
getProof());
1997 pfs.push_back(isIntBeta.
getProof());
2000 pf = newPf(
"dark_grayshadow_2ba", betaLEbx.
getExpr(),
2008 Expr g = grayShadow(bx, beta, 0, b-1);
2009 return newTheorem((d || g), A, pf);
2018 "ArithTheoremProducerOld::expandDarkShadow: not DARK_SHADOW: " +
2023 pf = newPf(
"expand_dark_shadow", theShadow, darkShadow.
getProof());
2033 "ArithTheoremProducerOld::expandGrayShadowConst0:"
2034 " not GRAY_SHADOW: " +
2037 "ArithTheoremProducerOld::expandGrayShadow0: c1!=c2: " +
2041 if(withProof()) pf = newPf(
"expand_gray_shadowconst0", theShadow,
2043 const Expr& v = theShadow[0];
2044 const Expr& e = theShadow[1];
2058 "ArithTheoremProducerOld::expandGrayShadowConst: not a shadow" +
2067 "ArithTheoremProducerOld::expandGrayShadow: " +
2071 const Expr& v = theShadow[0];
2072 const Expr& e = theShadow[1];
2076 Expr g1(grayShadow(v, e, c1, c));
2077 Expr g2(grayShadow(v, e, c+1, c2));
2081 exprs.push_back(theShadow);
2082 exprs.push_back(g1);
2083 exprs.push_back(g2);
2084 pf = newPf(
"split_gray_shadow", exprs, gThm.
getProof());
2095 "ArithTheoremProducerOld::expandGrayShadowConst: not a shadow" +
2104 "ArithTheoremProducerOld::expandGrayShadow: " +
2108 const Expr& v = theShadow[0];
2109 const Expr& e = theShadow[1];
2113 pf = newPf(
"expand_gray_shadow", theShadow, gThm.
getProof());
2122 ArithTheoremProducerOld::expandGrayShadowConst(
const Theorem& gThm) {
2124 const Expr& ax = theShadow[0];
2125 const Expr& cExpr = theShadow[1];
2126 const Expr& bExpr = theShadow[2];
2130 "ArithTheoremProducerOld::expandGrayShadowConst: "
2131 "'a' in a*x is not a const: " +theShadow.
toString());
2138 "ArithTheoremProducerOld::expandGrayShadowConst: "
2139 "not a GRAY_SHADOW: " +theShadow.
toString());
2141 "ArithTheoremProducerOld::expandGrayShadowConst: "
2142 "'a' is not integer: " +theShadow.
toString());
2144 "ArithTheoremProducerOld::expandGrayShadowConst: "
2145 "'c' is not rational" +theShadow.
toString());
2147 "ArithTheoremProducerOld::expandGrayShadowConst: b not integer: "
2153 Rational j = constRHSGrayShadow(c,b,a);
2165 pf = newPf(
"expand_gray_shadow_const_0", theShadow,
2167 conc = newTheorem(d_em->falseExpr(), assump, pf);
2168 }
else if(bAbs < a+j) {
2170 pf = newPf(
"expand_gray_shadow_const_1", theShadow,
2172 conc = newRWTheorem(ax, rat(c+b-signB*j), assump, pf);
2175 pf = newPf(
"expand_gray_shadow_const", theShadow,
2178 conc = newTheorem(ax.
eqExpr(rat(c+b-signB*j)).
orExpr(newGrayShadow),
2187 ArithTheoremProducerOld::grayShadowConst(
const Theorem& gThm) {
2195 const Expr& ax = g[0];
2196 const Expr& e = g[1];
2200 d_theoryArith->separateMonomial(ax, aExpr, x);
2204 "ArithTheoremProducerOld::grayShadowConst("+g.
toString()+
")");
2206 "ArithTheoremProducerOld::grayShadowConst("+g.
toString()+
")");
2214 "ArithTheoremProducerOld::grayShadowConst("+g.
toString()+
")");
2217 Rational newC1 = ceil((c1+c)/a), newC2 = floor((c2+c)/a);
2218 Expr newG((newC1 > newC2)? d_em->falseExpr()
2219 : grayShadow(x, rat(0), newC1, newC2));
2222 pf = newPf(
"gray_shadow_const", g, newG, gThm.
getProof());
2234 "ArithTheoremProducerOld::constRHSGrayShadow: a, b, c must be ints");
2238 return mod(a-(c+b), a);
2255 "ArithTheoremProducerOld::LTtoLE: ineq must be <");
2258 "ArithTheoremProducerOld::lessThanToLE: bad integrality check:\n"
2259 " ineq = "+ineq.
toString()+
"\n isIntLHS = "
2262 "ArithTheoremProducerOld::lessThanToLE: bad integrality check:\n"
2263 " ineq = "+ineq.
toString()+
"\n isIntRHS = "
2266 vector<Theorem> thms;
2267 thms.push_back(less);
2268 thms.push_back(isIntLHS);
2269 thms.push_back(isIntRHS);
2272 Expr le = changeRight?
2273 leExpr(ineq[0], ineq[1] + rat(-1))
2274 :
leExpr(ineq[0] + rat(1), ineq[1]);
2278 pfs.push_back(isIntLHS.
getProof());
2279 pfs.push_back(isIntRHS.
getProof());
2280 pf = newPf(changeRight?
"lessThan_To_LE_rhs" :
"lessThan_To_LE_lhs",
2284 return newRWTheorem(ineq, le, a, pf);
2297 ArithTheoremProducerOld::intVarEqnConst(
const Expr& eqn,
2308 "ArithTheoremProducerOld::intVarEqnConst: "
2309 "rhs has a wrong format: " + right.
toString());
2311 "ArithTheoremProducerOld:intVarEqnConst:left is not a zero: " +
2319 d_theoryArith->separateMonomial(right, aExpr, x);
2324 d_theoryArith->separateMonomial(right[1], aExpr, x);
2329 "ArithTheoremProducerOld:intVarEqnConst: "
2330 "bad integrality constraint:\n right = " +
2331 right.
toString()+
"\n isIntx = "+isIntxexpr.toString());
2332 CHECK_SOUND(a!=0,
"ArithTheoremProducerOld:intVarEqnConst: eqn = "
2357 pf = newPf(
"int_const_eq", eqn, x.
eqExpr(rat(r)),isIntx.
getProof());
2358 return newRWTheorem(eqn, x.
eqExpr(rat(r)), assump, pf);
2362 pf = newPf(
"int_const_eq", eqn, d_em->falseExpr(),isIntx.
getProof());
2363 return newRWTheorem(eqn, d_em->falseExpr(), assump, pf);
2369 ArithTheoremProducerOld::create_t(
const Expr& eqn) {
2370 const Expr& lhs = eqn[0];
2374 const Expr& x = lhs[1];
2379 sumModM(kids, eqn[1], m, m);
2381 kids.push_back(monomialModM(eqn[1], m, m));
2383 kids.push_back(
multExpr(rat(1/m), x));
2388 ArithTheoremProducerOld::create_t2(
const Expr& lhs,
const Expr& rhs,
2389 const Expr& sigma) {
2394 sumModM(kids, rhs, m, -1);
2396 kids.push_back(rat(0));
2397 Expr monom = monomialModM(rhs, m, -1);
2399 kids.push_back(monom);
2403 kids.push_back(rat(m)*sigma);
2408 ArithTheoremProducerOld::create_t3(
const Expr& lhs,
const Expr& rhs,
2409 const Expr& sigma) {
2415 sumMulF(kids, rhs, m, 1);
2417 kids.push_back(rat(0));
2418 Expr monom = monomialMulF(rhs, m, 1);
2420 kids.push_back(monom);
2424 kids.push_back(rat(-a)*sigma);
2432 Rational res((i - m*(floor((i/m) + half))));
2441 return (floor(i/m + half)+modEq(i,m));
2445 ArithTheoremProducerOld::sumModM(vector<Expr>& summands,
const Expr& sum,
2447 DebugAssert(divisor != 0,
"ArithTheoremProducerOld::sumModM: divisor = "
2452 C = modEq(C,m)/divisor;
2453 summands.push_back(rat(C));
2456 Expr monom = monomialModM(*i, m, divisor);
2458 summands.push_back(monom);
2465 ArithTheoremProducerOld::monomialModM(
const Expr& i,
2468 DebugAssert(divisor != 0,
"ArithTheoremProducerOld::monomialModM: divisor = "
2473 ai = modEq(ai,m)/divisor;
2474 if(0 == ai) res = rat(0);
2475 else if(1 == ai && i.
arity() == 2) res = i[1];
2477 vector<Expr> kids = i.
getKids();
2483 if(1 == ai) res = i;
2484 else res = rat(ai)*i;
2486 DebugAssert(!res.isNull(),
"ArithTheoremProducerOld::monomialModM()");
2488 +
", div="+divisor.
toString()+
") = ", res,
"");
2493 ArithTheoremProducerOld::sumMulF(vector<Expr>& summands,
const Expr& sum,
2495 DebugAssert(divisor != 0,
"ArithTheoremProducerOld::sumMulF: divisor = "
2501 summands.push_back(rat(C));
2504 Expr monom = monomialMulF(*i, m, divisor);
2506 summands.push_back(monom);
2513 ArithTheoremProducerOld::monomialMulF(
const Expr& i,
2516 DebugAssert(divisor != 0,
"ArithTheoremProducerOld::monomialMulF: divisor = "
2520 ai = f(ai,m)/divisor;
2521 if(0 == ai)
return rat(0);
2522 if(1 == ai)
return xi;
2534 i = eMap.
find(term);
2540 i = eMap.
find(term[1]);
2542 return term[0]*(*i).second;
2548 vector<Expr> output;
2550 output.push_back(substitute(*j, eMap));
2556 bool ArithTheoremProducerOld::greaterthan(
const Expr & l,
const Expr & r)
2559 if (l==r)
return false;
2578 ((r[1]==l[1]) && (r[0].getRational() < l[0].
getRational())));
2584 if (r[1] == l)
return false;
2585 return greaterthan(l, r[1]);
2593 return ((r < l[1]) || ((r == l[1]) && l[0].getRational() > 1));
2608 return ((l[1] == r) || greaterthan(l[1], r));
2618 for (; i != l.
end() && j != r.
end(); ++i, ++j) {
2621 return greaterthan(*i,*j);
2642 return ((l[1] == r) || greaterthan(l[1], r));
2657 return ((r[1] < l) || ((r[1] == l) && (r[0].getRational() < 1)));
2662 if (l == r[1])
return false;
2663 return greaterthan(l,r[1]);
2687 "Expected IS_INTEGER predicate");
2690 DebugAssert(!d_theoryArith->isInteger(expr),
"Expected non-integer");
2697 pf = newPf(
"isIntElim", isIntx.
getProof());
2700 Expr newVar = d_em->newBoundVarExpr(d_theoryArith->intType());
2703 return newTheorem(res, a, pf);
2709 const vector<Theorem>& isIntVars) {
2710 TRACE(
"arith eq",
"eqElimIntRule(", eqn.
getExpr(),
") {");
2715 "ArithTheoremProducerOld::eqElimInt: input must be an equation" +
2721 d_theoryArith->separateMonomial(lhs, a, x);
2727 "ArithTheoremProducerOld::eqElimInt\n eqn = "
2729 +
"\n isIntx = "+isIntxe.
toString());
2732 "ArithTheoremProducerOld::eqElimInt:\n lhs = "+lhs.
toString());
2736 "ArithTheoremProducerOld::eqElimInt:\n rhs = "+rhs.
toString());
2740 d_theoryArith->separateMonomial(rhs, c, v);
2743 && isIntVars[0].getExpr()[0] == v
2745 "ArithTheoremProducerOld::eqElimInt:\n rhs = "+rhs.
toString()
2746 +
"isIntVars.size = "+
int2string(isIntVars.size()));
2749 "ArithTheoremProducerOld::eqElimInt: rhs = "+rhs.
toString());
2752 "ArithTheoremProducerOld::eqElimInt: rhs = "+rhs.
toString());
2754 for(
size_t i=0, iend=isIntVars.size(); i<iend; ++i) {
2756 d_theoryArith->separateMonomial(rhs[i+1], c, v);
2757 const Expr&
isInt(isIntVars[i].getExpr());
2760 "ArithTheoremProducerOld::eqElimInt:\n rhs["+
int2string(i+1)
2768 static int varCount(0);
2769 Expr newVar = d_em->newBoundVarExpr(
"_int_var",
int2string(varCount++));
2771 Expr t2 = create_t2(lhs, rhs, newVar);
2772 Expr t3 = create_t3(lhs, rhs, newVar);
2774 vars.push_back(newVar);
2775 Expr res = d_em->newClosureExpr(
EXISTS, vars,
2778 vector<Theorem> thms(isIntVars);
2779 thms.push_back(isIntx);
2780 thms.push_back(eqn);
2787 vector<Theorem>::const_iterator i=isIntVars.begin(), iend=isIntVars.end();
2789 pfs.push_back(i->getProof());
2790 pf = newPf(
"eq_elim_int", eqn.
getExpr(), res, pfs);
2793 Theorem thm(newTheorem(res, assump, pf));
2794 TRACE(
"arith eq",
"eqElimIntRule => ", thm.
getExpr(),
" }");
2800 ArithTheoremProducerOld::isIntConst(
const Expr& e) {
2805 "ArithTheoremProducerOld::isIntConst(e = "
2809 pf = newPf(
"is_int_const", e);
2811 return newRWTheorem(e, isInt? d_em->trueExpr() : d_em->falseExpr(), Assumptions::emptyAssump(), pf);
2816 ArithTheoremProducerOld::equalLeaves1(
const Theorem& thm)
2823 e[1].getRational() ==
Rational(0) &&
2824 e[0].getKind() ==
PLUS &&
2825 e[0].arity() == 3 &&
2827 e[0][0].getRational() ==
Rational(0) &&
2828 e[0][1].getKind() ==
MULT &&
2829 e[0][1].arity() == 2 &&
2831 e[0][1][0].getRational() ==
Rational(-1),
2838 pf = newPf(
"equalLeaves1", e, pfs);
2840 return newRWTheorem(e, e[0][1][1].eqExpr(e[0][2]), thm.
getAssumptionsRef(), pf);
2845 ArithTheoremProducerOld::equalLeaves2(
const Theorem& thm)
2852 e[0].getRational() ==
Rational(0) &&
2853 e[1].getKind() ==
PLUS &&
2854 e[1].arity() == 3 &&
2856 e[1][0].getRational() ==
Rational(0) &&
2857 e[1][1].getKind() ==
MULT &&
2858 e[1][1].arity() == 2 &&
2860 e[1][1][0].getRational() ==
Rational(-1),
2867 pf = newPf(
"equalLeaves2", e, pfs);
2869 return newRWTheorem(e, e[1][1][1].eqExpr(e[1][2]), thm.
getAssumptionsRef(), pf);
2874 ArithTheoremProducerOld::equalLeaves3(
const Theorem& thm)
2881 e[1].getRational() ==
Rational(0) &&
2882 e[0].getKind() ==
PLUS &&
2883 e[0].arity() == 3 &&
2885 e[0][0].getRational() ==
Rational(0) &&
2886 e[0][2].getKind() ==
MULT &&
2887 e[0][2].arity() == 2 &&
2889 e[0][2][0].getRational() ==
Rational(-1),
2896 pf = newPf(
"equalLeaves3", e, pfs);
2898 return newRWTheorem(e, e[0][2][1].eqExpr(e[0][1]), thm.
getAssumptionsRef(), pf);
2903 ArithTheoremProducerOld::equalLeaves4(
const Theorem& thm)
2910 e[0].getRational() ==
Rational(0) &&
2911 e[1].getKind() ==
PLUS &&
2912 e[1].arity() == 3 &&
2914 e[1][0].getRational() ==
Rational(0) &&
2915 e[1][2].getKind() ==
MULT &&
2916 e[1][2].arity() == 2 &&
2918 e[1][2][0].getRational() ==
Rational(-1),
2925 pf = newPf(
"equalLeaves4", e, pfs);
2927 return newRWTheorem(e, e[1][2][1].eqExpr(e[1][1]), thm.
getAssumptionsRef(), pf);
2931 ArithTheoremProducerOld::diseqToIneq(
const Theorem& diseq) {
2938 "ArithTheoremProducerOld::diseqToIneq: expected disequality:\n"
2942 const Expr& x = e[0][0];
2943 const Expr& y = e[0][1];
2952 return newRWTheorem(e, d_em->trueExpr(), Assumptions::emptyAssump(), pf);
2963 "oneElimination: input must be a multiplication by one" + e.
toString());
2970 pf = newPf(
"oneElimination", e);
2973 return newRWTheorem(e, e[1], Assumptions::emptyAssump(), pf);
2979 const Expr& lowerBoundExpr = lowerBound.
getExpr();
2980 const Expr& upperBoundExpr = upperBound.
getExpr();
2984 CHECK_SOUND(
isLE(lowerBoundExpr) ||
isLT(lowerBoundExpr),
"clashingBounds: lowerBound should be >= or > " + lowerBoundExpr.
toString());
2985 CHECK_SOUND(
isGE(upperBoundExpr) ||
isGT(upperBoundExpr),
"clashingBounds: upperBound should be <= or < " + upperBoundExpr.
toString());
2988 CHECK_SOUND(lowerBoundExpr[1] == upperBoundExpr[1],
"clashingBounds: bounds not on the same term " + lowerBoundExpr.
toString() +
", " + upperBoundExpr.
toString());
2994 if (
isLE(lowerBoundExpr) &&
isGE(upperBoundExpr)) {
2995 CHECK_SOUND(upperBoundR < lowerBoundR,
"clashingBounds: bounds are satisfiable");
2997 CHECK_SOUND(upperBoundR <= lowerBoundR,
"clashingBounds: bounds are satisfiable");
3005 pf = newPf(
"clashingBounds", lowerBoundExpr, upperBoundExpr);
3009 assumptions.
add(lowerBound);
3010 assumptions.
add(upperBound);
3013 return newTheorem(d_em->falseExpr(), assumptions, pf);
3042 int kind = (kind1 == kind2) ? kind1 : ((kind1 ==
LT) || (kind2 ==
LT))?
LT :
GT;
3050 pf = newPf(
"addInequalities", expr1, expr2, pfs);
3058 return newTheorem(
Expr(kind, leftSide, rightSide), a, pf);
3065 Theorem ArithTheoremProducerOld::implyWeakerInequality(
const Expr& expr1,
const Expr& expr2) {
3075 CHECK_SOUND(expr1[0].
isRational() && expr1[0].getRational() == 0,
"implyWeakerInequality: expr1 should have a rational on the left side" + expr1.
toString());
3076 CHECK_SOUND(expr2[0].
isRational() && expr2[0].getRational() == 0,
"implyWeakerInequality: expr2 should have a rational on the left side" + expr2.
toString());
3080 vector<Expr> t1_children;
3087 int end_i = expr1[1].
arity();
3088 for(
int i = start_i; i < end_i; i ++) {
3089 const Expr& term = expr1[1][i];
3090 t1_children.push_back(term);
3093 t1_children.push_back(expr1[1]);
3094 Expr t1 = (t1_children.size() > 1 ?
plusExpr(t1_children) : t1_children[0]);
3098 vector<Expr> t2_children;
3105 int end_i = expr2[1].
arity();
3106 for(
int i = start_i; i < end_i; i ++) {
3107 const Expr& term = expr2[1][i];
3108 t2_children.push_back(term);
3111 t2_children.push_back(expr2[1]);
3112 Expr t2 = (t2_children.size() > 1 ?
plusExpr(t2_children) : t2_children[0]);
3119 if(withProof()) pf = newPf(
"implyWeakerInequality", expr1, expr2);
3122 return newTheorem(expr1.
impExpr(expr2), Assumptions::emptyAssump(), pf);
3131 Theorem ArithTheoremProducerOld::implyNegatedInequality(
const Expr& expr1,
const Expr& expr2) {
3142 CHECK_SOUND(expr1[0].
isRational() && expr1[0].getRational() == 0,
"implyNegatedInequality: expr1 should have a rational on the left side" + expr1.
toString());
3143 CHECK_SOUND(expr2[0].
isRational() && expr2[0].getRational() == 0,
"implyNegatedInequality: expr2 should have a rational on the left side" + expr2.
toString());
3147 vector<Expr> t1_children;
3154 int end_i = expr1[1].
arity();
3155 for(
int i = start_i; i < end_i; i ++) {
3156 const Expr& term = expr1[1][i];
3157 t1_children.push_back(term);
3160 t1_children.push_back(expr1[1]);
3161 Expr t1 = (t1_children.size() > 1 ?
plusExpr(t1_children) : t1_children[0]);
3165 vector<Expr> t2_children;
3172 int end_i = expr2[1].
arity();
3173 for(
int i = start_i; i < end_i; i ++) {
3174 const Expr& term = expr2[1][i];
3175 t2_children.push_back(term);
3178 t2_children.push_back(expr2[1]);
3179 Expr t2 = (t2_children.size() > 1 ?
plusExpr(t2_children) : t2_children[0]);
3184 for (
int i = 0; i < t1.
arity(); i++) {
3185 Expr term_t1 = t1[i];
3186 Expr term_t2 = t2[i];
3188 term_t1 = (
isMult(term_t1) ? term_t1[1] : term_t1);
3190 term_t2 = (
isMult(term_t2) ? term_t2[1] : term_t2);
3205 bool bothStrict = kind1 ==
LT && kind2 ==
LT;
3206 CHECK_SOUND(c1 + c2 < 0 || (c1 + c2 == 0 && bothStrict),
"implyNegatedInequality: sum of constants not negative!");
3211 if (withProof()) pf = newPf(
"implyNegatedInequality", expr1, expr2, expr2.
negate());
3214 return newTheorem(expr1.
impExpr(expr2.
negate()), Assumptions::emptyAssump(), pf);
3223 if (withProof()) pf = newPf(
"trustedRewrite", expr1, expr2);
3226 return newRWTheorem(expr1, expr2, Assumptions::emptyAssump(), pf);
3242 if (withProof()) pf = newPf(
"integerSplit", intVar, rat(intPoint));
3245 return newTheorem(split, Assumptions::emptyAssump(), pf);
3253 Theorem ArithTheoremProducerOld::rafineStrictInteger(
const Theorem& isIntConstrThm,
const Expr& constr) {
3259 CHECK_SOUND(constr[0].
isRational() && constr[0].getRational() == 0,
"rafineStrictInteger: left hand side must be 0");
3260 CHECK_SOUND(d_theoryArith->isLeaf(constr[1]) || constr[1][0].
isRational(),
"rafineStrictInteger: right side of the constraint must be a leaf or a sum, with the first one a rational");
3264 Expr ineqSum = constr[1];
3267 for (i = 0, j = 1; i < intSum.arity() && j < ineqSum.
arity(); i ++, j ++)
3268 if (!(intSum[i] == ineqSum[j]))
break;
3269 CHECK_SOUND(i == intSum.arity() && j == ineqSum.
arity(),
"rafineStrictInteger: proof of intger doesn't correspond to the constarint right side");
3271 CHECK_SOUND(intSum == ineqSum || intSum == ineqSum[1],
"rafineStrictInteger: proof of intger doesn't correspond to the constarint right side:" + intSum.
getString() +
" vs " + ineqSum[1].
getString());
3303 vector<Expr> newChildren;
3305 for (
int i = 0; i < constr[1].
arity(); i ++)
3306 if (constr[1][i].
isRational()) newChildren.push_back(rat(c));
3307 else newChildren.push_back(constr[1][i]);
3309 if (c != 0) newChildren.push_back(rat(c));
3310 newChildren.push_back(constr[1]);
3312 Expr newSum = newChildren.size() > 1 ?
plusExpr(newChildren) : newChildren[0];
3313 Expr newConstr(kind, rat(0), newSum);
3321 pf = newPf(
"rafineStrictInteger", constr,newConstr, isIntConstrThm.
getProof());
3324 return newRWTheorem(constr, newConstr, assump, pf);
3332 Theorem ArithTheoremProducerOld::intEqualityRationalConstant(
const Theorem& isIntConstrThm,
const Expr& constr) {
3340 CHECK_SOUND((sum_on_rhs && !sum_on_lhs) ||(!sum_on_rhs && sum_on_lhs),
3341 "intEqualityRationalConstant: left or right hand side must be 0");
3343 (sum_on_lhs && constr[0][0].
isRational() && !constr[0][0].getRational().isInteger()),
3344 "intEqualityRationalConstant: left or right side of the constraint must be a sum, with the first one a rational (non integer)");
3348 Expr eqSum = (sum_on_lhs ? constr[0] : constr[1]);
3351 for (i = 0, j = 1; i < intSum.
arity() && j < eqSum.
arity(); i ++, j ++)
3352 if (!(intSum[i] == eqSum[j]))
break;
3353 CHECK_SOUND(i == intSum.
arity() && j == eqSum.
arity(),
"intEqualityRationalConstant: proof of intger doesn't correspond to the constarint right side");
3355 CHECK_SOUND(intSum == eqSum[1],
"intEqualityRationalConstant: proof of intger doesn't correspond to the constarint right side:" + intSum.
getString() +
" vs " + eqSum[1].
getString());
3363 pf = newPf(
"intEqualityRationalConstant", constr, isIntConstrThm.
getProof());
3366 return newRWTheorem(constr, d_em->falseExpr(), assump, pf);
3369 Theorem ArithTheoremProducerOld::cycleConflict(
const vector<Theorem>& inequalitites) {
3374 for(
unsigned i = 0; i < inequalitites.size(); i++) {
3375 es.push_back(inequalitites[i].getExpr());
3376 pfs.push_back(inequalitites[i].getProof());
3378 pf = newPf(
"cycleConflict", es, pfs);
3382 for(
unsigned i = 0; i < inequalitites.size(); i ++)
3383 a.
add(inequalitites[i]);
3385 return newTheorem(d_em->falseExpr(), a, pf);
3388 Theorem ArithTheoremProducerOld::implyEqualities(
const std::vector<Theorem>& inequalities) {
3390 vector<Expr> conjuncts;
3391 for(
unsigned i = 0; i < inequalities.size(); i ++) {
3392 a.
add(inequalities[i]);
3393 Expr inequality = inequalities[i].getExpr();
3394 Expr equality = inequality[0].
eqExpr(inequality[1]);
3395 conjuncts.push_back(equality);
3402 for(
unsigned i = 0; i < inequalities.size(); i++) {
3403 es.push_back(inequalities[i].getExpr());
3404 pfs.push_back(inequalities[i].getProof());
3409 return newTheorem(
andExpr(conjuncts), a, pf);
3416 Theorem ArithTheoremProducerOld::lessThanToLERewrite(
const Expr& ineq,
3425 CHECK_SOUND(
isLT(ineq),
"ArithTheoremProducerOld::LTtoLE: ineq must be <");
3428 "ArithTheoremProducerOld::lessThanToLE: bad integrality check:\n"
3429 " ineq = "+ineq.
toString()+
"\n isIntLHS = "
3432 "ArithTheoremProducerOld::lessThanToLE: bad integrality check:\n"
3433 " ineq = "+ineq.
toString()+
"\n isIntRHS = "
3437 vector<Theorem> thms;
3438 thms.push_back(isIntLHS);
3439 thms.push_back(isIntRHS);
3442 Expr le = changeRight?
leExpr(ineq[0], ineq[1] + rat(-1)) :
leExpr(ineq[0] + rat(1), ineq[1]);
3445 pfs.push_back(isIntLHS.
getProof());
3446 pfs.push_back(isIntRHS.
getProof());
3447 pf = newPf(changeRight?
"lessThan_To_LE_rhs_rwr" :
"lessThan_To_LE_lhs_rwr", ineq, le, pfs);
3450 return newRWTheorem(ineq, le, a, pf);
3460 "ArithTheoremProducerOld::expandGrayShadowConst: not a shadow" +
3469 "ArithTheoremProducerOld::expandGrayShadow: " +
3473 const Expr& v = theShadow[0];
3474 const Expr& e = theShadow[1];
3476 vector<Expr> disjuncts;
3479 disjuncts.push_back(disjunct);
3486 exprs.push_back(theShadow);
3487 exprs.push_back(bigOr);
3488 pf = newPf(
"split_gray_shadow", exprs, gThm.
getProof());
3494 Theorem ArithTheoremProducerOld::implyWeakerInequalityDiffLogic(
const std::vector<Theorem>& antecedentThms,
const Expr& implied) {
3500 for(
unsigned i = 0; i < antecedentThms.size(); i++) {
3501 es.push_back(antecedentThms[i].getExpr());
3502 pfs.push_back(antecedentThms[i].getProof());
3504 pf = newPf(
"implyWeakerInequalityDiffLogic", implied,
Expr(
RAW_LIST,es), pfs);
3508 for(
unsigned i = 0; i < antecedentThms.size(); i ++) {
3509 a.
add(antecedentThms[i]);
3512 return newTheorem(implied, a, pf);
3516 Theorem ArithTheoremProducerOld::implyNegatedInequalityDiffLogic(
const std::vector<Theorem>& antecedentThms,
const Expr& implied) {
3522 for(
unsigned i = 0; i < antecedentThms.size(); i++) {
3523 es.push_back(antecedentThms[i].getExpr());
3524 pfs.push_back(antecedentThms[i].getProof());
3530 for(
unsigned i = 0; i < antecedentThms.size(); i ++) {
3531 a.
add(antecedentThms[i]);
3534 return newTheorem(implied.
notExpr(), a, pf);
3539 Theorem ArithTheoremProducerOld::expandGrayShadowRewrite(
const Expr& theShadow) {
3543 "ArithTheoremProducerOld::expandGrayShadowConst: not a shadow" +
3552 "ArithTheoremProducerOld::expandGrayShadow: " +
3556 const Expr& v = theShadow[0];
3557 const Expr& e = theShadow[1];
3561 pf = newPf(
"expand_gray_shadow", theShadow);
3564 return newRWTheorem(theShadow, ineq1 && ineq2, Assumptions::emptyAssump(), pf);
3567 Theorem ArithTheoremProducerOld::compactNonLinearTerm(
const Expr& nonLinear) {
3570 multiset<Expr> commonLeaves;
3574 for (
int i = 0; i < nonLinear.
arity(); i ++) {
3577 Expr monomial = nonLinear[i];
3580 multiset<Expr> currentLeaves;
3584 for (
int j = 0; j < monomial.
arity(); j ++)
3586 if (
isPow(monomial[j])) {
3588 currentLeaves.insert(monomial[j][1]);
3590 currentLeaves.insert(monomial[j]);
3592 }
else if (
isPow(monomial)) {
3594 currentLeaves.insert(monomial[1]);
3596 currentLeaves.insert(monomial);
3600 commonLeaves.swap(currentLeaves);
3603 multiset<Expr> intersectLeaves;
3604 set_intersection(currentLeaves.begin(), currentLeaves.end(),
3605 commonLeaves.begin(), commonLeaves.end(),
3606 insert_iterator< multiset<Expr> >
3607 (intersectLeaves, intersectLeaves.begin()));
3608 intersectLeaves.swap(commonLeaves);
3614 if (commonLeaves.size() > 0) {
3617 Expr constant = rat(0);
3620 vector<Expr> sumChildren;
3623 for (
int i = 0; i < nonLinear.
arity(); i ++) {
3626 Expr monomial = nonLinear[i];
3629 multiset<Expr> currentChildren;
3633 for (
int j = 0; j < monomial.
arity(); j ++)
3634 if (
isPow(monomial[j])) {
3636 currentChildren.insert(monomial[j][1]);
3638 currentChildren.insert(monomial[j]);
3639 }
else if (
isPow(monomial)) {
3641 currentChildren.insert(monomial[1]);
3643 currentChildren.insert(monomial);
3646 multiset<Expr> diffChildren;
3647 set_difference(currentChildren.begin(), currentChildren.end(),
3648 commonLeaves.begin(), commonLeaves.end(),
3649 insert_iterator< multiset<Expr> >
3650 (diffChildren, diffChildren.begin()));
3653 if (diffChildren.size() == 1) {
3654 sumChildren.push_back(*diffChildren.begin());
3655 }
else if (diffChildren.size() == 0) {
3656 sumChildren.push_back(rat(1));
3658 multiset<Expr>::iterator it = diffChildren.begin();
3659 multiset<Expr>::iterator it_end = diffChildren.end();
3660 vector<Expr> multChildren;
3661 while (it != it_end) {
3662 multChildren.push_back(*it);
3665 sumChildren.push_back(
multExpr(multChildren));
3668 constant = nonLinear[i];
3672 vector<Expr> multChildren;
3673 multChildren.push_back(
plusExpr(sumChildren));
3674 multiset<Expr>::iterator it = commonLeaves.begin();
3675 multiset<Expr>::iterator it_end = commonLeaves.end();
3676 for (; it != it_end; it ++)
3677 multChildren.push_back(*it);
3686 pf = newPf(
"compactNonlinear", nonLinear, result);
3688 return newRWTheorem(nonLinear, result, Assumptions::emptyAssump(), pf);
3706 CHECK_SOUND(c <= 0,
"ArithTheoremProducerOld::nonLinearIneqSignSplit: " + ineq.
toString());
3710 Expr signXor = d_em->trueExpr();
3712 for (
int i = 0; i < mult.
arity(); i ++) {
3713 Expr term = mult[i];
3715 term =
Expr(
POW, -term[0], term[1]);
3720 Expr zeroOr = d_em->falseExpr();
3721 for (
int i = 0; i < mult.
arity(); i ++) {
3722 Expr term = mult[i];
3725 signXor = zeroOr.
orExpr(signXor);
3731 exprs.push_back(ineq);
3732 exprs.push_back(signXor);
3733 pf = newPf(
"nonLinearIneqSignSplit", exprs, ineqThm.
getProof());
3737 assumptions.
add(ineqThm);
3739 return newTheorem(signXor, assumptions, pf);
3742 Theorem ArithTheoremProducerOld::implyDiffLogicBothBounds(
const Expr& x,
3743 std::vector<Theorem>& c1_le_x,
Rational c1,
3744 std::vector<Theorem>& x_le_c2,
Rational c2)
3751 for(
unsigned i = 0; i < c1_le_x.size(); i++) {
3752 es.push_back(c1_le_x[i].getExpr());
3753 pfs.push_back(c1_le_x[i].getProof());
3755 for(
unsigned i = 0; i < x_le_c2.size(); i++) {
3756 es.push_back(x_le_c2[i].getExpr());
3757 pfs.push_back(x_le_c2[i].getProof());
3759 pf = newPf(
"implyDiffLogicBothBounds", es, pfs);
3763 for(
unsigned i = 0; i < x_le_c2.size(); i ++) {
3766 for(
unsigned i = 0; i < x_le_c2.size(); i ++) {
3770 Expr implied = grayShadow(x, rat(0), c1, c2);
3772 return newTheorem(implied, a, pf);
3775 Theorem ArithTheoremProducerOld::addInequalities(
const vector<Theorem>& thms) {
3779 for (
unsigned i = 0; i < thms.size(); i ++) {
3780 Expr expr = thms[i].getExpr();
3788 for (
unsigned i = 0; i < thms.size(); i ++)
3793 for (
unsigned i = 0; i < thms.size(); i ++)
3794 if (thms[i].getExpr().getKind() ==
LT) kind =
LT;
3801 for (
unsigned i = 0; i < thms.size(); i ++) {
3802 pfs.push_back(thms[i].getProof());
3803 exps.push_back(thms[i].getExpr());
3805 pf = newPf(
"addInequalities", exps, pfs);
3809 vector<Expr> summandsLeft;
3810 vector<Expr> summandsRight;
3811 for (
unsigned i = 0; i < thms.size(); i ++) {
3812 summandsLeft.push_back(thms[i].getExpr()[0]);
3813 summandsRight.push_back(thms[i].getExpr()[1]);
3819 return newTheorem(
Expr(kind, leftSide, rightSide), a, pf);
3832 pf = newPf(
"power_of_one", e);
3834 return newRWTheorem(e, e[1], Assumptions::emptyAssump(), pf);
3845 if (e.
isAtomic() && d_theoryArith->isLeaf(e)) {
3850 if (it != cache.
end())
return;
3861 for (; k < e.
arity(); ++k) {
3862 getLeaves(e[k], s, cache);
3870 "invariant violated");
3873 set<Rational> lhs, rhs;
3875 getLeaves(e[0], lhs, cache);
3878 getLeaves(e[1], rhs, cache);
3883 set<Rational> common;
3884 set_intersection(lhs.begin(), lhs.end(), rhs.begin(), rhs.end(),
3885 inserter(common, common.begin()));
3886 if (common.empty()) {
3887 res = d_em->falseExpr();
3892 set<Rational>::iterator it;
3895 if ((*it) < (*(rhs.begin()))) {
3896 res = d_em->trueExpr();
3900 if ((*it) <= (*(lhs.begin()))) {
3901 res = d_em->falseExpr();
3907 set<Rational>::iterator it;
3910 if ((*it) <= (*(rhs.begin()))) {
3911 res = d_em->trueExpr();
3916 if ((*it) < (*(lhs.begin()))) {
3917 res = d_em->falseExpr();
3924 set<Rational>::iterator it;
3927 if ((*(lhs.begin())) > (*it)) {
3928 res = d_em->trueExpr();
3932 if ((*(rhs.begin())) >= (*it)) {
3933 res = d_em->falseExpr();
3939 set<Rational>::iterator it;
3942 if ((*(lhs.begin())) >= (*it)) {
3943 res = d_em->trueExpr();
3947 if ((*(rhs.begin())) > (*it)) {
3948 res = d_em->falseExpr();
3956 if (res.
isNull())
return d_theoryArith->reflexivityRule(e);
3960 pf = newPf(
"rewrite_leaves_const", e);
3961 return newRWTheorem(e, res, Assumptions::emptyAssump(), pf);
Expr minusExpr(const Expr &left, const Expr &right)
iterator begin() const
Begin iterator.
bool isAtomic() const
Test if e is atomic.
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)
bool isPropAtom() const
True iff expr is not a Bool connective.
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
Expr andExpr(const Expr &right) 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.
Expr iffExpr(const Expr &right) const
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 isIneq(const Expr &e)
Expr orExpr(const Expr &right) const
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)
iterator find(const Expr &e)
TRUSTED implementation of arithmetic proof rules.
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)
const std::string & getString() const
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)
map< Expr, Rational, MonomialLess > MonomMap
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.