45 os <<
"FreeConst(r=" << fc.
getConst() <<
", "
46 << (fc.
strict()?
"strict" :
"non-strict") <<
")";
55 os <<
"Ineq(" << ineq.
ineq().
getExpr() <<
", isolated on "
56 << (ineq.
varOnRHS()?
"RHS" :
"LHS") <<
", const = "
79 if(e == isIntE)
return thm;
84 int i, iend=e.
arity();
85 for(i=0; i<iend; ++i) {
86 res = isIntegerDerive(isIntE, getCommonRules()->andElim(thm, i));
87 if(!res.
isNull())
return res;
94 bool TheoryArithNew::kidsCanonical(
const Expr& e) {
95 if(isLeaf(e))
return true;
97 for(
int i=0; res && i<e.
arity(); ++i) {
98 Expr simp(canon(e[i]).getRHS());
100 IF_DEBUG(
if(!res) debugger.getOS() <<
"\ne[" << i <<
"] = " << e[i]
101 <<
"\nsimplified = " << simp <<
endl;)
126 TRACE(
"arith",
"canon(", e ,
") {");
140 result = d_rules->uMinusToMult(e[0]);
146 result = transitivityRule(result, canon(e2));
156 result = d_rules->canonPlus(e);
168 Theorem minus_eq_sum = d_rules->minusToPlus(e[0], e[1]);
171 Expr sum(minus_eq_sum.getRHS());
177 if(thm.getLHS() == thm.getRHS())
178 result = canonThm(minus_eq_sum);
183 Theorem sum_eq_canon = canonThm(substitutivityRule(sum, 1, thm));
186 result = transitivityRule(minus_eq_sum, sum_eq_canon);
198 result = d_rules->canonMult(e);
209 if (e[1].getKind() ==
PLUS)
213 result = d_rules->canonDivide(e);
223 if(e[1].
isRational()) result = d_rules->canonPowConst(e);
225 else result = reflexivityRule(e);
233 result = reflexivityRule(e);
240 TRACE(
"arith",
"canon => ",result,
" }");
248 TRACE(
"arith",
"canonSimplify(", e,
") {");
263 thm = transitivityRule(thm, find(thm.
getRHS()));
269 TRACE(
"arith",
"canonSimplify =>", thm,
" }");
279 TheoryArithNew::canonPred(
const Theorem& thm) {
280 vector<Theorem> thms;
282 "TheoryArithNew::canonPred: bad theorem: "+thm.
toString());
284 thms.push_back(canonSimplify(e[0]));
285 thms.push_back(canonSimplify(e[1]));
286 return iffMP(thm, substitutivityRule(e.
getOp(), thms));
297 vector<Theorem> thms;
306 thms.push_back(canonSimplify(e[0]));
307 thms.push_back(canonSimplify(e[1]));
310 return transitivityRule(thm, substitutivityRule(e.
getOp(), thms));
318 TheoryArithNew::canonConjunctionEquiv(
const Theorem& thm) {
319 vector<Theorem> thms;
334 TRACE(
"arith eq",
"doSolve(",e,
") {");
337 vector<Theorem> thms;
342 eqnThm = iffMP(thm, d_rules->rightMinusLeft(e));
343 eqnThm = canonPred(eqnThm);
350 Theorem result = iffMP(eqnThm, d_rules->constPredicate(eqnThm.getExpr()));
351 TRACE(
"arith eq",
"doSolve => ",result,
" }");
356 eqnThm = iffMP(eqnThm, normalize(eqnThm.getExpr()));
357 right = eqnThm.getRHS();
361 if(!isInteger(right)) {
364 res = processRealEq(eqnThm);
366 res = symmetryRule(eqnThm);
367 TRACE(
"arith eq",
"doSolve: failed to solve an equation: ", e,
"");
368 IF_DEBUG(debugger.counter(
"FAILED to solve real equalities")++;)
369 setIncomplete(
"Non-linear arithmetic inequalities");
371 IF_DEBUG(debugger.counter(
"solved real equalities")++;)
372 TRACE(
"arith eq",
"doSolve [real] => ", res,
" }");
376 Theorem res = processIntEq(eqnThm);
377 IF_DEBUG(debugger.counter(
"solved int equalities")++;)
378 TRACE(
"arith eq",
"doSolve [int] => ", res,
" }");
391 "TheoryArithNew::pickIntEqMonomial right is wrong :-): " +
394 "TheoryArithNew::pickIntEqMonomial. right[0] must be const" +
397 "TheoryArithNew::pickIntEqMonomial: right is of type int: " +
420 TheoryArithNew::processRealEq(
const Theorem& eqn)
437 for(
int i = right.
arity()-1; i>=0; --i) {
445 Expr leaf = isLeaf(c) ? c : c[1];
446 for (
int j = 0; j < right.
arity(); ++j) {
448 && isLeafIn(leaf, right[j])
464 else if ((
isMult(right) && right.
arity() == 2 && isLeaf(right[1])) ||
486 "TheoryArithNew::ProcessRealEq: left is integer:\n left = "
492 result = canonPred(result);
495 result = iffMP(result, d_rules->plusPredicate(result.getLHS(),
496 result.getRHS(),
left,
EQ));
497 result = canonPred(result);
498 TRACE(
"arith",
"processRealEq => ",result,
" }");
507 TheoryArithNew::processSimpleIntEq(
const Theorem& eqn)
509 TRACE(
"arith eq",
"processSimpleIntEq(", eqn.
getExpr(),
") {");
511 "TheoryArithNew::processSimpleIntEq: eqn must be equality" +
517 "TheoryArithNew::processSimpleIntEq: LHS must be 0:\n" +
524 separateMonomial(right, c, x);
528 TRACE(
"arith eq",
"processSimpleIntEq[0 = a*x] => ", res,
" }");
530 }
else if(
isPlus(right)) {
531 if(2 == right.arity()) {
534 separateMonomial(right[1], c, x);
539 TRACE(
"arith eq",
"processSimpleIntEq[0 = c + a*x] => ", res,
" }");
543 "TheoryArithNew::processSimpleIntEq: RHS is not in correct form:"
546 Expr isolated = pickIntEqMonomial(right);
547 TRACE(
"arith eq",
"processSimpleIntEq: isolated = ", isolated,
"");
554 ((isolated[0].getRational() > 0) ? -1 : 1) : -1;
559 result = iffMP(eqn, d_rules->multEqn(eqn.
getLHS(),
right, rat(r)));
560 result = canonPred(result);
564 result = iffMP(result,
569 const Rational& minusa = isolated[0].getRational();
571 isolated = (a == 1)? isolated[1] : rat(a) * isolated[1];
574 result = iffMP(eqn, d_rules->plusPredicate(eqn.
getLHS(),
578 result = canonPred(result);
581 if(!
isMult(isolated) || isolated[0].getRational() == 1) {
582 TRACE(
"arith eq",
"processSimpleIntEq[x = rhs] => ", result,
" }");
586 "TheoryArithNew::processSimpleIntEq: isolated must be mult "
587 "with coeff >= 2.\n isolated = " + isolated.toString());
593 separateMonomial(lhs, a, x);
594 Theorem isIntLHS = isIntegerThm(x);
595 vector<Theorem> isIntRHS;
598 separateMonomial(rhs, c, v);
599 isIntRHS.push_back(isIntegerThm(v));
606 for(; i!=iend; ++i) {
608 separateMonomial(*i, c, v);
609 isIntRHS.push_back(isIntegerThm(v));
614 result = d_rules->eqElimIntRule(result, isIntLHS, isIntRHS);
616 result = getCommonRules()->skolemize(result);
620 Theorem thm1 = canonPred(getCommonRules()->andElim(result, 0));
621 Theorem thm2 = canonPred(getCommonRules()->andElim(result, 1));
622 Theorem newRes = getCommonRules()->andIntro(thm1, thm2);
625 TRACE(
"arith eq",
"processSimpleIntEq => ", result,
" }");
630 Theorem result = symmetryRule(eqn);
631 TRACE(
"arith eq",
"processSimpleIntEq[x = 0] => ", result,
" }");
642 TheoryArithNew::processIntEq(
const Theorem& eqn)
644 TRACE(
"arith eq",
"processIntEq(", eqn.
getExpr(),
") {");
646 std::vector<Theorem> solvedAndNewEqs;
650 result = processSimpleIntEq(newEq);
653 solvedAndNewEqs.push_back(result);
660 solvedAndNewEqs.push_back(getCommonRules()->andElim(result, 0));
661 newEq = getCommonRules()->andElim(result, 1);
667 else res = solvedForm(solvedAndNewEqs);
668 TRACE(
"arith eq",
"processIntEq => ", res.
getExpr(),
" }");
681 TheoryArithNew::solvedForm(
const vector<Theorem>& solvedEqs)
683 DebugAssert(solvedEqs.size() > 0,
"TheoryArithNew::solvedForm()");
686 TRACE_MSG(
"arith eq",
"TheoryArithNew::solvedForm:solvedEqs(\n [");
687 IF_DEBUG(
if(debugger.trace(
"arith eq")) {
688 for(vector<Theorem>::const_iterator j = solvedEqs.begin(),
689 jend=solvedEqs.end(); j!=jend;++j)
690 TRACE(
"arith eq",
"", j->getExpr(),
",\n ");
695 vector<Theorem>::const_reverse_iterator
696 i = solvedEqs.rbegin(),
697 iend = solvedEqs.rend();
701 for(; i!=iend; ++i) {
703 Theorem thm = substAndCanonize(*i, subst);
704 TRACE(
"arith eq",
"solvedForm: subst["+i->getLHS().toString()+
"] = ",
706 subst[i->getLHS()] = thm;
711 "TheoryArithNew::solvedForm: an element of solvedEqs must "
712 "be either EQ or FALSE: "+i->toString());
718 vector<Theorem> thms;
721 thms.push_back(i->second);
723 return getCommonRules()->andIntro(thms);
738 TRACE(
"arith eq",
"substAndCanonize(", t,
") {");
741 Theorem res(reflexivityRule(t));
742 TRACE(
"arith eq",
"substAndCanonize[subst empty] => ", res,
" }");
748 TRACE(
"arith eq",
"substAndCanonize[subst] => ", i->second,
" }");
753 Theorem res(reflexivityRule(t));
754 TRACE(
"arith eq",
"substAndCanonize[i-leaf] => ", res,
" }");
758 vector<Theorem> thms;
759 vector<unsigned> changed;
760 for(
unsigned j=0, jend=t.
arity(); j!=jend; ++j) {
761 Theorem thm = substAndCanonize(t[j], subst);
762 if(thm.
getRHS() != t[j]) {
765 changed.push_back(j);
770 if(thms.size() > 0) {
771 res = substitutivityRule(t, changed, thms);
775 res = reflexivityRule(t);
776 TRACE(
"arith eq",
"substAndCanonize => ", res,
" }");
790 if(subst.
empty())
return eq;
796 Theorem thm = substAndCanonize(t, subst);
798 if(thm.
getRHS() == t)
return eq;
800 vector<Theorem> thms;
801 vector<unsigned> changed;
803 changed.push_back(1);
804 return iffMP(eq, substitutivityRule(eq.
getExpr(), changed, thms));
810 TRACE(
"arith ineq",
"updateStats("+c.
toString()+
", ", v,
")");
812 if(d_countRight.count(v) > 0) d_countRight[v] = d_countRight[v] + 1;
813 else d_countRight[v] = 1;
816 if(d_countLeft.count(v) > 0) d_countLeft[v] = d_countLeft[v] + 1;
817 else d_countLeft[v] = 1;
821 void TheoryArithNew::updateStats(
const Expr& monomial)
824 separateMonomial(monomial, c, m);
829 void TheoryArithNew::addToBuffer(
const Theorem& thm) {
835 if(!(e[0].
isRational() && e[0].getRational() == 0)) {
836 result = iffMP(result, d_rules->rightMinusLeft(e));
837 result = canonPred(result);
839 TRACE(
"arith ineq",
"addToBuffer(", result.
getExpr(),
")");
841 d_buffer.push_back(thm);
869 vector<Rational> nums, denoms;
872 for(
int i = 0, iend = right.
arity(); i < iend; i ++) {
877 switch(right[i].getKind()) {
882 c =
abs(right[i].getRational());
894 if (type == NORMALIZE_UNIT)
return rat(1/c);
897 sign = (c > 0 ? 1 : -1);
922 factor = (gcd_nums == 0)? 0 : (sign * lcm(denoms) / gcd_nums);
932 bool TheoryArithNew::lessThanVar(
const Expr& isolatedMonomial,
const Expr& var2)
935 "TheoryArithNew::findMaxVar: isolatedMonomial cannot be rational" +
938 separateMonomial(isolatedMonomial, c, var0);
939 separateMonomial(var2, c, var1);
944 void TheoryArithNew::separateMonomial(
const Expr& e,
Expr& c,
Expr& var) {
945 TRACE(
"separateMonomial",
"separateMonomial(", e,
")");
947 "TheoryArithNew::separateMonomial(e = "+e.
toString()+
")");
950 "TheoryArithNew::separateMonomial(e = "+e.
toString()+
")");
952 if(e.
arity() == 2) var = e[1];
954 vector<Expr> kids = e.
getKids();
965 "TheoryArithNew::separateMonomial(e = "
972 bool TheoryArithNew::VarOrderGraph::lessThan(
const Expr& e1,
const Expr& e2)
980 bool TheoryArithNew::VarOrderGraph::dfs(
const Expr& e1,
const Expr& e2)
984 if(d_cache.count(e2) > 0)
986 if(d_edges.count(e2) == 0)
989 vector<Expr>& e2Edges = d_edges[e2];
990 vector<Expr>::iterator i = e2Edges.begin();
991 vector<Expr>::iterator iend = e2Edges.end();
993 for(; i != iend && !dfs(e1,*i); ++i);
998 void TheoryArithNew::VarOrderGraph::selectSmallest(vector<Expr>& v1,
1001 int v1Size = v1.size();
1002 vector<bool> v3(v1Size);
1003 for(
int j=0; j < v1Size; ++j)
1006 for(
int j=0; j < v1Size; ++j) {
1008 for(
int i =0; i < v1Size; ++i) {
1009 if((i == j) || v3[i])
1011 if(lessThan(v1[i],v1[j])) {
1017 vector<Expr> new_v1;
1019 for(
int j = 0; j < v1Size; ++j)
1020 if(!v3[j]) v2.push_back(v1[j]);
1021 else new_v1.push_back(v1[j]);
1026 void TheoryArithNew::VarOrderGraph::selectLargest(
const vector<Expr>& v1,
1029 int v1Size = v1.size();
1030 vector<bool> v3(v1Size);
1031 for(
int j=0; j < v1Size; ++j)
1034 for(
int j=0; j < v1Size; ++j) {
1036 for(
int i =0; i < v1Size; ++i) {
1037 if((i == j) || v3[i])
1039 if(lessThan(v1[j],v1[i])) {
1046 for(
int j = 0; j < v1Size; ++j)
1047 if(!v3[j]) v2.push_back(v1[j]);
1057 d_diseq(core->getCM()->getCurrentContext()),
1058 d_diseqIdx(core->getCM()->getCurrentContext(), 0, 0),
1059 d_inModelCreation(core->getCM()->getCurrentContext(), false, 0),
1060 d_freeConstDB(core->getCM()->getCurrentContext()),
1061 d_buffer(core->getCM()->getCurrentContext()),
1063 d_bufferIdx(core->getCM()->getCurrentContext(), 0, 0),
1064 d_bufferThres(&(core->getFlags()[
"ineq-delay"].getInt())),
1065 d_countRight(core->getCM()->getCurrentContext()),
1066 d_countLeft(core->getCM()->getCurrentContext()),
1067 d_sharedTerms(core->getCM()->getCurrentContext()),
1068 d_sharedVars(core->getCM()->getCurrentContext()),
1069 consistent(core->getCM()->getCurrentContext()),
1070 lowerBound(core->getCM()->getCurrentContext()),
1071 upperBound(core->getCM()->getCurrentContext()),
1072 beta(core->getCM()->getCurrentContext()),
1073 assertedExprCount(core->getCM()->getCurrentContext()),
1074 integer_lemma(core->getCM()->getCurrentContext())
1105 kinds.push_back(
REAL);
1106 kinds.push_back(
INT);
1110 kinds.push_back(
PLUS);
1111 kinds.push_back(
MINUS);
1112 kinds.push_back(
MULT);
1114 kinds.push_back(
POW);
1116 kinds.push_back(
MOD);
1117 kinds.push_back(
LT);
1118 kinds.push_back(
LE);
1119 kinds.push_back(
GT);
1120 kinds.push_back(
GE);
1158 if(cache.count(e) > 0)
return;
1161 if(
isLeaf(e)) vars.push_back(e);
1172 DebugAssert(
isLE(ineq1),
"TheoryArithNew::processFiniteInterval: ineq1 = "
1174 DebugAssert(
isLE(ineq2),
"TheoryArithNew::processFiniteInterval: ineq2 = "
1183 const Expr& ax = ineq1[1];
1184 const Expr& bx = ineq2[0];
1186 "TheoryArithNew::processFiniteInterval:\n ax = "+ax.
toString());
1188 "TheoryArithNew::processFiniteInterval:\n bx = "+bx.
toString());
1192 Theorem thm1(alphaLEax), thm2(bxLEbeta);
1199 const Expr& alphaLEt = thm1.getExpr();
1200 const Expr& alpha = alphaLEt[0];
1201 const Expr& t = alphaLEt[1];
1211 vector<unsigned> changed;
1212 vector<Theorem> thms;
1213 changed.push_back(1);
1214 thms.push_back(bEQac);
1216 tLEac =
iffMP(thm2, tLEac);
1239 size_t sizeLeft = ineqsLeft.
size();
1240 size_t sizeRight = ineqsRight.
size();
1242 for(
size_t l=0; l<sizeLeft; ++l)
1243 for(
size_t r=0; r<sizeRight; ++r)
1255 for (
int k = 0; k < e.
arity(); ++k) {
1301 TRACE(
"model",
"refineCounterExample[TheoryArithNew] ",
"",
"{");
1307 for(; it!=iend; ++it) {
1309 Expr e1 = (*it).first;
1310 for(it2 = it, ++it2; it2!=iend; ++it2) {
1311 Expr e2 = (*it2).first;
1313 "TheoryArithNew::refineCounterExample: e1 = "+e1.
toString()
1317 "TheoryArithNew::refineCounterExample: e2 = "+e2.
toString()
1320 if (!eq.isBoolConst())
1325 TRACE(
"model",
"refineCounterExample[Theory::Arith] ",
"",
"}");
1338 "seperateMonomial failed");
1340 "smallest variable in graph, should not have variables"
1341 " in inequalities: ");
1342 DebugAssert(x == var,
"separateMonomial found different variable: "
1350 bool strictLB=
false, strictUB=
false;
1355 int numRight = 0, numLeft = 0;
1358 for(
unsigned int i=0; i<ratsLTe->
size(); i++) {
1359 DebugAssert((*ratsLTe)[i].varOnRHS(),
"variable on wrong side!");
1360 Expr ineq = (*ratsLTe)[i].ineq().getExpr();
1361 Expr leftSide = ineq[0], rightSide = ineq[1];
1364 if(numRight==0 || r>glb){
1366 strictLB =
isLT(ineq);
1374 for(
unsigned int i=0; i<ratsGTe->
size(); i++) {
1375 DebugAssert((*ratsGTe)[i].varOnLHS(),
"variable on wrong side!");
1376 Expr ineq = (*ratsGTe)[i].ineq().getExpr();
1377 Expr leftSide = ineq[0], rightSide = ineq[1];
1380 if(numLeft==0 || r<lub) {
1382 strictUB =
isLT(ineq);
1388 if(!left && !right) {
1392 if(!left && right) {lub = glb +2;}
1393 if(!right && left) {glb = lub-2;}
1394 DebugAssert(glb <= lub,
"Greatest lower bound needs to be smaller "
1395 "than least upper bound");
1402 while (v.size() > 0) {
1403 std::vector<Expr> bottom;
1405 TRACE(
"model",
"Finding variables to assign. Iteration # ", count,
"");
1406 for(
unsigned int i = 0; i<bottom.size(); i++) {
1408 TRACE(
"model",
"Found: ", e,
"");
1423 mid = (lub + glb)/2;
1424 TRACE(
"model",
"Assigning mid = ", mid,
" {");
1437 TRACE(
"model",
"Arith=>computeModel ",
"",
"{");
1438 for(
unsigned int i=0; i <v.size(); ++i) {
1439 const Expr& e = v[i];
1441 TRACE(
"model",
"arith variable:", e ,
"");
1445 TRACE(
"model",
"arith variable:", e ,
"");
1450 TRACE(
"model",
"Arith=>computeModel",
"",
"}");
1458 +e.
toString()+
")\n e is not assigned concrete value.\n"
1474 TRACE(
"arith",
"normalize(", e,
") {");
1488 if (
isMult(e[1])) factor =
rat(1/e[1][0].getRational());
1493 TRACE(
"arith",
"normalize: factor = ", factor,
"");
1499 if(factor.getRational() != 1)
1530 TRACE(
"arith",
"normalize => ", thm,
" }");
1553 if (isIntConstraintThm.
isNull())
return result;
1556 TRACE(
"integer",
"TheoryArithNew::rafineIntegerConstraints(", constr,
")");
1557 TRACE(
"integer",
"TheoryArithNew::rafineIntegerConstraints: int proof:", isIntConstraintThm,
"");
1576 TRACE(
"arith",
"TheoryArithNew::rewrite(", e,
") {");
1597 TRACE(
"arith",
"TheoryArithNew::rewrite[non-literal] => ", thm,
" }");
1632 DebugAssert(e[0].getKind() !=
EQ,
"TheoryArithNew::rewrite, not expecting equality under negation");
1664 const Expr& rightSide = normalised[1];
1665 const Expr& leftSide = normalised[0];
1693 TRACE(
"integer",
"Type ", e[0].getType().toString(),
"");
1704 FatalAssert(
false,
"Theory_Arith::rewrite: control should not reach here");
1727 TRACE(
"arith",
"TheoryArithNew::rewrite => ", thm,
" }");
1754 int arity(e.
arity());
1757 for (
int k = 0 ; k < arity; k ++) {
1763 TRACE(
"arith setup",
"e["+
int2string(k)+
"]: ", *(e[k].getNotify()),
"");
1772 IF_DEBUG(debugger.counter(
"arith update total")++;)
1779 vector<unsigned> changed;
1780 vector<Theorem> children;
1781 changed.push_back(1);
1782 children.push_back(e);
1791 IF_DEBUG(debugger.counter(
"arith update ineq")++;)
1796 TRACE(
"arith",
"TheoryArithNew::update(): thm = ", thm,
"");
1800 IF_DEBUG(debugger.counter(
"arith update find(d)=d")++;)
1848 TRACE(
"model",
"TheoryArithNew::computeModelTerm(", e,
"): a variable");
1852 TRACE(
"model",
"TheoryArithNew::computeModelTerm("+e.
toString()
1853 +
"): has find pointer to ", e2,
"");
1866 std::vector<Expr> kids;
1868 kids.push_back(
leExpr(tExpr[0], e));
1869 kids.push_back(
leExpr(e, tExpr[1]));
1889 if (e.
arity() > 0) {
1894 if (e.
arity() != 2 ||
1902 DebugAssert(
false,
"Unexpected kind in TheoryArithNew::checkType"
1909 bool enumerate,
bool computeSize)
1918 if (r <= typeExpr[1].getRational()) {
1954 for(
int k = 0; k < e.
arity(); ++k) {
1970 Expr numerator = e[0];
1971 Expr denominator = e[1];
1994 for (
int k = 0; k < e.
arity(); ++k) {
2012 DebugAssert(
false,
"TheoryArithNew::computeType: unexpected expression:\n "
2021 "TheoryArithNew::computeBaseType("+t.
toString()+
")");
2041 TRACE(
"parser",
"TheoryArithNew::parseExprOp(", e,
")");
2065 "TheoryArithNew::parseExprOp:\n e = "+e.
toString());
2067 const Expr& c1 = e[0][0];
2083 for(; i!=iend; ++i) k.push_back(
parseExpr(*i));
2089 else if(e.
arity() == 3)
2102 for(; i!=iend; ++i) k.push_back(
parseExpr(*i));
2139 "TheoryArithNew::parseExprOp: invalid input " + e.
toString());
2158 os <<
"ERROR:SUBRANGE:not supported in Simplify\n";
2161 os <<
"ERROR:IS_INTEGER:not supported in Simplify\n";
2164 int i=0, iend=e.
arity();
2166 if(i!=iend) os << e[i];
2168 for(; i!=iend; ++i) os <<
" " << e[i];
2173 os <<
"(- " << e[0] <<
" " << e[1]<<
")";
2179 int i=0, iend=e.arity();
2181 if(i!=iend) os << e[i];
2183 for(; i!=iend; ++i) os <<
" " << e[i];
2188 os <<
"(" <<
push << e[1] <<
space <<
"^ " << e[0] <<
push <<
")";
2191 os <<
"(" << push << e[0] <<
space <<
"/ " << e[1] << push <<
")";
2194 if (
isInt(e[0].getType()) ||
isInt(e[1].getType())) {
2196 os <<
"(< " << e[0] <<
" " << e[1] <<
")";
2199 os <<
"(<= " << e[0] <<
" " << e[1] <<
")";
2202 os <<
"(> " << e[0] <<
" " << e[1] <<
")";
2205 os <<
"(>= " << e[0] <<
" " << e[1] <<
")";
2209 os <<
"ERROR:SHADOW:not supported in Simplify\n";
2227 os <<
"ERROR:SUBRANGE:not supported in TPTP\n";
2230 os <<
"ERROR:IS_INTEGER:not supported in TPTP\n";
2234 os<<
"ERRPR:plus only supports inteters now in TPTP\n";
2238 int i=0, iend=e.
arity();
2240 os<<
"ERROR,plus must have more than two numbers in TPTP\n";
2244 for(i=0; i <= iend-2; ++i){
2251 for(i=0 ; i <= iend-2; ++i){
2258 os <<
"(- " << e[0] <<
" " << e[1]<<
")";
2264 int i=0, iend=e.arity();
2266 if(i!=iend) os << e[i];
2268 for(; i!=iend; ++i) os <<
" " << e[i];
2273 os <<
"(" <<
push << e[1] <<
space <<
"^ " << e[0] <<
push <<
")";
2276 os <<
"(" << push << e[0] <<
space <<
"/ " << e[1] << push <<
")";
2279 if (
isInt(e[0].getType()) ||
isInt(e[1].getType())) {
2281 os <<
"(< " << e[0] <<
" " << e[1] <<
")";
2284 os <<
"(<= " << e[0] <<
" " << e[1] <<
")";
2287 os <<
"(> " << e[0] <<
" " << e[1] <<
")";
2290 os <<
"(>= " << e[0] <<
" " << e[1] <<
")";
2294 os <<
"ERROR:SHADOW:not supported in TPTP\n";
2318 os <<
"[" <<
push << e[0] <<
".." << e[1] <<
push <<
"]";
2322 os <<
"IS_INTEGER(" << push << e[0] << push <<
")";
2327 int i=0, iend=e.
arity();
2329 if(i!=iend) os << e[i];
2331 for(; i!=iend; ++i) os <<
space <<
"+ " << e[i];
2336 os <<
"(" << push << e[0] <<
space <<
"- " << e[1] << push <<
")";
2339 os <<
"-(" << push << e[0] << push <<
")";
2342 int i=0, iend=e.
arity();
2344 if(i!=iend) os << e[i];
2346 for(; i!=iend; ++i) os <<
space <<
"* " << e[i];
2351 os <<
"(" << push << e[1] <<
space <<
"^ " << e[0] << push <<
")";
2354 os <<
"(" << push << e[0] <<
space <<
"/ " << e[1] << push <<
")";
2357 if (
isInt(e[0].getType()) ||
isInt(e[1].getType())) {
2359 os <<
"(" << push << e[0] <<
space <<
"< " << e[1] << push <<
")";
2362 os <<
"(" << push << e[0] <<
space <<
"<= " << e[1] << push <<
")";
2365 os <<
"(" << push << e[0] <<
space <<
"> " << e[1] << push <<
")";
2368 os <<
"(" << push << e[0] <<
space <<
">= " << e[1] << push <<
")";
2371 os <<
"DARK_SHADOW(" << push << e[0] <<
", " <<
space << e[1] << push <<
")";
2374 os <<
"GRAY_SHADOW(" << push << e[0] <<
"," <<
space << e[1]
2375 <<
"," <<
space << e[2] <<
"," <<
space << e[3] << push <<
")";
2401 throw SmtlibException(
"TheoryArithNew::print: SMTLIB: SUBRANGE not implemented");
2409 os <<
"(" <<
push <<
"IsInt" <<
space << e[0] <<
push <<
")";
2411 throw SmtlibException(
"TheoryArithNew::print: SMTLIB: IS_INTEGER used unexpectedly");
2417 os <<
"(" <<
push <<
"+";
2419 for(; i!=iend; ++i) {
2420 os <<
space << (*i);
2427 os <<
"(" <<
push <<
"- " << e[0] <<
space << e[1] <<
push <<
")";
2435 int i=0, iend=e.
arity();
2439 for(; i!=iend; ++i) {
2441 os <<
"(" <<
push <<
"*";
2443 os <<
space << e[i];
2445 for (i=0; i < iend-1; ++i) os <<
push <<
")";
2450 throw SmtlibException(
"TheoryArithNew::print: SMTLIB: POW not supported");
2454 throw SmtlibException(
"TheoryArithNew::print: SMTLIB: unexpected use of DIVIDE");
2460 os << e[0] << space << e[1] <<
push <<
")";
2466 os << e[0] << space << e[1] <<
push <<
")";
2472 os << e[0] << space << e[1] <<
push <<
")";
2478 os << e[0] << space << e[1] <<
push <<
")";
2482 throw SmtlibException(
"TheoryArithNew::print: SMTLIB: DARK_SHADOW not supported");
2483 os <<
"(" <<
push <<
"DARK_SHADOW" <<
space << e[0]
2487 throw SmtlibException(
"TheoryArithNew::print: SMTLIB: GRAY_SHADOW not supported");
2488 os <<
"GRAY_SHADOW(" << push << e[0] <<
"," <<
space << e[1]
2489 <<
"," <<
space << e[2] <<
"," <<
space << e[3] << push <<
")";
2492 throw SmtlibException(
"TheoryArithNew::print: SMTLIB: default not supported");
2513 os <<
"(" <<
push <<
"SUBRANGE" <<
space << e[0]
2518 os <<
"(" << push <<
"IS_INTEGER" <<
space << e[0] << push <<
")";
2523 int i=0, iend=e.
arity();
2524 os <<
"(" << push <<
"+";
2525 for(; i!=iend; ++i) os <<
space << e[i];
2531 os <<
"(" << push <<
"- " << e[0] <<
space << e[1] << push <<
")";
2534 os <<
"(" << push <<
"-" <<
space << e[0] << push <<
")";
2537 int i=0, iend=e.
arity();
2538 os <<
"(" << push <<
"*";
2539 for(; i!=iend; ++i) os <<
space << e[i];
2544 os <<
"(" << push <<
"^ " << e[1] <<
space << e[0] << push <<
")";
2547 os <<
"(" << push <<
"/ " << e[0] <<
space << e[1] << push <<
")";
2550 os <<
"(" << push <<
"< " << e[0] <<
space << e[1] << push <<
")";
2553 os <<
"(" << push <<
"<= " << e[0] <<
space << e[1] << push <<
")";
2556 os <<
"(" << push <<
"> " << e[1] <<
space << e[0] << push <<
")";
2559 os <<
"(" << push <<
">= " << e[0] <<
space << e[1] << push <<
")";
2562 os <<
"(" << push <<
"DARK_SHADOW" <<
space << e[0]
2563 <<
space << e[1] << push <<
")";
2566 os <<
"(" << push <<
"GRAY_SHADOW" <<
space << e[0] <<
space
2567 << e[1] <<
space << e[2] <<
space << e[3] << push <<
")";
2607 Theorem x_r_Theorem = (*it).second;
2644 const set<Expr>& dependent = (*find).second;
2645 set<Expr>::const_iterator it = dependent.begin();
2646 set<Expr>::const_iterator it_end = dependent.end();
2648 while (it != it_end) {
2651 const Expr& x_j = *it;
2707 set<Expr>::const_iterator it = dependent.begin();
2708 set<Expr>::const_iterator it_end = dependent.end();
2710 while (it != it_end) {
2713 const Expr& x_k = *it;
2746 DebugAssert(
isLeaf(x_i),
"TheoryArithNew::assertUpper wrong kind, expected an arithmetic leaf (variable) got " + x_i.
toString());
2780 DebugAssert(
isLeaf(x_i),
"TheoryArithNew::assertLower wrong kind, expected an arithmetic leaf (variable) got " + x_i.
toString());
2836 TRACE(
"simplex",
"TheoryArithNew::checkSat(fullEffort=",fullEffort?
"true" :
"false",
")");
2871 TRACE(
"simplex",
"TheoryArithNew::checkSatInteger()",
"",
"");
2885 while (x_i_it != x_i_it_end) {
2888 const Expr& x_i = (*x_i_it);
2897 if (beta.
isInteger()) { ++ x_i_it;
continue; }
2943 if (l_i > x_i_Value) {
2949 const Expr& x_i_RightSide = (*it).second.getExpr()[1];
2950 int non_basics_i_end = x_i_RightSide.
arity();
2951 for(
int non_basics_i = 0; non_basics_i < non_basics_i_end; ++ non_basics_i) {
2954 x_j = x_i_RightSide[non_basics_i][1];
2955 a_ij = x_i_RightSide[non_basics_i][0].
getRational();
2984 if (x_i_Value > u_i) {
2990 const Expr& x_i_RightSide = (*it).second.getExpr()[1];
2991 int non_basics_i_end = x_i_RightSide.
arity();
2992 for(
int non_basics_i = 0; non_basics_i < non_basics_i_end; ++ non_basics_i) {
2995 x_j = x_i_RightSide[non_basics_i][1];
2996 a_ij = x_i_RightSide[non_basics_i][0].
getRational();
3029 TRACE(
"simplex",
"TheoryArithNew::checkSatSimplex ==> new bounds : \n",
boundsAsString(),
"");
3030 TRACE(
"simplex",
"TheoryArithNew::checkSatSimplex ==> unsat : \n",
unsatAsString(),
"");
3046 static Rational zeroCoefficient(0);
3055 while (left <= right) {
3058 i = (left +
right ) / 2;
3061 const Expr& mult = expr[i];
3067 int cmp =
compare(mult[1], var);
3078 return zeroCoefficient;
3087 else return (*find).second.bound;
3095 else return (*find).second.bound;
3104 return (*find).second.theorem;
3113 return (*find).second.theorem;
3134 return (*find).second;
3144 TRACE(
"simplex",
"TheoryArithNew::assertFact(", expr,
")");
3154 const Expr& leftSide = expr[0];
3155 const Expr& rightSide = expr[1];
3177 if (!
isPlus(rightSide)) {
3180 DebugAssert(rightSide[0].
isRational() && rightSide[0].getRational() == 1,
"TheoryArithNew::assertFact, left side should be multiplication by one");
3196 var = introductionThm.
getExpr()[0];
3204 int i_end = rightSide.
arity();
3205 for(
int i = 0; i < i_end; ++ i)
3208 int i_end = rightSide.
arity();
3209 for(
int i = 0; i < i_end; ++ i)
3253 FatalAssert(
false,
"Theory_Arith::assertFact, control should not reach here");
3320 return (*find).second;
3329 int i_end = e.
arity();
3330 for (
int i = 0; i < i_end; ++ i)
3334 beta[var] = varValue;
3355 str = str + ((*row).second).getExpr().toString() +
"\n";
3375 while (it != it_end) {
3377 str = str + (*it).toString() +
" ";
3394 set<Expr> all_variables;
3399 for(; it != it_end; it ++) {
3402 all_variables.insert((*it).first);
3405 const Expr& rightSide = (*it).second.getExpr()[1];
3406 int term_i_end = rightSide.
arity();
3407 for(
int term_i = 0; term_i < term_i_end; ++ term_i)
3408 all_variables.insert(rightSide[term_i][1]);
3414 all_variables.insert((*bounds_it).first);
3416 all_variables.insert((*bounds_it).first);
3419 set<Expr>::iterator var_it = all_variables.begin();
3420 set<Expr>::iterator var_it_end = all_variables.end();
3423 while (var_it != var_it_end) {
3426 const Expr& var = *var_it;
3459 const Expr& rightSide = eqExpr[1];
3465 if(thm.
getRHS() == rightSide)
return eq;
3474 vector<Theorem> thms;
3475 vector<unsigned> changed;
3478 TRACE(
"simplex",
"TheoryArithNew::substAndCanonizeModTableaux(", sum,
")");
3484 int term_index_end = sum.
arity();
3485 for(
int term_index = 0; term_index < term_index_end; ++ term_index) {
3487 const Expr& term = sum[term_index];
3488 const Expr& var = term[1];
3500 DebugAssert(termTheorem.
getExpr() != term,
"substAndCanonizeModTableaux: got the same term in substitution");
3503 thms.push_back(termTheorem);
3506 changed.push_back(term_index);
3511 if(thms.size() > 0) {
3529 TRACE(
"simplex",
"TheoryArithNew::substAndCanonizeTableaux(", eq.
getExpr(),
")");
3535 DebugAssert(eqExpr.getKind() ==
EQ,
"TheoryArithNew::substAndCanonize, expected equality " + eqExpr.toString());
3538 const Expr& var = eqExpr[0];
3545 set<Expr>& dependent = (*find).second;
3546 set<Expr>::iterator it = dependent.begin();
3547 set<Expr>::iterator it_end = dependent.end();
3548 for(; it != it_end; ++ it) {
3551 const Expr& leftSide = *it;
3553 const Expr& rowExpr = (*row).second.getExpr();
3554 const Expr& rowRightSide = rowExpr[1];
3560 while (left <= right) {
3563 term_i = (left +
right) / 2;
3566 int cmp =
compare(rowRightSide[term_i][1], var);
3579 const Expr& newRowRightSide = result.
getRHS()[1];
3584 (*row).second =
iffMP((*row).second, result);
3606 const Expr& right_side = eqExpr[1];
3607 const Expr& left_side = eqExpr[0];
3616 DebugAssert(
isLeaf(left_side),
"TheoryArithNew::pivotRule, expected a leaf (variable) on the right-hand side : " + eqExpr.
toString());
3619 int term_i_end = right_side.
arity();
3620 for(
int term_i = 0; term_i < term_i_end; ++ term_i)
3622 if (right_side[term_i][1] == var) {
3625 const Expr& termExpr = right_side[term_i];
3626 const Expr& termVar = termExpr[1];
3649 TRACE(
"simplex",
"TheoryArithNew::pivotRule ==> ", result.getExpr().toString(),
"");
3664 vector<Theorem> upperBounds;
3667 Theorem tableauxTheorem = (*var_it).second;
3670 const Expr& var = (*var_it).first;
3673 const Expr& rightSide = tableauxTheorem.
getExpr()[1];
3676 int leftSide_i_end = rightSide.
arity();
3677 for(
int leftSide_i = 0; leftSide_i < leftSide_i_end; ++ leftSide_i) {
3680 const Expr& a = rightSide[leftSide_i][0];
3683 const Expr& x = rightSide[leftSide_i][1];
3701 upperBounds.push_back(thm);
3719 upperBounds.push_back(thm);
3724 Theorem sumInequalities = upperBounds[0];
3725 for(
unsigned int i = 1; i < upperBounds.size(); i ++) {
3740 varUpperBound =
iffMP(sumInequalities, varUpperBound);
3751 vector<Theorem> lowerBounds;
3754 Theorem tableauxTheorem = (*var_it).second;
3757 const Expr& var = (*var_it).first;
3760 const Expr& rightSide = tableauxTheorem.
getExpr()[1];
3763 TRACE(
"explanations",
"Generating explanation for the tableaux row ", tableauxTheorem.
getExpr(),
"");
3766 int rightSide_i_end = rightSide.
arity();
3767 for(
int rightSide_i = 0; rightSide_i < rightSide_i_end; ++ rightSide_i) {
3770 const Expr& a = rightSide[rightSide_i][0];
3773 const Expr& x = rightSide[rightSide_i][1];
3783 TRACE(
"explanations",
"Got ", thm.getExpr(),
"");
3791 TRACE(
"explanations",
"Got ", thm.getExpr(),
"");
3794 lowerBounds.push_back(thm);
3804 TRACE(
"explanations",
"Got ", thm.getExpr(),
"");
3812 TRACE(
"explanations",
"Got ", thm.getExpr(),
"");
3815 lowerBounds.push_back(thm);
3820 Theorem sumInequalities = lowerBounds[0];
3821 for(
unsigned int i = 1; i < lowerBounds.size(); i ++) {
3825 TRACE(
"explanations",
"Got sum ", sumInequalities.
getExpr(),
"");
3836 TRACE(
"explanations",
"Got sum ", sumInequalities.
getExpr(),
"");
3842 varLowerBound =
iffMP(sumInequalities, varLowerBound);
3845 TRACE(
"explanations",
"Got lower bound ", varLowerBound.getExpr(),
"");
3851 TRACE(
"explanations",
"Got upper bound ", varUpperBound.getExpr(),
"");
3853 TRACE(
"explanations",
"The var value (", var,
")" +
getBeta(var).toString());
3881 for(; term != term_end; term ++)
3894 for(; term != term_end; term ++)
3905 int oldSum_i = 0, newSum_i = 0;
3906 int oldSum_end = oldSum.
arity(), newSum_end = newSum.
arity();
3908 while (oldSum_i < oldSum_end && newSum_i < newSum_end) {
3911 const Expr oldVar = oldSum[oldSum_i][1];
3915 if (oldVar == newVar) {
3916 ++ oldSum_i; ++ newSum_i;
continue;
3920 if (oldVar > newVar) {
3922 if (oldVar != skipVar)
3928 if (newVar != skipVar)
3936 while (oldSum_i < oldSum_end) {
3938 const Expr& var = oldSum[oldSum_i ++][1];
3944 while (newSum_i < newSum_end) {
3946 const Expr& var = newSum[newSum_i ++][1];
3956 TRACE(
"propagate_arith",
"registerAtom(", e.
toString(),
")");
3961 Expr rightSide = e[1];
3984 FatalAssert(
false,
"TheoryArithNew::registerAtom: control should not reach here" + e.
toString());
4009 Expr rightSide = assertExpr[1];
4012 int kind = assertExpr.
getKind();
4015 DebugAssert(kind ==
LT || kind ==
LE || kind ==
GT || kind ==
GE ,
"TheoryArithNew::propagateTheory : expected an inequality");
4018 if (kind ==
LT || kind ==
LE) {
4020 BoundInfoSet::iterator
find =
allBounds.lower_bound(boundInfo);
4024 if (find == find_end)
return;
4027 while (find != find_end) {
4039 int findExprKind = findExpr.
getKind();
4042 if (rightSide != findExpr[1])
break;
4048 if (findExprKind ==
LT || findExprKind ==
LE)
4056 TRACE(
"propagate_arith",
"lemma ==>", lemma.
toString(),
"");
4066 BoundInfoSet::iterator
find =
allBounds.upper_bound(boundInfo);
4070 while (find != find_end) {
4077 int findExprKind = findExpr.
getKind();
4080 if (rightSide != findExpr[1])
break;
4086 if (findExprKind ==
GT || findExprKind ==
GE)
4093 TRACE(
"propagate_arith",
"lemma ==>", lemma.
toString(),
"");
4117 Rational f_0 = x_i_Value - floor(x_i_Value);