33 #include "../theory_core/core_proof_rules.h"
47 os <<
"FreeConst(r=" << fc.
getConst() <<
", "
48 << (fc.
strict()?
"strict" :
"non-strict") <<
")";
57 os <<
"Ineq(" << ineq.
ineq().
getExpr() <<
", isolated on "
58 << (ineq.
varOnRHS()?
"RHS" :
"LHS") <<
", const = "
74 if (
isInt(t))
return typePred(e);
84 if(e == isIntE)
return thm;
89 int i, iend=e.
arity();
90 for(i=0; i<iend; ++i) {
91 res = isIntegerDerive(isIntE, getCommonRules()->andElim(thm, i));
92 if(!res.
isNull())
return res;
98 const Rational& TheoryArithOld::freeConstIneq(
const Expr& ineq,
bool varOnRHS) {
100 const Expr& e = varOnRHS? ineq[0] : ineq[1];
102 switch(e.getKind()) {
104 return e[0].getRational();
106 return e.getRational();
116 TheoryArithOld::updateSubsumptionDB(
const Expr& ineq,
bool varOnRHS,
118 TRACE(
"arith ineq",
"TheoryArithOld::updateSubsumptionDB(", ineq,
119 ", var isolated on "+
string(varOnRHS?
"RHS" :
"LHS")+
")");
124 const Expr& t = varOnRHS? ineq[0] : ineq[1];
125 bool strict(
isLT(ineq));
137 kids.push_back(rat(0));
138 for(++i; i!=iend; ++i) kids.push_back(*i);
144 index =
leExpr(rat(0), canonSimplify(ineq[1] - newT).getRHS());
146 index =
leExpr(canonSimplify(ineq[0]-newT).getRHS(), rat(0));
150 index =
leExpr(rat(0), ineq[1]);
152 index =
leExpr(ineq[0], rat(0));
153 }
else if(
isLT(ineq))
154 index =
leExpr(ineq[0], ineq[1]);
159 iend=d_freeConstDB.end();
165 TRACE(
"arith ineq",
"freeConstDB["+index.toString()+
"] := ", obj,
"");
179 TRACE(
"arith ineq",
"freeConstDB["+index.toString()+
"] := ", obj,
"");
186 bool TheoryArithOld::kidsCanonical(
const Expr& e) {
187 if(isLeaf(e))
return true;
189 for(
int i=0; res && i<e.
arity(); ++i) {
190 Expr simp(canon(e[i]).getRHS());
191 res = (e[i] == simp);
192 IF_DEBUG(
if(!res) debugger.getOS() <<
"\ne[" << i <<
"] = " << e[i]
193 <<
"\nsimplified = " << simp <<
endl;)
220 TRACE(
"arith canon",
"canon(",e,
") {");
225 Theorem thm = d_rules->uMinusToMult(e[0]);
227 result = transitivityRule(thm, canon(e2));
237 result = d_rules->canonPlus(e);
241 Theorem minus_eq_sum = d_rules->minusToPlus(e[0], e[1]);
243 Expr sum(minus_eq_sum.getRHS());
245 if(thm.getLHS() == thm.getRHS())
246 result = canonThm(minus_eq_sum);
249 vector<unsigned> changed;
250 vector<Theorem> thms;
251 changed.push_back(1);
253 Theorem sum_eq_canon = canonThm(substitutivityRule(sum, changed, thms));
254 result = transitivityRule(minus_eq_sum, sum_eq_canon);
260 result = d_rules->canonMult(e);
345 if (e[1].getKind() ==
PLUS)
347 result = d_rules->canonDivide(e);
352 result = d_rules->canonPowConst(e);
355 if (e[0].
isRational() && e[0].getRational() == 1) {
356 result = d_rules->powerOfOne(e);
358 result = reflexivityRule(e);
362 result = reflexivityRule(e);
365 TRACE(
"arith canon",
"canon => ",result,
" }");
371 TheoryArithOld::canonSimplify(
const Expr& e) {
372 TRACE(
"arith simplify",
"canonSimplify(", e,
") {");
374 "TheoryArithOld::canonSimplify("+e.
toString()+
")");
375 DebugAssert(leavesAreSimp(e),
"Expected leaves to be simplified");
379 thm = transitivityRule(thm, find(thm.
getRHS()));
384 +
"\nsimplify(canon(e)) = "+simplifyExpr(thm.
getRHS()).toString());
393 TRACE(
"arith",
"canonSimplify =>", thm,
" }");
401 TheoryArithOld::canonPred(
const Theorem& thm) {
402 vector<Theorem> thms;
404 "TheoryArithOld::canonPred: bad theorem: "+thm.
toString());
406 thms.push_back(canonSimplify(e[0]));
407 thms.push_back(canonSimplify(e[1]));
408 Theorem result = iffMP(thm, substitutivityRule(e.
getOp(), thms));
417 TheoryArithOld::canonPredEquiv(
const Theorem& thm) {
418 vector<Theorem> thms;
420 "TheoryArithOld::canonPredEquiv: bad theorem: "+thm.
toString());
422 thms.push_back(canonSimplify(e[0]));
423 thms.push_back(canonSimplify(e[1]));
424 Theorem result = transitivityRule(thm, substitutivityRule(e.
getOp(), thms));
434 TheoryArithOld::canonConjunctionEquiv(
const Theorem& thm) {
435 vector<Theorem> thms;
451 TRACE(
"arith eq",
"doSolve(",e,
") {");
454 vector<Theorem> thms;
459 eqnThm = iffMP(thm, d_rules->rightMinusLeft(e));
460 eqnThm = canonPred(eqnThm);
467 Theorem result = iffMP(eqnThm, d_rules->constPredicate(eqnThm.getExpr()));
468 TRACE(
"arith eq",
"doSolve => ",result,
" }");
473 eqnThm = iffMP(eqnThm, normalize(eqnThm.getExpr()));
474 TRACE(
"arith eq",
"doSolve => ",eqnThm.getExpr(),
" }");
475 right = eqnThm.getRHS();
482 DebugAssert(right.arity() > 1,
"Expected arity > 1");
484 Rational r = right[0].getRational();
485 if (r == 0)
return getCommonRules()->trueTheorem();
487 enqueueFact(iffMP(eqnThm, d_rules->multEqZero(eqnThm.getExpr())));
488 return getCommonRules()->trueTheorem();
491 d_rules->multEqn(eqnThm.getLHS(),
493 res = canonPred(res);
497 enqueueFact(iffMP(eqnThm, d_rules->multEqZero(eqnThm.getExpr())));
498 return getCommonRules()->trueTheorem();
501 else if (
isPow(right)) {
502 DebugAssert(right.arity() == 2,
"Expected arity 2");
504 return doSolve(iffMP(eqnThm, d_rules->powEqZero(eqnThm.getExpr())));
506 throw ArithException(
"Can't solve exponential eqn: "+eqnThm.toString());
509 if(!isInteger(right)) {
510 return processRealEq(eqnThm);
513 return processIntEq(eqnThm);
563 bool TheoryArithOld::pickIntEqMonomial(
const Expr&
right,
Expr& isolated,
bool& nonlin)
566 "TheoryArithOld::pickIntEqMonomial right is wrong :-): " +
569 "TheoryArithOld::pickIntEqMonomial. right[0] must be const" +
583 for(; i != iend; ++i) {
588 else if (
isMult(*i) && (*i).arity() == 2 && (*i)[0].isRational() && isLeaf((*i)[1])) {
590 coeff =
abs((*i)[0].getRational());
596 for (j = istart; j != iend; ++j) {
597 if (j != i && isLeafIn(leaf, *j))
break;
600 if (!found || min > coeff) {
615 TheoryArithOld::processRealEq(
const Theorem& eqn)
619 "processRealEq invariant violated");
635 for(
int i = 1, iend = right.arity(); i < iend; ++i) {
641 Expr leaf = isLeaf(c) ? c : c[1];
643 for (j = 1; j < iend; ++j) {
645 && isLeafIn(leaf, right[j])
659 else if ((
isMult(right) && right.arity() == 2 && isLeaf(right[1])) ||
673 if (isNonlinearEq(eqn.
getExpr()))
674 return processIntEq(eqn);
688 "TheoryArithOld::ProcessRealEq: left is integer:\n left = "
694 result = canonPred(result);
697 result = iffMP(result, d_rules->plusPredicate(result.getLHS(),
698 result.getRHS(),
left,
EQ));
699 result = canonPred(result);
700 TRACE(
"arith",
"processRealEq => ",result,
" }");
705 void TheoryArithOld::getFactors(
const Expr& e, set<Expr>& factors)
711 for (; i != iend; ++i) {
712 getFactors(*i, factors);
721 if (isLeaf(e[1])) factors.insert(e[1]);
726 DebugAssert(factors.find(e) == factors.end(),
"expected new entry");
739 TheoryArithOld::processSimpleIntEq(
const Theorem& eqn)
741 TRACE(
"arith eq",
"processSimpleIntEq(", eqn.
getExpr(),
") {");
743 "TheoryArithOld::processSimpleIntEq: eqn must be equality" +
749 "TheoryArithOld::processSimpleIntEq: LHS must be 0:\n" +
754 if (2 == right.arity() &&
756 (
isMult(right[1]) && right[1].arity() == 2 && right[1][0].isRational() && isLeaf(right[1][1])))) {
759 separateMonomial(right[1], c, x);
764 TRACE(
"arith eq",
"processSimpleIntEq[0 = c + a*x] => ", res,
" }");
770 if (pickIntEqMonomial(right, isolated, nonlin)) {
771 TRACE(
"arith eq",
"processSimpleIntEq: isolated = ", isolated,
"");
783 result = iffMP(eqn, d_rules->multEqn(eqn.
getLHS(),
right, rat(r)));
784 result = canonPred(result);
788 result = iffMP(result,
795 isolated = (a == 1)? isolated[1] : rat(a) * isolated[1];
798 result = iffMP(eqn, d_rules->plusPredicate(eqn.
getLHS(),
802 result = canonPred(result);
805 if(!
isMult(isolated) || isolated[0].getRational() == 1) {
806 TRACE(
"arith eq",
"processSimpleIntEq[x = rhs] => ", result,
" }");
808 }
else if (!nonlin) {
810 "TheoryArithOld::processSimpleIntEq: isolated must be mult "
811 "with coeff >= 2.\n isolated = " + isolated.
toString());
817 separateMonomial(lhs, a, x);
818 Theorem isIntLHS = isIntegerThm(x);
819 vector<Theorem> isIntRHS;
822 separateMonomial(rhs, c, v);
823 isIntRHS.push_back(isIntegerThm(v));
830 for(; i!=iend; ++i) {
832 separateMonomial(*i, c, v);
833 isIntRHS.push_back(isIntegerThm(v));
838 result = d_rules->eqElimIntRule(result, isIntLHS, isIntRHS);
840 result = getCommonRules()->skolemize(result);
844 Theorem thm1 = canonPred(getCommonRules()->andElim(result, 0));
845 Theorem thm2 = canonPred(getCommonRules()->andElim(result, 1));
846 Theorem newRes = getCommonRules()->andIntro(thm1, thm2);
849 TRACE(
"arith eq",
"processSimpleIntEq => ", result,
" }");
857 Theorem result = symmetryRule(eqn);
858 TRACE(
"arith eq",
"processSimpleIntEq[x = 0] => ", result,
" }");
869 TheoryArithOld::processIntEq(
const Theorem& eqn)
871 TRACE(
"arith eq",
"processIntEq(", eqn.
getExpr(),
") {");
873 std::vector<Theorem> solvedAndNewEqs;
877 result = processSimpleIntEq(newEq);
880 solvedAndNewEqs.push_back(result);
890 solvedAndNewEqs.push_back(getCommonRules()->andElim(result, 0));
891 newEq = getCommonRules()->andElim(result, 1);
896 else if (solvedAndNewEqs.size() > 0)
897 res = solvedForm(solvedAndNewEqs);
899 TRACE(
"arith eq",
"processIntEq => ", res.
getExpr(),
" }");
912 TheoryArithOld::solvedForm(
const vector<Theorem>& solvedEqs)
914 DebugAssert(solvedEqs.size() > 0,
"TheoryArithOld::solvedForm()");
917 TRACE_MSG(
"arith eq",
"TheoryArithOld::solvedForm:solvedEqs(\n [");
918 IF_DEBUG(
if(debugger.trace(
"arith eq")) {
919 for(vector<Theorem>::const_iterator j = solvedEqs.begin(),
920 jend=solvedEqs.end(); j!=jend;++j)
921 TRACE(
"arith eq",
"", j->getExpr(),
",\n ");
926 vector<Theorem>::const_reverse_iterator
927 i = solvedEqs.rbegin(),
928 iend = solvedEqs.rend();
932 for(; i!=iend; ++i) {
934 Theorem thm = substAndCanonize(*i, subst);
935 TRACE(
"arith eq",
"solvedForm: subst["+i->getLHS().toString()+
"] = ",
937 subst[i->getLHS()] = thm;
942 "TheoryArithOld::solvedForm: an element of solvedEqs must "
943 "be either EQ or FALSE: "+i->toString());
949 vector<Theorem> thms;
952 thms.push_back(i->second);
954 if (thms.size() > 1)
return getCommonRules()->andIntro(thms);
955 else return thms.back();
968 TRACE(
"arith eq",
"substAndCanonize(", t,
") {");
971 Theorem res(reflexivityRule(t));
972 TRACE(
"arith eq",
"substAndCanonize[subst empty] => ", res,
" }");
978 TRACE(
"arith eq",
"substAndCanonize[subst] => ", i->second,
" }");
983 Theorem res(reflexivityRule(t));
984 TRACE(
"arith eq",
"substAndCanonize[i-leaf] => ", res,
" }");
988 vector<Theorem> thms;
989 vector<unsigned> changed;
990 for(
unsigned j=0, jend=t.
arity(); j!=jend; ++j) {
991 Theorem thm = substAndCanonize(t[j], subst);
992 if(thm.
getRHS() != t[j]) {
995 changed.push_back(j);
1000 if(thms.size() > 0) {
1001 res = substitutivityRule(t, changed, thms);
1002 res = canonThm(res);
1005 res = reflexivityRule(t);
1006 TRACE(
"arith eq",
"substAndCanonize => ", res,
" }");
1020 if(subst.
empty())
return eq;
1026 Theorem thm = substAndCanonize(t, subst);
1028 if(thm.
getRHS() == t)
return eq;
1030 vector<Theorem> thms;
1031 vector<unsigned> changed;
1032 thms.push_back(thm);
1033 changed.push_back(1);
1034 return iffMP(eq, substitutivityRule(eq.
getExpr(), changed, thms));
1037 void TheoryArithOld::processBuffer()
1043 if (diffLogicOnly)
return;
1045 while (!inconsistent() && (d_bufferIdx_0 < d_buffer_0.size() || d_bufferIdx_1 < d_buffer_1.size() || d_bufferIdx_2 < d_buffer_2.size() || d_bufferIdx_3 < d_buffer_3.size())) {
1049 if (d_bufferIdx_0 < d_buffer_0.size()) {
1050 ineqThm = d_buffer_0[d_bufferIdx_0];
1051 d_bufferIdx_0 = d_bufferIdx_0 + 1;
1052 }
else if (d_bufferIdx_1 < d_buffer_1.size()) {
1053 ineqThm = d_buffer_1[d_bufferIdx_1];
1054 d_bufferIdx_1 = d_bufferIdx_1 + 1;
1055 }
else if (d_bufferIdx_2 < d_buffer_2.size()) {
1056 ineqThm = d_buffer_2[d_bufferIdx_2];
1057 d_bufferIdx_2 = d_bufferIdx_2 + 1;
1059 ineqThm = d_buffer_3[d_bufferIdx_3];
1060 d_bufferIdx_3 = d_bufferIdx_3 + 1;
1070 Theorem inequalityFindThm = inequalityToFind(ineqThm,
true);
1071 Expr inequalityFind = inequalityFindThm.
getExpr();
1075 TRACE(
"arith buffer",
"processing: ", inequality,
"");
1076 TRACE(
"arith buffer",
"with find : ", inequalityFind,
"");
1078 if (!
isIneq(inequalityFind)) {
1079 TRACE(
"arith buffer",
"find not an inequality... ",
"",
"skipping");
1083 if (alreadyProjected.find(inequalityFind) != alreadyProjected.end()) {
1084 TRACE(
"arith buffer",
"already projected ... ",
"",
"skipping");
1093 alreadyProjected[inequality] = dummy;
1094 if (inequality != inequalityFind) {
1096 alreadyProjected[inequalityFind] = dummy;
1098 Expr rhs = inequalityFind[1];
1104 updateStats(monomial);
1116 extractTermsFromInequality(inequalityFind, c1, t1, c2, t2);
1117 if (termLowerBound.find(t1) != termLowerBound.end() && c1 != termLowerBound[t1]) {
1118 TRACE(
"arith ineq",
"skipping because stronger bounds asserted ", inequalityFind.
toString(),
":" + t1.
toString());
1119 DebugAssert(termLowerBoundThm.find(t1) != termLowerBoundThm.end(),
"No lower bound on asserted atom!!! " + t1.
toString());
1120 Theorem strongerBound = termLowerBoundThm[t1];
1125 Theorem thm1 = isolateVariable(inequalityFindThm, varOnRHS);
1128 setInconsistent(thm1);
1133 DebugAssert(varOnRHS? !
isPlus(ineq[1]) : !
isPlus(ineq[0]),
"TheoryArithOld::processBuffer(): bad result from isolateVariable:\nineq = "+ineq.
toString());
1135 updateConstrained(inequalityFindThm.
getExpr());
1137 projectInequalities(thm1, varOnRHS);
1145 TRACE(
"arith stats",
"updateStats("+c.
toString()+
", ", v,
")");
1150 if (v.
getType() != d_realType) {
1155 if (maxFind == maxCoefficientLeft.end()) {
1156 maxCoefficientLeft[v] = - c;
1157 TRACE(
"arith stats",
"max left",
"",
"");
1160 if ((*maxFind).second < -c) {
1161 TRACE(
"arith stats",
"max left",
"",
"");
1162 maxCoefficientLeft[v] = -c;
1167 if (maxFind == maxCoefficientRight.end()) {
1168 maxCoefficientRight[v] = c;
1169 TRACE(
"arith stats",
"max right",
"",
"");
1172 if((*maxFind).second < c) {
1173 TRACE(
"arith stats",
"max right",
"",
"");
1174 maxCoefficientRight[v] = c;
1180 if(d_countRight.count(v) > 0) d_countRight[v] = d_countRight[v] + 1;
1181 else d_countRight[v] = 1;
1184 if(d_countLeft.count(v) > 0) d_countLeft[v] = d_countLeft[v] + 1;
1185 else d_countLeft[v] = 1;
1189 void TheoryArithOld::updateStats(
const Expr& monomial)
1192 separateMonomial(monomial, c, m);
1196 int TheoryArithOld::extractTermsFromInequality(
const Expr& inequality,
1200 TRACE(
"arith extract",
"extract(", inequality.
toString(),
")");
1204 Expr rhs = inequality[1];
1209 vector<Expr> positive_children, negative_children;
1214 c1 = -rhs[0].getRational();
1216 int end_i = rhs.arity();
1217 for(
int i = start_i; i < end_i; i ++) {
1218 const Expr& term = rhs[i];
1219 positive_children.push_back(term);
1220 negative_children.push_back(canon(
multExpr(rat(-1),term)).getRHS());
1223 positive_children.push_back(rhs);
1224 negative_children.push_back(canon(
multExpr(rat(-1), rhs)).getRHS());
1227 int num_vars = positive_children.size();
1230 t1 = (num_vars > 1 ? canon(
plusExpr(positive_children)).getRHS() : positive_children[0]);
1234 t2 = (num_vars > 1 ? canon(
plusExpr(negative_children)).getRHS() : negative_children[0]);
1241 bool TheoryArithOld::addToBuffer(
const Theorem& thm,
bool priority) {
1248 bool nonLinear =
false;
1250 Expr compactNonLinear;
1257 updateStats(monomial);
1262 (monomial.
arity() == 2 &&
isPow(monomial[1])))
1267 compactNonLinearThm = d_rules->compactNonLinearTerm(rhs);
1268 compactNonLinear = compactNonLinearThm.
getRHS();
1279 compactNonLinear = rhs;
1280 compactNonLinearThm = reflexivityRule(compactNonLinear);
1284 if (bufferedInequalities.find(ineq) != bufferedInequalities.end()) {
1285 TRACE(
"arith buffer",
"addToBuffer()",
"",
"... already in db");
1286 if (formulaAtoms.find(ineq) != formulaAtoms.end()) {
1287 TRACE(
"arith buffer",
"it's a formula atom, enqueuing.",
"",
"");
1293 if (nonLinear && (
isMult(rhs) || compactNonLinear != rhs)) {
1294 TRACE(
"arith nonlinear",
"compact version of ", rhs,
" is " + compactNonLinear.
toString());
1296 Theorem thm1 = (compactNonLinear != rhs ?
1297 iffMP(thm, substitutivityRule(ineq, 1, compactNonLinearThm)) : thm);
1302 thm1 = d_rules->nonLinearIneqSignSplit(thm1);
1303 TRACE(
"arith nonlinear",
"spliting on signs : ", thm1.getExpr(),
"");
1311 int num_vars = extractTermsFromInequality(ineq, c1, t1, c2, t2);
1314 bool factIsDiffLogic =
false;
1315 if (num_vars <= 2) {
1317 TRACE(
"arith diff", t2,
" < ", c2);
1320 Expr ax = (num_vars == 2 ? t2[1] : t2);
1322 separateMonomial(ax, a_expr, x);
1324 Expr by = (num_vars == 2 ? t2[2] : (a < 0 ? zero : rat(-1)*zero));
1326 separateMonomial(by, b_expr, y);
1330 if (!isLeaf(x) || !isLeaf(y))
1331 setIncomplete(
"Non-linear arithmetic inequalities");
1333 if (a == 1 && b == -1) {
1334 diffLogicGraph.addEdge(x, y, c2, thm);
1335 factIsDiffLogic =
true;
1337 else if (a == -1 && b == 1) {
1338 diffLogicGraph.addEdge(y, x, c2, thm);
1339 factIsDiffLogic =
true;
1343 diffLogicOnly =
false;
1347 if (diffLogicGraph.isUnsat()) {
1348 TRACE(
"diff unsat",
"UNSAT",
" : ", diffLogicGraph.getUnsatTheorem());
1349 setInconsistent(diffLogicGraph.getUnsatTheorem());
1353 diffLogicOnly =
false;
1359 if (find_lower != termLowerBound.end()) {
1361 Rational found_c = (*find_lower).second;
1363 if (c1 <= found_c && !(found_c == c1 && ineq.getKind() ==
LT)) {
1364 TRACE(
"arith buffer",
"addToBuffer()",
"",
"... lower_bound subsumed");
1370 Theorem oldLowerBound = termLowerBoundThm[t1];
1372 if (formulaAtoms.find(oldIneq) != formulaAtoms.end())
1373 enqueueFact(getCommonRules()->implMP(thm, d_rules->implyWeakerInequality(ineq, oldIneq)));
1374 termLowerBound[t1] = c1;
1375 termLowerBoundThm[t1] = thm;
1378 termLowerBound[t1] = c1;
1379 termLowerBoundThm[t1] = thm;
1383 if (find_upper != termUpperBound.end()) {
1385 Rational found_c = (*find_upper).second;
1387 if (found_c <= c2 && !(found_c == c2 && ineq.getKind() ==
LT)) {
1388 TRACE(
"arith buffer",
"addToBuffer()",
"",
"... upper_bound subsumed");
1392 termUpperBound[t2] = c2;
1393 termUpperBoundThm[t2] = thm;
1396 termUpperBound[t2] = c2;
1397 termUpperBoundThm[t2] = thm;
1401 if (termUpperBound.find(t1) != termUpperBound.end() &&
1402 termLowerBound.find(t1) != termLowerBound.end() &&
1403 termUpperBound[t1] <= termLowerBound[t1]) {
1404 Theorem thm1 = termUpperBoundThm[t1];
1405 Theorem thm2 = termLowerBoundThm[t1];
1407 enqueueFact(d_rules->addInequalities(thm1, thm2));
1409 if (termUpperBound.find(t2) != termUpperBound.end() &&
1410 termLowerBound.find(t2) != termLowerBound.end() &&
1411 termUpperBound[t2] <= termLowerBound[t2]) {
1412 Theorem thm1 = termUpperBoundThm[t2];
1413 Theorem thm2 = termLowerBoundThm[t2];
1415 enqueueFact(d_rules->addInequalities(thm1, thm2));
1421 AtomsMap::iterator find = formulaAtomLowerBound.find(t1);
1422 AtomsMap::iterator find_end = formulaAtomLowerBound.end();
1423 if (find != find_end) {
1424 set< pair<Rational, Expr> >::iterator bounds = (*find).second.begin();
1425 set< pair<Rational, Expr> >::iterator bounds_end = (*find).second.end();
1426 while (bounds != bounds_end) {
1427 TRACE(
"arith atoms",
"trying propagation", ineq, (*bounds).second);
1428 const Expr& implied = (*bounds).second;
1430 if ((*bounds).first < c1 || (!(ineq.getKind() ==
LE && implied.
getKind() ==
LT) && (*bounds).first == c1)) {
1434 Theorem impliedThm = getCommonRules()->implMP(thm, d_rules->implyWeakerInequality(ineq, implied));
1435 enqueueFact(impliedThm);
1445 find = formulaAtomUpperBound.find(t1);
1446 find_end = formulaAtomUpperBound.end();
1447 if (find != find_end) {
1448 set< pair<Rational, Expr> >::iterator bounds = (*find).second.begin();
1449 set< pair<Rational, Expr> >::iterator bounds_end = (*find).second.end();
1450 while (bounds != bounds_end) {
1451 TRACE(
"arith atoms",
"trying propagation", ineq, (*bounds).second);
1452 const Expr& implied = (*bounds).second;
1454 if ((*bounds).first < c1) {
1455 Theorem impliedThm = getCommonRules()->implMP(thm, d_rules->implyNegatedInequality(ineq, implied));
1456 enqueueFact(impliedThm);
1464 theoryCore()->getResource();
1467 if (theoryCore()->outOfResources())
return false;
1471 if (alreadyProjected.find(ineq) == alreadyProjected.end()) {
1473 if (dontBuffer.find(ineq) == dontBuffer.end()) {
1476 d_buffer_0.push_back(thm);
1479 if (num_vars == 1) d_buffer_1.push_back(thm);
1480 else if (num_vars == 2) d_buffer_2.push_back(thm);
1481 else d_buffer_3.push_back(thm);
1484 if (factIsDiffLogic) diff_logic_size = diff_logic_size + 1;
1489 bufferedInequalities[ineq] = thm;
1492 if (!ineq.hasFind())
1493 theoryCore()->setupTerm(ineq,
this, thm);
1500 bool& isolatedVarOnRHS)
1504 TRACE(
"arith",
"isolateVariable(",e,
") {");
1505 TRACE(
"arith ineq",
"isolateVariable(", e,
") {");
1508 "TheoryArithOld::isolateVariable: " + e.
toString() +
1512 "TheoryArithOld::isolateVariable: theorem must be of "
1513 "the form 0 < rhs: " + inputThm.
toString());
1515 const Expr& zero = e[0];
1519 result = iffMP(result, d_rules->constPredicate(e));
1520 TRACE(
"arith ineq",
"isolateVariable => ",result.
getExpr(),
" }");
1521 TRACE(
"arith",
"isolateVariable => ",result,
" }");
1528 Expr factor(computeNormalFactor(right,
false));
1529 TRACE(
"arith",
"isolateVariable: factor = ", factor,
"");
1531 "isolateVariable: factor="+factor.
toString());
1534 result = iffMP(result, d_rules->multIneqn(e, factor));
1536 result = canonPred(result);
1537 result = rafineInequalityToInteger(result);
1538 right = result.getExpr()[1];
1545 isolatedMonomial = pickMonomial(right);
1547 TRACE(
"arith ineq",
"isolatedMonomial => ",isolatedMonomial,
"");
1552 alreadyProjected[e] = isolatedMonomial;
1555 isolatedVarOnRHS =
true;
1556 if (
isMult(isolatedMonomial)) {
1557 r = ((isolatedMonomial[0].
getRational()) >= 0)? -1 : 1;
1559 ((isolatedMonomial[0].
getRational()) >= 0)?
true :
false;
1561 isolatedMonomial = canon(rat(-1)*isolatedMonomial).getRHS();
1562 TRACE(
"arith ineq",
"-(isolatedMonomial) => ",isolatedMonomial,
"");
1564 result = iffMP(result, d_rules->plusPredicate(zero, right,
1565 isolatedMonomial, kind));
1567 TRACE(
"arith ineq",
"resutl => ",result,
"");
1568 result = canonPred(result);
1570 result = iffMP(result, d_rules->multIneqn(result.
getExpr(), rat(r)));
1571 result = canonPred(result);
1573 TRACE(
"arith ineq",
"isolateVariable => ",result.
getExpr(),
" }");
1574 TRACE(
"arith",
"isolateVariable => ",result,
" }");
1579 TheoryArithOld::computeNormalFactor(
const Expr&
right,
bool normalizeConstants) {
1584 vector<Rational> nums, denoms;
1585 for(
int i=0, iend=right.
arity(); i<iend; ++i) {
1586 switch(right[i].getKind()) {
1588 if (normalizeConstants) {
1603 denoms.push_back(1);
1612 factor = (gcd_nums==0)? 0 : (lcm(denoms) / gcd_nums);
1613 }
else if(
isMult(right)) {
1615 factor = (r==0)? 0 : (1/
abs(r));
1623 bool TheoryArithOld::lessThanVar(
const Expr& isolatedMonomial,
const Expr& var2)
1626 "TheoryArithOld::findMaxVar: isolatedMonomial cannot be rational" +
1629 separateMonomial(isolatedMonomial, c, var0);
1630 separateMonomial(var2, c, var1);
1639 bool TheoryArithOld::isStale(
const Expr& e) {
1641 return e != find(e).getRHS();
1646 stale = isStale(*i);
1652 TRACE(
"arith stale",
"isStale(", ineq,
") {");
1655 bool strict(
isLT(ineqExpr));
1660 if (ineqExpr.
hasFind() && find(ineqExpr[1]).getRHS() != ineqExpr[1])
1674 TRACE(
"arith ineq",
"isStale[subsumed] => ", res?
"true" :
"false",
" }");
1677 res = isStale(ineqExpr);
1678 TRACE(
"arith ineq",
"isStale[updated] => ", res?
"true" :
"false",
" }");
1685 TRACE(
"separateMonomial",
"separateMonomial(", e,
")");
1687 "TheoryArithOld::separateMonomial(e = "+e.
toString()+
")");
1690 "TheoryArithOld::separateMonomial(e = "+e.
toString()+
")");
1692 if(e.
arity() == 2) var = e[1];
1694 vector<Expr> kids = e.
getKids();
1705 "TheoryArithOld::separateMonomial(e = "
1710 void TheoryArithOld::projectInequalities(
const Theorem& theInequality,
1711 bool isolatedVarOnRHS)
1714 TRACE(
"arith project",
"projectInequalities(", theInequality.
getExpr(),
1715 ", isolatedVarOnRHS="+string(isolatedVarOnRHS?
"true" :
"false")
1719 "TheoryArithOld::projectIsolatedVar: "\
1720 "theInequality is of the wrong form: " +
1725 Theorem theIneqThm(theInequality);
1726 Expr theIneq = theIneqThm.getExpr();
1730 Theorem isIntLHS(isIntegerThm(theIneq[0]));
1731 Theorem isIntRHS(isIntegerThm(theIneq[1]));
1733 Theorem thm = d_rules->lessThanToLE(theInequality, isIntLHS, isIntRHS, !isolatedVarOnRHS);
1734 theIneqThm = canonPred(iffMP(theIneqThm, thm));
1735 theIneq = theIneqThm.getExpr();
1739 Expr isolatedMonomial = isolatedVarOnRHS ? theIneq[1] : theIneq[0];
1741 Expr monomialVar, a;
1742 separateMonomial(isolatedMonomial, a, monomialVar);
1745 const FreeConst& bestConst = updateSubsumptionDB(theIneq, isolatedVarOnRHS, subsumed);
1748 IF_DEBUG(debugger.counter(
"subsumed inequalities")++;)
1749 TRACE(
"arith ineq",
"subsumed inequality: ", theIneq,
"");
1754 setIncomplete(
"Non-linear arithmetic inequalities");
1760 theoryCore()->setupTerm(theIneq[0],
this, theIneqThm);
1761 theoryCore()->setupTerm(theIneq[1],
this, theIneqThm);
1763 ExprMap<CDList<Ineq> *>& db1 = isolatedVarOnRHS ? d_inequalitiesRightDB : d_inequalitiesLeftDB;
1765 if(it1 == db1.
end()) {
1767 list->
push_back(
Ineq(theIneqThm, isolatedVarOnRHS, bestConst));
1768 db1[monomialVar] = list;
1771 ((*it1).second)->
push_back(
Ineq(theIneqThm, isolatedVarOnRHS, bestConst));
1773 ExprMap<CDList<Ineq> *>& db2 = isolatedVarOnRHS ? d_inequalitiesLeftDB : d_inequalitiesRightDB;
1775 if(it == db2.
end()) {
1776 TRACE_MSG(
"arith ineq",
"projectInequalities[not in DB] => }");
1781 Theorem betaLTt, tLTalpha, thm;
1782 for(
int i = listOfDBIneqs.
size() - 1; !inconsistent() && i >= 0; --i) {
1783 const Ineq& ineqEntry = listOfDBIneqs[i];
1788 if(!isStale(ineqEntry)) {
1789 betaLTt = isolatedVarOnRHS ? theIneqThm : ineqThm;
1790 tLTalpha = isolatedVarOnRHS ? ineqThm : theIneqThm;
1792 thm = normalizeProjectIneqs(betaLTt, tLTalpha);
1793 if (thm.
isNull())
continue;
1795 IF_DEBUG(debugger.counter(
"real shadows")++;)
1801 setInconsistent(thm);
1802 TRACE_MSG(
"arith ineq",
"projectInequalities[inconsistent] => }");
1808 addToBuffer(thm,
false);
1814 IF_DEBUG(debugger.counter(
"stale inequalities")++;)
1819 TRACE_MSG(
"arith ineq",
"projectInequalities => }");
1827 Theorem betaLTt = ineqThm1, tLTalpha = ineqThm2;
1829 Expr ineq2 = tLTalpha.getExpr();
1831 separateMonomial(ineq2[0], c, x);
1833 Theorem isIntBeta(isIntegerThm(ineq1[0]));
1834 Theorem isIntAlpha(isIntegerThm(ineq2[1]));
1837 TRACE(
"arith ineq",
"normalizeProjectIneqs(", ineq1,
1841 "TheoryArithOld::normalizeProjectIneqs: Wrong Kind inputs: " +
1844 "TheoryArithOld::normalizeProjectIneqs: Wrong Kind inputs: " +
1863 if(isInt && (a >= 2 || b >= 2)) {
1866 intResult = d_rules->darkGrayShadow2ab(betaLTt, tLTalpha,
1867 isIntAlpha, isIntBeta, isIntx);
1869 intResult = d_rules->darkGrayShadow2ba(betaLTt, tLTalpha,
1870 isIntAlpha, isIntBeta, isIntx);
1871 enqueueFact(intResult);
1875 const Expr& G = DorG[1];
1882 Expr tmp = simplifyExpr(!G);
1883 if (!tmp.isBoolConst())
1884 addSplitter(tmp, 1);
1885 IF_DEBUG(debugger.counter(
"dark+gray shadows")++;)
1893 Theorem thm2 = iffMP(betaLTt, d_rules->multIneqn(ineq1, rat(factor1)));
1894 betaLTt = canonPred(thm2);
1895 ineq1 = betaLTt.getExpr();
1898 Theorem thm2 = iffMP(tLTalpha, d_rules->multIneqn(ineq2, rat(factor2)));
1899 tLTalpha = canonPred(thm2);
1900 ineq2 = tLTalpha.getExpr();
1905 Expr beta(ineq1[0]);
1906 Expr alpha(ineq2[1]);
1908 if(
isLE(ineq1) &&
isLE(ineq2) && alpha == beta) {
1909 Theorem result = d_rules->realShadowEq(betaLTt, tLTalpha);
1910 TRACE(
"arith ineq",
"normalizeProjectIneqs => ", result,
" }");
1924 Theorem result = d_rules->realShadow(betaLTt, tLTalpha);
1933 if(!(e[0].
isRational() && e[0].getRational() == 0))
1934 result = iffMP(result, d_rules->rightMinusLeft(e));
1935 result = canonPred(result);
1941 result = iffMP(result, d_rules->constPredicate(result.
getExpr()));
1943 result = normalize(result);
1944 TRACE(
"arith ineq",
"normalizeProjectIneqs => ", result,
" }");
1951 if (var.
getType() == d_realType)
return -100;
1956 if (findMaxLeft != maxCoefficientLeft.end())
1957 leftMax = (*findMaxLeft).second;
1962 if (findMaxRight != maxCoefficientRight.end())
1963 rightMax = (*findMaxRight).second;
1970 if (leftMax == -1) returnValue = rightMax;
1971 else if (rightMax == -1) returnValue = leftMax;
1972 else if (leftMax < rightMax) returnValue = rightMax;
1973 else returnValue = leftMax;
1975 TRACE(
"arith stats",
"max coeff of ", var.
toString(),
": " + returnValue.toString() +
"(left=" + leftMax.
toString() +
",right=" + rightMax.
toString());
1981 fixedMaxCoefficient[var] =
max;
1984 void TheoryArithOld::selectSmallestByCoefficient(
const vector<Expr>& input, vector<Expr>& output) {
1990 Expr best_variable = input[0];
1991 Rational best_coefficient = currentMaxCoefficient(best_variable);
1992 output.push_back(best_variable);
1994 for(
unsigned int i = 1; i < input.size(); i ++) {
1997 Expr current_variable = input[i];
1999 Rational current_coefficient = currentMaxCoefficient(current_variable);
2002 if ((current_coefficient < best_coefficient)) {
2003 best_variable = current_variable;
2004 best_coefficient = current_coefficient;
2009 if (current_coefficient == best_coefficient)
2010 output.push_back(current_variable);
2021 if(theoryCore()->getFlags()[
"var-order"].getBool()) {
2023 Expr isolatedMonomial = right[1];
2027 for(++i; i != right.
end(); ++i)
2028 if(lessThanVar(isolatedMonomial,*i))
2029 isolatedMonomial = *i;
2030 return isolatedMonomial;
2036 for(;i != iend; ++i) {
2040 separateMonomial(*i, c, var);
2041 var2monomial[var] = *i;
2042 vars.push_back(var);
2045 vector<Expr> largest;
2046 d_graph.selectLargest(vars, largest);
2048 "TheoryArithOld::pickMonomial: selectLargest: failed!!!!");
2051 vector<Expr> largest_small_coeff;
2052 selectSmallestByCoefficient(largest, largest_small_coeff);
2053 DebugAssert(0 < largest_small_coeff.size(),
"TheoryArithOld::pickMonomial: selectLargestByCOefficient: failed!!!!");
2055 size_t pickedVar = 0;
2059 size_t size = largest_small_coeff.size();
2060 int minProjections = -1;
2062 for(
size_t k=0; k< size; ++k) {
2063 const Expr& var(largest_small_coeff[k]), monom(var2monomial[var]);
2065 int nRight = (d_countRight.count(var) > 0)? d_countRight[var] : 0;
2066 int nLeft = (d_countLeft.count(var) > 0)? d_countLeft[var] : 0;
2067 int n(nRight*nLeft);
2068 TRACE(
"arith ineq",
"pickMonomial: var=", var,
2070 if(minProjections < 0 || minProjections > n) {
2074 TRACE(
"arith ineq",
"Number of projections for "+var.toString()+
" = ", n,
"");
2078 const Expr& largestVar = largest_small_coeff[pickedVar];
2083 for(
size_t k = 0; k < vars.size(); ++k) {
2084 if(vars[k] != largestVar)
2085 d_graph.addEdge(largestVar, vars[k]);
2088 TRACE(
"arith buffer",
"picked var : ", var2monomial[largestVar].toString(),
"");
2090 return var2monomial[largestVar];
2093 void TheoryArithOld::VarOrderGraph::addEdge(
const Expr& e1,
const Expr& e2)
2095 TRACE(
"arith var order",
"addEdge("+e1.
toString()+
" > ", e2,
")");
2096 DebugAssert(e1 != e2,
"TheoryArithOld::VarOrderGraph::addEdge("
2098 d_edges[e1].push_back(e2);
2103 bool TheoryArithOld::VarOrderGraph::lessThan(
const Expr& e1,
const Expr& e2)
2111 bool TheoryArithOld::VarOrderGraph::dfs(
const Expr& e1,
const Expr& e2)
2115 if(d_cache.count(e2) > 0)
2117 if(d_edges.count(e2) == 0)
2120 vector<Expr>& e2Edges = d_edges[e2];
2121 vector<Expr>::iterator i = e2Edges.begin();
2122 vector<Expr>::iterator iend = e2Edges.end();
2124 for(; i != iend && !dfs(e1,*i); ++i);
2128 void TheoryArithOld::VarOrderGraph::dfs(
const Expr& v, vector<Expr>& output_list)
2133 if (d_cache.count(v) > 0)
return;
2136 if(d_edges.count(v) != 0) {
2138 vector<Expr>& vEdges = d_edges[v];
2139 vector<Expr>::iterator e = vEdges.begin();
2140 vector<Expr>::iterator e_end = vEdges.end();
2141 while (e != e_end) {
2142 dfs(*e, output_list);
2149 output_list.push_back(v);
2152 void TheoryArithOld::VarOrderGraph::getVerticesTopological(vector<Expr>& output_list)
2156 output_list.clear();
2161 while (v_it != v_it_end)
2164 dfs(v_it->first, output_list);
2170 void TheoryArithOld::VarOrderGraph::selectSmallest(vector<Expr>& v1,
2173 int v1Size = v1.size();
2174 vector<bool> v3(v1Size);
2175 for(
int j=0; j < v1Size; ++j)
2178 for(
int j=0; j < v1Size; ++j) {
2180 for(
int i =0; i < v1Size; ++i) {
2181 if((i == j) || v3[i])
2183 if(lessThan(v1[i],v1[j])) {
2189 vector<Expr> new_v1;
2191 for(
int j = 0; j < v1Size; ++j)
2192 if(!v3[j]) v2.push_back(v1[j]);
2193 else new_v1.push_back(v1[j]);
2198 void TheoryArithOld::VarOrderGraph::selectLargest(
const vector<Expr>& v1,
2201 int v1Size = v1.size();
2202 vector<bool> v3(v1Size);
2203 for(
int j=0; j < v1Size; ++j)
2206 for(
int j=0; j < v1Size; ++j) {
2208 for(
int i =0; i < v1Size; ++i) {
2209 if((i == j) || v3[i])
2211 if(lessThan(v1[j],v1[i])) {
2218 for(
int j = 0; j < v1Size; ++j)
2219 if(!v3[j]) v2.push_back(v1[j]);
2229 d_diseq(core->getCM()->getCurrentContext()),
2230 d_diseqIdx(core->getCM()->getCurrentContext(), 0, 0),
2231 diseqSplitAlready(core->getCM()->getCurrentContext()),
2232 d_inModelCreation(core->getCM()->getCurrentContext(), false, 0),
2233 d_freeConstDB(core->getCM()->getCurrentContext()),
2234 d_buffer_0(core->getCM()->getCurrentContext()),
2235 d_buffer_1(core->getCM()->getCurrentContext()),
2236 d_buffer_2(core->getCM()->getCurrentContext()),
2237 d_buffer_3(core->getCM()->getCurrentContext()),
2239 d_bufferIdx_0(core->getCM()->getCurrentContext(), 0, 0),
2240 d_bufferIdx_1(core->getCM()->getCurrentContext(), 0, 0),
2241 d_bufferIdx_2(core->getCM()->getCurrentContext(), 0, 0),
2242 d_bufferIdx_3(core->getCM()->getCurrentContext(), 0, 0),
2243 diff_logic_size(core->getCM()->getCurrentContext(), 0, 0),
2244 d_bufferThres(&(core->getFlags()[
"ineq-delay"].getInt())),
2245 d_splitSign(&(core->getFlags()[
"nonlinear-sign-split"].getBool())),
2246 d_grayShadowThres(&(core->getFlags()[
"grayshadow-threshold"].getInt())),
2247 d_countRight(core->getCM()->getCurrentContext()),
2248 d_countLeft(core->getCM()->getCurrentContext()),
2249 d_sharedTerms(core->getCM()->getCurrentContext()),
2250 d_sharedTermsList(core->getCM()->getCurrentContext()),
2251 d_sharedVars(core->getCM()->getCurrentContext()),
2252 bufferedInequalities(core->getCM()->getCurrentContext()),
2253 termLowerBound(core->getCM()->getCurrentContext()),
2254 termLowerBoundThm(core->getCM()->getCurrentContext()),
2255 termUpperBound(core->getCM()->getCurrentContext()),
2256 termUpperBoundThm(core->getCM()->getCurrentContext()),
2257 alreadyProjected(core->getCM()->getCurrentContext()),
2258 dontBuffer(core->getCM()->getCurrentContext()),
2259 diffLogicOnly(core->getCM()->getCurrentContext(), true, 0),
2260 diffLogicGraph(0, core, 0, core->getCM()->getCurrentContext()),
2261 shared_index_1(core->getCM()->getCurrentContext(), 0, 0),
2262 shared_index_2(core->getCM()->getCurrentContext(), 0, 0),
2263 termUpperBounded(core->getCM()->getCurrentContext()),
2264 termLowerBounded(core->getCM()->getCurrentContext()),
2265 d_varConstrainedPlus(core->getCM()->getCurrentContext()),
2266 d_varConstrainedMinus(core->getCM()->getCurrentContext()),
2267 termConstrainedBelow(core->getCM()->getCurrentContext()),
2268 termConstrainedAbove(core->getCM()->getCurrentContext())
2362 if(cache.count(e) > 0)
return;
2365 if(
isLeaf(e)) vars.push_back(e);
2377 DebugAssert(
isLE(ineq1),
"TheoryArithOld::processFiniteInterval: ineq1 = "
2379 DebugAssert(
isLE(ineq2),
"TheoryArithOld::processFiniteInterval: ineq2 = "
2382 if(!isInteger(ineq1[0])
2383 || !isInteger(ineq1[1])
2384 || !isInteger(ineq2[0])
2385 || !isInteger(ineq2[1]))
2388 const Expr& ax = ineq1[1];
2389 const Expr& bx = ineq2[0];
2391 "TheoryArithOld::processFiniteInterval:\n ax = "+ax.
toString());
2393 "TheoryArithOld::processFiniteInterval:\n bx = "+bx.
toString());
2397 Theorem thm1(alphaLEax), thm2(bxLEbeta);
2400 thm1 = canonPred(iffMP(alphaLEax, d_rules->multIneqn(ineq1, b)));
2401 thm2 = canonPred(iffMP(bxLEbeta, d_rules->multIneqn(ineq2, a)));
2404 const Expr& alphaLEt = thm1.getExpr();
2405 const Expr& alpha = alphaLEt[0];
2406 const Expr& t = alphaLEt[1];
2408 Expr c = canon(beta - alpha).getRHS();
2414 Theorem bEQac = symmetryRule(canon(alpha + c));
2416 vector<unsigned> changed;
2417 vector<Theorem> thms;
2418 changed.push_back(1);
2419 thms.push_back(bEQac);
2420 Theorem tLEac = substitutivityRule(thm2.
getExpr(), changed, thms);
2421 tLEac = iffMP(thm2, tLEac);
2423 Theorem isInta(isIntegerThm(alpha));
2424 Theorem isIntt(isIntegerThm(t));
2425 if (d_sharedTerms.find(thm1.getExpr()[1]) != d_sharedTerms.end())
2426 enqueueFact(d_rules->finiteInterval(thm1, tLEac, isInta, isIntt));
2445 size_t sizeLeft = ineqsLeft.
size();
2446 size_t sizeRight = ineqsRight.
size();
2448 for(
size_t l=0; l<sizeLeft; ++l)
2449 for(
size_t r=0; r<sizeRight; ++r)
2461 for (
int k = 0; k < e.
arity(); ++k) {
2492 IF_DEBUG(debugger.counter(
"[arith] received disequalities")++;)
2495 else if (!expr.
isEq()){
2508 IF_DEBUG(debugger.counter(
"received DARK_SHADOW")++;)
2511 IF_DEBUG(debugger.counter(
"received GRAY_SHADOW")++;)
2512 const Rational& c1 = expr[2].getRational();
2517 setIncomplete(
"Some gray shadows ignored due to threshold");
2521 const Expr& v = expr[0];
2522 const Expr& ee = expr[1];
2530 IF_DEBUG(debugger.counter(
"reduced const GRAY_SHADOW")++;)
2539 else if(g[3].getRational() - g[2].
getRational() <= 5) {
2557 "expected LE or LT: "+expr.
toString());
2559 IF_DEBUG(debugger.counter(
"recevied inequalities")++;)
2566 TRACE(
"arith ineq",
"buffer.size() = ", total_buf_size,
2574 IF_DEBUG(debugger.counter(
"arith IS_INTEGER")++;)
2582 IF_DEBUG(debugger.counter(
"[arith] received t1=t2")++;)
2611 TRACE(
"arith checksat",
"checksat(fullEffort = ", fullEffort?
"true, modelCreation = " :
"false, modelCreation = ", (
d_inModelCreation ?
"true)" :
"false)"));
2612 TRACE(
"arith ineq",
"TheoryArithOld::checkSat(fullEffort=",
2613 fullEffort?
"true" :
"false",
")");
2633 TRACE(
"arith::unconstrained",
"checking disequaliy: ", diseq[0] ,
" already split");
2643 TRACE(
"arith::unconstrained",
"checking disequaliy: ", lhs.
eqExpr(rhs) ,
"");
2647 TRACE(
"arith::unconstrained",
"checking disequaliy: ", lhs.eqExpr(rhs) ,
" after find");
2652 TRACE(
"arith::unconstrained",
"checking disequaliy: ", lhs.eqExpr(rhs) ,
" skipping");
2660 if (unconstrained) {
2661 TRACE(
"arith::unconstrained",
"checking disequaliy: ", lhs.eqExpr(rhs) ,
" unconstrained skipping");
2665 if (!intConstraint) {
2666 TRACE(
"arith::unconstrained",
"checking disequaliy: ", lhs.eqExpr(rhs) ,
" not integer skipping");
2671 TRACE(
"arith::unconstrained",
"checking disequaliy: ", lhs.eqExpr(rhs) ,
" splitting");
2686 bool dejans_printouts =
false;
2687 if (dejans_printouts) {
2688 cerr <<
"Disequalities after CheckSat" <<
endl;
2689 for (
unsigned i = 0; i <
d_diseq.size(); i ++) {
2694 cerr <<
"Arith Buffer after CheckSat (0)" <<
endl;
2695 for (
unsigned i = 0; i <
d_buffer_0.size(); i ++) {
2700 cerr <<
"Arith Buffer after CheckSat (1)" <<
endl;
2701 for (
unsigned i = 0; i <
d_buffer_1.size(); i ++) {
2706 cerr <<
"Arith Buffer after CheckSat (2)" <<
endl;
2707 for (
unsigned i = 0; i <
d_buffer_2.size(); i ++) {
2712 cerr <<
"Arith Buffer after CheckSat (3)" <<
endl;
2713 for (
unsigned i = 0; i <
d_buffer_3.size(); i ++) {
2729 TRACE(
"model",
"refineCounterExample[TheoryArithOld] ",
"",
"{");
2735 for(; it!=iend; ++it) {
2737 Expr e1 = (*it).first;
2738 for(it2 = it, ++it2; it2!=iend; ++it2) {
2739 Expr e2 = (*it2).first;
2741 "TheoryArithOld::refineCounterExample: e1 = "+e1.
toString()
2745 "TheoryArithOld::refineCounterExample: e2 = "+e2.
toString()
2748 if (!eq.isBoolConst()) {
2754 TRACE(
"model",
"refineCounterExample[Theory::Arith] ",
"",
"}");
2767 throw ArithException(
"Could not generate the model due to non-linear arithmetic");
2770 "seperateMonomial failed");
2772 "smallest variable in graph, should not have variables"
2773 " in inequalities: ");
2774 DebugAssert(x == var,
"separateMonomial found different variable: "
2782 bool strictLB=
false, strictUB=
false;
2787 int numRight = 0, numLeft = 0;
2790 for(
unsigned int i=0; i<ratsLTe->
size(); i++) {
2791 DebugAssert((*ratsLTe)[i].varOnRHS(),
"variable on wrong side!");
2792 Expr ineq = (*ratsLTe)[i].ineq().getExpr();
2793 Expr leftSide = ineq[0], rightSide = ineq[1];
2796 if(numRight==0 || r>glb){
2798 strictLB =
isLT(ineq);
2806 for(
unsigned int i=0; i<ratsGTe->
size(); i++) {
2807 DebugAssert((*ratsGTe)[i].varOnLHS(),
"variable on wrong side!");
2808 Expr ineq = (*ratsGTe)[i].ineq().getExpr();
2809 Expr leftSide = ineq[0], rightSide = ineq[1];
2812 if(numLeft==0 || r<lub) {
2814 strictUB =
isLT(ineq);
2820 if(!left && !right) {
2824 if(!left && right) {lub = glb +2;}
2825 if(!right && left) {glb = lub-2;}
2826 DebugAssert(glb <= lub,
"Greatest lower bound needs to be smaller "
2827 "than least upper bound");
2840 for (
unsigned i = 0; i < v.size(); i ++) {
2848 while (v.size() > 0)
2850 std::vector<Expr> bottom;
2852 TRACE(
"model",
"Finding variables to assign. Iteration # ", count,
"");
2853 for(
unsigned int i = 0; i<bottom.size(); i++)
2856 TRACE(
"model",
"Found: ", e,
"");
2871 mid = (lub + glb)/2;
2873 TRACE(
"model",
"Assigning mid = ", mid,
" {");
2886 TRACE(
"model",
"Arith=>computeModel ",
"",
"{");
2887 for(
unsigned int i=0; i <v.size(); ++i) {
2888 const Expr& e = v[i];
2890 TRACE(
"model",
"arith variable:", e ,
"");
2894 TRACE(
"model",
"arith variable:", e ,
"");
2899 TRACE(
"model",
"Arith=>computeModel",
"",
"}");
2907 +e.
toString()+
")\n e is not assigned concrete value.\n"
2921 TRACE(
"arith rafine",
"TheoryArithOld::checkIntegerEquality(", eq,
")");
2926 Expr old_sum = (
isPlus(eq[1]) ? eq[1] : eq[0]);
2929 vector<Expr> children;
2930 bool const_is_integer =
true;
2931 for (
int i = 0; i < old_sum.
arity(); i ++)
2933 children.push_back(old_sum[i]);
2938 if (const_is_integer)
return thm;
2940 Expr sum = (children.size() > 1 ?
plusExpr(children) : children[0]);
2944 if (!isIntegerEquality.
isNull()) {
2947 else return iffMP(thm, false_thm);
2961 TRACE(
"arith rafine",
"TheoryArithOld::rafineInequalityToInteger(", ineq,
")");
2968 vector<Expr> children;
2970 for (
int i = 0; i < ineq[1].
arity(); i ++)
2972 children.push_back(ineq[1][i]);
2973 }
else children.push_back(ineq[1]);
2975 Expr sum = (children.size() > 1 ?
plusExpr(children) : children[0]);
2979 if (!isIntegerInequality.
isNull()) {
2981 TRACE(
"arith rafine",
"TheoryArithOld::rafineInequalityToInteger()",
"=>", rafine.
getRHS());
2997 TRACE(
"arith normalize",
"normalize(", e,
") {");
2999 "normalize: input must be Eq or Ineq: " + e.
toString());
3001 "normalize: if (e is ineq) then e[0] must be 0" +
3006 "normalize: if e is Eq and e[0] is rat then e[0]==0");
3011 "normalize: if e is Eq and e[1] is rat then e[1]==0\n"
3022 TRACE(
"arith normalize",
"normalize: factor = ", factor,
"");
3024 "normalize: factor="+ factor.
toString());
3057 ss <<
"normalize: control should not reach here " << kind;
3065 TRACE(
"arith normalize",
"normalize => ", thm,
" }");
3079 TRACE(
"arith",
"TheoryArithOld::rewrite(", e,
") {");
3092 eNew = thm.getRHS();
3113 TRACE(
"arith",
"TheoryArithOld::rewrite[non-literal] => ", thm,
" }");
3125 if((e[0].
isRational() && e[0].getRational() == 0)
3148 if(eq.
isEq() && eq[0] < eq[1])
3155 TRACE(
"arith nonlinear",
"nonlinear eq rewrite: ", nonlinearEq,
"");
3172 if (left[0].getRational() == 0) {
3176 set<Expr>::iterator is, isend;
3178 for (++i; i != iend; ++i) {
3181 for (is = factors.begin(), isend = factors.end(); is != isend;) {
3182 if (factors2.find(*is) == factors2.end()) {
3183 factors.erase(is ++);
3187 if (factors.empty())
break;
3189 if (!factors.empty()) {
3193 TRACE(
"arith nonlinear",
"nonlinear eq rewrite (factoring): ", thm.getRHS(),
"");
3206 TRACE(
"arith nonlinear",
"nonlinear eq rewrite (equal powers): ", thm.getRHS(),
"");
3212 if (pow1 % 2 == 0 && constant < 0) {
3214 TRACE(
"arith nonlinear",
"nonlinear eq rewrite (even power = negative): ", thm.
getRHS(),
"");
3217 DebugAssert(constant != 0,
"Expected nonzero const");
3222 TRACE(
"arith nonlinear",
"nonlinear eq rewrite (rational root): ", thm.getRHS(),
"");
3226 if (!isIntPower.
isNull()) {
3228 TRACE(
"arith nonlinear",
"nonlinear eq rewrite (irational root): ", thm.
getRHS(),
"");
3240 TRACE(
"arith nonlinear",
"nonlinear eq rewrite (not solvable): ", thm.getRHS(),
"");
3267 "Expected GE or GT");
3278 bool isInt = (!isIntLHS.
isNull() && !isIntRHS.
isNull());
3316 bool isInt = (!isIntLHS.
isNull() && !isIntRHS.
isNull());
3336 "Theory_Arith::rewrite: control should not reach here");
3350 TRACE(
"arith",
"TheoryArithOld::rewrite => ", thm,
" }");
3358 if (e.
isNot())
return;
3365 e[0].
isRational() && e[0].getRational() == 0,
3366 "TheoryArithOld::setup: expected 0 < rhs:" + e.
toString());
3382 int k(0), ar(e.
arity());
3383 for ( ; k < ar; ++k) {
3385 TRACE(
"arith setup",
"e["+
int2string(k)+
"]: ", *(e[k].getNotify()),
"");
3399 IF_DEBUG(debugger.counter(
"arith update total")++;)
3462 vector<unsigned> changed;
3463 vector<Theorem> children;
3464 changed.push_back(1);
3465 children.push_back(e);
3473 if ((thm.isNull() || thm.getRHS() !=
falseExpr()) &&
3476 TRACE(
"arith update",
"simplified but not projected : ", thm2.
getRHS(),
"");
3484 TRACE(
"arith update",
"in udpate, but no find",
"",
"");
3493 else if (thm.getRHS() ==
trueExpr()) {
3501 IF_DEBUG(debugger.counter(
"arith update ineq")++;)
3503 else if (d.
isEq()) {
3504 TRACE(
"arith nonlinear",
"TheoryArithOld::update() on equality ", d,
"");
3507 vector<unsigned> changed;
3508 vector<Theorem> children;
3509 changed.push_back(0);
3510 children.push_back(e);
3531 else if (
find(d).getRHS() == d) {
3590 TRACE(
"model",
"TheoryArithOld::computeModelTerm(", e,
"): a variable");
3594 TRACE(
"model",
"TheoryArithOld::computeModelTerm("+e.
toString()
3595 +
"): has find pointer to ", e2,
"");
3609 std::vector<Expr> kids;
3611 kids.push_back(
leExpr(tExpr[0], e));
3612 kids.push_back(
leExpr(e, tExpr[1]));
3628 "Not in solved form: lhs appears in rhs");
3633 "Expected at least one unsimplified leaf on lhs");
3636 "Expected canonSimp(rhs) = canonSimp(rhs)");
3642 vector<Theorem> eqs;
3646 for (index = 0; index < expr.
arity(); ++index) {
3651 eqs[index].getLHS().isTerm(),
"Expected equation");
3655 for (index = 0; index < expr.
arity(); ++index) {
3658 "Expected canonSimp(rhs) = canonSimp(rhs)");
3660 "Failed recursive canonSimp check");
3661 for (index2 = 0; index2 < expr.
arity(); ++index2) {
3663 eqs[index].getLHS() != eqs[index2].getLHS(),
3664 "Not in solved form: repeated lhs");
3666 "Not in solved form: lhs appears in rhs");
3678 if (e.
arity() > 0) {
3683 if (e.
arity() != 2 ||
3691 DebugAssert(
false,
"Unexpected kind in TheoryArithOld::checkType"
3698 bool enumerate,
bool computeSize)
3707 if (r <= typeExpr[1].getRational()) {
3743 for(
int k = 0; k < e.
arity(); ++k) {
3759 Expr numerator = e[0];
3760 Expr denominator = e[1];
3783 for (
int k = 0; k < e.
arity(); ++k) {
3801 DebugAssert(
false,
"TheoryArithOld::computeType: unexpected expression:\n "
3811 "TheoryArithOld::computeBaseType("+t.
toString()+
")");
3858 "TheoryArithOld::parseExprOp:\n e = "+e.
toString());
3860 const Expr& c1 = e[0][0];
3876 for(; i!=iend; ++i) k.push_back(
parseExpr(*i));
3880 if(e.
arity() == 2) {
3883 throw ParserException(
"Unary Minus should use '~' instead of '-' in SMT-LIB expr:"
3890 else if(e.
arity() == 3)
3903 for(; i!=iend; ++i) k.push_back(
parseExpr(*i));
3940 "TheoryArithOld::parseExprOp: invalid input " + e.
toString());
3960 os <<
"ERROR:SUBRANGE:not supported in Simplify\n";
3963 os <<
"ERROR:IS_INTEGER:not supported in Simplify\n";
3966 int i=0, iend=e.
arity();
3968 if(i!=iend) os << e[i];
3970 for(; i!=iend; ++i) os <<
" " << e[i];
3975 os <<
"(- " << e[0] <<
" " << e[1]<<
")";
3981 int i=0, iend=e.arity();
3983 if(i!=iend) os << e[i];
3985 for(; i!=iend; ++i) os <<
" " << e[i];
3990 os <<
"(" <<
push << e[1] <<
space <<
"^ " << e[0] <<
push <<
")";
3993 os <<
"(" << push << e[0] <<
space <<
"/ " << e[1] << push <<
")";
3996 if (
isInt(e[0].getType()) ||
isInt(e[1].getType())) {
3998 os <<
"(< " << e[0] <<
" " << e[1] <<
")";
4001 os <<
"(<= " << e[0] <<
" " << e[1] <<
")";
4004 os <<
"(> " << e[0] <<
" " << e[1] <<
")";
4007 os <<
"(>= " << e[0] <<
" " << e[1] <<
")";
4011 os <<
"ERROR:SHADOW:not supported in Simplify\n";
4028 os <<
"ERROR:SUBRANGE:not supported in TPTP\n";
4031 os <<
"ERROR:IS_INTEGER:not supported in TPTP\n";
4035 os<<
"ERRPR:plus only supports inteters now in TPTP\n";
4039 int i=0, iend=e.
arity();
4041 os<<
"ERROR,plus must have more than two numbers in TPTP\n";
4045 for(i=0; i <= iend-2; ++i){
4052 for(i=0 ; i <= iend-2; ++i){
4060 os<<
"ERRPR:arithmetic operations only support inteters now in TPTP\n";
4064 os <<
"$minus_int(" << e[0] <<
"," << e[1]<<
")";
4068 os<<
"ERRPR:arithmetic operations only support inteters now in TPTP\n";
4072 os <<
"$uminus_int(" << e[0] <<
")" ;
4076 os<<
"ERRPR:times only supports inteters now in TPTP\n";
4080 int i=0, iend=e.arity();
4082 os<<
"ERROR:times must have more than two numbers in TPTP\n";
4086 for(i=0; i <= iend-2; ++i){
4087 os <<
"$times_int(";
4093 for(i=0 ; i <= iend-2; ++i){
4102 os<<
"ERRPR:arithmetic operations only support inteters now in TPTP\n";
4106 os <<
"$power_int(" <<
push << e[1] <<
space <<
"^ " << e[0] <<
push <<
")";
4111 os<<
"ERRPR:arithmetic operations only support inteters now in TPTP\n";
4115 os <<
"divide_int(" <<e[0] <<
"," << e[1] <<
")";
4120 os<<
"ERRPR:arithmetic operations only support inteters now in TPTP\n";
4123 os <<
"$less_int(" << e[0] <<
"," << e[1] <<
")";
4128 os<<
"ERRPR:arithmetic operations only support inteters now in TPTP\n";
4132 os <<
"$lesseq_int(" << e[0] <<
"," << e[1] <<
")";
4137 os<<
"ERRPR:arithmetic operations only support inteters now in TPTP\n";
4141 os <<
"$greater_int(" << e[0] <<
"," << e[1] <<
")";
4146 os<<
"ERRPR:arithmetic operations only support inteters now in TPTP\n";
4150 os <<
"$greatereq_int(" << e[0] <<
"," << e[1] <<
")";
4154 os <<
"ERROR:SHADOW:not supported in TPTP\n";
4161 os <<
"ERROR:REAL not supported in TPTP\n";
4191 os <<
"[" <<
push << e[0] <<
".." << e[1] <<
push <<
"]";
4195 os <<
"IS_INTEGER(" << push << e[0] << push <<
")";
4200 int i=0, iend=e.
arity();
4202 if(i!=iend) os << e[i];
4204 for(; i!=iend; ++i) os <<
space <<
"+ " << e[i];
4209 os <<
"(" << push << e[0] <<
space <<
"- " << e[1] << push <<
")";
4212 os <<
"-(" << push << e[0] << push <<
")";
4215 int i=0, iend=e.
arity();
4217 if(i!=iend) os << e[i];
4219 for(; i!=iend; ++i) os <<
space <<
"* " << e[i];
4224 os <<
"(" << push << e[1] <<
space <<
"^ " << e[0] << push <<
")";
4227 os <<
"(" << push << e[0] <<
space <<
"/ " << e[1] << push <<
")";
4230 if (
isInt(e[0].getType()) ||
isInt(e[1].getType())) {
4232 os <<
"(" << push << e[0] <<
space <<
"< " << e[1] << push <<
")";
4235 os <<
"(" << push << e[0] <<
space <<
"<= " << e[1] << push <<
")";
4238 os <<
"(" << push << e[0] <<
space <<
"> " << e[1] << push <<
")";
4241 os <<
"(" << push << e[0] <<
space <<
">= " << e[1] << push <<
")";
4244 os <<
"DARK_SHADOW(" << push << e[0] <<
", " <<
space << e[1] << push <<
")";
4247 os <<
"GRAY_SHADOW(" << push << e[0] <<
"," <<
space << e[1]
4248 <<
"," <<
space << e[2] <<
"," <<
space << e[3] << push <<
")";
4267 throw SmtlibException(
"TheoryArithOld::print: SPASS: REAL not implemented");
4270 throw SmtlibException(
"TheoryArithOld::print: SPASS: INT not implemented");
4273 throw SmtlibException(
"TheoryArithOld::print: SPASS: SUBRANGE not implemented");
4276 throw SmtlibException(
"TheoryArithOld::print: SPASS: IS_INTEGER not implemented");
4278 int arity = e.
arity();
4280 os <<
push <<
"plus("
4281 << e[0] <<
"," <<
space << e[1]
4284 else if(2 < arity) {
4285 for (
int i = 0 ; i < arity - 2; i++){
4286 os <<
push <<
"plus(";
4287 os << e[i] <<
"," <<
space;
4289 os <<
push <<
"plus("
4290 << e[arity - 2] <<
"," <<
space << e[arity - 1]
4292 for (
int i = 0 ; i < arity - 2; i++){
4297 throw SmtlibException(
"TheoryArithOld::print: SPASS: Less than two arguments for plus");
4302 os <<
push <<
"plus(" << e[0]
4308 os <<
push <<
"plus(0,"
4314 int arity = e.
arity();
4316 os <<
push <<
"mult("
4317 << e[0] <<
"," <<
space << e[1]
4320 else if (2 < arity){
4321 for (
int i = 0 ; i < arity - 2; i++){
4322 os <<
push <<
"mult(";
4323 os << e[i] <<
"," <<
space;
4325 os <<
push <<
"mult("
4326 << e[arity - 2] <<
"," <<
space << e[arity - 1]
4328 for (
int i = 0 ; i < arity - 2; i++){
4333 throw SmtlibException(
"TheoryArithOld::print: SPASS: Less than two arguments for mult");
4340 for(; i!=iend; ++i) {
4342 os <<
push <<
"mult(";
4344 os << e[1] <<
"," <<
space;
4346 os <<
push <<
"mult("
4347 << e[1] <<
"," <<
space << e[1];
4348 for (i=0; i < iend-1; ++i) {
4357 os <<
"ERROR "<<
endl;
break;
4358 throw SmtlibException(
"TheoryArithOld::print: SPASS: unexpected use of DIVIDE");
4364 os << e[0] <<
"," << space << e[1] <<
push <<
")";
4370 os << e[0] <<
"," << space << e[1] <<
push <<
")";
4376 os << e[0] <<
"," << space << e[1] <<
push <<
")";
4382 os << e[0] <<
"," << space << e[1] <<
push <<
")";
4387 throw SmtlibException(
"TheoryArithOld::print: SPASS: default not supported");
4407 throw SmtlibException(
"TheoryArithOld::print: SMTLIB: SUBRANGE not implemented");
4414 if(e.
arity() == 1) {
4416 os <<
"(" <<
push <<
"IsInt" <<
space << e[0] <<
push <<
")";
4419 os <<
"(" <<
push <<
"is_int" <<
space << e[0] <<
push <<
")";
4423 throw SmtlibException(
"TheoryArithOld::print: SMTLIB: IS_INTEGER used unexpectedly");
4429 os <<
"(" <<
push <<
"+";
4431 for(; i!=iend; ++i) {
4432 os <<
space << (*i);
4439 os <<
"(" <<
push <<
"- " << e[0] <<
space << e[1] <<
push <<
")";
4452 int i=0, iend=e.
arity();
4456 for(; i!=iend; ++i) {
4458 os <<
"(" <<
push <<
"*";
4460 os <<
space << e[i];
4462 for (i=0; i < iend-1; ++i) os <<
push <<
")";
4469 for(; i!=iend; ++i) {
4471 os <<
"(" <<
push <<
"*";
4473 os <<
space << e[1];
4475 for (i=0; i < iend-1; ++i) os <<
push <<
")";
4482 throw SmtlibException(
"TheoryArithOld::print: SMTLIB: unexpected use of DIVIDE");
4488 os << e[0] << space << e[1] <<
push <<
")";
4494 os << e[0] << space << e[1] <<
push <<
")";
4500 os << e[0] << space << e[1] <<
push <<
")";
4506 os << e[0] << space << e[1] <<
push <<
")";
4510 throw SmtlibException(
"TheoryArithOld::print: SMTLIB: DARK_SHADOW not supported");
4511 os <<
"(" <<
push <<
"DARK_SHADOW" <<
space << e[0]
4515 throw SmtlibException(
"TheoryArithOld::print: SMTLIB: GRAY_SHADOW not supported");
4516 os <<
"GRAY_SHADOW(" << push << e[0] <<
"," <<
space << e[1]
4517 <<
"," <<
space << e[2] <<
"," <<
space << e[3] << push <<
")";
4520 throw SmtlibException(
"TheoryArithOld::print: SMTLIB: default not supported");
4541 os <<
"(" <<
push <<
"SUBRANGE" <<
space << e[0]
4546 os <<
"(" << push <<
"IS_INTEGER" <<
space << e[0] << push <<
")";
4551 int i=0, iend=e.
arity();
4552 os <<
"(" << push <<
"+";
4553 for(; i!=iend; ++i) os <<
space << e[i];
4559 os <<
"(" << push <<
"- " << e[0] <<
space << e[1] << push <<
")";
4562 os <<
"(" << push <<
"-" <<
space << e[0] << push <<
")";
4565 int i=0, iend=e.
arity();
4566 os <<
"(" << push <<
"*";
4567 for(; i!=iend; ++i) os <<
space << e[i];
4572 os <<
"(" << push <<
"^ " << e[1] <<
space << e[0] << push <<
")";
4575 os <<
"(" << push <<
"/ " << e[0] <<
space << e[1] << push <<
")";
4578 os <<
"(" << push <<
"< " << e[0] <<
space << e[1] << push <<
")";
4581 os <<
"(" << push <<
"<= " << e[0] <<
space << e[1] << push <<
")";
4584 os <<
"(" << push <<
"> " << e[1] <<
space << e[0] << push <<
")";
4587 os <<
"(" << push <<
">= " << e[0] <<
space << e[1] << push <<
")";
4590 os <<
"(" << push <<
"DARK_SHADOW" <<
space << e[0]
4591 <<
space << e[1] << push <<
")";
4594 os <<
"(" << push <<
"GRAY_SHADOW" <<
space << e[0] <<
space
4595 << e[1] <<
space << e[2] <<
space << e[3] << push <<
")";
4616 int index = (normalizeRHS ? 1 : 0);
4627 if (inequality[index].hasFind()) {
4629 Theorem rhsFindThm = inequality[index].getFind();
4635 if (rhsFind != inequality[index]) {
4637 vector<unsigned> changed;
4638 vector<Theorem> children;
4639 changed.push_back(index);
4640 children.push_back(rhsFindThm);
4644 inequalityFindThm = rhsFindThm;
4647 if (inequality[0].
isRational() && inequality[0].getRational() == 0)
4648 inequalityFindThm =
normalize(rhsFindThm);
4650 inequalityFindThm = rhsFindThm;
4652 inequalityFindThm = inequalityThm;
4654 inequalityFindThm = inequalityThm;
4657 TRACE(
"arith find",
"inequalityToFind ==>", inequalityFindThm.
getExpr(),
"");
4659 return inequalityFindThm;
4671 Expr rightSide = e[1];
4686 Rational boundValue = (*lowerBoundFind).second;
4689 if (boundValue > c1 || (boundValue == c1 && !(boundIneq.
getKind() ==
LE && e.
getKind() ==
LT))) {
4697 Rational boundValue = (*upperBoundFind).second;
4700 if (boundValue < c1 || (boundValue == c1 && boundIneq.
getKind() ==
LT && e.
getKind() ==
LT)) {
4712 : d_pathLenghtThres(&(core->getFlags()[
"pathlength-threshold"].getInt())),
4716 unsat_theorem(context),
4717 biggestEpsilon(context, 0, 0),
4718 smallestPathDifference(context, 1, 0),
4725 return unsat_theorem;
4729 return !getUnsatTheorem().isNull();
4735 Graph::iterator find_le = leGraph.find(index);
4736 if (find_le != leGraph.end()) {
4737 EdgeInfo edge_info = (*find_le).second;
4745 return (varInCycle.find(x) != varInCycle.end());
4753 if (x != y && !edge_info.
get().isDefined()) {
4756 core->getResource();
4758 EdgesList::iterator y_it = incomingEdges.find(y);
4759 if (y_it == incomingEdges.end() || (*y_it).second == 0) {
4762 incomingEdges[y] = list;
4766 EdgesList::iterator x_it = outgoingEdges.find(x);
4767 if (x_it == outgoingEdges.end() || (*x_it).second == 0) {
4770 outgoingEdges[x] = list;
4779 if (!existsEdge(x, y))
4780 return EpsRational::PlusInfinity;
4782 EdgeInfo edgeInfo = getEdge(x, y).get();
4790 TRACE(
"arith diff", x,
" --> ", y);
4791 DebugAssert(x != y,
"addEdge, given two equal expressions!");
4793 if (isUnsat())
return;
4796 if (core->outOfResources())
return;
4818 if (rationalDifference > 0 && rationalDifference < smallestPathDifference) {
4819 smallestPathDifference = rationalDifference;
4820 TRACE(
"diff model",
"smallest path difference : ", smallestPathDifference,
"");
4824 if (newEpsilon > biggestEpsilon) {
4825 biggestEpsilon = newEpsilon;
4826 TRACE(
"diff model",
"biggest epsilon : ", biggestEpsilon,
"");
4833 edgeInfoRef = edgeInfo;
4837 if (existsEdge(y, x)) {
4838 varInCycle[x] =
true;
4839 varInCycle[y] =
true;
4847 vector<Expr> updated_in_y;
4848 updated_in_y.push_back(x);
4852 IF_DEBUG(
int total = 0;
int updated = 0;);
4853 for (
unsigned it = 0; it < in_x->
size() && !isUnsat(); it ++) {
4854 const Expr& z = (*in_x)[it];
4855 if (z != arith->zero && z.
hasFind() && core->find(z).getRHS() != z)
continue;
4856 if (z != y && z != x && x != y) {
4859 if (tryUpdate(z, x, y)) {
4860 updated_in_y.push_back(z);
4871 for (
unsigned it_z1 = 0; it_z1 < updated_in_y.size() && !isUnsat(); it_z1 ++) {
4872 for (
unsigned it_z2 = 0; it_z2 < out_y->
size() && !isUnsat(); it_z2 ++) {
4873 const Expr& z1 = updated_in_y[it_z1];
4874 const Expr& z2 = (*out_y)[it_z2];
4875 if (z2 != arith->zero && z2.
hasFind() && core->find(z2).getRHS() != z2)
continue;
4876 if (z1 != z2 && z1 != y && z2 != y)
4877 tryUpdate(z1, y, z2);
4882 TRACE(
"arith propagate",
"could have propagated ", edge_thm.
getExpr(), edge_thm.
isAssump() ?
" ASSUMPTION " :
"not assumption");
4893 if (x != sourceVertex && z != sourceVertex)
4901 DebugAssert(y_z.isDefined(),
"getEdgeTheorems: the cycle edge is not defined!");
4902 getEdgeTheorems(x, y, x_y, outputTheorems);
4903 getEdgeTheorems(y, z, y_z, outputTheorems);
4916 vector<Theorem> inequalities;
4919 getEdgeTheorems(x, x, x_x_cycle, inequalities);
4922 unsat_theorem = rules->cycleConflict(inequalities);
4924 TRACE(
"diff unsat",
"negative cycle : ",
int2string(inequalities.size()),
" vertices.");
4930 if (existsEdge(z, x)) {
4931 varInCycle[x] =
true;
4932 varInCycle[y] =
true;
4933 varInCycle[z] =
true;
4948 bool cycle = (x == z);
4949 bool updated =
false;
4959 if (!cycle || combined_length <= EpsRational::Zero) {
4961 if (!cycle || combined_length < EpsRational::Zero) {
4968 if (rationalDifference > 0 && rationalDifference < smallestPathDifference) {
4969 smallestPathDifference = rationalDifference;
4970 TRACE(
"diff model",
"smallest path difference : ", smallestPathDifference,
"");
4972 if (newEpsilon > biggestEpsilon) {
4973 biggestEpsilon = newEpsilon;
4974 TRACE(
"diff model",
"biggest epsilon : ", biggestEpsilon,
"");
4979 bool addAndEnqueue =
false;
4980 if (core->okToEnqueue() && !combined_length.
isInteger())
4981 if (x.
getType() == arith->intType() && z.
getType() == arith->intType())
4982 addAndEnqueue =
true;
4984 x_z_le.
length = combined_length;
4987 x_z_le_ref = x_z_le;
4989 if (addAndEnqueue) {
4990 vector<Theorem> pathTheorems;
4991 getEdgeTheorems(x, z, x_z_le, pathTheorems);
4992 core->enqueueFact(rules->addInequalities(pathTheorems));
4998 if (core->okToEnqueue()) {
5000 vector<Theorem> antecedentThms;
5001 getEdgeTheorems(x, y, x_y_le, antecedentThms);
5002 getEdgeTheorems(y, z, y_z_le, antecedentThms);
5003 core->enqueueFact(rules->implyEqualities(antecedentThms));
5007 if (updated && !cycle && x != sourceVertex && z != sourceVertex && core->okToEnqueue())
5008 arith->tryPropagate(x, z, x_z_le,
LE);
5012 if (cycle && combined_length < EpsRational::Zero)
5013 analyseConflict(x,
LE);
5025 for (EdgesList::iterator it = incomingEdges.
begin(), it_end = incomingEdges.end(); it != it_end; it ++) {
5027 delete (*it).second;
5028 free ((*it).second);
5031 for (EdgesList::iterator it = outgoingEdges.
begin(), it_end = outgoingEdges.end(); it != it_end; it ++) {
5033 delete (*it).second;
5034 free ((*it).second);
5050 vector<Expr> t1_summands;
5051 t1_summands.push_back(
rat(0));
5052 if (y !=
zero) t1_summands.push_back(y);
5055 if (x !=
zero) t1_summands.push_back(
canon(
rat(-1)*x).getRHS());
5058 TRACE(
"diff atoms",
"trying propagation",
" t1 = " + t1.
toString(),
"");
5067 if (find != find_end) {
5068 set< pair<Rational, Expr> >::iterator bounds = (*find).second.begin();
5069 set< pair<Rational, Expr> >::iterator bounds_end = (*find).second.end();
5070 while (bounds != bounds_end) {
5071 const Expr& implied = (*bounds).second;
5073 if ((*bounds).first < c1 || (implied.
getKind() ==
LE && (*bounds).first == c1)) {
5074 TRACE(
"diff atoms",
"found propagation",
"",
"");
5078 vector<Theorem> antecedentThms;
5093 if (find != find_end) {
5094 set< pair<Rational, Expr> >::iterator bounds = (*find).second.begin();
5095 set< pair<Rational, Expr> >::iterator bounds_end = (*find).second.end();
5096 while (bounds != bounds_end) {
5097 const Expr& implied = (*bounds).second;
5099 if ((*bounds).first < c1) {
5100 TRACE(
"diff atoms",
"found negated propagation",
"",
"");
5101 vector<Theorem> antecedentThms;
5114 if (sourceVertex.isNull()) {
5115 Theorem thm_exists_zero = arith->getCommonRules()->varIntroSkolem(arith->zero);
5116 sourceVertex = thm_exists_zero.
getExpr()[1];
5123 EdgesList::iterator vertexIt = incomingEdges.begin();
5124 EdgesList::iterator vertexItEnd = incomingEdges.end();
5125 for (; vertexIt != vertexItEnd; vertexIt ++) {
5126 Expr vertex = (*vertexIt).first;
5127 if (core->find(vertex).getRHS() != vertex)
continue;
5128 if (vertex != sourceVertex && !existsEdge(sourceVertex, vertex))
5129 addEdge(sourceVertex, vertex, 0, thm);
5131 vertexIt = outgoingEdges.
begin();
5132 vertexItEnd = outgoingEdges.end();
5133 for (; vertexIt != vertexItEnd; vertexIt ++) {
5134 Expr vertex = (*vertexIt).first;
5135 if (core->find(vertex).getRHS() != vertex)
continue;
5136 if (vertex != sourceVertex && !existsEdge(sourceVertex, vertex))
5137 addEdge(sourceVertex, vertex, 0, thm);
5141 if (!existsEdge(sourceVertex, arith->zero))
5142 addEdge(sourceVertex, arith->zero, 0, thm);
5156 if (x == sourceVertex)
return 0;
5164 EdgeInfo zero_le_c = zero_le_c_ref;
5173 TRACE(
"diff model" ,
"biggest epsilon: ", biggestEpsilon,
"");
5174 TRACE(
"diff model" ,
"smallestPathDifference: ", smallestPathDifference,
"");
5181 TRACE(
"diff model",
"Value of ", x,
" : " + value.
toString());
5199 TRACE(
"arith var order",
"addPairToArithOrder(" + smaller.
toString(),
", ", bigger.
toString() +
")");
5211 if (
isPow(term))
return true;
5212 if (!
isMult(term))
return false;
5214 for (
int j = 0; j < term.
arity(); j ++)
5215 if (
isPow(term[j]))
return true;
5216 else if (
isLeaf(term[j])) {
5218 if (vars > 1)
return true;
5227 const Expr& lhs = e[0];
5228 const Expr& rhs = e[1];
5233 for (
int i = 0; i < lhs.arity(); i ++)
5237 for (
int i = 0; i < rhs.
arity(); i ++)
5248 if (!
isPlus(eq[0]))
return false;
5249 if (eq[0].arity() != 3)
return false;
5253 Expr term1 = eq[0][1];
5262 if (
isPow(term1[1])) {
5263 if (term1_c == 1) power1 = term1[1];
5264 else if (term1_c == -1) power2 = term1[1];
5266 }
else return false;
5267 }
else return false;
5268 }
else return false;
5271 Expr term2 = eq[0][2];
5280 if (
isPow(term2[1])) {
5281 if (term2_c == 1) power1 = term2[1];
5282 else if (term2_c == -1) power2 = term2[1];
5284 }
else return false;
5285 }
else return false;
5286 }
else return false;
5289 if (term1_c == term2_c)
return false;
5294 if (power1[0].getRational() != power2[0].getRational())
return false;
5303 if (!
isPlus(eq[0]))
return false;
5304 if (eq[0].arity() != 2)
return false;
5309 Expr term = eq[0][1];
5312 constant = -constant;
5319 constant = -constant;
5320 }
else if (term2_c == -1) {
5323 }
else return false;
5324 }
else return false;
5325 }
else return false;
5329 if (!power1[0].getRational().
isInteger())
return false;
5347 DebugAssert(right.
arity() > 1,
"TheoryArithOld::canPickEqMonomial, expecting > 1 child, got " + right.
arity());
5363 }
else if (
isMult(*i) && (*i).arity() == 2 && (*i)[0].isRational() &&
isLeaf((*i)[1])) {
5365 coeff =
abs((*i)[0].getRational());
5371 if (coeff != 1 && coeff != -1)
5376 for (j = istart; j != iend; ++j)
5404 TRACE(
"arith shared",
"getUpperBound(", t.
toString(),
") ==> " + (*find_t).second.toString());
5405 return (*find_t).second;
5408 TRACE(
"arith shared",
"getUpperBound(", t.
toString(),
") ==> +inf");
5432 for (
int i = 0; i < t.
arity(); i ++) {
5435 if (t_i_upperBound.
isFinite()) upperBound = upperBound + t_i_upperBound;
5441 if (i == t.
arity()) {
5442 TRACE(
"arith shared",
"getUpperBound(", t.
toString(),
") ==> constrained");
5476 TRACE(
"arith shared",
"getLowerBound(", t.
toString(),
") ==> " + (*t_find).second.toString());
5477 return (*t_find).second;
5480 TRACE(
"arith shared",
"getLowerBound(", t.
toString(),
") ==> -inf");
5504 for (
int i = 0; i < t.
arity(); i ++) {
5507 if (t_i_lowerBound.
isFinite()) lowerBound = lowerBound + t_i_lowerBound;
5513 if (i == t.
arity()) {
5514 TRACE(
"arith shared",
"getLowerBound(", t.
toString(),
") ==> constrained");
5537 int computeTermBoundsConstrainedCount = 0;
5539 vector<Expr> sorted_vars;
5551 for (
int i = sorted_vars.size() - 1; i >= 0; i --)
5554 Expr v = sorted_vars[i];
5572 if (!constrainedAbove) constrainedAbove = upperBound.
isFinite();
5581 if (left_list && left_list->
size() > 0) {
5582 for (
unsigned ineq_i = 0; ineq_i < left_list->
size(); ineq_i ++) {
5584 Ineq ineq = (*left_list)[ineq_i];
5591 if (currentUpperBound.
isFinite() && (!upperBound.
isFinite() || currentUpperBound < upperBound)) {
5592 upperBound = currentUpperBound;
5593 constrainedAbove =
true;
5602 else if (!constrainedAbove) {
5627 if (lowerBound.
isFinite()) lowerBound = -lowerBound;
5629 if (!constrainedBelow) constrainedBelow = lowerBound.
isFinite();
5638 if (right_list && right_list->
size() > 0) {
5639 for (
unsigned ineq_i = 0; ineq_i < right_list->
size(); ineq_i ++) {
5641 Ineq ineq = (*right_list)[ineq_i];
5648 if (currentLowerBound.
isFinite() && (!lowerBound.
isFinite() || currentLowerBound > lowerBound)) {
5649 lowerBound = currentLowerBound;
5650 constrainedBelow =
true;
5659 else if (!constrainedBelow) {
5680 if (constrainedAbove && constrainedBelow) computeTermBoundsConstrainedCount ++;
5682 TRACE(
"arith shared", (constrainedAbove && constrainedBelow ?
"constrained " :
"unconstrained "),
"",
"");
5684 computeTermBoundsConstrainedCount ++;
5687 TRACE(
"arith shared",
"number of constrained variables : ",
int2string(computeTermBoundsConstrainedCount),
" of " +
int2string(sorted_vars.size()));
5689 return computeTermBoundsConstrainedCount;
5694 TRACE(
"arith shared",
"isConstrainedAbove(", t.
toString(),
")");
5698 TRACE(
"arith shared",
"isConstrainedAbove() ==> true",
"",
"");
5705 TRACE(
"arith shared",
"isConstrainedAbove() ==> true",
"",
"");
5709 TRACE(
"arith shared",
"isConstrainedAbove() ==> false",
"",
"");
5713 bool constrainedAbove =
true;
5717 constrainedAbove =
false;
5732 for (
int i = 0; i < t.
arity() && constrainedAbove; i ++)
5740 TRACE(
"arith shared",
"isConstrainedAbove() ==> ", constrainedAbove ?
"true" :
"false",
"");
5743 return constrainedAbove;
5748 TRACE(
"arith shared",
"isConstrainedBelow(", t.
toString(),
")");
5756 TRACE(
"arith shared",
"isConstrainedBelow() ==> true",
"",
"");
5760 TRACE(
"arith shared",
"isConstrainedBelow() ==> false",
"",
"");
5764 bool constrainedBelow =
true;
5768 constrainedBelow =
false;
5783 constrainedBelow =
true;
5784 for (
int i = 0; i < t.
arity() && constrainedBelow; i ++)
5786 constrainedBelow =
false;
5793 TRACE(
"arith shared",
"isConstrainedBelow() ==> ", constrainedBelow ?
"true" :
"false",
"");
5796 return constrainedBelow;
5805 TRACE(
"arith shared",
"isConstrained(", t.
toString(), (result ?
") ==> true " :
") ==> false ") );
5811 EdgesList::iterator find_x = incomingEdges.find(x);
5814 if (find_x == incomingEdges.end())
return false;
5818 if (!list)
return false;
5821 if (sourceVertex.isNull())
5822 return list->
size() > 0;
5824 return list->
size() > 1;
5829 EdgesList::iterator find_x = outgoingEdges.find(x);
5832 if (find_x == outgoingEdges.end())
return false;
5836 if (!list)
return false;
5839 return list->
size() > 0;
5846 EdgesList::iterator incoming_it = incomingEdges.begin();
5847 EdgesList::iterator incoming_it_end = incomingEdges.end();
5848 while (incoming_it != incoming_it_end) {
5849 Expr var = (*incoming_it).first;
5850 if (var != sourceVertex)
5851 vars_set.insert(var);
5855 EdgesList::iterator outgoing_it = outgoingEdges.begin();
5856 EdgesList::iterator outgoing_it_end = outgoingEdges.end();
5857 while (outgoing_it != outgoing_it_end) {
5858 Expr var = (*outgoing_it).first;
5859 if (var != sourceVertex)
5860 vars_set.insert(var);
5864 set<Expr>::iterator set_it = vars_set.begin();
5865 set<Expr>::iterator set_it_end = vars_set.end();
5866 while (set_it != set_it_end) {
5867 variables.push_back(*set_it);
5874 out <<
"digraph G {" <<
endl;
5876 EdgesList::iterator incoming_it = incomingEdges.begin();
5877 EdgesList::iterator incoming_it_end = incomingEdges.end();
5878 while (incoming_it != incoming_it_end) {
5880 Expr var_u = (*incoming_it).first;
5884 for (
unsigned edge_i = 0; edge_i < edges->
size(); edge_i ++) {
5885 Expr var_v = (*edges)[edge_i];
5897 for (
int i = 0; i < t.
arity(); ++ i) {
5899 TRACE(
"arith::unconstrained",
"isUnconstrained(", t,
") => true (subterm)");
5907 TRACE(
"arith::unconstrained",
"isUnconstrained(", t,
") => false (rational)");
5911 TRACE(
"arith::unconstrained",
"isUnconstrained(", t,
") => false (multiplication)");
5922 TRACE(
"arith::unconstrained",
"isUnconstrained(", t,
") => false");
5927 TRACE(
"arith::unconstrained",
"updateConstrained(", t,
")");
5931 for (
int i = 0; i < t.
arity(); ++ i) {