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;
93 const Rational& TheoryArith3::freeConstIneq(
const Expr& ineq,
bool varOnRHS) {
95 const Expr& e = varOnRHS? ineq[0] : ineq[1];
99 return e[0].getRational();
101 return e.getRational();
111 TheoryArith3::updateSubsumptionDB(
const Expr& ineq,
bool varOnRHS,
113 TRACE(
"arith ineq",
"TheoryArith3::updateSubsumptionDB(", ineq,
114 ", var isolated on "+
string(varOnRHS?
"RHS" :
"LHS")+
")");
119 const Expr& t = varOnRHS? ineq[0] : ineq[1];
120 bool strict(
isLT(ineq));
132 for(++i; i!=iend; ++i) kids.push_back(*i);
138 index =
leExpr(newT, ineq[1]);
140 index =
leExpr(ineq[0], newT);
144 index =
leExpr(rat(0), ineq[1]);
146 index =
leExpr(ineq[0], rat(0));
147 }
else if(
isLT(ineq))
148 index =
leExpr(ineq[0], ineq[1]);
153 iend=d_freeConstDB.end();
159 TRACE(
"arith ineq",
"freeConstDB["+index.toString()+
"] := ", obj,
"");
173 TRACE(
"arith ineq",
"freeConstDB["+index.toString()+
"] := ", obj,
"");
180 bool TheoryArith3::kidsCanonical(
const Expr& e) {
181 if(isLeaf(e))
return true;
183 for(
int i=0; res && i<e.
arity(); ++i) {
184 Expr simp(canon(e[i]).getRHS());
185 res = (e[i] == simp);
186 IF_DEBUG(
if(!res) debugger.getOS() <<
"\ne[" << i <<
"] = " << e[i]
187 <<
"\nsimplified = " << simp <<
endl;)
214 TRACE(
"arith canon",
"canon(",e,
") {");
219 Theorem thm = d_rules->uMinusToMult(e[0]);
221 result = transitivityRule(thm, canon(e2));
231 result = d_rules->canonPlus(e);
235 Theorem minus_eq_sum = d_rules->minusToPlus(e[0], e[1]);
237 Expr sum(minus_eq_sum.getRHS());
239 if(thm.getLHS() == thm.getRHS())
240 result = canonThm(minus_eq_sum);
243 vector<unsigned> changed;
244 vector<Theorem> thms;
245 changed.push_back(1);
247 Theorem sum_eq_canon = canonThm(substitutivityRule(sum, changed, thms));
248 result = transitivityRule(minus_eq_sum, sum_eq_canon);
254 result = d_rules->canonMult(e);
339 if (e[1].getKind() ==
PLUS)
341 result = d_rules->canonDivide(e);
346 result = d_rules->canonPowConst(e);
348 result = reflexivityRule(e);
351 result = reflexivityRule(e);
354 TRACE(
"arith canon",
"canon => ",result,
" }");
360 TheoryArith3::canonSimplify(
const Expr& e) {
361 TRACE(
"arith",
"canonSimplify(", e,
") {");
363 "TheoryArith3::canonSimplify("+e.
toString()+
")");
364 DebugAssert(leavesAreSimp(e),
"Expected leaves to be simplified");
368 thm = transitivityRule(thm, find(thm.
getRHS()));
373 +
"\nsimplify(canon(e)) = "+simplifyExpr(thm.
getRHS()).toString());
382 TRACE(
"arith",
"canonSimplify =>", thm,
" }");
391 vector<Theorem> thms;
393 "TheoryArith3::canonPred: bad theorem: "+thm.
toString());
395 thms.push_back(canonSimplify(e[0]));
396 thms.push_back(canonSimplify(e[1]));
397 return iffMP(thm, substitutivityRule(e.
getOp(), thms));
404 TheoryArith3::canonPredEquiv(
const Theorem& thm) {
405 vector<Theorem> thms;
407 "TheoryArith3::canonPredEquiv: bad theorem: "+thm.
toString());
409 thms.push_back(canonSimplify(e[0]));
410 thms.push_back(canonSimplify(e[1]));
411 return transitivityRule(thm, substitutivityRule(e.
getOp(), thms));
419 TheoryArith3::canonConjunctionEquiv(
const Theorem& thm) {
420 vector<Theorem> thms;
435 TRACE(
"arith eq",
"doSolve(",e,
") {");
438 vector<Theorem> thms;
443 eqnThm = iffMP(thm, d_rules->rightMinusLeft(e));
444 eqnThm = canonPred(eqnThm);
451 Theorem result = iffMP(eqnThm, d_rules->constPredicate(eqnThm.getExpr()));
452 TRACE(
"arith eq",
"doSolve => ",result,
" }");
457 eqnThm = iffMP(eqnThm, normalize(eqnThm.getExpr()));
458 right = eqnThm.getRHS();
468 if (r == 0)
return getCommonRules()->trueTheorem();
470 enqueueFact(iffMP(eqnThm, d_rules->multEqZero(eqnThm.getExpr())));
471 return getCommonRules()->trueTheorem();
474 d_rules->multEqn(eqnThm.getLHS(),
476 res = canonPred(res);
480 enqueueFact(iffMP(eqnThm, d_rules->multEqZero(eqnThm.getExpr())));
481 return getCommonRules()->trueTheorem();
484 else if (
isPow(right)) {
487 return doSolve(iffMP(eqnThm, d_rules->powEqZero(eqnThm.getExpr())));
489 throw ArithException(
"Can't solve exponential eqn: "+eqnThm.toString());
492 if(!isInteger(right)) {
493 return processRealEq(eqnThm);
496 return processIntEq(eqnThm);
506 if (right[0].getRational() == 0) {
510 set<Expr>::iterator is, isend;
511 getFactors(*i, factors);
512 for (++i; i != iend; ++i) {
514 getFactors(*i, factors2);
515 for (is = factors.begin(), isend = factors.end(); is != isend; ++is) {
516 if (factors2.find(*is) == factors2.end()) {
520 if (factors.empty())
break;
522 if (!factors.empty()) {
523 enqueueFact(iffMP(eqnThm, d_rules->divideEqnNonConst(rat(0), right, *(factors.begin()))));
524 return getCommonRules()->trueTheorem();
529 Expr isolated = right[1];
534 isolated = canon(isolated / rat(coeff)).getRHS();
536 res = iffMP(eqnThm, d_rules->multEqn(rat(0), right, rat(-1/coeff)));
537 res = canonPred(res);
538 res = iffMP(res, d_rules->plusPredicate(res.getLHS(), res.getRHS(),
540 res = canonPred(res);
543 if (
isPow(res.getLHS())) {
545 if (isInteger(left[0])) {
548 right = res.getRHS();
549 if (
isPow(right) && right[0] == left[0]) {
550 enqueueFact(iffMP(res, d_rules->elimPower(res.getExpr())));
551 return getCommonRules()->trueTheorem();
555 if (pow % 2 == 0 && r < 0) {
556 return iffMP(res, d_rules->evenPowerEqNegConst(res.getExpr()));
561 enqueueFact(iffMP(res, d_rules->elimPowerConst(res.getExpr(), root)));
562 return getCommonRules()->trueTheorem();
564 else if (
isInt(left[1].getType())) {
567 return iffMP(res, d_rules->intEqIrrational(res.getExpr(),
isIntx));
575 res = symmetryRule(eqnThm);
577 TRACE(
"arith eq",
"doSolve: failed to solve an equation: ", e,
"");
578 IF_DEBUG(debugger.counter(
"FAILED to solve equalities")++;)
579 setIncomplete(
"Non-linear arithmetic equalities");
590 bool TheoryArith3::pickIntEqMonomial(
const Expr&
right,
Expr& isolated,
bool& nonlin)
593 "TheoryArith3::pickIntEqMonomial right is wrong :-): " +
596 "TheoryArith3::pickIntEqMonomial. right[0] must be const" +
599 "TheoryArith3::pickIntEqMonomial: right is of type int: " +
610 for(; i != iend; ++i) {
615 else if (
isMult(*i) && (*i).arity() == 2 && (*i)[0].isRational() && isLeaf((*i)[1])) {
617 coeff =
abs((*i)[0].getRational());
623 for (j = istart; j != iend; ++j) {
624 if (j != i && isLeafIn(leaf, *j))
break;
627 if (!found || min > coeff) {
642 TheoryArith3::processRealEq(
const Theorem& eqn)
646 "processRealEq invariant violated");
662 for(
int i = right.arity()-1; i>=0; --i) {
670 Expr leaf = isLeaf(c) ? c : c[1];
671 for (
int j = 0; j < right.arity(); ++j) {
673 && isLeafIn(leaf, right[j])
688 else if ((
isMult(right) && right.arity() == 2 && isLeaf(right[1])) ||
708 "TheoryArith3::ProcessRealEq: left is integer:\n left = "
714 result = canonPred(result);
717 result = iffMP(result, d_rules->plusPredicate(result.getLHS(),
718 result.getRHS(),
left,
EQ));
719 result = canonPred(result);
720 TRACE(
"arith",
"processRealEq => ",result,
" }");
725 void TheoryArith3::getFactors(
const Expr& e, set<Expr>& factors)
731 for (; i != iend; ++i) {
732 getFactors(*i, factors);
741 if (isLeaf(e[1])) factors.insert(e[1]);
746 DebugAssert(factors.find(e) == factors.end(),
"expected new entry");
759 TheoryArith3::processSimpleIntEq(
const Theorem& eqn)
761 TRACE(
"arith eq",
"processSimpleIntEq(", eqn.
getExpr(),
") {");
763 "TheoryArith3::processSimpleIntEq: eqn must be equality" +
769 "TheoryArith3::processSimpleIntEq: LHS must be 0:\n" +
774 if (2 == right.arity() &&
776 (
isMult(right[1]) && right[1].arity() == 2 && right[1][0].isRational() && isLeaf(right[1][1])))) {
779 separateMonomial(right[1], c, x);
784 TRACE(
"arith eq",
"processSimpleIntEq[0 = c + a*x] => ", res,
" }");
790 if (pickIntEqMonomial(right, isolated, nonlin)) {
791 TRACE(
"arith eq",
"processSimpleIntEq: isolated = ", isolated,
"");
803 result = iffMP(eqn, d_rules->multEqn(eqn.
getLHS(),
right, rat(r)));
804 result = canonPred(result);
808 result = iffMP(result,
815 isolated = (a == 1)? isolated[1] : rat(a) * isolated[1];
818 result = iffMP(eqn, d_rules->plusPredicate(eqn.
getLHS(),
822 result = canonPred(result);
825 if(!
isMult(isolated) || isolated[0].getRational() == 1) {
826 TRACE(
"arith eq",
"processSimpleIntEq[x = rhs] => ", result,
" }");
828 }
else if (!nonlin) {
830 "TheoryArith3::processSimpleIntEq: isolated must be mult "
831 "with coeff >= 2.\n isolated = " + isolated.
toString());
837 separateMonomial(lhs, a, x);
838 Theorem isIntLHS = isIntegerThm(x);
839 vector<Theorem> isIntRHS;
842 separateMonomial(rhs, c, v);
843 isIntRHS.push_back(isIntegerThm(v));
850 for(; i!=iend; ++i) {
852 separateMonomial(*i, c, v);
853 isIntRHS.push_back(isIntegerThm(v));
858 result = d_rules->eqElimIntRule(result, isIntLHS, isIntRHS);
860 result = getCommonRules()->skolemize(result);
864 Theorem thm1 = canonPred(getCommonRules()->andElim(result, 0));
865 Theorem thm2 = canonPred(getCommonRules()->andElim(result, 1));
866 Theorem newRes = getCommonRules()->andIntro(thm1, thm2);
869 TRACE(
"arith eq",
"processSimpleIntEq => ", result,
" }");
877 Theorem result = symmetryRule(eqn);
878 TRACE(
"arith eq",
"processSimpleIntEq[x = 0] => ", result,
" }");
889 TheoryArith3::processIntEq(
const Theorem& eqn)
891 TRACE(
"arith eq",
"processIntEq(", eqn.
getExpr(),
") {");
893 std::vector<Theorem> solvedAndNewEqs;
897 result = processSimpleIntEq(newEq);
900 solvedAndNewEqs.push_back(result);
910 solvedAndNewEqs.push_back(getCommonRules()->andElim(result, 0));
911 newEq = getCommonRules()->andElim(result, 1);
916 else if (solvedAndNewEqs.size() > 0)
917 res = solvedForm(solvedAndNewEqs);
919 TRACE(
"arith eq",
"processIntEq => ", res.
getExpr(),
" }");
932 TheoryArith3::solvedForm(
const vector<Theorem>& solvedEqs)
934 DebugAssert(solvedEqs.size() > 0,
"TheoryArith3::solvedForm()");
937 TRACE_MSG(
"arith eq",
"TheoryArith3::solvedForm:solvedEqs(\n [");
938 IF_DEBUG(
if(debugger.trace(
"arith eq")) {
939 for(vector<Theorem>::const_iterator j = solvedEqs.begin(),
940 jend=solvedEqs.end(); j!=jend;++j)
941 TRACE(
"arith eq",
"", j->getExpr(),
",\n ");
946 vector<Theorem>::const_reverse_iterator
947 i = solvedEqs.rbegin(),
948 iend = solvedEqs.rend();
952 for(; i!=iend; ++i) {
954 Theorem thm = substAndCanonize(*i, subst);
955 TRACE(
"arith eq",
"solvedForm: subst["+i->getLHS().toString()+
"] = ",
957 subst[i->getLHS()] = thm;
962 "TheoryArith3::solvedForm: an element of solvedEqs must "
963 "be either EQ or FALSE: "+i->toString());
969 vector<Theorem> thms;
972 thms.push_back(i->second);
974 return getCommonRules()->andIntro(thms);
989 TRACE(
"arith eq",
"substAndCanonize(", t,
") {");
992 Theorem res(reflexivityRule(t));
993 TRACE(
"arith eq",
"substAndCanonize[subst empty] => ", res,
" }");
999 TRACE(
"arith eq",
"substAndCanonize[subst] => ", i->second,
" }");
1004 Theorem res(reflexivityRule(t));
1005 TRACE(
"arith eq",
"substAndCanonize[i-leaf] => ", res,
" }");
1009 vector<Theorem> thms;
1010 vector<unsigned> changed;
1011 for(
unsigned j=0, jend=t.
arity(); j!=jend; ++j) {
1012 Theorem thm = substAndCanonize(t[j], subst);
1013 if(thm.
getRHS() != t[j]) {
1014 thm = canonThm(thm);
1015 thms.push_back(thm);
1016 changed.push_back(j);
1021 if(thms.size() > 0) {
1022 res = substitutivityRule(t, changed, thms);
1023 res = canonThm(res);
1026 res = reflexivityRule(t);
1027 TRACE(
"arith eq",
"substAndCanonize => ", res,
" }");
1041 if(subst.
empty())
return eq;
1047 Theorem thm = substAndCanonize(t, subst);
1049 if(thm.
getRHS() == t)
return eq;
1051 vector<Theorem> thms;
1052 vector<unsigned> changed;
1053 thms.push_back(thm);
1054 changed.push_back(1);
1055 return iffMP(eq, substitutivityRule(eq.
getExpr(), changed, thms));
1059 void TheoryArith3::processBuffer()
1064 for(; !inconsistent() && d_bufferIdx < d_buffer.size();
1065 d_bufferIdx = d_bufferIdx+1) {
1066 const Theorem& ineqThm = d_buffer[d_bufferIdx];
1068 if(isStale(ineqThm.
getExpr()))
continue;
1069 Theorem thm1 = isolateVariable(ineqThm, varOnRHS);
1071 if((ineq).isFalse())
1072 setInconsistent(thm1);
1073 else if(!ineq.
isTrue()) {
1076 "TheoryArith3::processBuffer(): bad result from "
1077 "isolateVariable:\nineq = "+ineq.
toString());
1079 projectInequalities(thm1, varOnRHS);
1087 TRACE(
"arith ineq",
"updateStats("+c.
toString()+
", ", v,
")");
1093 if (maxFind == maxCoefficientLeft.end())
1094 maxCoefficientLeft[v] = - c;
1096 if ((*maxFind).second < -c)
1097 (*maxFind).second = -c;
1101 if (maxFind == maxCoefficientRight.end())
1102 maxCoefficientRight[v] = c;
1104 if((*maxFind).second < c)
1105 (*maxFind).second = c;
1109 if(d_countRight.count(v) > 0) d_countRight[v] = d_countRight[v] + 1;
1110 else d_countRight[v] = 1;
1113 if(d_countLeft.count(v) > 0) d_countLeft[v] = d_countLeft[v] + 1;
1114 else d_countLeft[v] = 1;
1118 void TheoryArith3::updateStats(
const Expr& monomial)
1121 separateMonomial(monomial, c, m);
1126 void TheoryArith3::addToBuffer(
const Theorem& thm) {
1132 if(!(e[0].
isRational() && e[0].getRational() == 0)) {
1133 result = iffMP(result, d_rules->rightMinusLeft(e));
1134 result = canonPred(result);
1136 TRACE(
"arith ineq",
"addToBuffer(", result.
getExpr(),
")");
1138 d_buffer.push_back(thm);
1151 bool& isolatedVarOnRHS)
1155 TRACE(
"arith",
"isolateVariable(",e,
") {");
1156 TRACE(
"arith ineq",
"isolateVariable(", e,
") {");
1159 "TheoryArith3::isolateVariable: " + e.
toString() +
1163 "TheoryArith3::isolateVariable: theorem must be of "
1164 "the form 0 < rhs: " + inputThm.
toString());
1166 const Expr& zero = e[0];
1170 result = iffMP(result, d_rules->constPredicate(e));
1171 TRACE(
"arith ineq",
"isolateVariable => ",result.
getExpr(),
" }");
1172 TRACE(
"arith",
"isolateVariable => ",result,
" }");
1179 Expr factor(computeNormalFactor(right));
1180 TRACE(
"arith",
"isolateVariable: factor = ", factor,
"");
1182 "isolateVariable: factor="+factor.
toString());
1185 result = iffMP(result, d_rules->multIneqn(e, factor));
1187 result = canonPred(result);
1188 right = result.getExpr()[1];
1195 isolatedMonomial = pickMonomial(right);
1198 isolatedVarOnRHS =
true;
1199 if (
isMult(isolatedMonomial)) {
1200 r = ((isolatedMonomial[0].
getRational()) >= 0)? -1 : 1;
1202 ((isolatedMonomial[0].
getRational()) >= 0)?
true :
false;
1204 isolatedMonomial = canon(rat(-1)*isolatedMonomial).getRHS();
1206 result = iffMP(result, d_rules->plusPredicate(zero, right,
1207 isolatedMonomial, kind));
1209 result = canonPred(result);
1211 result = iffMP(result, d_rules->multIneqn(result.getExpr(), rat(r)));
1212 result = canonPred(result);
1214 TRACE(
"arith ineq",
"isolateVariable => ",result.getExpr(),
" }");
1215 TRACE(
"arith",
"isolateVariable => ",result,
" }");
1225 vector<Rational> nums, denoms;
1226 for(
int i=0, iend=right.
arity(); i<iend; ++i) {
1227 switch(right[i].getKind()) {
1242 denoms.push_back(1);
1251 factor = (gcd_nums==0)? 0 : (lcm(denoms) / gcd_nums);
1252 }
else if(
isMult(right)) {
1254 factor = (r==0)? 0 : (1/
abs(r));
1262 bool TheoryArith3::lessThanVar(
const Expr& isolatedMonomial,
const Expr& var2)
1265 "TheoryArith3::findMaxVar: isolatedMonomial cannot be rational" +
1268 separateMonomial(isolatedMonomial, c, var0);
1269 separateMonomial(var2, c, var1);
1278 bool TheoryArith3::isStale(
const Expr& e) {
1280 return e != find(e).getRHS();
1285 stale = isStale(*i);
1291 TRACE(
"arith ineq",
"isStale(", ineq,
") {");
1294 bool strict(
isLT(ineqExpr));
1310 TRACE(
"arith ineq",
"isStale[subsumed] => ", res?
"true" :
"false",
" }");
1313 res = isStale(ineqExpr);
1314 TRACE(
"arith ineq",
"isStale[updated] => ", res?
"true" :
"false",
" }");
1321 TRACE(
"separateMonomial",
"separateMonomial(", e,
")");
1323 "TheoryArith3::separateMonomial(e = "+e.
toString()+
")");
1326 "TheoryArith3::separateMonomial(e = "+e.
toString()+
")");
1328 if(e.
arity() == 2) var = e[1];
1330 vector<Expr> kids = e.
getKids();
1341 "TheoryArith3::separateMonomial(e = "
1346 void TheoryArith3::projectInequalities(
const Theorem& theInequality,
1347 bool isolatedVarOnRHS)
1349 TRACE(
"arith ineq",
"projectInequalities(", theInequality.
getExpr(),
1350 ", isolatedVarOnRHS="+string(isolatedVarOnRHS?
"true" :
"false")
1354 "TheoryArith3::projectIsolatedVar: "\
1355 "theInequality is of the wrong form: " +
1359 Theorem theIneqThm(theInequality);
1360 Expr theIneq = theIneqThm.getExpr();
1362 Theorem isIntLHS(isIntegerThm(theIneq[0]));
1363 Theorem isIntRHS(isIntegerThm(theIneq[1]));
1367 Theorem thm = d_rules->lessThanToLE(theInequality, isIntLHS, isIntRHS,
1369 theIneqThm = canonPred(iffMP(theIneqThm, thm));
1370 theIneq = theIneqThm.getExpr();
1372 Expr isolatedMonomial =
1373 isolatedVarOnRHS ? theIneq[1] : theIneq[0];
1375 Expr monomialVar, a;
1376 separateMonomial(isolatedMonomial, a, monomialVar);
1380 updateSubsumptionDB(theIneq, isolatedVarOnRHS, subsumed);
1383 IF_DEBUG(debugger.counter(
"subsumed inequalities")++;)
1384 TRACE(
"arith ineq",
"subsumed inequality: ", theIneq,
"");
1389 setIncomplete(
"Non-linear arithmetic inequalities");
1395 theoryCore()->setupTerm(theIneq[0],
this, theIneqThm);
1396 theoryCore()->setupTerm(theIneq[1],
this, theIneqThm);
1399 isolatedVarOnRHS ? d_inequalitiesRightDB : d_inequalitiesLeftDB;
1401 if(it1 == db1.
end()) {
1403 list->
push_back(
Ineq(theIneqThm, isolatedVarOnRHS, bestConst));
1404 db1[monomialVar] = list;
1407 ((*it1).second)->
push_back(
Ineq(theIneqThm, isolatedVarOnRHS, bestConst));
1410 isolatedVarOnRHS ? d_inequalitiesLeftDB : d_inequalitiesRightDB;
1412 if(it == db2.
end()) {
1413 TRACE_MSG(
"arith ineq",
"projectInequalities[not in DB] => }");
1418 Theorem betaLTt, tLTalpha, thm;
1419 for(
size_t i = 0, iend=listOfDBIneqs.
size(); i!=iend; ++i) {
1420 const Ineq& ineqEntry = listOfDBIneqs[i];
1422 if(!isStale(ineqEntry)) {
1423 betaLTt = isolatedVarOnRHS ? theIneqThm : ineqThm;
1424 tLTalpha = isolatedVarOnRHS ? ineqThm : theIneqThm;
1425 thm = normalizeProjectIneqs(betaLTt, tLTalpha);
1427 IF_DEBUG(debugger.counter(
"real shadows")++;)
1431 setInconsistent(thm);
1432 TRACE_MSG(
"arith ineq",
"projectInequalities[inconsistent] => }");
1442 IF_DEBUG(debugger.counter(
"stale inequalities")++;)
1446 TRACE_MSG(
"arith ineq",
"projectInequalities => }");
1454 Theorem betaLTt = ineqThm1, tLTalpha = ineqThm2;
1456 Expr ineq2 = tLTalpha.getExpr();
1458 separateMonomial(ineq2[0], c, x);
1460 Theorem isIntBeta(isIntegerThm(ineq1[0]));
1461 Theorem isIntAlpha(isIntegerThm(ineq2[1]));
1464 TRACE(
"arith ineq",
"normalizeProjectIneqs(", ineq1,
1468 "TheoryArith3::normalizeProjectIneqs: Wrong Kind inputs: " +
1471 "TheoryArith3::normalizeProjectIneqs: Wrong Kind inputs: " +
1490 if(isInt && (a >= 2 || b >= 2)) {
1493 intResult = d_rules->darkGrayShadow2ab(betaLTt, tLTalpha,
1494 isIntAlpha, isIntBeta, isIntx);
1496 intResult = d_rules->darkGrayShadow2ba(betaLTt, tLTalpha,
1497 isIntAlpha, isIntBeta, isIntx);
1498 enqueueFact(intResult);
1502 const Expr& D = DorG[0];
1503 const Expr& G = DorG[1];
1507 Expr tmp = simplifyExpr(D);
1508 if (!tmp.isBoolConst())
1509 addSplitter(tmp, 5);
1511 tmp = simplifyExpr(!G);
1512 if (!tmp.isBoolConst())
1513 addSplitter(tmp, 1);
1514 IF_DEBUG(debugger.counter(
"dark+gray shadows")++;)
1519 std::vector<Theorem> thms1;
1520 Theorem thm2 = iffMP(betaLTt, d_rules->multIneqn(ineq1, rat(factor1)));
1521 betaLTt = canonPred(thm2);
1522 ineq1 = betaLTt.getExpr();
1525 std::vector<Theorem> thms1;
1526 Theorem thm2 = iffMP(tLTalpha, d_rules->multIneqn(ineq2, rat(factor2)));
1527 tLTalpha = canonPred(thm2);
1528 ineq2 = tLTalpha.getExpr();
1533 Expr beta(ineq1[0]);
1534 Expr alpha(ineq2[1]);
1536 if(
isLE(ineq1) &&
isLE(ineq2) && alpha == beta) {
1537 Theorem result = d_rules->realShadowEq(betaLTt, tLTalpha);
1538 TRACE(
"arith ineq",
"normalizeProjectIneqs => ", result,
" }");
1544 processFiniteInterval(betaLTt, tLTalpha);
1548 Theorem result = d_rules->realShadow(betaLTt, tLTalpha);
1557 if(!(e[0].
isRational() && e[0].getRational() == 0)) {
1558 result = iffMP(result, d_rules->rightMinusLeft(e));
1559 result = canonPred(result);
1566 result = iffMP(result, d_rules->constPredicate(result.
getExpr()));
1567 TRACE(
"arith ineq",
"normalizeProjectIneqs => ", result,
" }");
1573 bool foundLeft =
false;
1574 bool foundRight =
false;
1580 if (findFixed != fixedMaxCoefficient.end())
1581 return (*findFixed).second;
1585 if (findMaxLeft != maxCoefficientLeft.end()) {
1587 leftMax = (*findMaxLeft).second;
1592 if (findMaxRight != maxCoefficientRight.end()) {
1594 rightMax = (*findMaxRight).second;
1597 if (foundLeft && foundRight) {
1598 if (leftMax < rightMax)
return rightMax;
1599 else return leftMax;
1602 return Rational(1) / (leftMax * rightMax);
1606 fixedMaxCoefficient[var] =
max;
1609 void TheoryArith3::selectSmallestByCoefficient(vector<Expr> input, vector<Expr>& output) {
1615 Expr best_variable = input[0];
1616 Rational best_coefficient = currentMaxCoefficient(best_variable);
1617 output.push_back(best_variable);
1619 for(
unsigned int i = 1; i < input.size(); i ++) {
1622 Expr current_variable = input[i];
1624 Rational current_coefficient = currentMaxCoefficient(current_variable);
1627 if ((current_coefficient < best_coefficient)) {
1628 best_variable = current_variable;
1629 best_coefficient = current_coefficient;
1634 if (current_coefficient == best_coefficient)
1635 output.push_back(current_variable);
1639 fixCurrentMaxCoefficient(best_variable, best_coefficient);
1646 if(theoryCore()->getFlags()[
"var-order"].getBool()) {
1648 Expr isolatedMonomial = right[1];
1652 for(++i; i != right.
end(); ++i)
1653 if(lessThanVar(isolatedMonomial,*i))
1654 isolatedMonomial = *i;
1655 return isolatedMonomial;
1661 for(;i != iend; ++i) {
1665 separateMonomial(*i, c, var);
1666 var2monomial[var] = *i;
1667 vars.push_back(var);
1670 vector<Expr> largest;
1671 d_graph.selectLargest(vars, largest);
1673 "TheoryArith3::pickMonomial: selectLargest: failed!!!!");
1676 vector<Expr> largest_small_coeff;
1677 selectSmallestByCoefficient(largest, largest_small_coeff);
1678 DebugAssert(0 < largest_small_coeff.size(),
"TheoryArith3::pickMonomial: selectLargestByCOefficient: failed!!!!");
1680 size_t pickedVar = 0;
1684 size_t size = largest_small_coeff.size();
1685 int minProjections = -1;
1687 for(
size_t k=0; k< size; ++k) {
1688 const Expr& var(largest_small_coeff[k]), monom(var2monomial[var]);
1690 int nRight = (d_countRight.count(var) > 0)? d_countRight[var] : 0;
1691 int nLeft = (d_countLeft.count(var) > 0)? d_countLeft[var] : 0;
1692 int n(nRight*nLeft);
1693 TRACE(
"arith ineq",
"pickMonomial: var=", var,
1695 if(minProjections < 0 || minProjections > n) {
1699 TRACE(
"arith ineq",
"Number of projections for "+var.toString()+
" = ", n,
"");
1703 const Expr& largestVar = largest_small_coeff[pickedVar];
1708 for(
size_t k = 0; k < vars.size(); ++k) {
1709 if(vars[k] != largestVar)
1710 d_graph.addEdge(largestVar, vars[k]);
1713 return var2monomial[largestVar];
1716 void TheoryArith3::VarOrderGraph::addEdge(
const Expr& e1,
const Expr& e2)
1718 TRACE(
"arith var order",
"addEdge("+e1.
toString()+
" > ", e2,
")");
1719 DebugAssert(e1 != e2,
"TheoryArith3::VarOrderGraph::addEdge("
1721 d_edges[e1].push_back(e2);
1726 bool TheoryArith3::VarOrderGraph::lessThan(
const Expr& e1,
const Expr& e2)
1734 bool TheoryArith3::VarOrderGraph::dfs(
const Expr& e1,
const Expr& e2)
1738 if(d_cache.count(e2) > 0)
1740 if(d_edges.count(e2) == 0)
1743 vector<Expr>& e2Edges = d_edges[e2];
1744 vector<Expr>::iterator i = e2Edges.begin();
1745 vector<Expr>::iterator iend = e2Edges.end();
1747 for(; i != iend && !dfs(e1,*i); ++i);
1752 void TheoryArith3::VarOrderGraph::selectSmallest(vector<Expr>& v1,
1755 int v1Size = v1.size();
1756 vector<bool> v3(v1Size);
1757 for(
int j=0; j < v1Size; ++j)
1760 for(
int j=0; j < v1Size; ++j) {
1762 for(
int i =0; i < v1Size; ++i) {
1763 if((i == j) || v3[i])
1765 if(lessThan(v1[i],v1[j])) {
1771 vector<Expr> new_v1;
1773 for(
int j = 0; j < v1Size; ++j)
1774 if(!v3[j]) v2.push_back(v1[j]);
1775 else new_v1.push_back(v1[j]);
1780 void TheoryArith3::VarOrderGraph::selectLargest(
const vector<Expr>& v1,
1783 int v1Size = v1.size();
1784 vector<bool> v3(v1Size);
1785 for(
int j=0; j < v1Size; ++j)
1788 for(
int j=0; j < v1Size; ++j) {
1790 for(
int i =0; i < v1Size; ++i) {
1791 if((i == j) || v3[i])
1793 if(lessThan(v1[j],v1[i])) {
1800 for(
int j = 0; j < v1Size; ++j)
1801 if(!v3[j]) v2.push_back(v1[j]);
1811 d_diseq(core->getCM()->getCurrentContext()),
1812 d_diseqIdx(core->getCM()->getCurrentContext(), 0, 0),
1813 d_inModelCreation(core->getCM()->getCurrentContext(), false, 0),
1814 d_freeConstDB(core->getCM()->getCurrentContext()),
1815 d_buffer(core->getCM()->getCurrentContext()),
1817 d_bufferIdx(core->getCM()->getCurrentContext(), 0, 0),
1818 d_bufferThres(&(core->getFlags()[
"ineq-delay"].getInt())),
1819 d_countRight(core->getCM()->getCurrentContext()),
1820 d_countLeft(core->getCM()->getCurrentContext()),
1821 d_sharedTerms(core->getCM()->getCurrentContext()),
1822 d_sharedVars(core->getCM()->getCurrentContext()),
1823 maxCoefficientLeft(core->getCM()->getCurrentContext()),
1824 maxCoefficientRight(core->getCM()->getCurrentContext()),
1825 fixedMaxCoefficient(core->getCM()->getCurrentContext())
1856 kinds.push_back(
REAL);
1857 kinds.push_back(
INT);
1861 kinds.push_back(
PLUS);
1862 kinds.push_back(
MINUS);
1863 kinds.push_back(
MULT);
1865 kinds.push_back(
POW);
1867 kinds.push_back(
MOD);
1868 kinds.push_back(
LT);
1869 kinds.push_back(
LE);
1870 kinds.push_back(
GT);
1871 kinds.push_back(
GE);
1907 if(cache.count(e) > 0)
return;
1910 if(
isLeaf(e)) vars.push_back(e);
1921 DebugAssert(
isLE(ineq1),
"TheoryArith3::processFiniteInterval: ineq1 = "
1923 DebugAssert(
isLE(ineq2),
"TheoryArith3::processFiniteInterval: ineq2 = "
1932 const Expr& ax = ineq1[1];
1933 const Expr& bx = ineq2[0];
1935 "TheoryArith3::processFiniteInterval:\n ax = "+ax.
toString());
1937 "TheoryArith3::processFiniteInterval:\n bx = "+bx.
toString());
1941 Theorem thm1(alphaLEax), thm2(bxLEbeta);
1948 const Expr& alphaLEt = thm1.getExpr();
1949 const Expr& alpha = alphaLEt[0];
1950 const Expr& t = alphaLEt[1];
1960 vector<unsigned> changed;
1961 vector<Theorem> thms;
1962 changed.push_back(1);
1963 thms.push_back(bEQac);
1965 tLEac =
iffMP(thm2, tLEac);
1988 size_t sizeLeft = ineqsLeft.
size();
1989 size_t sizeRight = ineqsRight.
size();
1991 for(
size_t l=0; l<sizeLeft; ++l)
1992 for(
size_t r=0; r<sizeRight; ++r)
2004 for (
int k = 0; k < e.
arity(); ++k) {
2024 if (expr.isNot() && expr[0].isEq()) {
2025 IF_DEBUG(debugger.counter(
"[arith] received disequalities")++;)
2028 else if (!expr.isEq()){
2036 IF_DEBUG(debugger.counter(
"received DARK_SHADOW")++;)
2039 IF_DEBUG(debugger.counter(
"received GRAY_SHADOW")++;)
2040 const Rational& c1 = expr[2].getRational();
2041 const Rational& c2 = expr[3].getRational();
2042 const Expr& v = expr[0];
2043 const Expr& ee = expr[1];
2051 IF_DEBUG(debugger.counter(
"reduced const GRAY_SHADOW")++;)
2067 DebugAssert(thm2.getExpr().isAnd() && thm2.getExpr().arity()==2,
2068 "thm2 = "+thm2.getExpr().toString());
2069 const Expr& G1orG2 = thm2.getExpr()[0];
2071 "G1orG2 = "+G1orG2.toString());
2072 const Expr& G1 = G1orG2[0];
2073 const Expr& G2 = G1orG2[1];
2078 if (!tmp.isBoolConst())
2081 if (!tmp.isBoolConst())
2088 "expected LE or LT: "+expr.toString());
2090 IF_DEBUG(debugger.counter(
"recevied inequalities")++;)
2114 IF_DEBUG(debugger.counter(
"arith IS_INTEGER")++;)
2119 IF_DEBUG(debugger.counter(
"[arith] received t1=t2")++;)
2129 TRACE(
"arith checksat",
"checksat(", fullEffort?
"true" :
"false",
")");
2130 TRACE(
"arith ineq",
"TheoryArith3::checkSat(fullEffort=",
2131 fullEffort?
"true" :
"false",
")");
2137 TRACE(
"model",
"[arith] refining diseq: ",
2150 TRACE(
"model",
"refineCounterExample[TheoryArith3] ",
"",
"{");
2156 for(; it!=iend; ++it) {
2158 Expr e1 = (*it).first;
2159 for(it2 = it, ++it2; it2!=iend; ++it2) {
2160 Expr e2 = (*it2).first;
2162 "TheoryArith3::refineCounterExample: e1 = "+e1.
toString()
2166 "TheoryArith3::refineCounterExample: e2 = "+e2.
toString()
2169 if (!eq.isBoolConst())
2174 TRACE(
"model",
"refineCounterExample[Theory::Arith] ",
"",
"}");
2187 "seperateMonomial failed");
2189 "smallest variable in graph, should not have variables"
2190 " in inequalities: ");
2191 DebugAssert(x == var,
"separateMonomial found different variable: "
2199 bool strictLB=
false, strictUB=
false;
2204 int numRight = 0, numLeft = 0;
2207 for(
unsigned int i=0; i<ratsLTe->
size(); i++) {
2208 DebugAssert((*ratsLTe)[i].varOnRHS(),
"variable on wrong side!");
2209 Expr ineq = (*ratsLTe)[i].ineq().getExpr();
2210 Expr leftSide = ineq[0], rightSide = ineq[1];
2213 if(numRight==0 || r>glb){
2215 strictLB =
isLT(ineq);
2223 for(
unsigned int i=0; i<ratsGTe->
size(); i++) {
2224 DebugAssert((*ratsGTe)[i].varOnLHS(),
"variable on wrong side!");
2225 Expr ineq = (*ratsGTe)[i].ineq().getExpr();
2226 Expr leftSide = ineq[0], rightSide = ineq[1];
2229 if(numLeft==0 || r<lub) {
2231 strictUB =
isLT(ineq);
2237 if(!left && !right) {
2241 if(!left && right) {lub = glb +2;}
2242 if(!right && left) {glb = lub-2;}
2243 DebugAssert(glb <= lub,
"Greatest lower bound needs to be smaller "
2244 "than least upper bound");
2251 while (v.size() > 0) {
2252 std::vector<Expr> bottom;
2254 TRACE(
"model",
"Finding variables to assign. Iteration # ", count,
"");
2255 for(
unsigned int i = 0; i<bottom.size(); i++) {
2257 TRACE(
"model",
"Found: ", e,
"");
2272 mid = (lub + glb)/2;
2273 TRACE(
"model",
"Assigning mid = ", mid,
" {");
2286 TRACE(
"model",
"Arith=>computeModel ",
"",
"{");
2287 for(
unsigned int i=0; i <v.size(); ++i) {
2288 const Expr& e = v[i];
2290 TRACE(
"model",
"arith variable:", e ,
"");
2294 TRACE(
"model",
"arith variable:", e ,
"");
2299 TRACE(
"model",
"Arith=>computeModel",
"",
"}");
2307 +e.
toString()+
")\n e is not assigned concrete value.\n"
2322 TRACE(
"arith",
"normalize(", e,
") {");
2324 "normalize: input must be Eq or Ineq: " + e.
toString());
2326 "normalize: if (e is ineq) then e[0] must be 0" +
2331 "normalize: if e is Eq and e[0] is rat then e[0]==0");
2336 "normalize: if e is Eq and e[1] is rat then e[1]==0\n"
2347 TRACE(
"arith",
"normalize: factor = ", factor,
"");
2349 "normalize: factor="+ factor.
toString());
2372 ss <<
"normalize: control should not reach here " << kind;
2377 TRACE(
"arith",
"normalize => ", thm,
" }");
2390 TRACE(
"arith",
"TheoryArith3::rewrite(", e,
") {");
2396 TRACE(
"arith",
"TheoryArith3::rewrite[non-literal] => ", thm,
" }");
2408 if((e[0].
isRational() && e[0].getRational() == 0)
2431 if(eq.
isEq() && eq[0] < eq[1])
2456 "Expected GE or GT");
2494 "Theory_Arith::rewrite: control should not reach here");
2507 TRACE(
"arith",
"TheoryArith3::rewrite => ", thm,
" }");
2521 e[0].
isRational() && e[0].getRational() == 0,
2522 "TheoryArith3::setup: expected 0 < rhs:" + e.
toString());
2526 int k(0), ar(e.
arity());
2527 for ( ; k < ar; ++k) {
2529 TRACE(
"arith setup",
"e["+
int2string(k)+
"]: ", *(e[k].getNotify()),
"");
2537 IF_DEBUG(debugger.counter(
"arith update total")++;)
2544 vector<unsigned> changed;
2545 vector<Theorem> children;
2546 changed.push_back(1);
2547 children.push_back(e);
2556 IF_DEBUG(debugger.counter(
"arith update ineq")++;)
2560 TRACE(
"arith",
"TheoryArith3::update(): thm = ", thm,
"");
2564 IF_DEBUG(debugger.counter(
"arith update find(d)=d")++;)
2612 TRACE(
"model",
"TheoryArith3::computeModelTerm(", e,
"): a variable");
2616 TRACE(
"model",
"TheoryArith3::computeModelTerm("+e.
toString()
2617 +
"): has find pointer to ", e2,
"");
2631 std::vector<Expr> kids;
2633 kids.push_back(
leExpr(tExpr[0], e));
2634 kids.push_back(
leExpr(e, tExpr[1]));
2650 "Not in solved form: lhs appears in rhs");
2655 "Expected at least one unsimplified leaf on lhs");
2658 "Expected canonSimp(rhs) = canonSimp(rhs)");
2664 vector<Theorem> eqs;
2668 for (index = 0; index < expr.
arity(); ++index) {
2673 eqs[index].getLHS().isTerm(),
"Expected equation");
2677 for (index = 0; index < expr.
arity(); ++index) {
2680 "Expected canonSimp(rhs) = canonSimp(rhs)");
2682 "Failed recursive canonSimp check");
2683 for (index2 = 0; index2 < expr.
arity(); ++index2) {
2685 eqs[index].getLHS() != eqs[index2].getLHS(),
2686 "Not in solved form: repeated lhs");
2688 "Not in solved form: lhs appears in rhs");
2700 if (e.
arity() > 0) {
2705 if (e.
arity() != 2 ||
2713 DebugAssert(
false,
"Unexpected kind in TheoryArith3::checkType"
2720 bool enumerate,
bool computeSize)
2729 if (r <= typeExpr[1].getRational()) {
2765 for(
int k = 0; k < e.
arity(); ++k) {
2781 Expr numerator = e[0];
2782 Expr denominator = e[1];
2805 for (
int k = 0; k < e.
arity(); ++k) {
2823 DebugAssert(
false,
"TheoryArith3::computeType: unexpected expression:\n "
2833 "TheoryArith3::computeBaseType("+t.
toString()+
")");
2856 TRACE(
"parser",
"TheoryArith3::parseExprOp(", e,
")");
2880 "TheoryArith3::parseExprOp:\n e = "+e.
toString());
2882 const Expr& c1 = e[0][0];
2898 for(; i!=iend; ++i) k.push_back(
parseExpr(*i));
2904 else if(e.
arity() == 3)
2917 for(; i!=iend; ++i) k.push_back(
parseExpr(*i));
2954 "TheoryArith3::parseExprOp: invalid input " + e.
toString());
2974 os <<
"ERROR:SUBRANGE:not supported in Simplify\n";
2977 os <<
"ERROR:IS_INTEGER:not supported in Simplify\n";
2980 int i=0, iend=e.
arity();
2982 if(i!=iend) os << e[i];
2984 for(; i!=iend; ++i) os <<
" " << e[i];
2989 os <<
"(- " << e[0] <<
" " << e[1]<<
")";
2995 int i=0, iend=e.arity();
2997 if(i!=iend) os << e[i];
2999 for(; i!=iend; ++i) os <<
" " << e[i];
3004 os <<
"(" <<
push << e[1] <<
space <<
"^ " << e[0] <<
push <<
")";
3007 os <<
"(" << push << e[0] <<
space <<
"/ " << e[1] << push <<
")";
3010 if (
isInt(e[0].getType()) ||
isInt(e[1].getType())) {
3012 os <<
"(< " << e[0] <<
" " << e[1] <<
")";
3015 os <<
"(<= " << e[0] <<
" " << e[1] <<
")";
3018 os <<
"(> " << e[0] <<
" " << e[1] <<
")";
3021 os <<
"(>= " << e[0] <<
" " << e[1] <<
")";
3025 os <<
"ERROR:SHADOW:not supported in Simplify\n";
3042 os <<
"ERROR:SUBRANGE:not supported in TPTP\n";
3045 os <<
"ERROR:IS_INTEGER:not supported in TPTP\n";
3049 os<<
"ERRPR:plus only supports inteters now in TPTP\n";
3053 int i=0, iend=e.
arity();
3055 os<<
"ERROR,plus must have more than two numbers in TPTP\n";
3059 for(i=0; i <= iend-2; ++i){
3066 for(i=0 ; i <= iend-2; ++i){
3074 os<<
"ERRPR:arithmetic operations only support inteters now in TPTP\n";
3078 os <<
"$minus_int(" << e[0] <<
"," << e[1]<<
")";
3082 os<<
"ERRPR:arithmetic operations only support inteters now in TPTP\n";
3086 os <<
"$uminus_int(" << e[0] <<
")" ;
3090 os<<
"ERRPR:times only supports inteters now in TPTP\n";
3094 int i=0, iend=e.arity();
3096 os<<
"ERROR:times must have more than two numbers in TPTP\n";
3100 for(i=0; i <= iend-2; ++i){
3101 os <<
"$times_int(";
3107 for(i=0 ; i <= iend-2; ++i){
3116 os<<
"ERRPR:arithmetic operations only support inteters now in TPTP\n";
3120 os <<
"$power_int(" <<
push << e[1] <<
space <<
"^ " << e[0] <<
push <<
")";
3125 os<<
"ERRPR:arithmetic operations only support inteters now in TPTP\n";
3129 os <<
"divide_int(" <<e[0] <<
"," << e[1] <<
")";
3134 os<<
"ERRPR:arithmetic operations only support inteters now in TPTP\n";
3137 os <<
"$less_int(" << e[0] <<
"," << e[1] <<
")";
3142 os<<
"ERRPR:arithmetic operations only support inteters now in TPTP\n";
3146 os <<
"$lesseq_int(" << e[0] <<
"," << e[1] <<
")";
3151 os<<
"ERRPR:arithmetic operations only support inteters now in TPTP\n";
3155 os <<
"$greater_int(" << e[0] <<
"," << e[1] <<
")";
3160 os<<
"ERRPR:arithmetic operations only support inteters now in TPTP\n";
3164 os <<
"$greatereq_int(" << e[0] <<
"," << e[1] <<
")";
3168 os <<
"ERROR:SHADOW:not supported in TPTP\n";
3175 os <<
"ERROR:REAL not supported in TPTP\n";
3205 os <<
"[" <<
push << e[0] <<
".." << e[1] <<
push <<
"]";
3209 os <<
"IS_INTEGER(" << push << e[0] << push <<
")";
3214 int i=0, iend=e.
arity();
3216 if(i!=iend) os << e[i];
3218 for(; i!=iend; ++i) os <<
space <<
"+ " << e[i];
3223 os <<
"(" << push << e[0] <<
space <<
"- " << e[1] << push <<
")";
3226 os <<
"-(" << push << e[0] << push <<
")";
3229 int i=0, iend=e.
arity();
3231 if(i!=iend) os << e[i];
3233 for(; i!=iend; ++i) os <<
space <<
"* " << e[i];
3238 os <<
"(" << push << e[1] <<
space <<
"^ " << e[0] << push <<
")";
3241 os <<
"(" << push << e[0] <<
space <<
"/ " << e[1] << push <<
")";
3244 if (
isInt(e[0].getType()) ||
isInt(e[1].getType())) {
3246 os <<
"(" << push << e[0] <<
space <<
"< " << e[1] << push <<
")";
3249 os <<
"(" << push << e[0] <<
space <<
"<= " << e[1] << push <<
")";
3252 os <<
"(" << push << e[0] <<
space <<
"> " << e[1] << push <<
")";
3255 os <<
"(" << push << e[0] <<
space <<
">= " << e[1] << push <<
")";
3258 os <<
"DARK_SHADOW(" << push << e[0] <<
", " <<
space << e[1] << push <<
")";
3261 os <<
"GRAY_SHADOW(" << push << e[0] <<
"," <<
space << e[1]
3262 <<
"," <<
space << e[2] <<
"," <<
space << e[3] << push <<
")";
3288 throw SmtlibException(
"TheoryArith3::print: SMTLIB: SUBRANGE not implemented");
3296 os <<
"(" <<
push <<
"IsInt" <<
space << e[0] <<
push <<
")";
3298 throw SmtlibException(
"TheoryArith3::print: SMTLIB: IS_INTEGER used unexpectedly");
3304 os <<
"(" <<
push <<
"+";
3306 for(; i!=iend; ++i) {
3307 os <<
space << (*i);
3314 os <<
"(" <<
push <<
"- " << e[0] <<
space << e[1] <<
push <<
")";
3322 int i=0, iend=e.
arity();
3326 for(; i!=iend; ++i) {
3328 os <<
"(" <<
push <<
"*";
3330 os <<
space << e[i];
3332 for (i=0; i < iend-1; ++i) os <<
push <<
")";
3337 throw SmtlibException(
"TheoryArith3::print: SMTLIB: POW not supported");
3341 throw SmtlibException(
"TheoryArith3::print: SMTLIB: unexpected use of DIVIDE");
3347 os << e[0] << space << e[1] <<
push <<
")";
3353 os << e[0] << space << e[1] <<
push <<
")";
3359 os << e[0] << space << e[1] <<
push <<
")";
3365 os << e[0] << space << e[1] <<
push <<
")";
3369 throw SmtlibException(
"TheoryArith3::print: SMTLIB: DARK_SHADOW not supported");
3370 os <<
"(" <<
push <<
"DARK_SHADOW" <<
space << e[0]
3374 throw SmtlibException(
"TheoryArith3::print: SMTLIB: GRAY_SHADOW not supported");
3375 os <<
"GRAY_SHADOW(" << push << e[0] <<
"," <<
space << e[1]
3376 <<
"," <<
space << e[2] <<
"," <<
space << e[3] << push <<
")";
3379 throw SmtlibException(
"TheoryArith3::print: SMTLIB: default not supported");
3400 os <<
"(" <<
push <<
"SUBRANGE" <<
space << e[0]
3405 os <<
"(" << push <<
"IS_INTEGER" <<
space << e[0] << push <<
")";
3410 int i=0, iend=e.
arity();
3411 os <<
"(" << push <<
"+";
3412 for(; i!=iend; ++i) os <<
space << e[i];
3418 os <<
"(" << push <<
"- " << e[0] <<
space << e[1] << push <<
")";
3421 os <<
"(" << push <<
"-" <<
space << e[0] << push <<
")";
3424 int i=0, iend=e.
arity();
3425 os <<
"(" << push <<
"*";
3426 for(; i!=iend; ++i) os <<
space << e[i];
3431 os <<
"(" << push <<
"^ " << e[1] <<
space << e[0] << push <<
")";
3434 os <<
"(" << push <<
"/ " << e[0] <<
space << e[1] << push <<
")";
3437 os <<
"(" << push <<
"< " << e[0] <<
space << e[1] << push <<
")";
3440 os <<
"(" << push <<
"<= " << e[0] <<
space << e[1] << push <<
")";
3443 os <<
"(" << push <<
"> " << e[1] <<
space << e[0] << push <<
")";
3446 os <<
"(" << push <<
">= " << e[0] <<
space << e[1] << push <<
")";
3449 os <<
"(" << push <<
"DARK_SHADOW" <<
space << e[0]
3450 <<
space << e[1] << push <<
")";
3453 os <<
"(" << push <<
"GRAY_SHADOW" <<
space << e[0] <<
space
3454 << e[1] <<
space << e[2] <<
space << e[3] << push <<
")";