/*****************************************************************************/
/*!
* \file theory_arith_old.cpp
*
* Author: Clark Barrett, Vijay Ganesh.
*
* Created: Fri Jan 17 18:39:18 2003
*
*
*
* License to use, copy, modify, sell and/or distribute this software
* and its documentation for any purpose is hereby granted without
* royalty, subject to the terms and conditions defined in the \ref
* LICENSE file provided with this distribution.
*
*
*
*/
/*****************************************************************************/
#include "theory_arith_old.h"
#include "arith_proof_rules.h"
//#include "arith_expr.h"
#include "arith_exception.h"
#include "typecheck_exception.h"
#include "eval_exception.h"
#include "parser_exception.h"
#include "smtlib_exception.h"
#include "theory_core.h"
#include "command_line_flags.h"
//TODO: remove this dependency
#include "../theory_core/core_proof_rules.h"
using namespace std;
using namespace CVC3;
///////////////////////////////////////////////////////////////////////////////
// TheoryArithOld::FreeConst Methods //
///////////////////////////////////////////////////////////////////////////////
namespace CVC3 {
ostream& operator<<(ostream& os, const TheoryArithOld::FreeConst& fc) {
os << "FreeConst(r=" << fc.getConst() << ", "
<< (fc.strict()? "strict" : "non-strict") << ")";
return os;
}
///////////////////////////////////////////////////////////////////////////////
// TheoryArithOld::Ineq Methods //
///////////////////////////////////////////////////////////////////////////////
ostream& operator<<(ostream& os, const TheoryArithOld::Ineq& ineq) {
os << "Ineq(" << ineq.ineq().getExpr() << ", isolated on "
<< (ineq.varOnRHS()? "RHS" : "LHS") << ", const = "
<< ineq.getConst() << ")";
return os;
}
} // End of namespace CVC3
///////////////////////////////////////////////////////////////////////////////
// TheoryArithOld Private Methods //
///////////////////////////////////////////////////////////////////////////////
Theorem TheoryArithOld::isIntegerThm(const Expr& e) {
// Quick checks
Type t = e.getType();
if (isReal(t)) return Theorem();
if (isInt(t)) return typePred(e);
// Try harder
return isIntegerDerive(Expr(IS_INTEGER, e), typePred(e));
}
Theorem TheoryArithOld::isIntegerDerive(const Expr& isIntE, const Theorem& thm) {
const Expr& e = thm.getExpr();
// We found it!
if(e == isIntE) return thm;
Theorem res;
// If the theorem is an AND, look inside each child
if(e.isAnd()) {
int i, iend=e.arity();
for(i=0; iandElim(thm, i));
if(!res.isNull()) return res;
}
}
return res;
}
const Rational& TheoryArithOld::freeConstIneq(const Expr& ineq, bool varOnRHS) {
DebugAssert(isIneq(ineq), "TheoryArithOld::freeConstIneq("+ineq.toString()+")");
const Expr& e = varOnRHS? ineq[0] : ineq[1];
switch(e.getKind()) {
case PLUS:
return e[0].getRational();
case RATIONAL_EXPR:
return e.getRational();
default: { // MULT, DIV, or Variable
static Rational zero(0);
return zero;
}
}
}
const TheoryArithOld::FreeConst&
TheoryArithOld::updateSubsumptionDB(const Expr& ineq, bool varOnRHS,
bool& subsumed) {
TRACE("arith ineq", "TheoryArithOld::updateSubsumptionDB(", ineq,
", var isolated on "+string(varOnRHS? "RHS" : "LHS")+")");
DebugAssert(isLT(ineq) || isLE(ineq), "TheoryArithOld::updateSubsumptionDB("
+ineq.toString()+")");
// Indexing expression: same as ineq only without the free const
Expr index;
const Expr& t = varOnRHS? ineq[0] : ineq[1];
bool strict(isLT(ineq));
Rational c(0);
if(isPlus(t)) {
DebugAssert(t.arity() >= 2, "TheoryArithOld::updateSubsumptionDB("
+ineq.toString()+")");
c = t[0].getRational(); // Extract the free const in ineq
Expr newT;
if(t.arity() == 2) {
newT = t[1];
} else {
vector kids;
Expr::iterator i=t.begin(), iend=t.end();
kids.push_back(rat(0));
for(++i; i!=iend; ++i) kids.push_back(*i);
DebugAssert(kids.size() > 0, "kids.size = "+int2string(kids.size())
+", ineq = "+ineq.toString());
newT = plusExpr(kids);
}
if(varOnRHS)
index = leExpr(rat(0), canonSimplify(ineq[1] - newT).getRHS());
else
index = leExpr(canonSimplify(ineq[0]-newT).getRHS(), rat(0));
} else if(isRational(t)) {
c = t.getRational();
if(varOnRHS)
index = leExpr(rat(0), ineq[1]);
else
index = leExpr(ineq[0], rat(0));
} else if(isLT(ineq))
index = leExpr(ineq[0], ineq[1]);
else
index = ineq;
// Now update the database, check for subsumption, and extract the constant
CDMap::iterator i=d_freeConstDB.find(index),
iend=d_freeConstDB.end();
if(i == iend) {
subsumed = false;
// Create a new entry
CDOmap& obj = d_freeConstDB[index];
obj = FreeConst(c,strict);
TRACE("arith ineq", "freeConstDB["+index.toString()+"] := ", obj, "");
return obj.get();
} else {
CDOmap& obj = d_freeConstDB[index];
const FreeConst& fc = obj.get();
if(varOnRHS) {
subsumed = (c < fc.getConst() ||
(c == fc.getConst() && (!strict || fc.strict())));
} else {
subsumed = (c > fc.getConst() ||
(c == fc.getConst() && (strict || !fc.strict())));
}
if(!subsumed) {
obj = FreeConst(c,strict);
TRACE("arith ineq", "freeConstDB["+index.toString()+"] := ", obj, "");
}
return obj.get();
}
}
bool TheoryArithOld::kidsCanonical(const Expr& e) {
if(isLeaf(e)) return true;
bool res(true);
for(int i=0; res && iuMinusToMult(e[0]);
Expr e2 = thm.getRHS();
result = transitivityRule(thm, canon(e2));
}
break;
case PLUS: /* {
Theorem plusThm, plusThm1;
plusThm = d_rules->canonFlattenSum(e);
plusThm1 = d_rules->canonComboLikeTerms(plusThm.getRHS());
result = transitivityRule(plusThm,plusThm1);
}
*/
result = d_rules->canonPlus(e);
break;
case MINUS: {
DebugAssert(e.arity() == 2,"");
Theorem minus_eq_sum = d_rules->minusToPlus(e[0], e[1]);
// this produces e0 + (-1)*e1; we have to canonize it in 2 steps
Expr sum(minus_eq_sum.getRHS());
Theorem thm(canon(sum[1]));
if(thm.getLHS() == thm.getRHS())
result = canonThm(minus_eq_sum);
// The sum changed; do the work
else {
vector changed;
vector thms;
changed.push_back(1);
thms.push_back(thm);
Theorem sum_eq_canon = canonThm(substitutivityRule(sum, changed, thms));
result = transitivityRule(minus_eq_sum, sum_eq_canon);
}
break;
}
case MULT:
result = d_rules->canonMult(e);
break;
/*
case MULT: {
Theorem thmMult, thmMult1;
Expr exprMult;
Expr e0 = e[0];
Expr e1 = e[1];
if(e0.isRational()) {
if(rat(0) == e0)
result = d_rules->canonMultZero(e1);
else if (rat(1) == e0)
result = d_rules->canonMultOne(e1);
else
switch(e1.getKind()) {
case RATIONAL_EXPR :
result = d_rules->canonMultConstConst(e0,e1);
break;
case MULT:
DebugAssert(e1[0].isRational(),
"theory_arith::canon:\n "
"canon:MULT:MULT child is not canonical: "
+ e1[0].toString());
thmMult = d_rules->canonMultConstTerm(e0,e1[0],e1[1]);
result = transitivityRule(thmMult,canon(thmMult.getRHS()));
break;
case PLUS:{
Theorem thmPlus, thmPlus1;
Expr ePlus;
std::vector thmPlusVector;
thmPlus = d_rules->canonMultConstSum(e0,e1);
ePlus = thmPlus.getRHS();
Expr::iterator i = ePlus.begin();
for(;i != ePlus.end();++i)
thmPlusVector.push_back(canon(*i));
thmPlus1 = substitutivityRule(PLUS, thmPlusVector);
result = transitivityRule(thmPlus, thmPlus1);
break;
}
default:
result = reflexivityRule(e);
break;
}
}
else {
if(e1.isRational()){
// canonMultTermConst just reverses the order of the const and the
// term. Then canon is called again.
Theorem t1 = d_rules->canonMultTermConst(e1,e0);
result = transitivityRule(t1,canon(t1.getRHS()));
}
else
// This is where the assertion for non-linear multiplication is
// produced.
result = d_rules->canonMultTerm1Term2(e0,e1);
}
break;
}
*/
case DIVIDE:{
/*
case DIVIDE:{
if (e[1].isRational()) {
if (e[1].getRational() == 0)
throw ArithException("Divide by 0 error in "+e.toString());
Theorem thm = d_rules->canonDivideVar(e[0], e[1]);
Expr e2 = thm.getRHS();
result = transitivityRule(thm, canon(e2));
}
else
{
// TODO: to be handled
throw ArithException("Divide by a non-const not handled in "+e.toString());
}
break;
}
*/
// Division by 0 is OK (total extension, protected by TCCs)
// if (e[1].isRational() && e[1].getRational() == 0)
// throw ArithException("Divide by 0 error in "+e.toString());
if (e[1].getKind() == PLUS)
throw ArithException("Divide by a PLUS expression not handled in"+e.toString());
result = d_rules->canonDivide(e);
break;
}
case POW:
if(e[1].isRational())
result = d_rules->canonPowConst(e);
else {
// x ^ 1 --> x
if (e[0].isRational() && e[0].getRational() == 1) {
result = d_rules->powerOfOne(e);
} else
result = reflexivityRule(e);
}
break;
default:
result = reflexivityRule(e);
break;
}
TRACE("arith canon","canon => ",result," }");
return result;
}
Theorem
TheoryArithOld::canonSimplify(const Expr& e) {
TRACE("arith simplify", "canonSimplify(", e, ") {");
DebugAssert(kidsCanonical(e),
"TheoryArithOld::canonSimplify("+e.toString()+")");
DebugAssert(leavesAreSimp(e), "Expected leaves to be simplified");
Expr tmp(e);
Theorem thm = canon(e);
if(thm.getRHS().hasFind())
thm = transitivityRule(thm, find(thm.getRHS()));
// We shouldn't rely on simplification in this function anymore
DebugAssert(thm.getRHS() == simplifyExpr(thm.getRHS()),
"canonSimplify("+e.toString()+")\n"
+"canon(e) = "+thm.getRHS().toString()
+"\nsimplify(canon(e)) = "+simplifyExpr(thm.getRHS()).toString());
// if(tmp != thm.getRHS())
// thm = transitivityRule(thm, simplifyThm(thm.getRHS()));
// while(tmp != thm.getRHS()) {
// tmp = thm.getRHS();
// thm = canon(thm);
// if(tmp != thm.getRHS())
// thm = transitivityRule(thm, simplifyThm(thm.getRHS()));
// }
TRACE("arith", "canonSimplify =>", thm, " }");
return thm;
}
/*! accepts a theorem, canonizes it, applies iffMP and substituvity to
* derive the canonized thm
*/
Theorem
TheoryArithOld::canonPred(const Theorem& thm) {
vector thms;
DebugAssert(thm.getExpr().arity() == 2,
"TheoryArithOld::canonPred: bad theorem: "+thm.toString());
Expr e(thm.getExpr());
thms.push_back(canonSimplify(e[0]));
thms.push_back(canonSimplify(e[1]));
Theorem result = iffMP(thm, substitutivityRule(e.getOp(), thms));
return result;
}
/*! accepts an equivalence theorem, canonizes it, applies iffMP and
* substituvity to derive the canonized thm
*/
Theorem
TheoryArithOld::canonPredEquiv(const Theorem& thm) {
vector thms;
DebugAssert(thm.getRHS().arity() == 2,
"TheoryArithOld::canonPredEquiv: bad theorem: "+thm.toString());
Expr e(thm.getRHS());
thms.push_back(canonSimplify(e[0]));
thms.push_back(canonSimplify(e[1]));
Theorem result = transitivityRule(thm, substitutivityRule(e.getOp(), thms));
return result;
}
/*! accepts an equivalence theorem whose RHS is a conjunction,
* canonizes it, applies iffMP and substituvity to derive the
* canonized thm
*/
Theorem
TheoryArithOld::canonConjunctionEquiv(const Theorem& thm) {
vector thms;
return thm;
}
/*! Pseudo-code for doSolve. (Input is an equation) (output is a Theorem)
* -# translate e to the form e' = 0
* -# if (e'.isRational()) then {if e' != 0 return false else true}
* -# a for loop checks if all the variables are integers.
* - if not isolate a suitable real variable and call processRealEq().
* - if all variables are integers then isolate suitable variable
* and call processIntEq().
*/
Theorem TheoryArithOld::doSolve(const Theorem& thm)
{
const Expr& e = thm.getExpr();
if (e.isTrue() || e.isFalse()) return thm;
TRACE("arith eq","doSolve(",e,") {");
DebugAssert(thm.isRewrite(), "thm = "+thm.toString());
Theorem eqnThm;
vector thms;
// Move LHS to the RHS, if necessary
if(e[0].isRational() && e[0].getRational() == 0)
eqnThm = thm;
else {
eqnThm = iffMP(thm, d_rules->rightMinusLeft(e));
eqnThm = canonPred(eqnThm);
}
// eqnThm is of the form 0 = e'
// 'right' is of the form e'
Expr right = eqnThm.getRHS();
// Check for trivial equation
if (right.isRational()) {
Theorem result = iffMP(eqnThm, d_rules->constPredicate(eqnThm.getExpr()));
TRACE("arith eq","doSolve => ",result," }");
return result;
}
//normalize
eqnThm = iffMP(eqnThm, normalize(eqnThm.getExpr()));
TRACE("arith eq","doSolve => ",eqnThm.getExpr()," }");
right = eqnThm.getRHS();
//eqn is of the form 0 = e' and is normalized where 'right' denotes e'
//FIXME: change processRealEq to accept equations as well instead of theorems
try {
if (isMult(right)) {
DebugAssert(right.arity() > 1, "Expected arity > 1");
if (right[0].isRational()) {
Rational r = right[0].getRational();
if (r == 0) return getCommonRules()->trueTheorem();
else if (r == 1) {
enqueueFact(iffMP(eqnThm, d_rules->multEqZero(eqnThm.getExpr())));
return getCommonRules()->trueTheorem();
}
Theorem res = iffMP(eqnThm,
d_rules->multEqn(eqnThm.getLHS(),
right, rat(1/r)));
res = canonPred(res);
return doSolve(res);
}
else {
enqueueFact(iffMP(eqnThm, d_rules->multEqZero(eqnThm.getExpr())));
return getCommonRules()->trueTheorem();
}
}
else if (isPow(right)) {
DebugAssert(right.arity() == 2, "Expected arity 2");
if (right[0].isRational()) {
return doSolve(iffMP(eqnThm, d_rules->powEqZero(eqnThm.getExpr())));
}
throw ArithException("Can't solve exponential eqn: "+eqnThm.toString());
}
else {
if(!isInteger(right)) {
return processRealEq(eqnThm);
}
else {
return processIntEq(eqnThm);
}
}
} catch(ArithException& e) {
FatalAssert(false, "We should never get here!!! : " + e.toString());
// // Nonlinear bail out
// Theorem res;
// if (isPlus(right)) {
// // Solve for something
// // Try to simulate groebner basis by picking the highest term
// Expr isolated = right[1];
// int isolated_degree = termDegree(isolated);
// for (int i = 2; i < right.arity(); i ++) {
// int degree = termDegree(right[i]);
// if (degree > isolated_degree) {
// isolated = right[i];
// isolated_degree = degree;
// }
// }
// Rational coeff;
// if (isMult(isolated) && isolated[0].isRational()) {
// coeff = isolated[0].getRational();
// DebugAssert(coeff != 0, "Expected nonzero coeff");
// isolated = canon(isolated / rat(coeff)).getRHS();
// } else coeff = 1;
// res = iffMP(eqnThm, d_rules->multEqn(rat(0), right, rat(-1/coeff)));
// res = canonPred(res);
// res = iffMP(res, d_rules->plusPredicate(res.getLHS(), res.getRHS(), isolated, EQ));
// res = canonPred(res);
// TRACE("arith nonlinear", "solved for: ", res.getExpr(), "");
// } else
// res = symmetryRule(eqnThm); // Flip to e' = 0
// TRACE("arith eq", "doSolve: failed to solve an equation: ", e, "");
// IF_DEBUG(debugger.counter("FAILED to solve equalities")++;)
// setIncomplete("Non-linear arithmetic equalities");
//
// // Since we are forgetting about this equation, setup for updates
// TRACE("arith nonlinear", "adding setup to ", eqnThm.getExpr(), "");
// setupRec(eqnThm.getExpr());
// return getCommonRules()->trueTheorem();
}
FatalAssert(false, "");
return Theorem();
}
/*! pick a monomial for the input equation. This function is used only
* if the equation is an integer equation. Choose the monomial with
* the smallest absolute value of coefficient.
*/
bool TheoryArithOld::pickIntEqMonomial(const Expr& right, Expr& isolated, bool& nonlin)
{
DebugAssert(isPlus(right) && right.arity() > 1,
"TheoryArithOld::pickIntEqMonomial right is wrong :-): " +
right.toString());
DebugAssert(right[0].isRational(),
"TheoryArithOld::pickIntEqMonomial. right[0] must be const" +
right.toString());
// DebugAssert(isInteger(right),
// "TheoryArithOld::pickIntEqMonomial: right is of type int: " +
// right.toString());
//right is of the form "C + a1x1 + ... + anxn". min is initialized
//to a1
Expr::iterator istart = right.begin(), iend = right.end();
istart++;
Expr::iterator i = istart, j;
bool found = false;
nonlin = false;
Rational min, coeff;
Expr leaf;
for(; i != iend; ++i) {
if (isLeaf(*i)) {
leaf = *i;
coeff = 1;
}
else if (isMult(*i) && (*i).arity() == 2 && (*i)[0].isRational() && isLeaf((*i)[1])) {
leaf = (*i)[1];
coeff = abs((*i)[0].getRational());
}
else {
nonlin = true;
continue;
}
for (j = istart; j != iend; ++j) {
if (j != i && isLeafIn(leaf, *j)) break;
}
if (j == iend) {
if (!found || min > coeff) {
min = coeff;
isolated = *i;
found = true;
}
}
}
return found;
}
/*! input is 0=e' Theorem and some of the vars in e' are of
* type REAL. isolate one of them and send back to framework. output
* is "var = e''" Theorem.
*/
Theorem
TheoryArithOld::processRealEq(const Theorem& eqn)
{
DebugAssert(eqn.getLHS().isRational() &&
eqn.getLHS().getRational() == 0,
"processRealEq invariant violated");
Expr right = eqn.getRHS();
// Find variable to isolate and store it in left. Pick the largest
// (according to the total ordering) variable. FIXME: change from
// total ordering to the ordering we devised for inequalities.
// TODO: I have to pick a variable that appears as a variable in the
// term but does not appear as a variable anywhere else. The variable
// must appear as a single leaf and not in a MULT expression with some
// other variables and nor in a POW expression.
bool found = false;
Expr left;
if (isPlus(right)) {
DebugAssert(right[0].isRational(), "Expected first term to be rational");
for(int i = 1, iend = right.arity(); i < iend; ++i) {
Expr c = right[i];
DebugAssert(!isRational(c), "Expected non-rational");
if(!isInteger(c)) {
if (isLeaf(c) ||
((isMult(c) && c.arity() == 2 && isLeaf(c[1])))) {
Expr leaf = isLeaf(c) ? c : c[1];
int j;
for (j = 1; j < iend; ++j) {
if (j!= i
&& isLeafIn(leaf, right[j])
) {
break;
}
}
if (j == iend) {
left = c;
found = true;
break;
}
}
}
}
}
else if ((isMult(right) && right.arity() == 2 && isLeaf(right[1])) ||
isLeaf(right)) {
left = right;
found = true;
}
if (!found) {
// The only way we can not get an isolated in the reals is if all of them
// are non-linear. In this case we might have some integers to solve for
// so we try that. The integer solver shouldn't be able to solve for the
// reals, as they are not solvable and we should be safe. One of such
// examples is if some constant ITE got skolemized and we have an equation
// like SKOLEM = x^2 (bug79), in which case we should solve for the SKOLEM
// where skolem is an INT variable.
if (isNonlinearEq(eqn.getExpr()))
return processIntEq(eqn);
else throw
ArithException("Can't find a leaf for solve in "+eqn.toString());
}
Rational r = -1;
if (isMult(left)) {
DebugAssert(left.arity() == 2, "only leaf should be chosen as lhs");
DebugAssert(left[0].getRational() != 0, "left = "+left.toString());
r = -1/left[0].getRational();
left = left[1];
}
DebugAssert(isReal(getBaseType(left)) && !isInteger(left),
"TheoryArithOld::ProcessRealEq: left is integer:\n left = "
+left.toString());
// Normalize equation so that coefficient of the monomial
// corresponding to "left" in eqn[1] is -1
Theorem result(iffMP(eqn,
d_rules->multEqn(eqn.getLHS(), eqn.getRHS(), rat(r))));
result = canonPred(result);
// Isolate left
result = iffMP(result, d_rules->plusPredicate(result.getLHS(),
result.getRHS(), left, EQ));
result = canonPred(result);
TRACE("arith","processRealEq => ",result," }");
return result;
}
void TheoryArithOld::getFactors(const Expr& e, set& factors)
{
switch (e.getKind()) {
case RATIONAL_EXPR: break;
case MULT: {
Expr::iterator i = e.begin(), iend = e.end();
for (; i != iend; ++i) {
getFactors(*i, factors);
}
break;
}
case POW: {
DebugAssert(e.arity() == 2, "invariant violated");
if (!isIntegerConst(e[0]) || e[0].getRational() <= 0) {
throw ArithException("not positive integer exponent in "+e.toString());
}
if (isLeaf(e[1])) factors.insert(e[1]);
break;
}
default: {
DebugAssert(isLeaf(e), "expected leaf");
DebugAssert(factors.find(e) == factors.end(), "expected new entry");
factors.insert(e);
break;
}
}
}
/*!
* \param eqn is a single equation 0 = e
* \return an equivalent Theorem (x = t AND 0 = e'), or just x = t
*/
Theorem
TheoryArithOld::processSimpleIntEq(const Theorem& eqn)
{
TRACE("arith eq", "processSimpleIntEq(", eqn.getExpr(), ") {");
DebugAssert(eqn.isRewrite(),
"TheoryArithOld::processSimpleIntEq: eqn must be equality" +
eqn.getExpr().toString());
Expr right = eqn.getRHS();
DebugAssert(eqn.getLHS().isRational() && 0 == eqn.getLHS().getRational(),
"TheoryArithOld::processSimpleIntEq: LHS must be 0:\n" +
eqn.getExpr().toString());
DebugAssert(!isMult(right) && !isPow(right), "should have been handled above");
if (isPlus(right)) {
if (2 == right.arity() &&
(isLeaf(right[1]) ||
(isMult(right[1]) && right[1].arity() == 2 && right[1][0].isRational() && isLeaf(right[1][1])))) {
//we take care of special cases like 0 = c + a.x, 0 = c + x,
Expr c,x;
separateMonomial(right[1], c, x);
Theorem isIntx(isIntegerThm(x));
DebugAssert(!isIntx.isNull(), "right = "+right.toString()
+"\n x = "+x.toString());
Theorem res(iffMP(eqn, d_rules->intVarEqnConst(eqn.getExpr(), isIntx)));
TRACE("arith eq", "processSimpleIntEq[0 = c + a*x] => ", res, " }");
return res;
}
// Pick a suitable monomial. isolated can be of the form x, a.x, -a.x
Expr isolated;
bool nonlin;
if (pickIntEqMonomial(right, isolated, nonlin)) {
TRACE("arith eq", "processSimpleIntEq: isolated = ", isolated, "");
// First, we compute the 'sign factor' with which to multiply the
// eqn. if the coeff of isolated is positive (i.e. 'isolated' is
// of the form x or a.x where a>0 ) then r must be -1 and if coeff
// of 'isolated' is negative, r=1.
Rational r = isMult(isolated) ?
((isolated[0].getRational() > 0) ? -1 : 1) : -1;
Theorem result;
if (-1 == r) {
// r=-1 and hence 'isolated' is 'x' or 'a.x' where a is
// positive. modify eqn (0=e') to the equation (0=canon(-1*e'))
result = iffMP(eqn, d_rules->multEqn(eqn.getLHS(), right, rat(r)));
result = canonPred(result);
Expr e = result.getRHS();
// Isolate the 'isolated'
result = iffMP(result,
d_rules->plusPredicate(result.getLHS(),result.getRHS(),
isolated, EQ));
} else {
//r is 1 and hence isolated is -a.x. Make 'isolated' positive.
const Rational& minusa = isolated[0].getRational();
Rational a = -1*minusa;
isolated = (a == 1)? isolated[1] : rat(a) * isolated[1];
// Isolate the 'isolated'
result = iffMP(eqn, d_rules->plusPredicate(eqn.getLHS(),
right,isolated,EQ));
}
// Canonize the result
result = canonPred(result);
//if isolated is 'x' or 1*x, then return result else continue processing.
if(!isMult(isolated) || isolated[0].getRational() == 1) {
TRACE("arith eq", "processSimpleIntEq[x = rhs] => ", result, " }");
return result;
} else if (!nonlin) {
DebugAssert(isMult(isolated) && isolated[0].getRational() >= 2,
"TheoryArithOld::processSimpleIntEq: isolated must be mult "
"with coeff >= 2.\n isolated = " + isolated.toString());
// Compute IS_INTEGER() for lhs and rhs
Expr lhs = result.getLHS();
Expr rhs = result.getRHS();
Expr a, x;
separateMonomial(lhs, a, x);
Theorem isIntLHS = isIntegerThm(x);
vector isIntRHS;
if(!isPlus(rhs)) { // rhs is a MULT
Expr c, v;
separateMonomial(rhs, c, v);
isIntRHS.push_back(isIntegerThm(v));
DebugAssert(!isIntRHS.back().isNull(), "");
} else { // rhs is a PLUS
DebugAssert(isPlus(rhs), "rhs = "+rhs.toString());
DebugAssert(rhs.arity() >= 2, "rhs = "+rhs.toString());
Expr::iterator i=rhs.begin(), iend=rhs.end();
++i; // Skip the free constant
for(; i!=iend; ++i) {
Expr c, v;
separateMonomial(*i, c, v);
isIntRHS.push_back(isIntegerThm(v));
DebugAssert(!isIntRHS.back().isNull(), "");
}
}
// Derive (EXISTS (x:INT): x = t2 AND 0 = t3)
result = d_rules->eqElimIntRule(result, isIntLHS, isIntRHS);
// Skolemize the quantifier
result = getCommonRules()->skolemize(result);
// Canonize t2 and t3 generated by this rule
DebugAssert(result.getExpr().isAnd() && result.getExpr().arity() == 2,
"processSimpleIntEq: result = "+result.getExpr().toString());
Theorem thm1 = canonPred(getCommonRules()->andElim(result, 0));
Theorem thm2 = canonPred(getCommonRules()->andElim(result, 1));
Theorem newRes = getCommonRules()->andIntro(thm1, thm2);
if(newRes.getExpr() != result.getExpr()) result = newRes;
TRACE("arith eq", "processSimpleIntEq => ", result, " }");
return result;
}
}
throw
ArithException("Can't find a leaf for solve in "+eqn.toString());
} else {
// eqn is 0 = x. Flip it and return
Theorem result = symmetryRule(eqn);
TRACE("arith eq", "processSimpleIntEq[x = 0] => ", result, " }");
return result;
}
}
/*! input is 0=e' Theorem and all of the vars in e' are of
* type INT. isolate one of them and send back to framework. output
* is "var = e''" Theorem and some associated equations in
* solved form.
*/
Theorem
TheoryArithOld::processIntEq(const Theorem& eqn)
{
TRACE("arith eq", "processIntEq(", eqn.getExpr(), ") {");
// Equations in the solved form.
std::vector solvedAndNewEqs;
Theorem newEq(eqn), result;
bool done(false);
do {
result = processSimpleIntEq(newEq);
// 'result' is of the from (x1=t1) AND 0=t'
if(result.isRewrite()) {
solvedAndNewEqs.push_back(result);
done = true;
}
else if (result.getExpr().isBoolConst()) {
done = true;
}
else {
DebugAssert(result.getExpr().isAnd() && result.getExpr().arity() == 2,
"TheoryArithOld::processIntEq("+eqn.getExpr().toString()
+")\n result = "+result.getExpr().toString());
solvedAndNewEqs.push_back(getCommonRules()->andElim(result, 0));
newEq = getCommonRules()->andElim(result, 1);
}
} while(!done);
Theorem res;
if (result.getExpr().isFalse()) res = result;
else if (solvedAndNewEqs.size() > 0)
res = solvedForm(solvedAndNewEqs);
else res = result;
TRACE("arith eq", "processIntEq => ", res.getExpr(), " }");
return res;
}
/*!
* Takes a vector of equations and for every equation x_i=t_i
* substitutes t_j for x_j in t_i for all j>i. This turns the system
* of equations into a solved form.
*
* Assumption: variables x_j may appear in the RHS terms t_i ONLY for
* i=j.
*/
Theorem
TheoryArithOld::solvedForm(const vector& solvedEqs)
{
DebugAssert(solvedEqs.size() > 0, "TheoryArithOld::solvedForm()");
// Trace code
TRACE_MSG("arith eq", "TheoryArithOld::solvedForm:solvedEqs(\n [");
IF_DEBUG(if(debugger.trace("arith eq")) {
for(vector::const_iterator j = solvedEqs.begin(),
jend=solvedEqs.end(); j!=jend;++j)
TRACE("arith eq", "", j->getExpr(), ",\n ");
})
TRACE_MSG("arith eq", " ]) {");
// End of Trace code
vector::const_reverse_iterator
i = solvedEqs.rbegin(),
iend = solvedEqs.rend();
// Substitution map: a variable 'x' is mapped to a Theorem x=t.
// This map accumulates the resulting solved form.
ExprMap subst;
for(; i!=iend; ++i) {
if(i->isRewrite()) {
Theorem thm = substAndCanonize(*i, subst);
TRACE("arith eq", "solvedForm: subst["+i->getLHS().toString()+"] = ",
thm.getExpr(), "");
subst[i->getLHS()] = thm;
}
else {
// This is the FALSE case: just return the contradiction
DebugAssert(i->getExpr().isFalse(),
"TheoryArithOld::solvedForm: an element of solvedEqs must "
"be either EQ or FALSE: "+i->toString());
return *i;
}
}
// Now we've collected the solved form in 'subst'. Wrap it up into
// a conjunction and return.
vector thms;
for(ExprMap::iterator i=subst.begin(), iend=subst.end();
i!=iend; ++i)
thms.push_back(i->second);
if (thms.size() > 1) return getCommonRules()->andIntro(thms);
else return thms.back();
}
/*!
* ASSUMPTION: 't' is a fully canonized arithmetic term, and every
* element of subst is a fully canonized equation of the form x=e,
* indexed by the LHS variable.
*/
Theorem
TheoryArithOld::substAndCanonize(const Expr& t, ExprMap& subst)
{
TRACE("arith eq", "substAndCanonize(", t, ") {");
// Quick and dirty check: return immediately if subst is empty
if(subst.empty()) {
Theorem res(reflexivityRule(t));
TRACE("arith eq", "substAndCanonize[subst empty] => ", res, " }");
return res;
}
// Check if we can substitute 't' directly
ExprMap::iterator i = subst.find(t), iend=subst.end();
if(i!=iend) {
TRACE("arith eq", "substAndCanonize[subst] => ", i->second, " }");
return i->second;
}
// The base case: t is an i-leaf
if(isLeaf(t)) {
Theorem res(reflexivityRule(t));
TRACE("arith eq", "substAndCanonize[i-leaf] => ", res, " }");
return res;
}
// 't' is an arithmetic term; recurse into the children
vector thms;
vector changed;
for(unsigned j=0, jend=t.arity(); j!=jend; ++j) {
Theorem thm = substAndCanonize(t[j], subst);
if(thm.getRHS() != t[j]) {
thm = canonThm(thm);
thms.push_back(thm);
changed.push_back(j);
}
}
// Do the actual substitution and canonize the result
Theorem res;
if(thms.size() > 0) {
res = substitutivityRule(t, changed, thms);
res = canonThm(res);
}
else
res = reflexivityRule(t);
TRACE("arith eq", "substAndCanonize => ", res, " }");
return res;
}
/*!
* ASSUMPTION: 't' is a fully canonized equation of the form x = t,
* and so is every element of subst, indexed by the LHS variable.
*/
Theorem
TheoryArithOld::substAndCanonize(const Theorem& eq, ExprMap& subst)
{
// Quick and dirty check: return immediately if subst is empty
if(subst.empty()) return eq;
DebugAssert(eq.isRewrite(), "TheoryArithOld::substAndCanonize: t = "
+eq.getExpr().toString());
const Expr& t = eq.getRHS();
// Do the actual substitution in the term t
Theorem thm = substAndCanonize(t, subst);
// Substitution had no result: return the original equation
if(thm.getRHS() == t) return eq;
// Otherwise substitute the result into the equation
vector thms;
vector changed;
thms.push_back(thm);
changed.push_back(1);
return iffMP(eq, substitutivityRule(eq.getExpr(), changed, thms));
}
void TheoryArithOld::processBuffer()
{
// Process the inequalities in the buffer
bool varOnRHS;
// If we are in difference logic only, just return
if (diffLogicOnly) return;
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())) {
// Get the unprojected inequality
Theorem ineqThm;
if (d_bufferIdx_0 < d_buffer_0.size()) {
ineqThm = d_buffer_0[d_bufferIdx_0];
d_bufferIdx_0 = d_bufferIdx_0 + 1;
} else if (d_bufferIdx_1 < d_buffer_1.size()) {
ineqThm = d_buffer_1[d_bufferIdx_1];
d_bufferIdx_1 = d_bufferIdx_1 + 1;
} else if (d_bufferIdx_2 < d_buffer_2.size()) {
ineqThm = d_buffer_2[d_bufferIdx_2];
d_bufferIdx_2 = d_bufferIdx_2 + 1;
} else {
ineqThm = d_buffer_3[d_bufferIdx_3];
d_bufferIdx_3 = d_bufferIdx_3 + 1;
}
// // Skip this inequality if it is stale
// if(isStale(ineqThm.getExpr())) {
// TRACE("arith buffer", "processBuffer(", ineqThm.getExpr(), ")... skipping stale");
// continue;
// }
// Dejan: project the finds, not the originals (if not projected already)
const Expr& inequality = ineqThm.getExpr();
Theorem inequalityFindThm = inequalityToFind(ineqThm, true);
Expr inequalityFind = inequalityFindThm.getExpr();
// if (inequality != inequalityFind)
// enqueueFact(inequalityFindThm);
TRACE("arith buffer", "processing: ", inequality, "");
TRACE("arith buffer", "with find : ", inequalityFind, "");
if (!isIneq(inequalityFind)) {
TRACE("arith buffer", "find not an inequality... ", "", "skipping");
continue;
}
if (alreadyProjected.find(inequalityFind) != alreadyProjected.end()) {
TRACE("arith buffer", "already projected ... ", "", "skipping");
continue;
}
// We put the dummy for now, isolate variable will set it properly (or the find's one)
// This one is just if the find is different. If the find is different
// We will not check it again in update, so we're fine
Expr dummy;
alreadyProjected[inequality] = dummy;
if (inequality != inequalityFind) {
alreadyProjected[inequalityFind] = dummy;
Expr rhs = inequalityFind[1];
// Collect the statistics about variables
if(isPlus(rhs)) {
for(Expr::iterator i=rhs.begin(), iend=rhs.end(); i!=iend; ++i) {
Expr monomial = *i;
updateStats(monomial);
}
} else // It's a monomial
updateStats(rhs);
}
// See if this one is subsumed by a stronger inequality
// c1 <= t1, t2 <= c2
Rational c1, c2;
Expr t1, t2;
// Every term in the buffer has to have a lower bound set!!!
// Except for the ones that changed the find
extractTermsFromInequality(inequalityFind, c1, t1, c2, t2);
if (termLowerBound.find(t1) != termLowerBound.end() && c1 != termLowerBound[t1]) {
TRACE("arith ineq", "skipping because stronger bounds asserted ", inequalityFind.toString(), ":" + t1.toString());
DebugAssert(termLowerBoundThm.find(t1) != termLowerBoundThm.end(), "No lower bound on asserted atom!!! " + t1.toString());
Theorem strongerBound = termLowerBoundThm[t1];
//enqueueFact(d_rules->implyWeakerInequality(strongerBound.getExpr(), inequalityFindThm.getExpr()));
continue;
}
Theorem thm1 = isolateVariable(inequalityFindThm, varOnRHS);
const Expr& ineq = thm1.getExpr();
if (ineq.isFalse())
setInconsistent(thm1);
else
if(!ineq.isTrue()) {
// Check that the variable is indeed isolated correctly
DebugAssert(varOnRHS? !isPlus(ineq[1]) : !isPlus(ineq[0]), "TheoryArithOld::processBuffer(): bad result from isolateVariable:\nineq = "+ineq.toString());
// Update the constained maps
updateConstrained(inequalityFindThm.getExpr());
// and project the inequality
projectInequalities(thm1, varOnRHS);
}
}
}
void TheoryArithOld::updateStats(const Rational& c, const Expr& v)
{
TRACE("arith stats", "updateStats("+c.toString()+", ", v, ")");
// we can get numbers as checking for variables is not possible (nonlinear stuff)
if (v.isRational()) return;
if (v.getType() != d_realType) {
// Dejan: update the max coefficient of the variable
if (c < 0) {
// Goes to the left side
ExprMap::iterator maxFind = maxCoefficientLeft.find(v);
if (maxFind == maxCoefficientLeft.end()) {
maxCoefficientLeft[v] = - c;
TRACE("arith stats", "max left", "", "");
}
else
if ((*maxFind).second < -c) {
TRACE("arith stats", "max left", "", "");
maxCoefficientLeft[v] = -c;
}
} else {
// Stays on the right side
ExprMap::iterator maxFind = maxCoefficientRight.find(v);
if (maxFind == maxCoefficientRight.end()) {
maxCoefficientRight[v] = c;
TRACE("arith stats", "max right", "", "");
}
else
if((*maxFind).second < c) {
TRACE("arith stats", "max right", "", "");
maxCoefficientRight[v] = c;
}
}
}
if(c > 0) {
if(d_countRight.count(v) > 0) d_countRight[v] = d_countRight[v] + 1;
else d_countRight[v] = 1;
}
else
if(d_countLeft.count(v) > 0) d_countLeft[v] = d_countLeft[v] + 1;
else d_countLeft[v] = 1;
}
void TheoryArithOld::updateStats(const Expr& monomial)
{
Expr c, m;
separateMonomial(monomial, c, m);
updateStats(c.getRational(), m);
}
int TheoryArithOld::extractTermsFromInequality(const Expr& inequality,
Rational& c1, Expr& t1,
Rational& c2, Expr& t2) {
TRACE("arith extract", "extract(", inequality.toString(), ")");
DebugAssert(isIneq(inequality), "extractTermsFromInequality: expexting an inequality got: " + inequality.getString() + ")");
Expr rhs = inequality[1];
c1 = 0;
// Extract the non-constant term (both sides)
vector positive_children, negative_children;
if (isPlus(rhs)) {
int start_i = 0;
if (rhs[0].isRational()) {
start_i = 1;
c1 = -rhs[0].getRational();
}
int end_i = rhs.arity();
for(int i = start_i; i < end_i; i ++) {
const Expr& term = rhs[i];
positive_children.push_back(term);
negative_children.push_back(canon(multExpr(rat(-1),term)).getRHS());
}
} else {
positive_children.push_back(rhs);
negative_children.push_back(canon(multExpr(rat(-1), rhs)).getRHS());
}
int num_vars = positive_children.size();
// c1 <= t1
t1 = (num_vars > 1 ? canon(plusExpr(positive_children)).getRHS() : positive_children[0]);
// c2 is the upper bound on t2 : t2 <= c2
c2 = -c1;
t2 = (num_vars > 1 ? canon(plusExpr(negative_children)).getRHS() : negative_children[0]);
TRACE("arith extract", "extract: ", c1.toString() + " <= ", t1.toString());
return num_vars;
}
bool TheoryArithOld::addToBuffer(const Theorem& thm, bool priority) {
TRACE("arith buffer", "addToBuffer(", thm.getExpr().toString(), ")");
Expr ineq = thm.getExpr();
const Expr& rhs = thm.getExpr()[1];
bool nonLinear = false;
Rational nonLinearConstant = 0;
Expr compactNonLinear;
Theorem compactNonLinearThm;
// Collect the statistics about variables and check for non-linearity
if(isPlus(rhs)) {
for(Expr::iterator i=rhs.begin(), iend=rhs.end(); i!=iend; ++i) {
Expr monomial = *i;
updateStats(monomial);
// check for non-linear
if (isMult(monomial)) {
if ((monomial[0].isRational() && monomial.arity() >= 3) ||
(!monomial[0].isRational() && monomial.arity() >= 2) ||
(monomial.arity() == 2 && isPow(monomial[1])))
nonLinear = true;
}
}
if (nonLinear) {
compactNonLinearThm = d_rules->compactNonLinearTerm(rhs);
compactNonLinear = compactNonLinearThm.getRHS();
}
}
else // It's a monomial
{
updateStats(rhs);
if (isMult(rhs))
if ((rhs[0].isRational() && rhs.arity() >= 3)
|| (!rhs[0].isRational() && rhs.arity() >= 2)
|| (rhs.arity() == 2 && isPow(rhs[1]))) {
nonLinear = true;
compactNonLinear = rhs;
compactNonLinearThm = reflexivityRule(compactNonLinear);
}
}
if (bufferedInequalities.find(ineq) != bufferedInequalities.end()) {
TRACE("arith buffer", "addToBuffer()", "", "... already in db");
if (formulaAtoms.find(ineq) != formulaAtoms.end()) {
TRACE("arith buffer", "it's a formula atom, enqueuing.", "", "");
enqueueFact(thm);
}
return false;
}
if (nonLinear && (isMult(rhs) || compactNonLinear != rhs)) {
TRACE("arith nonlinear", "compact version of ", rhs, " is " + compactNonLinear.toString());
// Replace the rhs with the compacted nonlinear term
Theorem thm1 = (compactNonLinear != rhs ?
iffMP(thm, substitutivityRule(ineq, 1, compactNonLinearThm)) : thm);
// Now, try to deduce the signednes of multipliers
Rational c = (isMult(rhs) ? 0 : compactNonLinear[0].getRational());
// We can deduct the signs if the constant is not bigger than 0
if (c <= 0) {
thm1 = d_rules->nonLinearIneqSignSplit(thm1);
TRACE("arith nonlinear", "spliting on signs : ", thm1.getExpr(), "");
enqueueFact(thm1);
}
}
// Get c1, c2, t1, t2 such that c1 <= t1 and t2 <= c2
Expr t1, t2;
Rational c1, c2;
int num_vars = extractTermsFromInequality(ineq, c1, t1, c2, t2);
// If 2 variable, do add to difference logic (allways, just in case)
bool factIsDiffLogic = false;
if (num_vars <= 2) {
TRACE("arith diff", t2, " < ", c2);
// c1 <= t1, check if difference logic
// t1 of the form 0 + ax + by
Expr ax = (num_vars == 2 ? t2[1] : t2);
Expr a_expr, x;
separateMonomial(ax, a_expr, x);
Rational a = a_expr.getRational();
Expr by = (num_vars == 2 ? t2[2] : (a < 0 ? zero : rat(-1)*zero));
Expr b_expr, y;
separateMonomial(by, b_expr, y);
Rational b = b_expr.getRational();
// Check for non-linear
if (!isLeaf(x) || !isLeaf(y))
setIncomplete("Non-linear arithmetic inequalities");
if (a == 1 && b == -1) {
diffLogicGraph.addEdge(x, y, c2, thm);
factIsDiffLogic = true;
}
else if (a == -1 && b == 1) {
diffLogicGraph.addEdge(y, x, c2, thm);
factIsDiffLogic = true;
}
// Not difference logic, put it in the 3 or more vars buffer
else {
diffLogicOnly = false;
TRACE("arith diff", "not diff logic", thm.getExpr().toString(), "");
}
if (diffLogicGraph.isUnsat()) {
TRACE("diff unsat", "UNSAT", " : ", diffLogicGraph.getUnsatTheorem());
setInconsistent(diffLogicGraph.getUnsatTheorem());
return false;
}
} else {
diffLogicOnly = false;
TRACE("arith diff", "not diff logic", thm.getExpr().toString(), "");
}
// For now we treat all the bound as LE, weaker
CDMap::iterator find_lower = termLowerBound.find(t1);
if (find_lower != termLowerBound.end()) {
// found bound c <= t1
Rational found_c = (*find_lower).second;
// If found c is bigger than the new one, we are done
if (c1 <= found_c && !(found_c == c1 && ineq.getKind() == LT)) {
TRACE("arith buffer", "addToBuffer()", "", "... lower_bound subsumed");
// Removed assert. Can happen that an atom is not asserted yet, and get's implied as
// a formula atom and then asserted here. it's fine
//DebugAssert(!thm.isAssump(), "Should have been propagated: " + ineq.toString() + "");
return false;
} else {
Theorem oldLowerBound = termLowerBoundThm[t1];
Expr oldIneq = oldLowerBound.getExpr();
if (formulaAtoms.find(oldIneq) != formulaAtoms.end())
enqueueFact(getCommonRules()->implMP(thm, d_rules->implyWeakerInequality(ineq, oldIneq)));
termLowerBound[t1] = c1;
termLowerBoundThm[t1] = thm;
}
} else {
termLowerBound[t1] = c1;
termLowerBoundThm[t1] = thm;
}
CDMap::iterator find_upper = termUpperBound.find(t2);
if (find_upper != termUpperBound.end()) {
// found bound t2 <= c
Rational found_c = (*find_upper).second;
// If found c is smaller than the new one, we are done
if (found_c <= c2 && !(found_c == c2 && ineq.getKind() == LT)) {
TRACE("arith buffer", "addToBuffer()", "", "... upper_bound subsumed");
//DebugAssert(!thm.isAssump(), "Should have been propagated: " + ineq.toString() + "");
return false;
} else {
termUpperBound[t2] = c2;
termUpperBoundThm[t2] = thm;
}
} else {
termUpperBound[t2] = c2;
termUpperBoundThm[t2] = thm;
}
// See if the bounds on the term can infer conflict or equality
if (termUpperBound.find(t1) != termUpperBound.end() &&
termLowerBound.find(t1) != termLowerBound.end() &&
termUpperBound[t1] <= termLowerBound[t1]) {
Theorem thm1 = termUpperBoundThm[t1];
Theorem thm2 = termLowerBoundThm[t1];
TRACE("arith propagate", "adding inequalities: ", thm1.getExpr().toString(), " with " + thm2.getExpr().toString());
enqueueFact(d_rules->addInequalities(thm1, thm2));
} else
if (termUpperBound.find(t2) != termUpperBound.end() &&
termLowerBound.find(t2) != termLowerBound.end() &&
termUpperBound[t2] <= termLowerBound[t2]) {
Theorem thm1 = termUpperBoundThm[t2];
Theorem thm2 = termLowerBoundThm[t2];
TRACE("arith propagate", "adding inequalities: ", thm1.getExpr().toString(), " with " + thm2.getExpr().toString());
enqueueFact(d_rules->addInequalities(thm1, thm2));
}
if (true) {
// See if we can propagate anything to the formula atoms
// c1 <= t1 ===> c <= t1 for c < c1
AtomsMap::iterator find = formulaAtomLowerBound.find(t1);
AtomsMap::iterator find_end = formulaAtomLowerBound.end();
if (find != find_end) {
set< pair >::iterator bounds = (*find).second.begin();
set< pair >::iterator bounds_end = (*find).second.end();
while (bounds != bounds_end) {
TRACE("arith atoms", "trying propagation", ineq, (*bounds).second);
const Expr& implied = (*bounds).second;
// Try to do some theory propagation
if ((*bounds).first < c1 || (!(ineq.getKind() == LE && implied.getKind() == LT) && (*bounds).first == c1)) {
// c1 <= t1 => c <= t1 (for c <= c1)
// c1 < t1 => c <= t1 (for c <= c1)
// c1 <= t1 => c < t1 (for c < c1)
Theorem impliedThm = getCommonRules()->implMP(thm, d_rules->implyWeakerInequality(ineq, implied));
enqueueFact(impliedThm);
}
bounds ++;
}
}
//
// c1 <= t1 ==> !(t1 <= c) for c < c1
// ==> !(-c <= t2)
// i.e. all coefficient in in the implied are opposite of t1
find = formulaAtomUpperBound.find(t1);
find_end = formulaAtomUpperBound.end();
if (find != find_end) {
set< pair >::iterator bounds = (*find).second.begin();
set< pair >::iterator bounds_end = (*find).second.end();
while (bounds != bounds_end) {
TRACE("arith atoms", "trying propagation", ineq, (*bounds).second);
const Expr& implied = (*bounds).second;
// Try to do some theory propagation
if ((*bounds).first < c1) {
Theorem impliedThm = getCommonRules()->implMP(thm, d_rules->implyNegatedInequality(ineq, implied));
enqueueFact(impliedThm);
}
bounds ++;
}
}
}
// Register this as a resource
theoryCore()->getResource();
// If out of resources, bail out
if (theoryCore()->outOfResources()) return false;
// Checking because we could have projected it as a find of some other
// equation
if (alreadyProjected.find(ineq) == alreadyProjected.end()) {
// We buffer it if it's not marked for not buffering
if (dontBuffer.find(ineq) == dontBuffer.end()) {
// We give priority to the one that can produce a conflict
if (priority)
d_buffer_0.push_back(thm);
else {
// Push it into the buffer (one var)
if (num_vars == 1) d_buffer_1.push_back(thm);
else if (num_vars == 2) d_buffer_2.push_back(thm);
else d_buffer_3.push_back(thm);
}
if (factIsDiffLogic) diff_logic_size = diff_logic_size + 1;
}
}
// Remember that it's in the buffer
bufferedInequalities[ineq] = thm;
// Since we care about this atom, lets set it up
if (!ineq.hasFind())
theoryCore()->setupTerm(ineq, this, thm);
return true;
}
Theorem TheoryArithOld::isolateVariable(const Theorem& inputThm,
bool& isolatedVarOnRHS)
{
Theorem result(inputThm);
const Expr& e = inputThm.getExpr();
TRACE("arith","isolateVariable(",e,") {");
TRACE("arith ineq", "isolateVariable(", e, ") {");
//we assume all the children of e are canonized
DebugAssert(isLT(e)||isLE(e),
"TheoryArithOld::isolateVariable: " + e.toString() +
" wrong kind");
int kind = e.getKind();
DebugAssert(e[0].isRational() && e[0].getRational() == 0,
"TheoryArithOld::isolateVariable: theorem must be of "
"the form 0 < rhs: " + inputThm.toString());
const Expr& zero = e[0];
Expr right = e[1];
// Check for trivial in-equation.
if (right.isRational()) {
result = iffMP(result, d_rules->constPredicate(e));
TRACE("arith ineq","isolateVariable => ",result.getExpr()," }");
TRACE("arith","isolateVariable => ",result," }");
return result;
}
// Normalization of inequality to make coefficients integer and
// relatively prime.
Expr factor(computeNormalFactor(right, false));
TRACE("arith", "isolateVariable: factor = ", factor, "");
DebugAssert(factor.getRational() > 0,
"isolateVariable: factor="+factor.toString());
// Now multiply the inequality by the factor, unless it is 1
if(factor.getRational() != 1) {
result = iffMP(result, d_rules->multIneqn(e, factor));
// And canonize the result
result = canonPred(result);
result = rafineInequalityToInteger(result);
right = result.getExpr()[1];
}
// Find monomial to isolate and store it in isolatedMonomial
Expr isolatedMonomial = right;
if (isPlus(right))
isolatedMonomial = pickMonomial(right);
TRACE("arith ineq", "isolatedMonomial => ",isolatedMonomial,"");
// Set the correct isolated monomial
// Now, if something gets updated, but this monomial is not changed, we don't
// Have to rebuffer it as the projection will still be accurate when updated
alreadyProjected[e] = isolatedMonomial;
Rational r = -1;
isolatedVarOnRHS = true;
if (isMult(isolatedMonomial)) {
r = ((isolatedMonomial[0].getRational()) >= 0)? -1 : 1;
isolatedVarOnRHS =
((isolatedMonomial[0].getRational()) >= 0)? true : false;
}
isolatedMonomial = canon(rat(-1)*isolatedMonomial).getRHS();
TRACE("arith ineq", "-(isolatedMonomial) => ",isolatedMonomial,"");
// Isolate isolatedMonomial on to the LHS
result = iffMP(result, d_rules->plusPredicate(zero, right,
isolatedMonomial, kind));
// Canonize the resulting inequality
TRACE("arith ineq", "resutl => ",result,"");
result = canonPred(result);
if(1 != r) {
result = iffMP(result, d_rules->multIneqn(result.getExpr(), rat(r)));
result = canonPred(result);
}
TRACE("arith ineq","isolateVariable => ",result.getExpr()," }");
TRACE("arith","isolateVariable => ",result," }");
return result;
}
Expr
TheoryArithOld::computeNormalFactor(const Expr& right, bool normalizeConstants) {
// Strategy: compute f = lcm(d1...dn)/gcd(c1...cn), where the RHS is
// of the form c1/d1*x1 + ... + cn/dn*xn
Rational factor;
if(isPlus(right)) {
vector nums, denoms;
for(int i=0, iend=right.arity(); i fc.getConst() ||
(c == fc.getConst() && strict && !fc.strict()));
}
bool res;
if(subsumed) {
res = true;
TRACE("arith ineq", "isStale[subsumed] => ", res? "true" : "false", " }");
}
else {
res = isStale(ineqExpr);
TRACE("arith ineq", "isStale[updated] => ", res? "true" : "false", " }");
}
return res;
}
void TheoryArithOld::separateMonomial(const Expr& e, Expr& c, Expr& var) {
TRACE("separateMonomial", "separateMonomial(", e, ")");
DebugAssert(!isPlus(e),
"TheoryArithOld::separateMonomial(e = "+e.toString()+")");
if(isMult(e)) {
DebugAssert(e.arity() >= 2,
"TheoryArithOld::separateMonomial(e = "+e.toString()+")");
c = e[0];
if(e.arity() == 2) var = e[1];
else {
vector kids = e.getKids();
kids[0] = rat(1);
var = multExpr(kids);
}
} else {
c = rat(1);
var = e;
}
DebugAssert(c.isRational(), "TheoryArithOld::separateMonomial(e = "
+e.toString()+", c = "+c.toString()+")");
DebugAssert(!isMult(var) || (var[0].isRational() && var[0].getRational()==1),
"TheoryArithOld::separateMonomial(e = "
+e.toString()+", var = "+var.toString()+")");
}
void TheoryArithOld::projectInequalities(const Theorem& theInequality,
bool isolatedVarOnRHS)
{
TRACE("arith project", "projectInequalities(", theInequality.getExpr(),
", isolatedVarOnRHS="+string(isolatedVarOnRHS? "true" : "false")
+") {");
DebugAssert(isLE(theInequality.getExpr()) ||
isLT(theInequality.getExpr()),
"TheoryArithOld::projectIsolatedVar: "\
"theInequality is of the wrong form: " +
theInequality.toString());
//TODO: DebugAssert to check if the isolatedMonomial is of the right
//form and the whether we are indeed getting inequalities.
Theorem theIneqThm(theInequality);
Expr theIneq = theIneqThm.getExpr();
// If the inequality is strict and integer, change it to non-strict
if(isLT(theIneq)) {
Theorem isIntLHS(isIntegerThm(theIneq[0]));
Theorem isIntRHS(isIntegerThm(theIneq[1]));
if ((!isIntLHS.isNull() && !isIntRHS.isNull())) {
Theorem thm = d_rules->lessThanToLE(theInequality, isIntLHS, isIntRHS, !isolatedVarOnRHS);
theIneqThm = canonPred(iffMP(theIneqThm, thm));
theIneq = theIneqThm.getExpr();
}
}
Expr isolatedMonomial = isolatedVarOnRHS ? theIneq[1] : theIneq[0];
Expr monomialVar, a;
separateMonomial(isolatedMonomial, a, monomialVar);
bool subsumed;
const FreeConst& bestConst = updateSubsumptionDB(theIneq, isolatedVarOnRHS, subsumed);
if(subsumed) {
IF_DEBUG(debugger.counter("subsumed inequalities")++;)
TRACE("arith ineq", "subsumed inequality: ", theIneq, "");
} else {
// If the isolated variable is actually a non-linear term, we are
// incomplete
if(isMult(monomialVar) || isPow(monomialVar))
setIncomplete("Non-linear arithmetic inequalities");
// First, we need to make sure the isolated inequality is
// setup properly.
// setupRec(theIneq[0]);
// setupRec(theIneq[1]);
theoryCore()->setupTerm(theIneq[0], this, theIneqThm);
theoryCore()->setupTerm(theIneq[1], this, theIneqThm);
// Add the inequality into the appropriate DB.
ExprMap *>& db1 = isolatedVarOnRHS ? d_inequalitiesRightDB : d_inequalitiesLeftDB;
ExprMap *>::iterator it1 = db1.find(monomialVar);
if(it1 == db1.end()) {
CDList * list = new(true) CDList(theoryCore()->getCM()->getCurrentContext());
list->push_back(Ineq(theIneqThm, isolatedVarOnRHS, bestConst));
db1[monomialVar] = list;
}
else
((*it1).second)->push_back(Ineq(theIneqThm, isolatedVarOnRHS, bestConst));
ExprMap *>& db2 = isolatedVarOnRHS ? d_inequalitiesLeftDB : d_inequalitiesRightDB;
ExprMap *>::iterator it = db2.find(monomialVar);
if(it == db2.end()) {
TRACE_MSG("arith ineq", "projectInequalities[not in DB] => }");
return;
}
CDList& listOfDBIneqs = *((*it).second);
Theorem betaLTt, tLTalpha, thm;
for(int i = listOfDBIneqs.size() - 1; !inconsistent() && i >= 0; --i) {
const Ineq& ineqEntry = listOfDBIneqs[i];
const Theorem& ineqThm = ineqEntry.ineq(); //inequalityToFind(ineqEntry.ineq(), isolatedVarOnRHS);
// ineqExntry might be stale
if(!isStale(ineqEntry)) {
betaLTt = isolatedVarOnRHS ? theIneqThm : ineqThm;
tLTalpha = isolatedVarOnRHS ? ineqThm : theIneqThm;
thm = normalizeProjectIneqs(betaLTt, tLTalpha);
if (thm.isNull()) continue;
IF_DEBUG(debugger.counter("real shadows")++;)
// Check for TRUE and FALSE theorems
Expr e(thm.getExpr());
if(e.isFalse()) {
setInconsistent(thm);
TRACE_MSG("arith ineq", "projectInequalities[inconsistent] => }");
return;
}
else {
if(!e.isTrue() && !e.isEq()) {
// setup the term so that it comes out in updates
addToBuffer(thm, false);
}
else if(e.isEq())
enqueueFact(thm);
}
} else {
IF_DEBUG(debugger.counter("stale inequalities")++;)
}
}
}
TRACE_MSG("arith ineq", "projectInequalities => }");
}
Theorem TheoryArithOld::normalizeProjectIneqs(const Theorem& ineqThm1,
const Theorem& ineqThm2)
{
//ineq1 is of the form beta < b.x or beta < x [ or with <= ]
//ineq2 is of the form a.x < alpha or x < alpha.
Theorem betaLTt = ineqThm1, tLTalpha = ineqThm2;
Expr ineq1 = betaLTt.getExpr();
Expr ineq2 = tLTalpha.getExpr();
Expr c,x;
separateMonomial(ineq2[0], c, x);
Theorem isIntx(isIntegerThm(x));
Theorem isIntBeta(isIntegerThm(ineq1[0]));
Theorem isIntAlpha(isIntegerThm(ineq2[1]));
bool isInt = !(isIntx.isNull() || isIntBeta.isNull() || isIntAlpha.isNull());
TRACE("arith ineq", "normalizeProjectIneqs(", ineq1,
", "+ineq2.toString()+") {");
DebugAssert((isLE(ineq1) || isLT(ineq1)) &&
(isLE(ineq2) || isLT(ineq2)),
"TheoryArithOld::normalizeProjectIneqs: Wrong Kind inputs: " +
ineq1.toString() + ineq2.toString());
DebugAssert(!isPlus(ineq1[1]) && !isPlus(ineq2[0]),
"TheoryArithOld::normalizeProjectIneqs: Wrong Kind inputs: " +
ineq1.toString() + ineq2.toString());
//compute the factors to multiply the two inequalities with
//so that they get the form beta < t and t < alpha.
Rational factor1 = 1, factor2 = 1;
Rational b = isMult(ineq1[1]) ? (ineq1[1])[0].getRational() : 1;
Rational a = isMult(ineq2[0]) ? (ineq2[0])[0].getRational() : 1;
if(b != a) {
factor1 = a;
factor2 = b;
}
//if the ineqs are of type int then apply one of the gray
//dark shadow rules.
// FIXME: intResult should also be checked for immediate
// optimizations, as those below for 'result'. Also, if intResult
// is a single inequality, we may want to handle it similarly to the
// 'result' rather than enqueuing directly.
if(isInt && (a >= 2 || b >= 2)) {
Theorem intResult;
if(a <= b)
intResult = d_rules->darkGrayShadow2ab(betaLTt, tLTalpha,
isIntAlpha, isIntBeta, isIntx);
else
intResult = d_rules->darkGrayShadow2ba(betaLTt, tLTalpha,
isIntAlpha, isIntBeta, isIntx);
enqueueFact(intResult);
// Fetch dark and gray shadows
const Expr& DorG = intResult.getExpr();
DebugAssert(DorG.isOr() && DorG.arity()==2, "DorG = "+DorG.toString());
const Expr& G = DorG[1];
DebugAssert(G.getKind()==GRAY_SHADOW, "G = "+G.toString());
// Set the higher splitter priority for dark shadow
// Expr tmp = simplifyExpr(D);
// if (!tmp.isBoolConst())
// addSplitter(tmp, 5);
// Also set a higher priority to the NEGATION of GRAY_SHADOW
Expr tmp = simplifyExpr(!G);
if (!tmp.isBoolConst())
addSplitter(tmp, 1);
IF_DEBUG(debugger.counter("dark+gray shadows")++;)
// Dejan: Let's forget about the real shadow, we are doing integers
// /return intResult;
}
//actually normalize the inequalities
if(1 != factor1) {
Theorem thm2 = iffMP(betaLTt, d_rules->multIneqn(ineq1, rat(factor1)));
betaLTt = canonPred(thm2);
ineq1 = betaLTt.getExpr();
}
if(1 != factor2) {
Theorem thm2 = iffMP(tLTalpha, d_rules->multIneqn(ineq2, rat(factor2)));
tLTalpha = canonPred(thm2);
ineq2 = tLTalpha.getExpr();
}
//IF_DEBUG(debugger.counter("real shadows")++;)
Expr beta(ineq1[0]);
Expr alpha(ineq2[1]);
// In case of alpha <= t <= alpha, we generate t = alpha
if(isLE(ineq1) && isLE(ineq2) && alpha == beta) {
Theorem result = d_rules->realShadowEq(betaLTt, tLTalpha);
TRACE("arith ineq", "normalizeProjectIneqs => ", result, " }");
return result;
}
// Check if this inequality is a finite interval
// if(isInt)
// processFiniteInterval(betaLTt, tLTalpha);
// // Only do the real shadow if a and b = 1
// if (isInt && a > 1 && b > 1)
// return Theorem();
//project the normalized inequalities.
Theorem result = d_rules->realShadow(betaLTt, tLTalpha);
// FIXME: Clark's changes. Is 'rewrite' more or less efficient?
// result = iffMP(result, rewrite(result.getExpr()));
// TRACE("arith ineq", "normalizeProjectIneqs => ", result, " }");
// Now, transform the result into 0 < rhs and see if rhs is a const
Expr e(result.getExpr());
// int kind = e.getKind();
if(!(e[0].isRational() && e[0].getRational() == 0))
result = iffMP(result, d_rules->rightMinusLeft(e));
result = canonPred(result);
//result is "0 kind e'". where e' is equal to canon(e[1]-e[0])
Expr right = result.getExpr()[1];
// Check for trivial inequality
if (right.isRational())
result = iffMP(result, d_rules->constPredicate(result.getExpr()));
else
result = normalize(result);
TRACE("arith ineq", "normalizeProjectIneqs => ", result, " }");
return result;
}
Rational TheoryArithOld::currentMaxCoefficient(Expr var)
{
// We prefer real variables
if (var.getType() == d_realType) return -100;
// Find the biggest left side coefficient
ExprMap::iterator findMaxLeft = maxCoefficientLeft.find(var);
Rational leftMax = -1;
if (findMaxLeft != maxCoefficientLeft.end())
leftMax = (*findMaxLeft).second;
//
ExprMap::iterator findMaxRight = maxCoefficientRight.find(var);
Rational rightMax = -1;
if (findMaxRight != maxCoefficientRight.end())
rightMax = (*findMaxRight).second;
// What is the max coefficient
// If one is undefined, dont take it. My first thought was to project away unbounded
// ones, but it happens that you get another constraint on it later and the hell breaks
// loose if they have big coefficients.
Rational returnValue;
if (leftMax == -1) returnValue = rightMax;
else if (rightMax == -1) returnValue = leftMax;
else if (leftMax < rightMax) returnValue = rightMax;
else returnValue = leftMax;
TRACE("arith stats", "max coeff of ", var.toString(), ": " + returnValue.toString() + "(left=" + leftMax.toString() + ",right=" + rightMax.toString());
return returnValue;
}
void TheoryArithOld::fixCurrentMaxCoefficient(Expr var, Rational max) {
fixedMaxCoefficient[var] = max;
}
void TheoryArithOld::selectSmallestByCoefficient(const vector& input, vector& output) {
// Clear the output vector
output.clear();
// Get the first variable, and set it as best
Expr best_variable = input[0];
Rational best_coefficient = currentMaxCoefficient(best_variable);
output.push_back(best_variable);
for(unsigned int i = 1; i < input.size(); i ++) {
// Get the current variable
Expr current_variable = input[i];
// Get the current variable's max coefficient
Rational current_coefficient = currentMaxCoefficient(current_variable);
// If strictly better than the current best, remember it
if ((current_coefficient < best_coefficient)) {
best_variable = current_variable;
best_coefficient = current_coefficient;
output.clear();
}
// If equal to the current best, push it to the stack (in 10% range)
if (current_coefficient == best_coefficient)
output.push_back(current_variable);
}
// Fix the selected best coefficient
//fixCurrentMaxCoefficient(best_variable, best_coefficient);
}
Expr TheoryArithOld::pickMonomial(const Expr& right)
{
DebugAssert(isPlus(right), "TheoryArithOld::pickMonomial: Wrong Kind: " +
right.toString());
if(theoryCore()->getFlags()["var-order"].getBool()) {
Expr::iterator i = right.begin();
Expr isolatedMonomial = right[1];
//PLUS always has at least two elements and the first element is
//always a constant. hence ++i in the initialization of the for
//loop.
for(++i; i != right.end(); ++i)
if(lessThanVar(isolatedMonomial,*i))
isolatedMonomial = *i;
return isolatedMonomial;
}
ExprMap var2monomial;
vector vars;
Expr::iterator i = right.begin(), iend = right.end();
for(;i != iend; ++i) {
if(i->isRational())
continue;
Expr c, var;
separateMonomial(*i, c, var);
var2monomial[var] = *i;
vars.push_back(var);
}
vector largest;
d_graph.selectLargest(vars, largest);
DebugAssert(0 < largest.size(),
"TheoryArithOld::pickMonomial: selectLargest: failed!!!!");
// DEJAN: Rafine the largest by coefficient values
vector largest_small_coeff;
selectSmallestByCoefficient(largest, largest_small_coeff);
DebugAssert(0 < largest_small_coeff.size(), "TheoryArithOld::pickMonomial: selectLargestByCOefficient: failed!!!!");
size_t pickedVar = 0;
// Pick the variable which will generate the fewest number of
// projections
size_t size = largest_small_coeff.size();
int minProjections = -1;
if (size > 1)
for(size_t k=0; k< size; ++k) {
const Expr& var(largest_small_coeff[k]), monom(var2monomial[var]);
// Grab the counters for the variable
int nRight = (d_countRight.count(var) > 0)? d_countRight[var] : 0;
int nLeft = (d_countLeft.count(var) > 0)? d_countLeft[var] : 0;
int n(nRight*nLeft);
TRACE("arith ineq", "pickMonomial: var=", var,
", nRight="+int2string(nRight)+", nLeft="+int2string(nLeft));
if(minProjections < 0 || minProjections > n) {
minProjections = n;
pickedVar = k;
}
TRACE("arith ineq", "Number of projections for "+var.toString()+" = ", n, "");
}
const Expr& largestVar = largest_small_coeff[pickedVar];
// FIXME: TODO: update the counters (subtract counts for the vars
// other than largestVar
// Update the graph (all edges to the largest in the graph, not just the small coefficients).
for(size_t k = 0; k < vars.size(); ++k) {
if(vars[k] != largestVar)
d_graph.addEdge(largestVar, vars[k]);
}
TRACE("arith buffer", "picked var : ", var2monomial[largestVar].toString(), "");
return var2monomial[largestVar];
}
void TheoryArithOld::VarOrderGraph::addEdge(const Expr& e1, const Expr& e2)
{
TRACE("arith var order", "addEdge("+e1.toString()+" > ", e2, ")");
DebugAssert(e1 != e2, "TheoryArithOld::VarOrderGraph::addEdge("
+e1.toString()+", "+e2.toString()+")");
d_edges[e1].push_back(e2);
}
//returns true if e1 < e2, else false(i.e e2 < e1 or e1,e2 are not
//comparable)
bool TheoryArithOld::VarOrderGraph::lessThan(const Expr& e1, const Expr& e2)
{
d_cache.clear();
//returns true if e1 is in the subtree rooted at e2 implying e1 < e2
return dfs(e1,e2);
}
//returns true if e1 is in the subtree rooted at e2 implying e1 < e2
bool TheoryArithOld::VarOrderGraph::dfs(const Expr& e1, const Expr& e2)
{
if(e1 == e2)
return true;
if(d_cache.count(e2) > 0)
return false;
if(d_edges.count(e2) == 0)
return false;
d_cache[e2] = true;
vector& e2Edges = d_edges[e2];
vector::iterator i = e2Edges.begin();
vector::iterator iend = e2Edges.end();
//if dfs finds e1 then i != iend else i is equal to iend
for(; i != iend && !dfs(e1,*i); ++i);
return (i != iend);
}
void TheoryArithOld::VarOrderGraph::dfs(const Expr& v, vector& output_list)
{
TRACE("arith shared", "dfs(", v.toString(), ")");
// If visited already we are done
if (d_cache.count(v) > 0) return;
// Dfs further
if(d_edges.count(v) != 0) {
// We have edges, so lets dfs it further
vector& vEdges = d_edges[v];
vector::iterator e = vEdges.begin();
vector::iterator e_end = vEdges.end();
while (e != e_end) {
dfs(*e, output_list);
e ++;
}
}
// Mark as visited and add to the output list
d_cache[v] = true;
output_list.push_back(v);
}
void TheoryArithOld::VarOrderGraph::getVerticesTopological(vector& output_list)
{
// Clear the cache
d_cache.clear();
output_list.clear();
// Go through all the vertices and run a dfs from them
ExprMap< vector >::iterator v_it = d_edges.begin();
ExprMap< vector >::iterator v_it_end = d_edges.end();
while (v_it != v_it_end)
{
// Run dfs from this vertex
dfs(v_it->first, output_list);
// Go to the next one
v_it ++;
}
}
void TheoryArithOld::VarOrderGraph::selectSmallest(vector& v1,
vector& v2)
{
int v1Size = v1.size();
vector v3(v1Size);
for(int j=0; j < v1Size; ++j)
v3[j] = false;
for(int j=0; j < v1Size; ++j) {
if(v3[j]) continue;
for(int i =0; i < v1Size; ++i) {
if((i == j) || v3[i])
continue;
if(lessThan(v1[i],v1[j])) {
v3[j] = true;
break;
}
}
}
vector new_v1;
for(int j = 0; j < v1Size; ++j)
if(!v3[j]) v2.push_back(v1[j]);
else new_v1.push_back(v1[j]);
v1 = new_v1;
}
void TheoryArithOld::VarOrderGraph::selectLargest(const vector& v1,
vector& v2)
{
int v1Size = v1.size();
vector v3(v1Size);
for(int j=0; j < v1Size; ++j)
v3[j] = false;
for(int j=0; j < v1Size; ++j) {
if(v3[j]) continue;
for(int i =0; i < v1Size; ++i) {
if((i == j) || v3[i])
continue;
if(lessThan(v1[j],v1[i])) {
v3[j] = true;
break;
}
}
}
for(int j = 0; j < v1Size; ++j)
if(!v3[j]) v2.push_back(v1[j]);
}
///////////////////////////////////////////////////////////////////////////////
// TheoryArithOld Public Methods //
///////////////////////////////////////////////////////////////////////////////
TheoryArithOld::TheoryArithOld(TheoryCore* core)
: TheoryArith(core, "ArithmeticOld"),
d_diseq(core->getCM()->getCurrentContext()),
d_diseqIdx(core->getCM()->getCurrentContext(), 0, 0),
diseqSplitAlready(core->getCM()->getCurrentContext()),
d_inModelCreation(core->getCM()->getCurrentContext(), false, 0),
d_freeConstDB(core->getCM()->getCurrentContext()),
d_buffer_0(core->getCM()->getCurrentContext()),
d_buffer_1(core->getCM()->getCurrentContext()),
d_buffer_2(core->getCM()->getCurrentContext()),
d_buffer_3(core->getCM()->getCurrentContext()),
// Initialize index to 0 at scope 0
d_bufferIdx_0(core->getCM()->getCurrentContext(), 0, 0),
d_bufferIdx_1(core->getCM()->getCurrentContext(), 0, 0),
d_bufferIdx_2(core->getCM()->getCurrentContext(), 0, 0),
d_bufferIdx_3(core->getCM()->getCurrentContext(), 0, 0),
diff_logic_size(core->getCM()->getCurrentContext(), 0, 0),
d_bufferThres(&(core->getFlags()["ineq-delay"].getInt())),
d_splitSign(&(core->getFlags()["nonlinear-sign-split"].getBool())),
d_grayShadowThres(&(core->getFlags()["grayshadow-threshold"].getInt())),
d_countRight(core->getCM()->getCurrentContext()),
d_countLeft(core->getCM()->getCurrentContext()),
d_sharedTerms(core->getCM()->getCurrentContext()),
d_sharedTermsList(core->getCM()->getCurrentContext()),
d_sharedVars(core->getCM()->getCurrentContext()),
bufferedInequalities(core->getCM()->getCurrentContext()),
termLowerBound(core->getCM()->getCurrentContext()),
termLowerBoundThm(core->getCM()->getCurrentContext()),
termUpperBound(core->getCM()->getCurrentContext()),
termUpperBoundThm(core->getCM()->getCurrentContext()),
alreadyProjected(core->getCM()->getCurrentContext()),
dontBuffer(core->getCM()->getCurrentContext()),
diffLogicOnly(core->getCM()->getCurrentContext(), true, 0),
diffLogicGraph(0, core, 0, core->getCM()->getCurrentContext()),
shared_index_1(core->getCM()->getCurrentContext(), 0, 0),
shared_index_2(core->getCM()->getCurrentContext(), 0, 0),
termUpperBounded(core->getCM()->getCurrentContext()),
termLowerBounded(core->getCM()->getCurrentContext()),
d_varConstrainedPlus(core->getCM()->getCurrentContext()),
d_varConstrainedMinus(core->getCM()->getCurrentContext()),
termConstrainedBelow(core->getCM()->getCurrentContext()),
termConstrainedAbove(core->getCM()->getCurrentContext())
{
IF_DEBUG(d_diseq.setName("CDList[TheoryArithOld::d_diseq]");)
IF_DEBUG(d_buffer_0.setName("CDList[TheoryArithOld::d_buffer_0]");)
IF_DEBUG(d_buffer_1.setName("CDList[TheoryArithOld::d_buffer_1]");)
IF_DEBUG(d_buffer_2.setName("CDList[TheoryArithOld::d_buffer_2]");)
IF_DEBUG(d_buffer_3.setName("CDList[TheoryArithOld::d_buffer_3]");)
IF_DEBUG(d_bufferIdx_1.setName("CDList[TheoryArithOld::d_bufferIdx_0]");)
IF_DEBUG(d_bufferIdx_1.setName("CDList[TheoryArithOld::d_bufferIdx_1]");)
IF_DEBUG(d_bufferIdx_2.setName("CDList[TheoryArithOld::d_bufferIdx_2]");)
IF_DEBUG(d_bufferIdx_3.setName("CDList[TheoryArithOld::d_bufferIdx_3]");)
getEM()->newKind(REAL, "_REAL", true);
getEM()->newKind(INT, "_INT", true);
getEM()->newKind(SUBRANGE, "_SUBRANGE", true);
getEM()->newKind(UMINUS, "_UMINUS");
getEM()->newKind(PLUS, "_PLUS");
getEM()->newKind(MINUS, "_MINUS");
getEM()->newKind(MULT, "_MULT");
getEM()->newKind(DIVIDE, "_DIVIDE");
getEM()->newKind(POW, "_POW");
getEM()->newKind(INTDIV, "_INTDIV");
getEM()->newKind(MOD, "_MOD");
getEM()->newKind(LT, "_LT");
getEM()->newKind(LE, "_LE");
getEM()->newKind(GT, "_GT");
getEM()->newKind(GE, "_GE");
getEM()->newKind(IS_INTEGER, "_IS_INTEGER");
getEM()->newKind(NEGINF, "_NEGINF");
getEM()->newKind(POSINF, "_POSINF");
getEM()->newKind(DARK_SHADOW, "_DARK_SHADOW");
getEM()->newKind(GRAY_SHADOW, "_GRAY_SHADOW");
getEM()->newKind(REAL_CONST, "_REAL_CONST");
d_kinds.push_back(REAL);
d_kinds.push_back(INT);
d_kinds.push_back(SUBRANGE);
d_kinds.push_back(IS_INTEGER);
d_kinds.push_back(UMINUS);
d_kinds.push_back(PLUS);
d_kinds.push_back(MINUS);
d_kinds.push_back(MULT);
d_kinds.push_back(DIVIDE);
d_kinds.push_back(POW);
d_kinds.push_back(INTDIV);
d_kinds.push_back(MOD);
d_kinds.push_back(LT);
d_kinds.push_back(LE);
d_kinds.push_back(GT);
d_kinds.push_back(GE);
d_kinds.push_back(RATIONAL_EXPR);
d_kinds.push_back(NEGINF);
d_kinds.push_back(POSINF);
d_kinds.push_back(DARK_SHADOW);
d_kinds.push_back(GRAY_SHADOW);
d_kinds.push_back(REAL_CONST);
registerTheory(this, d_kinds, true);
d_rules = createProofRulesOld();
diffLogicGraph.setRules(d_rules);
diffLogicGraph.setArith(this);
d_realType = Type(getEM()->newLeafExpr(REAL));
d_intType = Type(getEM()->newLeafExpr(INT));
// Make the zero variable
Theorem thm_exists_zero = getCommonRules()->varIntroSkolem(rat(0));
zero = thm_exists_zero.getExpr()[1];
}
// Destructor: delete the proof rules class if it's present
TheoryArithOld::~TheoryArithOld() {
if(d_rules != NULL) delete d_rules;
// Clear the inequality databases
for(ExprMap *>::iterator i=d_inequalitiesRightDB.begin(),
iend=d_inequalitiesRightDB.end(); i!=iend; ++i) {
delete (i->second);
free(i->second);
}
for(ExprMap *>::iterator i=d_inequalitiesLeftDB.begin(),
iend=d_inequalitiesLeftDB.end(); i!=iend; ++i) {
delete (i->second);
free (i->second);
}
unregisterTheory(this, d_kinds, true);
}
void TheoryArithOld::collectVars(const Expr& e, vector& vars,
set& cache) {
// Check the cache first
if(cache.count(e) > 0) return;
// Not processed yet. Cache the expression and proceed
cache.insert(e);
if(isLeaf(e)) vars.push_back(e);
else
for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i)
collectVars(*i, vars, cache);
}
void
TheoryArithOld::processFiniteInterval
(const Theorem& alphaLEax,
const Theorem& bxLEbeta) {
const Expr& ineq1(alphaLEax.getExpr());
const Expr& ineq2(bxLEbeta.getExpr());
DebugAssert(isLE(ineq1), "TheoryArithOld::processFiniteInterval: ineq1 = "
+ineq1.toString());
DebugAssert(isLE(ineq2), "TheoryArithOld::processFiniteInterval: ineq2 = "
+ineq2.toString());
// If the inequalities are not integer, just return (nothing to do)
if(!isInteger(ineq1[0])
|| !isInteger(ineq1[1])
|| !isInteger(ineq2[0])
|| !isInteger(ineq2[1]))
return;
const Expr& ax = ineq1[1];
const Expr& bx = ineq2[0];
DebugAssert(!isPlus(ax) && !isRational(ax),
"TheoryArithOld::processFiniteInterval:\n ax = "+ax.toString());
DebugAssert(!isPlus(bx) && !isRational(bx),
"TheoryArithOld::processFiniteInterval:\n bx = "+bx.toString());
Expr a = isMult(ax)? ax[0] : rat(1);
Expr b = isMult(bx)? bx[0] : rat(1);
Theorem thm1(alphaLEax), thm2(bxLEbeta);
// Multiply the inequalities by 'b' and 'a', and canonize them, if necessary
if(a != b) {
thm1 = canonPred(iffMP(alphaLEax, d_rules->multIneqn(ineq1, b)));
thm2 = canonPred(iffMP(bxLEbeta, d_rules->multIneqn(ineq2, a)));
}
// Check that a*beta - b*alpha == c > 0
const Expr& alphaLEt = thm1.getExpr();
const Expr& alpha = alphaLEt[0];
const Expr& t = alphaLEt[1];
const Expr& beta = thm2.getExpr()[1];
Expr c = canon(beta - alpha).getRHS();
if(c.isRational() && c.getRational() >= 1) {
// This is a finite interval. First, derive t <= alpha + c:
// canon(alpha+c) => (alpha+c == beta) ==> [symmetry] beta == alpha+c
// Then substitute that in thm2
Theorem bEQac = symmetryRule(canon(alpha + c));
// Substitute beta == alpha+c for the second child of thm2
vector changed;
vector thms;
changed.push_back(1);
thms.push_back(bEQac);
Theorem tLEac = substitutivityRule(thm2.getExpr(), changed, thms);
tLEac = iffMP(thm2, tLEac);
// Derive and enqueue the finite interval constraint
Theorem isInta(isIntegerThm(alpha));
Theorem isIntt(isIntegerThm(t));
if (d_sharedTerms.find(thm1.getExpr()[1]) != d_sharedTerms.end())
enqueueFact(d_rules->finiteInterval(thm1, tLEac, isInta, isIntt));
}
}
void
TheoryArithOld::processFiniteIntervals(const Expr& x) {
// If x is not integer, do not bother
if(!isInteger(x)) return;
// Process every pair of the opposing inequalities for 'x'
ExprMap *>::iterator iLeft, iRight;
iLeft = d_inequalitiesLeftDB.find(x);
if(iLeft == d_inequalitiesLeftDB.end()) return;
iRight = d_inequalitiesRightDB.find(x);
if(iRight == d_inequalitiesRightDB.end()) return;
// There are some opposing inequalities; get the lists
CDList& ineqsLeft = *(iLeft->second);
CDList& ineqsRight = *(iRight->second);
// Get the sizes of the lists
size_t sizeLeft = ineqsLeft.size();
size_t sizeRight = ineqsRight.size();
// Process all the pairs of the opposing inequalities
for(size_t l=0; lwithout
* caching until it hits a node that is already setup. Be
* careful on what expressions you are calling it.
*/
void
TheoryArithOld::setupRec(const Expr& e) {
if(e.hasFind()) return;
// First, set up the kids recursively
for (int k = 0; k < e.arity(); ++k) {
setupRec(e[k]);
}
// Create a find pointer for e
e.setFind(reflexivityRule(e));
e.setEqNext(reflexivityRule(e));
// And call our own setup()
setup(e);
}
void TheoryArithOld::addSharedTerm(const Expr& e) {
return;
if (d_sharedTerms.find(e) == d_sharedTerms.end()) {
d_sharedTerms[e] = true;
d_sharedTermsList.push_back(e);
}
}
void TheoryArithOld::assertFact(const Theorem& e)
{
TRACE("arith assert", "assertFact(", e.getExpr().toString(), ")");
// Pick up any multiplicative case splits and enqueue them
for (unsigned i = 0; i < multiplicativeSignSplits.size(); i ++)
enqueueFact(multiplicativeSignSplits[i]);
multiplicativeSignSplits.clear();
const Expr& expr = e.getExpr();
if (expr.isNot() && expr[0].isEq()) {
IF_DEBUG(debugger.counter("[arith] received disequalities")++;)
d_diseq.push_back(e);
}
else if (!expr.isEq()){
if (expr.isNot()) {
// If expr[0] is asserted to *not* be an integer, we track it
// so we will detect if it ever becomes equal to an integer.
if (expr[0].getKind() == IS_INTEGER) {
expr[0][0].addToNotify(this, expr[0]);
}
// This can only be negation of dark or gray shadows, or
// disequalities, which we ignore. Negations of inequalities
// are handled in rewrite, we don't even receive them here.
}
else if(isDarkShadow(expr)) {
enqueueFact(d_rules->expandDarkShadow(e));
IF_DEBUG(debugger.counter("received DARK_SHADOW")++;)
}
else if(isGrayShadow(expr)) {
IF_DEBUG(debugger.counter("received GRAY_SHADOW")++;)
const Rational& c1 = expr[2].getRational();
const Rational& c2 = expr[3].getRational();
// If gray shadow bigger than the treshold, we are done
if (*d_grayShadowThres > -1 && (c2 - c1 > *d_grayShadowThres)) {
setIncomplete("Some gray shadows ignored due to threshold");
return;
}
const Expr& v = expr[0];
const Expr& ee = expr[1];
if(c1 == c2)
enqueueFact(d_rules->expandGrayShadow0(e));
else {
Theorem gThm(e);
// Check if we can reduce the number of cases in G(ax,c,c1,c2)
if(ee.isRational() && isMult(v)
&& v[0].isRational() && v[0].getRational() >= 2) {
IF_DEBUG(debugger.counter("reduced const GRAY_SHADOW")++;)
gThm = d_rules->grayShadowConst(e);
}
// (Possibly) new gray shadow
const Expr& g = gThm.getExpr();
if(g.isFalse())
setInconsistent(gThm);
else if(g[2].getRational() == g[3].getRational())
enqueueFact(d_rules->expandGrayShadow0(gThm));
else if(g[3].getRational() - g[2].getRational() <= 5) {
// Assert c1+e <= v <= c2+e
enqueueFact(d_rules->expandGrayShadow(gThm));
// Split G into 2 cases x = l_bound and the other
Theorem thm2 = d_rules->splitGrayShadowSmall(gThm);
enqueueFact(thm2);
}
else {
// Assert c1+e <= v <= c2+e
enqueueFact(d_rules->expandGrayShadow(gThm));
// Split G into 2 cases (binary search b/w c1 and c2)
Theorem thm2 = d_rules->splitGrayShadow(gThm);
enqueueFact(thm2);
}
}
}
else {
DebugAssert(isLE(expr) || isLT(expr) || isIntPred(expr),
"expected LE or LT: "+expr.toString());
if(isLE(expr) || isLT(expr)) {
IF_DEBUG(debugger.counter("recevied inequalities")++;)
// Buffer the inequality
addToBuffer(e);
unsigned total_buf_size = d_buffer_0.size() + d_buffer_1.size() + d_buffer_2.size() + d_buffer_3.size();
unsigned processed = d_bufferIdx_0 + d_bufferIdx_1 + d_bufferIdx_2 + d_bufferIdx_3;
TRACE("arith ineq", "buffer.size() = ", total_buf_size,
", index="+int2string(processed)
+", threshold="+int2string(*d_bufferThres));
if(!diffLogicOnly && *d_bufferThres >= 0 && (total_buf_size > *d_bufferThres + processed) && !d_inModelCreation) {
processBuffer();
}
} else {
IF_DEBUG(debugger.counter("arith IS_INTEGER")++;)
if (!isInteger(expr[0])) {
enqueueFact(d_rules->IsIntegerElim(e));
}
}
}
}
else {
IF_DEBUG(debugger.counter("[arith] received t1=t2")++;)
// const Expr lhs = e.getExpr()[0];
// const Expr rhs = e.getExpr()[1];
//
// CDMap::iterator l_bound_find = termLowerBound[lhs];
// if (l_bound_find != termLowerBound.end()) {
// Rational lhs_bound = (*l_bound_find).second;
// CDMap::iterator l_bound_find_rhs = termLowerBound[rhs];
// if (l_bound_find_rhs != termLowerBound.end()) {
//
// } else {
// // Add the new bound for the rhs
// termLowerBound[rhs] = lhs_bound;
// termLowerBoundThm =
// }
//
// }
}
}
void TheoryArithOld::checkSat(bool fullEffort)
{
// vector::const_iterator e;
// vector::const_iterator eEnd;
// TODO: convert back to use iterators
TRACE("arith checksat", "checksat(fullEffort = ", fullEffort? "true, modelCreation = " : "false, modelCreation = ", (d_inModelCreation ? "true)" : "false)"));
TRACE("arith ineq", "TheoryArithOld::checkSat(fullEffort=",
fullEffort? "true" : "false", ")");
if (fullEffort) {
// Process the buffer if necessary
if (!inconsistent())
processBuffer();
if (!inconsistent()) {
// If in model creation we might have to reconsider some of the dis-equalities
if (d_inModelCreation) d_diseqIdx = 0;
// Now go and try to split
for(; d_diseqIdx < d_diseq.size(); d_diseqIdx = d_diseqIdx+1) {
// Get the disequality theorem and the expression
Theorem diseqThm = d_diseq[d_diseqIdx];
Expr diseq = diseqThm.getExpr();
// If we split on this one already
if (diseqSplitAlready.find(diseq) != diseqSplitAlready.end()) {
TRACE("arith::unconstrained", "checking disequaliy: ", diseq[0] , " already split");
continue;
}
// Get the equality
Expr eq = diseq[0];
// Get the left-hand-side and the right-hands side
Expr lhs = eq[0];
Expr rhs = eq[1];
TRACE("arith::unconstrained", "checking disequaliy: ", lhs.eqExpr(rhs) , "");
DebugAssert(lhs.hasFind() && rhs.hasFind(), "Part of dis-equality has no find!");
lhs = find(lhs).getRHS();
rhs = find(rhs).getRHS();
TRACE("arith::unconstrained", "checking disequaliy: ", lhs.eqExpr(rhs) , " after find");
// If the value of the equality is already determined by instantiation, we just skip it
// This can happen a lot as we infer equalities in difference logic
if (lhs.isRational() && rhs.isRational()) {
TRACE("arith::unconstrained", "checking disequaliy: ", lhs.eqExpr(rhs) , " skipping");
continue;
}
// We can allow ourselfs not to care about specific values if we are
// not in model creation or it's not an integer constraint
if (!d_inModelCreation) {
bool unconstrained = isUnconstrained(lhs) || isUnconstrained(rhs);
if (unconstrained) {
TRACE("arith::unconstrained", "checking disequaliy: ", lhs.eqExpr(rhs) , " unconstrained skipping");
continue;
}
bool intConstraint = !isIntegerThm(lhs).isNull() && !isIntegerThm(rhs).isNull();
if (!intConstraint) {
TRACE("arith::unconstrained", "checking disequaliy: ", lhs.eqExpr(rhs) , " not integer skipping");
continue;
}
}
TRACE("arith::unconstrained", "checking disequaliy: ", lhs.eqExpr(rhs) , " splitting");
// We don't know the value of the disequality, split on it (for now)
Theorem lemma = d_rules->diseqToIneq(diseqThm);
// Enqueue it
enqueueFact(lemma);
// Mark it as split already
diseqSplitAlready[diseq] = true;
}
}
IF_DEBUG(
{
bool dejans_printouts = false;
if (dejans_printouts) {
cerr << "Disequalities after CheckSat" << endl;
for (unsigned i = 0; i < d_diseq.size(); i ++) {
Expr diseq = d_diseq[i].getExpr();
Expr d_find = find(diseq[0]).getRHS();
cerr << diseq.toString() << ":" << d_find.toString() << endl;
}
cerr << "Arith Buffer after CheckSat (0)" << endl;
for (unsigned i = 0; i < d_buffer_0.size(); i ++) {
Expr ineq = d_buffer_0[i].getExpr();
Expr rhs = find(ineq[1]).getRHS();
cerr << ineq.toString() << ":" << rhs.toString() << endl;
}
cerr << "Arith Buffer after CheckSat (1)" << endl;
for (unsigned i = 0; i < d_buffer_1.size(); i ++) {
Expr ineq = d_buffer_1[i].getExpr();
Expr rhs = find(ineq[1]).getRHS();
cerr << ineq.toString() << ":" << rhs.toString() << endl;
}
cerr << "Arith Buffer after CheckSat (2)" << endl;
for (unsigned i = 0; i < d_buffer_2.size(); i ++) {
Expr ineq = d_buffer_2[i].getExpr();
Expr rhs = find(ineq[1]).getRHS();
cerr << ineq.toString() << ":" << rhs.toString() << endl;
}
cerr << "Arith Buffer after CheckSat (3)" << endl;
for (unsigned i = 0; i < d_buffer_3.size(); i ++) {
Expr ineq = d_buffer_3[i].getExpr();
Expr rhs = find(ineq[1]).getRHS();
cerr << ineq.toString() << ":" << rhs.toString() << endl;
}
}
}
)
}
}
void TheoryArithOld::refineCounterExample()
{
d_inModelCreation = true;
TRACE("model", "refineCounterExample[TheoryArithOld] ", "", "{");
CDMap::iterator it = d_sharedTerms.begin(), it2,
iend = d_sharedTerms.end();
// Add equalities over all pairs of shared terms as suggested
// splitters. Notice, that we want to split on equality
// (positively) first, to reduce the size of the model.
for(; it!=iend; ++it) {
// Copy by value: the elements in the pair from *it are NOT refs in CDMap
Expr e1 = (*it).first;
for(it2 = it, ++it2; it2!=iend; ++it2) {
Expr e2 = (*it2).first;
DebugAssert(isReal(getBaseType(e1)),
"TheoryArithOld::refineCounterExample: e1 = "+e1.toString()
+"\n type(e1) = "+e1.getType().toString());
if(findExpr(e1) != findExpr(e2)) {
DebugAssert(isReal(getBaseType(e2)),
"TheoryArithOld::refineCounterExample: e2 = "+e2.toString()
+"\n type(e2) = "+e2.getType().toString());
Expr eq = simplifyExpr(e1.eqExpr(e2));
if (!eq.isBoolConst()) {
addSplitter(eq);
}
}
}
}
TRACE("model", "refineCounterExample[Theory::Arith] ", "", "}");
}
void
TheoryArithOld::findRationalBound(const Expr& varSide, const Expr& ratSide,
const Expr& var,
Rational &r)
{
Expr c, x;
separateMonomial(varSide, c, x);
if (!findExpr(ratSide).isRational() && isNonlinearEq(ratSide.eqExpr(rat(0))))
throw ArithException("Could not generate the model due to non-linear arithmetic");
DebugAssert(findExpr(c).isRational(),
"seperateMonomial failed");
DebugAssert(findExpr(ratSide).isRational(),
"smallest variable in graph, should not have variables"
" in inequalities: ");
DebugAssert(x == var, "separateMonomial found different variable: "
+ var.toString());
r = findExpr(ratSide).getRational() / findExpr(c).getRational();
}
bool
TheoryArithOld::findBounds(const Expr& e, Rational& lub, Rational& glb)
{
bool strictLB=false, strictUB=false;
bool right = (d_inequalitiesRightDB.count(e) > 0
&& d_inequalitiesRightDB[e]->size() > 0);
bool left = (d_inequalitiesLeftDB.count(e) > 0
&& d_inequalitiesLeftDB[e]->size() > 0);
int numRight = 0, numLeft = 0;
if(right) { //rationals less than e
CDList * ratsLTe = d_inequalitiesRightDB[e];
for(unsigned int i=0; isize(); i++) {
DebugAssert((*ratsLTe)[i].varOnRHS(), "variable on wrong side!");
Expr ineq = (*ratsLTe)[i].ineq().getExpr();
Expr leftSide = ineq[0], rightSide = ineq[1];
Rational r;
findRationalBound(rightSide, leftSide, e , r);
if(numRight==0 || r>glb){
glb = r;
strictLB = isLT(ineq);
}
numRight++;
}
TRACE("model", " =>Lower bound ", glb.toString(), "");
}
if(left) { //rationals greater than e
CDList * ratsGTe = d_inequalitiesLeftDB[e];
for(unsigned int i=0; isize(); i++) {
DebugAssert((*ratsGTe)[i].varOnLHS(), "variable on wrong side!");
Expr ineq = (*ratsGTe)[i].ineq().getExpr();
Expr leftSide = ineq[0], rightSide = ineq[1];
Rational r;
findRationalBound(leftSide, rightSide, e, r);
if(numLeft==0 || rUpper bound ", lub.toString(), "");
}
if(!left && !right) {
lub = 0;
glb = 0;
}
if(!left && right) {lub = glb +2;}
if(!right && left) {glb = lub-2;}
DebugAssert(glb <= lub, "Greatest lower bound needs to be smaller "
"than least upper bound");
return strictLB;
}
void TheoryArithOld::assignVariables(std::vector&v)
{
int count = 0;
if (diffLogicOnly)
{
// Compute the model
diffLogicGraph.computeModel();
// Get values for the variables
for (unsigned i = 0; i < v.size(); i ++) {
Expr x = v[i];
assignValue(x, rat(diffLogicGraph.getValuation(x)));
}
// Done
return;
}
while (v.size() > 0)
{
std::vector bottom;
d_graph.selectSmallest(v, bottom);
TRACE("model", "Finding variables to assign. Iteration # ", count, "");
for(unsigned int i = 0; i& v)
{
d_inModelCreation = true;
vector reps;
TRACE("model", "Arith=>computeModel ", "", "{");
for(unsigned int i=0; i is defined by: ", findExpr(e) , "");
}
}
assignVariables(reps);
TRACE("model", "Arith=>computeModel", "", "}");
d_inModelCreation = false;
}
// For any arith expression 'e', if the subexpressions are assigned
// concrete values, then find(e) must already be a concrete value.
void TheoryArithOld::computeModel(const Expr& e, vector& vars) {
DebugAssert(findExpr(e).isRational(), "TheoryArithOld::computeModel("
+e.toString()+")\n e is not assigned concrete value.\n"
+" find(e) = "+findExpr(e).toString());
assignValue(simplify(e));
vars.push_back(e);
}
Theorem TheoryArithOld::checkIntegerEquality(const Theorem& thm) {
// Check if this is a rewrite theorem
bool rewrite = thm.isRewrite();
// If it's an integer theorem, then rafine it to integer domain
Expr eq = (rewrite ? thm.getRHS() : thm.getExpr());
TRACE("arith rafine", "TheoryArithOld::checkIntegerEquality(", eq, ")");
DebugAssert(eq.getKind() == EQ, "checkIntegerEquality: must be an equality");
// Trivial equalities, we don't care
if (!isPlus(eq[1]) && !isPlus(eq[0])) return thm;
Expr old_sum = (isPlus(eq[1]) ? eq[1] : eq[0]);
// Get the sum part
vector children;
bool const_is_integer = true; // Assuming only one constant is present (canon called before this)
for (int i = 0; i < old_sum.arity(); i ++)
if (!old_sum[i].isRational())
children.push_back(old_sum[i]);
else
const_is_integer = old_sum[i].getRational().isInteger();
// If the constants are integers, we don't care
if (const_is_integer) return thm;
Expr sum = (children.size() > 1 ? plusExpr(children) : children[0]);
// Check for integer of the remainder of the sum
Theorem isIntegerEquality = isIntegerThm(sum);
// If it is an integer, it's unsat
if (!isIntegerEquality.isNull()) {
Theorem false_thm = d_rules->intEqualityRationalConstant(isIntegerEquality, eq);
if (rewrite) return transitivityRule(thm, false_thm);
else return iffMP(thm, false_thm);
}
else return thm;
}
Theorem TheoryArithOld::rafineInequalityToInteger(const Theorem& thm) {
// Check if this is a rewrite theorem
bool rewrite = thm.isRewrite();
// If it's an integer theorem, then rafine it to integer domain
Expr ineq = (rewrite ? thm.getRHS() : thm.getExpr());
TRACE("arith rafine", "TheoryArithOld::rafineInequalityToInteger(", ineq, ")");
DebugAssert(isIneq(ineq), "rafineInequalityToInteger: must be an inequality");
// Trivial inequalities are rafined
// if (!isPlus(ineq[1])) return thm;
// Get the sum part
vector children;
if (isPlus(ineq[1])) {
for (int i = 0; i < ineq[1].arity(); i ++)
if (!ineq[1][i].isRational())
children.push_back(ineq[1][i]);
} else children.push_back(ineq[1]);
Expr sum = (children.size() > 1 ? plusExpr(children) : children[0]);
// Check for integer of the remainder of the sum
Theorem isIntegerInequality = isIntegerThm(sum);
// If it is an integer, do rafine it
if (!isIntegerInequality.isNull()) {
Theorem rafine = d_rules->rafineStrictInteger(isIntegerInequality, ineq);
TRACE("arith rafine", "TheoryArithOld::rafineInequalityToInteger()", "=>", rafine.getRHS());
if (rewrite) return canonPredEquiv(transitivityRule(thm, rafine));
else return canonPred(iffMP(thm, rafine));
}
else return thm;
}
/*! accepts a rewrite theorem over eqn|ineqn and normalizes it
* and returns a theorem to that effect. assumes e is non-trivial
* i.e. e is not '0=const' or 'const=0' or '0 <= const' etc.
*/
Theorem TheoryArithOld::normalize(const Expr& e) {
//e is an eqn or ineqn. e is not a trivial eqn or ineqn
//trivial means 0 = const or 0 <= const.
TRACE("arith normalize", "normalize(", e, ") {");
DebugAssert(e.isEq() || isIneq(e),
"normalize: input must be Eq or Ineq: " + e.toString());
DebugAssert(!isIneq(e) || (0 == e[0].getRational()),
"normalize: if (e is ineq) then e[0] must be 0" +
e.toString());
if(e.isEq()) {
if(e[0].isRational()) {
DebugAssert(0 == e[0].getRational(),
"normalize: if e is Eq and e[0] is rat then e[0]==0");
}
else {
//if e[0] is not rational then e[1] must be rational.
DebugAssert(e[1].isRational() && 0 == e[1].getRational(),
"normalize: if e is Eq and e[1] is rat then e[1]==0\n"
" e = "+e.toString());
}
}
Expr factor;
if(e[0].isRational())
factor = computeNormalFactor(e[1], false);
else
factor = computeNormalFactor(e[0], false);
TRACE("arith normalize", "normalize: factor = ", factor, "");
DebugAssert(factor.getRational() > 0,
"normalize: factor="+ factor.toString());
Theorem thm(reflexivityRule(e));
// Now multiply the equality by the factor, unless it is 1
if(factor.getRational() != 1) {
int kind = e.getKind();
switch(kind) {
case EQ:
//TODO: DEJAN FIX
thm = d_rules->multEqn(e[0], e[1], factor);
// And canonize the result
thm = canonPredEquiv(thm);
// If this is an equation of the form 0 = c + sum, c is not integer, but sum is
// then equation has no solutions
thm = checkIntegerEquality(thm);
break;
case LE:
case LT:
case GE:
case GT: {
thm = d_rules->multIneqn(e, factor);
// And canonize the result
thm = canonPredEquiv(thm);
// Try to rafine to integer domain
thm = rafineInequalityToInteger(thm);
break;
}
default:
// MS .net doesn't accept "..." + int
ostringstream ss;
ss << "normalize: control should not reach here " << kind;
DebugAssert(false, ss.str());
break;
}
} else
if (e.getKind() == EQ)
thm = checkIntegerEquality(thm);
TRACE("arith normalize", "normalize => ", thm, " }");
return(thm);
}
Theorem TheoryArithOld::normalize(const Theorem& eIffEqn) {
if (eIffEqn.isRewrite()) return transitivityRule(eIffEqn, normalize(eIffEqn.getRHS()));
else return iffMP(eIffEqn, normalize(eIffEqn.getExpr()));
}
Theorem TheoryArithOld::rewrite(const Expr& e)
{
DebugAssert(leavesAreSimp(e), "Expected leaves to be simplified");
TRACE("arith", "TheoryArithOld::rewrite(", e, ") {");
Theorem thm;
if (!e.isTerm()) {
if (!e.isAbsLiteral()) {
if (e.isPropAtom() && leavesAreNumConst(e)) {
if (e.getSize() < 200) {
Expr eNew = e;
thm = reflexivityRule(eNew);
while (eNew.containsTermITE()) {
thm = transitivityRule(thm, getCommonRules()->liftOneITE(eNew));
DebugAssert(!thm.isRefl(), "Expected non-reflexive");
thm = transitivityRule(thm, theoryCore()->getCoreRules()->rewriteIteCond(thm.getRHS()));
thm = transitivityRule(thm, simplify(thm.getRHS()));
eNew = thm.getRHS();
}
}
else {
thm = d_rules->rewriteLeavesConst(e);
if (thm.isRefl()) {
e.setRewriteNormal();
}
else {
thm = transitivityRule(thm, simplify(thm.getRHS()));
}
}
// if (!thm.getRHS().isBoolConst()) {
// e.setRewriteNormal();
// thm = reflexivityRule(e);
// }
}
else {
e.setRewriteNormal();
thm = reflexivityRule(e);
}
TRACE("arith", "TheoryArithOld::rewrite[non-literal] => ", thm, " }");
return thm;
}
switch(e.getKind()) {
case EQ:
{
// canonical form for an equality of two leaves
// is just l == r instead of 0 + (-1 * l) + r = 0.
if (isLeaf(e[0]) && isLeaf(e[1]))
thm = reflexivityRule(e);
else { // Otherwise, it is "lhs = 0"
//first convert e to the form 0=e'
if((e[0].isRational() && e[0].getRational() == 0)
|| (e[1].isRational() && e[1].getRational() == 0))
//already in 0=e' or e'=0 form
thm = reflexivityRule(e);
else {
thm = d_rules->rightMinusLeft(e);
thm = canonPredEquiv(thm);
}
// Check for trivial equation
if ((thm.getRHS())[0].isRational() && (thm.getRHS())[1].isRational()) {
thm = transitivityRule(thm, d_rules->constPredicate(thm.getRHS()));
} else {
//else equation is non-trivial
thm = normalize(thm);
// Normalization may yield non-simplified terms
if (!thm.getRHS().isBoolConst())
thm = canonPredEquiv(thm);
}
}
// Equations must be oriented such that lhs >= rhs as Exprs;
// this ordering is given by operator<(Expr,Expr).
const Expr& eq = thm.getRHS();
if(eq.isEq() && eq[0] < eq[1])
thm = transitivityRule(thm, getCommonRules()->rewriteUsingSymmetry(eq));
// Check if the equation is nonlinear
Expr nonlinearEq = thm.getRHS();
if (nonlinearEq.isEq() && isNonlinearEq(nonlinearEq)) {
TRACE("arith nonlinear", "nonlinear eq rewrite: ", nonlinearEq, "");
Expr left = nonlinearEq[0];
Expr right = nonlinearEq[1];
// Check for multiplicative equations, i.e. x*y = 0
if (isNonlinearSumTerm(left) && right.isRational() && right.getRational() == 0) {
Theorem eq_thm = d_rules->multEqZero(nonlinearEq);
thm = transitivityRule(thm, eq_thm);
thm = transitivityRule(thm, theoryCore()->simplify(thm.getRHS()));
break;
}
// Heuristics for a sum
if (isPlus(left)) {
// Search for common factor
if (left[0].getRational() == 0) {
Expr::iterator i = left.begin(), iend = left.end();
++ i;
set factors;
set::iterator is, isend;
getFactors(*i, factors);
for (++i; i != iend; ++i) {
set factors2;
getFactors(*i, factors2);
for (is = factors.begin(), isend = factors.end(); is != isend;) {
if (factors2.find(*is) == factors2.end()) {
factors.erase(is ++);
} else
++ is;
}
if (factors.empty()) break;
}
if (!factors.empty()) {
thm = transitivityRule(thm, d_rules->divideEqnNonConst(left, rat(0), *(factors.begin())));
// got (factor != 0) OR (left / factor = right / factor), need to simplify
thm = transitivityRule(thm, simplify(thm.getRHS()));
TRACE("arith nonlinear", "nonlinear eq rewrite (factoring): ", thm.getRHS(), "");
break;
}
}
// Look for equal powers (eq in the form of c + pow1 - pow2 = 0)
Rational constant;
Expr power1;
Expr power2;
if (isPowersEquality(nonlinearEq, power1, power2)) {
// Eliminate the powers
thm = transitivityRule(thm, d_rules->elimPower(nonlinearEq));
thm = transitivityRule(thm, simplify(thm.getRHS()));
TRACE("arith nonlinear", "nonlinear eq rewrite (equal powers): ", thm.getRHS(), "");
break;
} else
// Look for one power equality (c - pow = 0);
if (isPowerEquality(nonlinearEq, constant, power1)) {
Rational pow1 = power1[0].getRational();
if (pow1 % 2 == 0 && constant < 0) {
thm = transitivityRule(thm, d_rules->evenPowerEqNegConst(nonlinearEq));
TRACE("arith nonlinear", "nonlinear eq rewrite (even power = negative): ", thm.getRHS(), "");
break;
}
DebugAssert(constant != 0, "Expected nonzero const");
Rational root = ratRoot(constant, pow1.getUnsigned());
if (root != 0) {
thm = transitivityRule(thm, d_rules->elimPowerConst(nonlinearEq, root));
thm = transitivityRule(thm, simplify(thm.getRHS()));
TRACE("arith nonlinear", "nonlinear eq rewrite (rational root): ", thm.getRHS(), "");
break;
} else {
Theorem isIntPower(isIntegerThm(left));
if (!isIntPower.isNull()) {
thm = transitivityRule(thm, d_rules->intEqIrrational(nonlinearEq, isIntPower));
TRACE("arith nonlinear", "nonlinear eq rewrite (irational root): ", thm.getRHS(), "");
break;
}
}
}
}
// Non-solvable nonlinear equations are rewritten as conjunction of inequalities
if ( (nonlinearEq[0].arity() > 1 && !canPickEqMonomial(nonlinearEq[0])) ||
(nonlinearEq[1].arity() > 1 && !canPickEqMonomial(nonlinearEq[1])) ) {
thm = transitivityRule(thm, d_rules->eqToIneq(nonlinearEq));
thm = transitivityRule(thm, simplify(thm.getRHS()));
TRACE("arith nonlinear", "nonlinear eq rewrite (not solvable): ", thm.getRHS(), "");
break;
}
}
}
break;
case GRAY_SHADOW:
case DARK_SHADOW:
thm = reflexivityRule(e);
break;
case IS_INTEGER: {
Theorem res(isIntegerDerive(e, typePred(e[0])));
if(!res.isNull())
thm = getCommonRules()->iffTrue(res);
else
thm = reflexivityRule(e);
break;
}
case NOT:
if (!isIneq(e[0]))
//in this case we have "NOT of DARK or GRAY_SHADOW."
thm = reflexivityRule(e);
else {
//In this case we have the "NOT of ineq". get rid of NOT
//and then treat like an ineq
thm = d_rules->negatedInequality(e);
DebugAssert(isGE(thm.getRHS()) || isGT(thm.getRHS()),
"Expected GE or GT");
thm = transitivityRule(thm, d_rules->flipInequality(thm.getRHS()));
thm = transitivityRule(thm, d_rules->rightMinusLeft(thm.getRHS()));
thm = canonPredEquiv(thm);
// If the inequality is strict and integer, change it to non-strict
Expr theIneq = thm.getRHS();
if(isLT(theIneq)) {
// Check if integer
Theorem isIntLHS(isIntegerThm(theIneq[0]));
Theorem isIntRHS(isIntegerThm(theIneq[1]));
bool isInt = (!isIntLHS.isNull() && !isIntRHS.isNull());
if (isInt) {
thm = canonPredEquiv(
transitivityRule(thm, d_rules->lessThanToLERewrite(theIneq, isIntLHS, isIntRHS, true)));
}
}
// Check for trivial inequation
if ((thm.getRHS())[1].isRational())
thm = transitivityRule(thm, d_rules->constPredicate(thm.getRHS()));
else {
//else ineq is non-trivial
thm = normalize(thm);
// Normalization may yield non-simplified terms
thm = canonPredEquiv(thm);
}
}
break;
case LT:
case GT:
case LE:
case GE: {
if (isGE(e) || isGT(e)) {
thm = d_rules->flipInequality(e);
thm = transitivityRule(thm, d_rules->rightMinusLeft(thm.getRHS()));
}
else
thm = d_rules->rightMinusLeft(e);
thm = canonPredEquiv(thm);
// If the inequality is strict and integer, change it to non-strict
Expr theIneq = thm.getRHS();
if(isLT(theIneq)) {
// Check if integer
Theorem isIntLHS(isIntegerThm(theIneq[0]));
Theorem isIntRHS(isIntegerThm(theIneq[1]));
bool isInt = (!isIntLHS.isNull() && !isIntRHS.isNull());
if (isInt) {
thm = canonPredEquiv(
transitivityRule(thm, d_rules->lessThanToLERewrite(theIneq, isIntLHS, isIntRHS, true)));
}
}
// Check for trivial inequation
if ((thm.getRHS())[1].isRational())
thm = transitivityRule(thm, d_rules->constPredicate(thm.getRHS()));
else { // ineq is non-trivial
thm = normalize(thm);
thm = canonPredEquiv(thm);
if (thm.getRHS()[1].isRational())
thm = transitivityRule(thm, d_rules->constPredicate(thm.getRHS()));
}
break;
}
default:
DebugAssert(false,
"Theory_Arith::rewrite: control should not reach here");
break;
}
}
else {
if (e.isAtomic())
thm = canon(e);
else
thm = reflexivityRule(e);
}
// TODO: this needs to be reviewed, esp for non-linear case
// Arith canonization is idempotent
if (theoryOf(thm.getRHS()) == this)
thm.getRHS().setRewriteNormal();
TRACE("arith", "TheoryArithOld::rewrite => ", thm, " }");
return thm;
}
void TheoryArithOld::setup(const Expr& e)
{
if (!e.isTerm()) {
if (e.isNot()) return;
// if(e.getKind() == IS_INTEGER) {
// e[0].addToNotify(this, e);
// return;
// }
if (isIneq(e)) {
DebugAssert((isLT(e)||isLE(e)) &&
e[0].isRational() && e[0].getRational() == 0,
"TheoryArithOld::setup: expected 0 < rhs:" + e.toString());
e[1].addToNotify(this, e);
} else {
// if (e.isEq()) {
// // Nonlinear solved equations
// if (isNonlinearEq(e) && e[0].isRational() && e[0].getRational() == 0)
// e[0].addToNotify(this, e);
// }
//
// DebugAssert(isGrayShadow(e), "TheoryArithOld::setup: expected grayshadow" + e.toString());
//
// // Do not add the variable, just the subterm e[0].addToNotify(this, e);
// e[1].addToNotify(this, e);
}
return;
}
int k(0), ar(e.arity());
for ( ; k < ar; ++k) {
e[k].addToNotify(this, e);
TRACE("arith setup", "e["+int2string(k)+"]: ", *(e[k].getNotify()), "");
}
}
void TheoryArithOld::update(const Theorem& e, const Expr& d)
{
TRACE("arith update", "update on " + d.toString() + " with ", e.getRHS().toString(), ".");
if (inconsistent()) return;
// We accept atoms without find, but only inequalities (they come from the buffer)
DebugAssert(d.hasFind() || isIneq(d), "update on a non-inequality term/atom");
IF_DEBUG(debugger.counter("arith update total")++;)
// if (isGrayShadow(d)) {
// TRACE("shadow update", "updating index of " + d.toString() + " with ", e.getRHS().toString(), ".");
//
// // Substitute e[1] for e[0] in d and enqueue new shadow
// DebugAssert(e.getLHS() == d[1], "Mismatch");
// Theorem thm = find(d);
//
// // DebugAssert(thm.getRHS() == trueExpr(), "Expected find = true");
// vector changed;
// vector children;
// changed.push_back(1);
// children.push_back(e);
// Theorem thm2 = substitutivityRule(d, changed, children);
// if (thm.getRHS() == trueExpr()) {
// enqueueFact(iffMP(getCommonRules()->iffTrueElim(thm), thm2));
// }
// else {
// enqueueFact(getCommonRules()->iffFalseElim(
// transitivityRule(symmetryRule(thm2), thm)));
// }
// IF_DEBUG(debugger.counter("arith update ineq")++;)
// }
// else
if (isIneq(d)) {
// Substitute e[1] for e[0] in d and enqueue new inequality
DebugAssert(e.getLHS() == d[1], "Mismatch");
Theorem thm;
if (d.hasFind()) thm = find(d);
// bool diff_logic = false;
// Expr new_rhs = e.getRHS();
// if (!isPlus(new_rhs)) {
// if (isLeaf(new_rhs)) diff_logic = true;
// }
// else {
// int arity = new_rhs.arity();
// if (arity == 2) {
// if (new_rhs[0].isRational()) diff_logic = true;
// else {
// Expr ax = new_rhs[0], a, x;
// Expr by = new_rhs[1], b, y;
// separateMonomial(ax, a, x);
// separateMonomial(by, b, y);
// if ((a.getRational() == 1 && b.getRational() == -1) ||
// (a.getRational() == -1 && b.getRational() == 1))
// diff_logic = true;
// }
// } else {
// if (arity == 3 && new_rhs[0].isRational()) {
// Expr ax = new_rhs[1], a, x;
// Expr by = new_rhs[2], b, y;
// separateMonomial(ax, a, x);
// separateMonomial(by, b, y);
// if ((a.getRational() == 1 && b.getRational() == -1) ||
// (a.getRational() == -1 && b.getRational() == 1))
// diff_logic = true;
// }
// }
// }
// DebugAssert(thm.getRHS() == trueExpr(), "Expected find = true");
vector changed;
vector children;
changed.push_back(1);
children.push_back(e);
Theorem thm2 = substitutivityRule(d, changed, children);
Expr newIneq = thm2.getRHS();
// If this inequality is bufferred but not yet projected, just wait for it
// but don't add the find to the buffer as it will be projected as a find
// We DO want it to pass through all the buffer stuff but NOT get into the buffer
// NOTE: this means that the difference logic WILL get processed
if ((thm.isNull() || thm.getRHS() != falseExpr()) &&
bufferedInequalities.find(d) != bufferedInequalities.end() &&
alreadyProjected.find(d) == alreadyProjected.end()) {
TRACE("arith update", "simplified but not projected : ", thm2.getRHS(), "");
dontBuffer[thm2.getRHS()] = true;
}
if (thm.isNull()) {
// This hy is in the buffer, not in the core
// if it has been projected, than it's parent has been projected and will get reprojected
// accuratlz. If it has not been projected, we don't care it's still there
TRACE("arith update", "in udpate, but no find", "", "");
if (bufferedInequalities.find(d) != bufferedInequalities.end()) {
if (thm2.getRHS()[1].isRational()) enqueueFact(iffMP(bufferedInequalities[d], thm2));
else if (alreadyProjected.find(d) != alreadyProjected.end()) {
// the parent will get reprojected
alreadyProjected[d] = d;
}
}
}
else if (thm.getRHS() == trueExpr()) {
if (!newIneq[1].isRational() || newIneq[1].getRational() <= 0)
enqueueFact(iffMP(getCommonRules()->iffTrueElim(thm), thm2));
}
else {
enqueueFact(getCommonRules()->iffFalseElim(
transitivityRule(symmetryRule(thm2), thm)));
}
IF_DEBUG(debugger.counter("arith update ineq")++;)
}
else if (d.isEq()) {
TRACE("arith nonlinear", "TheoryArithOld::update() on equality ", d, "");
// We get equalitites from the non-solve nonlinear equations
// only the right hand sides get updated
vector changed;
vector children;
changed.push_back(0);
children.push_back(e);
Theorem thm = substitutivityRule(d, changed, children);
Expr newEq = thm.getRHS();
Theorem d_find = find(d);
if (d_find.getRHS() == trueExpr()) enqueueFact(iffMP(getCommonRules()->iffTrueElim(d_find), thm));
else enqueueFact(getCommonRules()->iffFalseElim(transitivityRule(symmetryRule(thm), d_find)));
}
else if (d.getKind() == IS_INTEGER) {
// This should only happen if !d has been asserted
DebugAssert(e.getRHS() == findExpr(d[0]), "Unexpected");
if (isInteger(e.getRHS())) {
Theorem thm = substitutivityRule(d, find(d[0]));
thm = transitivityRule(symmetryRule(find(d)), thm);
thm = iffMP(thm, simplify(thm.getExpr()));
setInconsistent(thm);
}
else {
e.getRHS().addToNotify(this, d);
}
}
else if (find(d).getRHS() == d) {
// Theorem thm = canonSimp(d);
// TRACE("arith", "TheoryArithOld::update(): thm = ", thm, "");
// DebugAssert(leavesAreSimp(thm.getRHS()), "updateHelper error: "
// +thm.getExpr().toString());
// assertEqualities(transitivityRule(thm, rewrite(thm.getRHS())));
// IF_DEBUG(debugger.counter("arith update find(d)=d")++;)
Theorem thm = simplify(d);
// If the original is was a shared term, add this one as as a shared term also
if (d_sharedTerms.find(d) != d_sharedTerms.end()) addSharedTerm(thm.getRHS());
DebugAssert(thm.getRHS().isAtomic(), "Expected atomic");
assertEqualities(thm);
}
}
Theorem TheoryArithOld::solve(const Theorem& thm)
{
DebugAssert(thm.isRewrite() && thm.getLHS().isTerm(), "");
const Expr& lhs = thm.getLHS();
const Expr& rhs = thm.getRHS();
// Check for already solved equalities.
// Have to be careful about the types: integer variable cannot be
// assigned a real term. Also, watch for e[0] being a subexpression
// of e[1]: this would create an unsimplifiable expression.
if (isLeaf(lhs) && !isLeafIn(lhs, rhs)
&& (!isInteger(lhs) || isInteger(rhs))
// && !e[0].subExprOf(e[1])
)
return thm;
// Symmetric version is already solved
if (isLeaf(rhs) && !isLeafIn(rhs, lhs)
&& (!isInteger(rhs) || isInteger(lhs))
// && !e[1].subExprOf(e[0])
)
return symmetryRule(thm);
return doSolve(thm);
}
void TheoryArithOld::computeModelTerm(const Expr& e, std::vector& v) {
switch(e.getKind()) {
case RATIONAL_EXPR: // Skip the constants
break;
case PLUS:
case MULT:
case DIVIDE:
case POW: // This is not a variable; extract the variables from children
for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i)
// getModelTerm(*i, v);
v.push_back(*i);
break;
default: { // Otherwise it's a variable. Check if it has a find pointer
Expr e2(findExpr(e));
if(e==e2) {
TRACE("model", "TheoryArithOld::computeModelTerm(", e, "): a variable");
// Leave it alone (it has no descendants)
// v.push_back(e);
} else {
TRACE("model", "TheoryArithOld::computeModelTerm("+e.toString()
+"): has find pointer to ", e2, "");
v.push_back(e2);
}
}
}
}
Expr TheoryArithOld::computeTypePred(const Type& t, const Expr& e) {
Expr tExpr = t.getExpr();
switch(tExpr.getKind()) {
case INT:
return Expr(IS_INTEGER, e);
case SUBRANGE: {
std::vector kids;
kids.push_back(Expr(IS_INTEGER, e));
kids.push_back(leExpr(tExpr[0], e));
kids.push_back(leExpr(e, tExpr[1]));
return andExpr(kids);
}
default:
return e.getEM()->trueExpr();
}
}
void TheoryArithOld::checkAssertEqInvariant(const Theorem& e)
{
if (e.isRewrite()) {
DebugAssert(e.getLHS().isTerm(), "Expected equation");
if (isLeaf(e.getLHS())) {
// should be in solved form
DebugAssert(!isLeafIn(e.getLHS(),e.getRHS()),
"Not in solved form: lhs appears in rhs");
}
else {
DebugAssert(e.getLHS().hasFind(), "Expected lhs to have find");
DebugAssert(!leavesAreSimp(e.getLHS()),
"Expected at least one unsimplified leaf on lhs");
}
DebugAssert(canonSimp(e.getRHS()).getRHS() == e.getRHS(),
"Expected canonSimp(rhs) = canonSimp(rhs)");
}
else {
Expr expr = e.getExpr();
if (expr.isFalse()) return;
vector eqs;
Theorem thm;
int index, index2;
for (index = 0; index < expr.arity(); ++index) {
thm = getCommonRules()->andElim(e, index);
eqs.push_back(thm);
if (thm.getExpr().isFalse()) return;
DebugAssert(eqs[index].isRewrite() &&
eqs[index].getLHS().isTerm(), "Expected equation");
}
// Check for solved form
for (index = 0; index < expr.arity(); ++index) {
DebugAssert(isLeaf(eqs[index].getLHS()), "expected leaf on lhs");
DebugAssert(canonSimp(eqs[index].getRHS()).getRHS() == eqs[index].getRHS(),
"Expected canonSimp(rhs) = canonSimp(rhs)");
DebugAssert(recursiveCanonSimpCheck(eqs[index].getRHS()),
"Failed recursive canonSimp check");
for (index2 = 0; index2 < expr.arity(); ++index2) {
DebugAssert(index == index2 ||
eqs[index].getLHS() != eqs[index2].getLHS(),
"Not in solved form: repeated lhs");
DebugAssert(!isLeafIn(eqs[index].getLHS(),eqs[index2].getRHS()),
"Not in solved form: lhs appears in rhs");
}
}
}
}
void TheoryArithOld::checkType(const Expr& e)
{
switch (e.getKind()) {
case INT:
case REAL:
if (e.arity() > 0) {
throw Exception("Ill-formed arithmetic type: "+e.toString());
}
break;
case SUBRANGE:
if (e.arity() != 2 ||
!isIntegerConst(e[0]) ||
!isIntegerConst(e[1]) ||
e[0].getRational() > e[1].getRational()) {
throw Exception("bad SUBRANGE type expression"+e.toString());
}
break;
default:
DebugAssert(false, "Unexpected kind in TheoryArithOld::checkType"
+getEM()->getKindName(e.getKind()));
}
}
Cardinality TheoryArithOld::finiteTypeInfo(Expr& e, Unsigned& n,
bool enumerate, bool computeSize)
{
Cardinality card = CARD_INFINITE;
switch (e.getKind()) {
case SUBRANGE: {
card = CARD_FINITE;
Expr typeExpr = e;
if (enumerate) {
Rational r = typeExpr[0].getRational() + n;
if (r <= typeExpr[1].getRational()) {
e = rat(r);
}
else e = Expr();
}
if (computeSize) {
Rational r = typeExpr[1].getRational() - typeExpr[0].getRational() + 1;
n = r.getUnsigned();
}
break;
}
default:
break;
}
return card;
}
void TheoryArithOld::computeType(const Expr& e)
{
switch (e.getKind()) {
case REAL_CONST:
e.setType(d_realType);
break;
case RATIONAL_EXPR:
if(e.getRational().isInteger())
e.setType(d_intType);
else
e.setType(d_realType);
break;
case UMINUS:
case PLUS:
case MINUS:
case MULT:
case POW: {
bool isInt = true;
for(int k = 0; k < e.arity(); ++k) {
if(d_realType != getBaseType(e[k]))
throw TypecheckException("Expecting type REAL with `" +
getEM()->getKindName(e.getKind()) + "',\n"+
"but got a " + getBaseType(e[k]).toString()+
" for:\n" + e.toString());
if(isInt && !isInteger(e[k]))
isInt = false;
}
if(isInt)
e.setType(d_intType);
else
e.setType(d_realType);
break;
}
case DIVIDE: {
Expr numerator = e[0];
Expr denominator = e[1];
if (getBaseType(numerator) != d_realType ||
getBaseType(denominator) != d_realType) {
throw TypecheckException("Expecting only REAL types with `DIVIDE',\n"
"but got " + getBaseType(numerator).toString()+
" and " + getBaseType(denominator).toString() +
" for:\n" + e.toString());
}
if(denominator.isRational() && 1 == denominator.getRational())
e.setType(numerator.getType());
else
e.setType(d_realType);
break;
}
case LT:
case LE:
case GT:
case GE:
case GRAY_SHADOW:
// Need to know types for all exprs -Clark
// e.setType(boolType());
// break;
case DARK_SHADOW:
for (int k = 0; k < e.arity(); ++k) {
if (d_realType != getBaseType(e[k]))
throw TypecheckException("Expecting type REAL with `" +
getEM()->getKindName(e.getKind()) + "',\n"+
"but got a " + getBaseType(e[k]).toString()+
" for:\n" + e.toString());
}
e.setType(boolType());
break;
case IS_INTEGER:
if(d_realType != getBaseType(e[0]))
throw TypecheckException("Expected type REAL, but got "
+getBaseType(e[0]).toString()
+"\n\nExpr = "+e.toString());
e.setType(boolType());
break;
default:
DebugAssert(false,"TheoryArithOld::computeType: unexpected expression:\n "
+e.toString());
break;
}
}
Type TheoryArithOld::computeBaseType(const Type& t) {
IF_DEBUG(int kind = t.getExpr().getKind();)
DebugAssert(kind==INT || kind==REAL || kind==SUBRANGE,
"TheoryArithOld::computeBaseType("+t.toString()+")");
return realType();
}
Expr
TheoryArithOld::computeTCC(const Expr& e) {
Expr tcc(Theory::computeTCC(e));
switch(e.getKind()) {
case DIVIDE:
DebugAssert(e.arity() == 2, "");
return tcc.andExpr(!(e[1].eqExpr(rat(0))));
default:
return tcc;
}
}
///////////////////////////////////////////////////////////////////////////////
//parseExprOp:
//translating special Exprs to regular EXPR??
///////////////////////////////////////////////////////////////////////////////
Expr
TheoryArithOld::parseExprOp(const Expr& e) {
//TRACE("parser", "TheoryArithOld::parseExprOp(", e, ")");
//std::cout << "Were here";
// If the expression is not a list, it must have been already
// parsed, so just return it as is.
switch(e.getKind()) {
case ID: {
int kind = getEM()->getKind(e[0].getString());
switch(kind) {
case NULL_KIND: return e; // nothing to do
case REAL:
case INT:
case NEGINF:
case POSINF: return getEM()->newLeafExpr(kind);
default:
DebugAssert(false, "Bad use of bare keyword: "+e.toString());
return e;
}
}
case RAW_LIST: break; // break out of switch, do the hard work
default:
return e;
}
DebugAssert(e.getKind() == RAW_LIST && e.arity() > 0,
"TheoryArithOld::parseExprOp:\n e = "+e.toString());
const Expr& c1 = e[0][0];
int kind = getEM()->getKind(c1.getString());
switch(kind) {
case UMINUS: {
if(e.arity() != 2)
throw ParserException("UMINUS requires exactly one argument: "
+e.toString());
return uminusExpr(parseExpr(e[1]));
}
case PLUS: {
vector k;
Expr::iterator i = e.begin(), iend=e.end();
// Skip first element of the vector of kids in 'e'.
// The first element is the operator.
++i;
// Parse the kids of e and push them into the vector 'k'
for(; i!=iend; ++i) k.push_back(parseExpr(*i));
return plusExpr(k);
}
case MINUS: {
if(e.arity() == 2) {
if (false && (getEM()->getInputLang() == SMTLIB_LANG
|| getEM()->getInputLang() == SMTLIB_V2_LANG)) {
throw ParserException("Unary Minus should use '~' instead of '-' in SMT-LIB expr:"
+e.toString());
}
else {
return uminusExpr(parseExpr(e[1]));
}
}
else if(e.arity() == 3)
return minusExpr(parseExpr(e[1]), parseExpr(e[2]));
else
throw ParserException("MINUS requires one or two arguments:"
+e.toString());
}
case MULT: {
vector k;
Expr::iterator i = e.begin(), iend=e.end();
// Skip first element of the vector of kids in 'e'.
// The first element is the operator.
++i;
// Parse the kids of e and push them into the vector 'k'
for(; i!=iend; ++i) k.push_back(parseExpr(*i));
return multExpr(k);
}
case POW: {
return powExpr(parseExpr(e[1]), parseExpr(e[2]));
}
case DIVIDE:
{ return divideExpr(parseExpr(e[1]), parseExpr(e[2])); }
case LT:
{ return ltExpr(parseExpr(e[1]), parseExpr(e[2])); }
case LE:
{ return leExpr(parseExpr(e[1]), parseExpr(e[2])); }
case GT:
{ return gtExpr(parseExpr(e[1]), parseExpr(e[2])); }
case GE:
{ return geExpr(parseExpr(e[1]), parseExpr(e[2])); }
case INTDIV:
case MOD:
case SUBRANGE: {
vector k;
Expr::iterator i = e.begin(), iend=e.end();
// Skip first element of the vector of kids in 'e'.
// The first element is the operator.
++i;
// Parse the kids of e and push them into the vector 'k'
for(; i!=iend; ++i)
k.push_back(parseExpr(*i));
return Expr(kind, k, e.getEM());
}
case IS_INTEGER: {
if(e.arity() != 2)
throw ParserException("IS_INTEGER requires exactly one argument: "
+e.toString());
return Expr(IS_INTEGER, parseExpr(e[1]));
}
default:
DebugAssert(false,
"TheoryArithOld::parseExprOp: invalid input " + e.toString());
break;
}
return e;
}
///////////////////////////////////////////////////////////////////////////////
// Pretty-printing //
///////////////////////////////////////////////////////////////////////////////
ExprStream&
TheoryArithOld::print(ExprStream& os, const Expr& e) {
switch(os.lang()) {
case SIMPLIFY_LANG:
switch(e.getKind()) {
case RATIONAL_EXPR:
e.print(os);
break;
case SUBRANGE:
os <<"ERROR:SUBRANGE:not supported in Simplify\n";
break;
case IS_INTEGER:
os <<"ERROR:IS_INTEGER:not supported in Simplify\n";
break;
case PLUS: {
int i=0, iend=e.arity();
os << "(+ ";
if(i!=iend) os << e[i];
++i;
for(; i!=iend; ++i) os << " " << e[i];
os << ")";
break;
}
case MINUS:
os << "(- " << e[0] << " " << e[1]<< ")";
break;
case UMINUS:
os << "-" << e[0] ;
break;
case MULT: {
int i=0, iend=e.arity();
os << "(* " ;
if(i!=iend) os << e[i];
++i;
for(; i!=iend; ++i) os << " " << e[i];
os << ")";
break;
}
case POW:
os << "(" << push << e[1] << space << "^ " << e[0] << push << ")";
break;
case DIVIDE:
os << "(" << push << e[0] << space << "/ " << e[1] << push << ")";
break;
case LT:
if (isInt(e[0].getType()) || isInt(e[1].getType())) {
}
os << "(< " << e[0] << " " << e[1] <<")";
break;
case LE:
os << "(<= " << e[0] << " " << e[1] << ")";
break;
case GT:
os << "(> " << e[0] << " " << e[1] << ")";
break;
case GE:
os << "(>= " << e[0] << " " << e[1] << ")";
break;
case DARK_SHADOW:
case GRAY_SHADOW:
os <<"ERROR:SHADOW:not supported in Simplify\n";
break;
default:
// Print the top node in the default LISP format, continue with
// pretty-printing for children.
e.print(os);
break;
}
break; // end of case SIMPLIFY_LANG
case TPTP_LANG:
switch(e.getKind()) {
case RATIONAL_EXPR:
e.print(os);
break;
case SUBRANGE:
os <<"ERROR:SUBRANGE:not supported in TPTP\n";
break;
case IS_INTEGER:
os <<"ERROR:IS_INTEGER:not supported in TPTP\n";
break;
case PLUS: {
if(!isInteger(e[0])){
os<<"ERRPR:plus only supports inteters now in TPTP\n";
break;
}
int i=0, iend=e.arity();
if(iend <=1){
os<<"ERROR,plus must have more than two numbers in TPTP\n";
break;
}
for(i=0; i <= iend-2; ++i){
os << "$plus_int(";
os << e[i] << ",";
}
os<< e[iend-1];
for(i=0 ; i <= iend-2; ++i){
os << ")";
}
break;
}
case MINUS:
if(!isInteger(e[0])){
os<<"ERRPR:arithmetic operations only support inteters now in TPTP\n";
break;
}
os << "$minus_int(" << e[0] << "," << e[1]<< ")";
break;
case UMINUS:
if(!isInteger(e[0])){
os<<"ERRPR:arithmetic operations only support inteters now in TPTP\n";
break;
}
os << "$uminus_int(" << e[0] <<")" ;
break;
case MULT: {
if(!isInteger(e[0])){
os<<"ERRPR:times only supports inteters now in TPTP\n";
break;
}
int i=0, iend=e.arity();
if(iend <=1){
os<<"ERROR:times must have more than two numbers in TPTP\n";
break;
}
for(i=0; i <= iend-2; ++i){
os << "$times_int(";
os << e[i] << ",";
}
os<< e[iend-1];
for(i=0 ; i <= iend-2; ++i){
os << ")";
}
break;
}
case POW:
if(!isInteger(e[0])){
os<<"ERRPR:arithmetic operations only support inteters now in TPTP\n";
break;
}
os << "$power_int(" << push << e[1] << space << "^ " << e[0] << push << ")";
break;
case DIVIDE:
if(!isInteger(e[0])){
os<<"ERRPR:arithmetic operations only support inteters now in TPTP\n";
break;
}
os << "divide_int(" < " << e[1] << push << ")";
break;
case GE:
os << "(" << push << e[0] << space << ">= " << e[1] << push << ")";
break;
case DARK_SHADOW:
os << "DARK_SHADOW(" << push << e[0] << ", " << space << e[1] << push << ")";
break;
case GRAY_SHADOW:
os << "GRAY_SHADOW(" << push << e[0] << "," << space << e[1]
<< "," << space << e[2] << "," << space << e[3] << push << ")";
break;
default:
// Print the top node in the default LISP format, continue with
// pretty-printing for children.
e.printAST(os);
break;
}
break; // end of case PRESENTATION_LANG
case SPASS_LANG: {
switch(e.getKind()) {
case REAL_CONST:
printRational(os, e[0].getRational(), true);
break;
case RATIONAL_EXPR:
printRational(os, e.getRational());
break;
case REAL:
throw SmtlibException("TheoryArithOld::print: SPASS: REAL not implemented");
break;
case INT:
throw SmtlibException("TheoryArithOld::print: SPASS: INT not implemented");
break;
case SUBRANGE:
throw SmtlibException("TheoryArithOld::print: SPASS: SUBRANGE not implemented");
break;
case IS_INTEGER:
throw SmtlibException("TheoryArithOld::print: SPASS: IS_INTEGER not implemented");
case PLUS: {
int arity = e.arity();
if(2 == arity) {
os << push << "plus("
<< e[0] << "," << space << e[1]
<< push << ")";
}
else if(2 < arity) {
for (int i = 0 ; i < arity - 2; i++){
os << push << "plus(";
os << e[i] << "," << space;
}
os << push << "plus("
<< e[arity - 2] << "," << space << e[arity - 1]
<< push << ")";
for (int i = 0 ; i < arity - 2; i++){
os << push << ")";
}
}
else {
throw SmtlibException("TheoryArithOld::print: SPASS: Less than two arguments for plus");
}
break;
}
case MINUS: {
os << push << "plus(" << e[0]
<< "," << space << push << "mult(-1,"
<< space << e[1] << push << ")" << push << ")";
break;
}
case UMINUS: {
os << push << "plus(0,"
<< space << push << "mult(-1,"
<< space << e[0] << push << ")" << push << ")";
break;
}
case MULT: {
int arity = e.arity();
if (2 == arity){
os << push << "mult("
<< e[0] << "," << space << e[1]
<< push << ")";
}
else if (2 < arity){
for (int i = 0 ; i < arity - 2; i++){
os << push << "mult(";
os << e[i] << "," << space;
}
os << push << "mult("
<< e[arity - 2] << "," << space << e[arity - 1]
<< push << ")";
for (int i = 0 ; i < arity - 2; i++){
os << push << ")";
}
}
else{
throw SmtlibException("TheoryArithOld::print: SPASS: Less than two arguments for mult");
}
break;
}
case POW:
if (e[0].isRational() && e[0].getRational().isInteger()) {
int i=0, iend=e[0].getRational().getInt();
for(; i!=iend; ++i) {
if (i < iend-2) {
os << push << "mult(";
}
os << e[1] << "," << space;
}
os << push << "mult("
<< e[1] << "," << space << e[1];
for (i=0; i < iend-1; ++i) {
os << push << ")";
}
}
else {
throw SmtlibException("TheoryArithOld::print: SPASS: POW not supported: " + e.toString(PRESENTATION_LANG));
}
break;
case DIVIDE: {
os << "ERROR "<< endl;break;
throw SmtlibException("TheoryArithOld::print: SPASS: unexpected use of DIVIDE");
break;
}
case LT: {
Rational r;
os << push << "ls(" << space;
os << e[0] << "," << space << e[1] << push << ")";
break;
}
case LE: {
Rational r;
os << push << "le(" << space;
os << e[0] << "," << space << e[1] << push << ")";
break;
}
case GT: {
Rational r;
os << push << "gs(" << space;
os << e[0] << "," << space << e[1] << push << ")";
break;
}
case GE: {
Rational r;
os << push << "ge(" << space;
os << e[0] << "," << space << e[1] << push << ")";
break;
}
default:
throw SmtlibException("TheoryArithOld::print: SPASS: default not supported");
}
break; // end of case SPASS_LANG
}
case SMTLIB_LANG:
case SMTLIB_V2_LANG: {
switch(e.getKind()) {
case REAL_CONST:
printRational(os, e[0].getRational(), true);
break;
case RATIONAL_EXPR:
printRational(os, e.getRational());
break;
case REAL:
os << "Real";
break;
case INT:
os << "Int";
break;
case SUBRANGE:
throw SmtlibException("TheoryArithOld::print: SMTLIB: SUBRANGE not implemented");
// if(e.arity() != 2) e.print(os);
// else
// os << "(" << push << "SUBRANGE" << space << e[0]
// << space << e[1] << push << ")";
break;
case IS_INTEGER:
if(e.arity() == 1) {
if (os.lang() == SMTLIB_LANG) {
os << "(" << push << "IsInt" << space << e[0] << push << ")";
}
else {
os << "(" << push << "is_int" << space << e[0] << push << ")";
}
}
else
throw SmtlibException("TheoryArithOld::print: SMTLIB: IS_INTEGER used unexpectedly");
break;
case PLUS: {
if(e.arity() == 1 && os.lang() == SMTLIB_V2_LANG) {
os << e[0];
} else {
os << "(" << push << "+";
Expr::iterator i = e.begin(), iend = e.end();
for(; i!=iend; ++i) {
os << space << (*i);
}
os << push << ")";
}
break;
}
case MINUS: {
os << "(" << push << "- " << e[0] << space << e[1] << push << ")";
break;
}
case UMINUS: {
if (os.lang() == SMTLIB_LANG) {
os << "(" << push << "~" << space << e[0] << push << ")";
}
else {
os << "(" << push << "-" << space << e[0] << push << ")";
}
break;
}
case MULT: {
int i=0, iend=e.arity();
if(iend == 1 && os.lang() == SMTLIB_V2_LANG) {
os << e[0];
} else {
for(; i!=iend; ++i) {
if (i < iend-1) {
os << "(" << push << "*";
}
os << space << e[i];
}
for (i=0; i < iend-1; ++i) os << push << ")";
}
break;
}
case POW:
if (e[0].isRational() && e[0].getRational().isInteger()) {
int i=0, iend=e[0].getRational().getInt();
for(; i!=iend; ++i) {
if (i < iend-1) {
os << "(" << push << "*";
}
os << space << e[1];
}
for (i=0; i < iend-1; ++i) os << push << ")";
}
else
throw SmtlibException("TheoryArithOld::print: SMTLIB: POW not supported: " + e.toString(PRESENTATION_LANG));
// os << "(" << push << "^ " << e[1] << space << e[0] << push << ")";
break;
case DIVIDE: {
throw SmtlibException("TheoryArithOld::print: SMTLIB: unexpected use of DIVIDE");
break;
}
case LT: {
Rational r;
os << "(" << push << "<" << space;
os << e[0] << space << e[1] << push << ")";
break;
}
case LE: {
Rational r;
os << "(" << push << "<=" << space;
os << e[0] << space << e[1] << push << ")";
break;
}
case GT: {
Rational r;
os << "(" << push << ">" << space;
os << e[0] << space << e[1] << push << ")";
break;
}
case GE: {
Rational r;
os << "(" << push << ">=" << space;
os << e[0] << space << e[1] << push << ")";
break;
}
case DARK_SHADOW:
throw SmtlibException("TheoryArithOld::print: SMTLIB: DARK_SHADOW not supported");
os << "(" << push << "DARK_SHADOW" << space << e[0]
<< space << e[1] << push << ")";
break;
case GRAY_SHADOW:
throw SmtlibException("TheoryArithOld::print: SMTLIB: GRAY_SHADOW not supported");
os << "GRAY_SHADOW(" << push << e[0] << "," << space << e[1]
<< "," << space << e[2] << "," << space << e[3] << push << ")";
break;
default:
throw SmtlibException("TheoryArithOld::print: SMTLIB: default not supported");
// Print the top node in the default LISP format, continue with
// pretty-printing for children.
e.printAST(os);
break;
}
break; // end of case SMTLIB_LANG
}
case LISP_LANG:
switch(e.getKind()) {
case REAL:
case INT:
case RATIONAL_EXPR:
case NEGINF:
case POSINF:
e.print(os);
break;
case SUBRANGE:
if(e.arity() != 2) e.printAST(os);
else
os << "(" << push << "SUBRANGE" << space << e[0]
<< space << e[1] << push << ")";
break;
case IS_INTEGER:
if(e.arity() == 1)
os << "(" << push << "IS_INTEGER" << space << e[0] << push << ")";
else
e.printAST(os);
break;
case PLUS: {
int i=0, iend=e.arity();
os << "(" << push << "+";
for(; i!=iend; ++i) os << space << e[i];
os << push << ")";
break;
}
case MINUS:
//os << "(" << push << e[0] << space << "- " << e[1] << push << ")";
os << "(" << push << "- " << e[0] << space << e[1] << push << ")";
break;
case UMINUS:
os << "(" << push << "-" << space << e[0] << push << ")";
break;
case MULT: {
int i=0, iend=e.arity();
os << "(" << push << "*";
for(; i!=iend; ++i) os << space << e[i];
os << push << ")";
break;
}
case POW:
os << "(" << push << "^ " << e[1] << space << e[0] << push << ")";
break;
case DIVIDE:
os << "(" << push << "/ " << e[0] << space << e[1] << push << ")";
break;
case LT:
os << "(" << push << "< " << e[0] << space << e[1] << push << ")";
break;
case LE:
os << "(" << push << "<= " << e[0] << space << e[1] << push << ")";
break;
case GT:
os << "(" << push << "> " << e[1] << space << e[0] << push << ")";
break;
case GE:
os << "(" << push << ">= " << e[0] << space << e[1] << push << ")";
break;
case DARK_SHADOW:
os << "(" << push << "DARK_SHADOW" << space << e[0]
<< space << e[1] << push << ")";
break;
case GRAY_SHADOW:
os << "(" << push << "GRAY_SHADOW" << space << e[0] << space
<< e[1] << space << e[2] << space << e[3] << push << ")";
break;
default:
// Print the top node in the default LISP format, continue with
// pretty-printing for children.
e.printAST(os);
break;
}
break; // end of case LISP_LANG
default:
// Print the top node in the default LISP format, continue with
// pretty-printing for children.
e.printAST(os);
}
return os;
}
Theorem TheoryArithOld::inequalityToFind(const Theorem& inequalityThm, bool normalizeRHS) {
// Which side of the inequality
int index = (normalizeRHS ? 1 : 0);
TRACE("arith find", "inequalityToFind(", int2string(index) + ", " + inequalityThm.getExpr().toString(), ")");
// Get the inequality expression
const Expr& inequality = inequalityThm.getExpr();
// The theorem we will return
Theorem inequalityFindThm;
// If the inequality side has a find
if (inequality[index].hasFind()) {
// Get the find of the rhs (lhs)
Theorem rhsFindThm = inequality[index].getFind();
// Get the theorem simplifys the find (in case the updates haven't updated all the finds yet
// Fixed with d_theroyCore.inUpdate()
rhsFindThm = transitivityRule(rhsFindThm, simplify(rhsFindThm.getRHS()));
// If not the same as the original
Expr rhsFind = rhsFindThm.getRHS();
if (rhsFind != inequality[index]) {
// Substitute in the inequality
vector changed;
vector children;
changed.push_back(index);
children.push_back(rhsFindThm);
rhsFindThm = iffMP(inequalityThm, substitutivityRule(inequality, changed, children));
// If on the left-hand side, we are done
if (index == 0)
inequalityFindThm = rhsFindThm;
else
// If on the right-hand side and left-hand side is 0, normalize it
if (inequality[0].isRational() && inequality[0].getRational() == 0)
inequalityFindThm = normalize(rhsFindThm);
else
inequalityFindThm = rhsFindThm;
} else
inequalityFindThm = inequalityThm;
} else
inequalityFindThm = inequalityThm;
TRACE("arith find", "inequalityToFind ==>", inequalityFindThm.getExpr(), "");
return inequalityFindThm;
}
void TheoryArithOld::registerAtom(const Expr& e) {
// Trace it
TRACE("arith atoms", "registerAtom(", e.toString(), ")");
// Mark it
formulaAtoms[e] = true;
// If it is a atomic formula, add it to the map
if (e.isAbsAtomicFormula() && isIneq(e)) {
Expr rightSide = e[1];
Rational leftSide = e[0].getRational();
//Get the terms for : c1 op t1 and t2 -op c2
Expr t1, t2;
Rational c1, c2;
extractTermsFromInequality(e, c1, t1, c2, t2);
if (true) {
TRACE("arith atoms", "registering lower bound for ", t1.toString(), " = " + c1.toString() + ")");
formulaAtomLowerBound[t1].insert(pair(c1, e));
// See if the bounds on the registered term can infered from already asserted facts
CDMap::iterator lowerBoundFind = termLowerBound.find(t1);
if (lowerBoundFind != termLowerBound.end()) {
Rational boundValue = (*lowerBoundFind).second;
Theorem boundThm = termLowerBoundThm[t1];
Expr boundIneq = boundThm.getExpr();
if (boundValue > c1 || (boundValue == c1 && !(boundIneq.getKind() == LE && e.getKind() == LT))) {
enqueueFact(getCommonRules()->implMP(boundThm, d_rules->implyWeakerInequality(boundIneq, e)));
}
}
// See if the bounds on the registered term can falsified from already asserted facts
CDMap::iterator upperBoundFind = termUpperBound.find(t1);
if (upperBoundFind != termUpperBound.end()) {
Rational boundValue = (*upperBoundFind).second;
Theorem boundThm = termUpperBoundThm[t1];
Expr boundIneq = boundThm.getExpr();
if (boundValue < c1 || (boundValue == c1 && boundIneq.getKind() == LT && e.getKind() == LT)) {
enqueueFact(getCommonRules()->implMP(boundThm, d_rules->implyNegatedInequality(boundIneq, e)));
}
}
TRACE("arith atoms", "registering upper bound for ", t2.toString(), " = " + c2.toString() + ")");
formulaAtomUpperBound[t2].insert(pair(c2, e));
}
}
}
TheoryArithOld::DifferenceLogicGraph::DifferenceLogicGraph(TheoryArithOld* arith, TheoryCore* core, ArithProofRules* rules, Context* context)
: d_pathLenghtThres(&(core->getFlags()["pathlength-threshold"].getInt())),
arith(arith),
core(core),
rules(rules),
unsat_theorem(context),
biggestEpsilon(context, 0, 0),
smallestPathDifference(context, 1, 0),
leGraph(context),
varInCycle(context)
{
}
Theorem TheoryArithOld::DifferenceLogicGraph::getUnsatTheorem() {
return unsat_theorem;
}
bool TheoryArithOld::DifferenceLogicGraph::isUnsat() {
return !getUnsatTheorem().isNull();
}
bool TheoryArithOld::DifferenceLogicGraph::existsEdge(const Expr& x, const Expr& y) {
Expr index = x - y;
Graph::iterator find_le = leGraph.find(index);
if (find_le != leGraph.end()) {
EdgeInfo edge_info = (*find_le).second;
if (edge_info.isDefined()) return true;
}
return false;
}
bool TheoryArithOld::DifferenceLogicGraph::inCycle(const Expr& x) {
return (varInCycle.find(x) != varInCycle.end());
}
TheoryArithOld::DifferenceLogicGraph::Graph::ElementReference TheoryArithOld::DifferenceLogicGraph::getEdge(const Expr& x, const Expr& y) {
Expr index = x - y;
Graph::ElementReference edge_info = leGraph[index];
// If a new edge and x != y, then add vertices to the apropriate lists
if (x != y && !edge_info.get().isDefined()) {
// Adding a new edge, take a resource
core->getResource();
EdgesList::iterator y_it = incomingEdges.find(y);
if (y_it == incomingEdges.end() || (*y_it).second == 0) {
CDList* list = new(true) CDList(core->getCM()->getCurrentContext());
list->push_back(x);
incomingEdges[y] = list;
} else
((*y_it).second)->push_back(x);
EdgesList::iterator x_it = outgoingEdges.find(x);
if (x_it == outgoingEdges.end() || (*x_it).second == 0) {
CDList* list = new(true) CDList(core->getCM()->getCurrentContext());
list->push_back(y);
outgoingEdges[x] = list;
} else
((*x_it).second)->push_back(y);
}
return edge_info;
}
TheoryArithOld::DifferenceLogicGraph::EpsRational TheoryArithOld::DifferenceLogicGraph::getEdgeWeight(const Expr& x, const Expr& y) {
if (!existsEdge(x, y))
return EpsRational::PlusInfinity;
else {
EdgeInfo edgeInfo = getEdge(x, y).get();
return edgeInfo.length;
}
}
void TheoryArithOld::DifferenceLogicGraph::addEdge(const Expr& x, const Expr& y, const Rational& bound, const Theorem& edge_thm) {
TRACE("arith diff", x, " --> ", y);
DebugAssert(x != y, "addEdge, given two equal expressions!");
if (isUnsat()) return;
// If out of resources, bail out
if (core->outOfResources()) return;
// Get the kind of the inequality (NOTE isNull -- for model computation we add a vertex with no theorem)
// FIXME: Later, add a debug assert for the theorem that checks that this variable is cvc3diffLogicSource
int kind = (edge_thm.isNull() ? LE : edge_thm.getExpr().getKind());
DebugAssert(kind == LT || kind == LE, "addEdge, not an <= or 0 && rationalDifference < smallestPathDifference) {
smallestPathDifference = rationalDifference;
TRACE("diff model", "smallest path difference : ", smallestPathDifference, "");
}
}
Rational newEpsilon = - c.getEpsilon();
if (newEpsilon > biggestEpsilon) {
biggestEpsilon = newEpsilon;
TRACE("diff model", "biggest epsilon : ", biggestEpsilon, "");
}
// Set the edge info
edgeInfo.length = c;
edgeInfo.explanation = edge_thm;
edgeInfo.path_length_in_edges = 1;
edgeInfoRef = edgeInfo;
// Try simple cycle x --> y --> x, to keep invariants (no cycles or one negative)
if (existsEdge(y, x)) {
varInCycle[x] = true;
varInCycle[y] = true;
tryUpdate(x, y, x);
if (isUnsat())
return;
}
// For all edges coming into x, z ---> x, update z ---> y and add updated ones to the updated_in_y vector
CDList* in_x = incomingEdges[x];
vector updated_in_y;
updated_in_y.push_back(x);
// If there
if (in_x) {
IF_DEBUG(int total = 0; int updated = 0;);
for (unsigned it = 0; it < in_x->size() && !isUnsat(); it ++) {
const Expr& z = (*in_x)[it];
if (z != arith->zero && z.hasFind() && core->find(z).getRHS() != z) continue;
if (z != y && z != x && x != y) {
IF_DEBUG(total ++;);
TRACE("diff update", "trying with ", z.toString() + " --> ", x.toString());
if (tryUpdate(z, x, y)) {
updated_in_y.push_back(z);
IF_DEBUG(updated++;);
}
}
}
TRACE("diff updates", "Updates : ", int2string(updated), " of " + int2string(total));
}
// For all edges coming into y, z_1 ---> y, and all edges going out of y, y ---> z_2, update z1 --> z_2
CDList* out_y = outgoingEdges[y];
if (out_y)
for (unsigned it_z1 = 0; it_z1 < updated_in_y.size() && !isUnsat(); it_z1 ++) {
for (unsigned it_z2 = 0; it_z2 < out_y->size() && !isUnsat(); it_z2 ++) {
const Expr& z1 = updated_in_y[it_z1];
const Expr& z2 = (*out_y)[it_z2];
if (z2 != arith->zero && z2.hasFind() && core->find(z2).getRHS() != z2) continue;
if (z1 != z2 && z1 != y && z2 != y)
tryUpdate(z1, y, z2);
}
}
} else {
TRACE("arith propagate", "could have propagated ", edge_thm.getExpr(), edge_thm.isAssump() ? " ASSUMPTION " : "not assumption");
}
}
void TheoryArithOld::DifferenceLogicGraph::getEdgeTheorems(const Expr& x, const Expr& z, const EdgeInfo& edgeInfo, std::vector& outputTheorems) {
TRACE("arith diff", "Getting theorems from ", x, " to " + z.toString() + " length = " + edgeInfo.length.toString() + ", edge_length = " + int2string(edgeInfo.path_length_in_edges));
if (edgeInfo.path_length_in_edges == 1) {
DebugAssert(x == sourceVertex || z == sourceVertex || !edgeInfo.explanation.isNull(), "Edge from " + x.toString() + " to " + z.toString() + " has no theorem!");
if (x != sourceVertex && z != sourceVertex)
outputTheorems.push_back(edgeInfo.explanation);
}
else {
const Expr& y = edgeInfo.in_path_vertex;
EdgeInfo x_y = getEdge(x, y);
DebugAssert(x_y.isDefined(), "getEdgeTheorems: the cycle edge is not defined!");
EdgeInfo y_z = getEdge(y, z);
DebugAssert(y_z.isDefined(), "getEdgeTheorems: the cycle edge is not defined!");
getEdgeTheorems(x, y, x_y, outputTheorems);
getEdgeTheorems(y, z, y_z, outputTheorems);
}
}
void TheoryArithOld::DifferenceLogicGraph::analyseConflict(const Expr& x, int kind) {
// Get the cycle info
Graph::ElementReference x_x_cycle_ref = getEdge(x, x);
EdgeInfo x_x_cycle = x_x_cycle_ref.get();
DebugAssert(x_x_cycle.isDefined(), "analyseConflict: the cycle edge is not defined!");
// Vector to keep the theorems in
vector inequalities;
// Get the theorems::analyse
getEdgeTheorems(x, x, x_x_cycle, inequalities);
// Set the unsat theorem
unsat_theorem = rules->cycleConflict(inequalities);
TRACE("diff unsat", "negative cycle : ", int2string(inequalities.size()), " vertices.");
}
bool TheoryArithOld::DifferenceLogicGraph::tryUpdate(const Expr& x, const Expr& y, const Expr& z) {
// x -> y -> z, if z -> x they are all in a cycle
if (existsEdge(z, x)) {
varInCycle[x] = true;
varInCycle[y] = true;
varInCycle[z] = true;
}
//Get all the edges
Graph::ElementReference x_y_le_ref = getEdge(x, y);
EdgeInfo x_y_le = x_y_le_ref;
if (*d_pathLenghtThres >= 0 && x_y_le.path_length_in_edges > *d_pathLenghtThres) return false;
Graph::ElementReference y_z_le_ref = getEdge(y, z);
EdgeInfo y_z_le = y_z_le_ref;
if (*d_pathLenghtThres >= 0 && y_z_le.path_length_in_edges > *d_pathLenghtThres) return false;
Graph::ElementReference x_z_le_ref = getEdge(x, z);
EdgeInfo x_z_le = x_z_le_ref;
bool cycle = (x == z);
bool updated = false;
// Try <= + <= --> <=
if (!isUnsat() && x_y_le.isDefined() && y_z_le.isDefined()) {
EpsRational combined_length = x_y_le.length + y_z_le.length;
int combined_edge_length = x_y_le.path_length_in_edges + y_z_le.path_length_in_edges;
if (!x_z_le.isDefined() || combined_length < x_z_le.length ||
(combined_length == x_z_le.length && (combined_edge_length < x_z_le.path_length_in_edges))) {
if (!cycle || combined_length <= EpsRational::Zero) {
if (!cycle || combined_length < EpsRational::Zero) {
// Remember the path differences
if (!cycle) {
EpsRational difference = x_z_le.length - combined_length;
Rational rationalDifference = difference.getRational();
Rational newEpsilon = - x_z_le.length.getEpsilon();
if (rationalDifference > 0 && rationalDifference < smallestPathDifference) {
smallestPathDifference = rationalDifference;
TRACE("diff model", "smallest path difference : ", smallestPathDifference, "");
}
if (newEpsilon > biggestEpsilon) {
biggestEpsilon = newEpsilon;
TRACE("diff model", "biggest epsilon : ", biggestEpsilon, "");
}
}
// If we have a constraint among two integers variables strenghten it
bool addAndEnqueue = false;
if (core->okToEnqueue() && !combined_length.isInteger())
if (x.getType() == arith->intType() && z.getType() == arith->intType())
addAndEnqueue = true;
x_z_le.length = combined_length;
x_z_le.path_length_in_edges = combined_edge_length;
x_z_le.in_path_vertex = y;
x_z_le_ref = x_z_le;
if (addAndEnqueue) {
vector pathTheorems;
getEdgeTheorems(x, z, x_z_le, pathTheorems);
core->enqueueFact(rules->addInequalities(pathTheorems));
}
TRACE("arith diff", x.toString() + " -- > " + z.toString(), " : ", combined_length.toString());
updated = true;
} else
if (core->okToEnqueue()) {
// 0 length cycle
vector antecedentThms;
getEdgeTheorems(x, y, x_y_le, antecedentThms);
getEdgeTheorems(y, z, y_z_le, antecedentThms);
core->enqueueFact(rules->implyEqualities(antecedentThms));
}
// Try to propagate somthing in the original formula
if (updated && !cycle && x != sourceVertex && z != sourceVertex && core->okToEnqueue())
arith->tryPropagate(x, z, x_z_le, LE);
}
if (cycle && combined_length < EpsRational::Zero)
analyseConflict(x, LE);
}
}
return updated;
}
void TheoryArithOld::DifferenceLogicGraph::expandSharedTerm(const Expr& x) {
}
TheoryArithOld::DifferenceLogicGraph::~DifferenceLogicGraph() {
for (EdgesList::iterator it = incomingEdges.begin(), it_end = incomingEdges.end(); it != it_end; it ++) {
if ((*it).second) {
delete (*it).second;
free ((*it).second);
}
}
for (EdgesList::iterator it = outgoingEdges.begin(), it_end = outgoingEdges.end(); it != it_end; it ++) {
if ((*it).second) {
delete (*it).second;
free ((*it).second);
}
}
}
void TheoryArithOld::tryPropagate(const Expr& x, const Expr& y, const DifferenceLogicGraph::EdgeInfo& x_y_edge, int kind) {
TRACE("diff atoms", "trying propagation", " x = " + x.toString(), " y = " + y.toString());
// bail on non representative terms (we don't pass non-representative terms)
// if (x.hasFind() && find(x).getRHS() != x) return;
// if (y.hasFind() && find(y).getRHS() != y) return;
// given edge x - z (kind) lenth
// Make the index (c1 <= y - x)
vector t1_summands;
t1_summands.push_back(rat(0));
if (y != zero) t1_summands.push_back(y);
// We have to canonize in case it is nonlinear
// nonlinear terms are canonized with a constants --> 1*x*y, hence (-1)*1*x*y will not be canonical
if (x != zero) t1_summands.push_back(canon(rat(-1)*x).getRHS());
Expr t1 = canon(plusExpr(t1_summands)).getRHS();
TRACE("diff atoms", "trying propagation", " t1 = " + t1.toString(), "");
// The constant c1 <= y - x
Rational c1 = - x_y_edge.length.getRational();
// See if we can propagate anything to the formula atoms
// c1 <= t1 ===> c <= t1 for c < c1
AtomsMap::iterator find = formulaAtomLowerBound.find(t1);
AtomsMap::iterator find_end = formulaAtomLowerBound.end();
if (find != find_end) {
set< pair >::iterator bounds = (*find).second.begin();
set< pair >::iterator bounds_end = (*find).second.end();
while (bounds != bounds_end) {
const Expr& implied = (*bounds).second;
// Try to do some theory propagation
if ((*bounds).first < c1 || (implied.getKind() == LE && (*bounds).first == c1)) {
TRACE("diff atoms", "found propagation", "", "");
// c1 <= t1 => c <= t1 (for c <= c1)
// c1 < t1 => c <= t1 (for c <= c1)
// c1 <= t1 => c < t1 (for c < c1)
vector antecedentThms;
diffLogicGraph.getEdgeTheorems(x, y, x_y_edge, antecedentThms);
Theorem impliedThm = d_rules->implyWeakerInequalityDiffLogic(antecedentThms, implied);
enqueueFact(impliedThm);
}
bounds ++;
}
}
//
// c1 <= t1 ==> !(t1 <= c) for c < c1
// ==> !(-c <= t2)
// i.e. all coefficient in in the implied are opposite of t1
find = formulaAtomUpperBound.find(t1);
find_end = formulaAtomUpperBound.end();
if (find != find_end) {
set< pair >::iterator bounds = (*find).second.begin();
set< pair >::iterator bounds_end = (*find).second.end();
while (bounds != bounds_end) {
const Expr& implied = (*bounds).second;
// Try to do some theory propagation
if ((*bounds).first < c1) {
TRACE("diff atoms", "found negated propagation", "", "");
vector antecedentThms;
diffLogicGraph.getEdgeTheorems(x, y, x_y_edge, antecedentThms);
Theorem impliedThm = d_rules->implyNegatedInequalityDiffLogic(antecedentThms, implied);
enqueueFact(impliedThm);
}
bounds ++;
}
}
}
void TheoryArithOld::DifferenceLogicGraph::computeModel() {
// If source vertex is null, create it
if (sourceVertex.isNull()) {
Theorem thm_exists_zero = arith->getCommonRules()->varIntroSkolem(arith->zero);
sourceVertex = thm_exists_zero.getExpr()[1];
}
// The empty theorem to pass around
Theorem thm;
// Add an edge to all the vertices
EdgesList::iterator vertexIt = incomingEdges.begin();
EdgesList::iterator vertexItEnd = incomingEdges.end();
for (; vertexIt != vertexItEnd; vertexIt ++) {
Expr vertex = (*vertexIt).first;
if (core->find(vertex).getRHS() != vertex) continue;
if (vertex != sourceVertex && !existsEdge(sourceVertex, vertex))
addEdge(sourceVertex, vertex, 0, thm);
}
vertexIt = outgoingEdges.begin();
vertexItEnd = outgoingEdges.end();
for (; vertexIt != vertexItEnd; vertexIt ++) {
Expr vertex = (*vertexIt).first;
if (core->find(vertex).getRHS() != vertex) continue;
if (vertex != sourceVertex && !existsEdge(sourceVertex, vertex))
addEdge(sourceVertex, vertex, 0, thm);
}
// Also add an edge to cvcZero
if (!existsEdge(sourceVertex, arith->zero))
addEdge(sourceVertex, arith->zero, 0, thm);
// For the < edges we will have a small enough epsilon to add
// So, we will upper-bound the number of vertices and then divide
// the smallest edge with that number so as to not be able to bypass
}
Rational TheoryArithOld::DifferenceLogicGraph::getValuation(const Expr& x) {
// For numbers, return it's value
if (x.isRational()) return x.getRational();
// For the source vertex, we don't care
if (x == sourceVertex) return 0;
// The path from source to targer vertex
Graph::ElementReference x_le_c_ref = getEdge(sourceVertex, x);
EdgeInfo x_le_c = x_le_c_ref;
// The path from source to zero (adjusment)
Graph::ElementReference zero_le_c_ref = getEdge(sourceVertex, arith->zero);
EdgeInfo zero_le_c = zero_le_c_ref;
TRACE("diff model", "zero adjustment: ", zero_le_c.length.getRational(), "");
TRACE("diff model", "zero adjustment (eps): ", zero_le_c.length.getEpsilon(), "");
// Value adjusted with the epsilon
Rational epsAdjustment = (biggestEpsilon > 0 ? (x_le_c.length.getEpsilon() - zero_le_c.length.getEpsilon()) * smallestPathDifference / (2 * (biggestEpsilon + 1)) : 0);
Rational value = x_le_c.length.getRational() + epsAdjustment;
TRACE("diff model" , "biggest epsilon: ", biggestEpsilon, "");
TRACE("diff model" , "smallestPathDifference: ", smallestPathDifference, "");
TRACE("diff model" , "x_le_c.getEpsilon: ", x_le_c.length.getEpsilon(), "");
TRACE("diff model" , "x_le_c.length: ", x_le_c.length.getRational(), "");
// Value adjusted with the shift for zero
value = zero_le_c.length.getRational() - value;
TRACE("diff model", "Value of ", x, " : " + value.toString());
// Return it
return value;
}
// The infinity constant
const TheoryArithOld::DifferenceLogicGraph::EpsRational TheoryArithOld::DifferenceLogicGraph::EpsRational::PlusInfinity(PLUS_INFINITY);
// The negative infinity constant
const TheoryArithOld::DifferenceLogicGraph::EpsRational TheoryArithOld::DifferenceLogicGraph::EpsRational::MinusInfinity(MINUS_INFINITY);
// The negative infinity constant
const TheoryArithOld::DifferenceLogicGraph::EpsRational TheoryArithOld::DifferenceLogicGraph::EpsRational::Zero;
void TheoryArithOld::addMultiplicativeSignSplit(const Theorem& case_split_thm) {
multiplicativeSignSplits.push_back(case_split_thm);
}
bool TheoryArithOld::addPairToArithOrder(const Expr& smaller, const Expr& bigger) {
TRACE("arith var order", "addPairToArithOrder(" + smaller.toString(), ", ", bigger.toString() + ")");
// We only accept arithmetic terms
if (!isReal(smaller.getType()) && !isInt(smaller.getType())) return false;
if (!isReal(bigger.getType()) && !isInt(bigger.getType())) return false;
// We don't want to introduce loops
FatalAssert(!d_graph.lessThan(smaller, bigger), "The pair (" + bigger.toString() + "," + smaller.toString() + ") is already in the order");
// Update the graph
d_graph.addEdge(smaller, bigger);
return true;
}
bool TheoryArithOld::isNonlinearSumTerm(const Expr& term) {
if (isPow(term)) return true;
if (!isMult(term)) return false;
int vars = 0;
for (int j = 0; j < term.arity(); j ++)
if (isPow(term[j])) return true;
else if (isLeaf(term[j])) {
vars ++;
if (vars > 1) return true;
}
return false;
}
bool TheoryArithOld::isNonlinearEq(const Expr& e) {
DebugAssert(e.isEq(), "TheoryArithOld::isNonlinear: expecting an equation" + e.toString());
const Expr& lhs = e[0];
const Expr& rhs = e[1];
if (isNonlinearSumTerm(lhs) || isNonlinearSumTerm(rhs)) return true;
// Check the right-hand side
for (int i = 0; i < lhs.arity(); i ++)
if (isNonlinearSumTerm(lhs[i])) return true;
// Check the left hand side
for (int i = 0; i < rhs.arity(); i ++)
if (isNonlinearSumTerm(rhs[i])) return true;
return false;
}
bool TheoryArithOld::isPowersEquality(const Expr& eq, Expr& power1, Expr& power2) {
// equality should be in the form 0 + x1^n - x2^n = 0
DebugAssert(eq.isEq(), "TheoryArithOld::isPowersEquality, expecting an equality got " + eq.toString());
if (!isPlus(eq[0])) return false;
if (eq[0].arity() != 3) return false;
if (!(eq[0][0].isRational()) || !(eq[0][0].getRational() == 0)) return false;
// Process the first term
Expr term1 = eq[0][1];
Rational term1_c;
if (isPow(term1)) {
term1_c = 1;
power1 = term1;
} else
if (isMult(term1) && term1.arity() == 2) {
if (term1[0].isRational()) {
term1_c = term1[0].getRational();
if (isPow(term1[1])) {
if (term1_c == 1) power1 = term1[1];
else if (term1_c == -1) power2 = term1[1];
else return false;
} else return false;
} else return false;
} else return false;
// Process the second term
Expr term2 = eq[0][2];
Rational term2_c;
if (isPow(term2)) {
term2_c = 1;
power1 = term2;
} else
if (isMult(term2) && term2.arity() == 2) {
if (term2[0].isRational()) {
term2_c = term2[0].getRational();
if (isPow(term2[1])) {
if (term2_c == 1) power1 = term2[1];
else if (term2_c == -1) power2 = term2[1];
else return false;
} else return false;
} else return false;
} else return false;
// Check that they are of opposite signs
if (term1_c == term2_c) return false;
// Check that the powers are equal numbers
if (!power1[0].isRational()) return false;
if (!power2[0].isRational()) return false;
if (power1[0].getRational() != power2[0].getRational()) return false;
// Everything is fine
return true;
}
bool TheoryArithOld::isPowerEquality(const Expr& eq, Rational& constant, Expr& power1) {
DebugAssert(eq.isEq(), "TheoryArithOld::isPowerEquality, expecting an equality got " + eq.toString());
if (!isPlus(eq[0])) return false;
if (eq[0].arity() != 2) return false;
if (!eq[0][0].isRational()) return false;
constant = eq[0][0].getRational();
Expr term = eq[0][1];
if (isPow(term)) {
power1 = term;
constant = -constant;
} else
if (isMult(term) && term.arity() == 2) {
if (term[0].isRational() && isPow(term[1])) {
Rational term2_c = term[0].getRational();
if (term2_c == 1) {
power1 = term[1];
constant = -constant;
} else if (term2_c == -1) {
power1 = term[1];
return true;
} else return false;
} else return false;
} else return false;
// Check that the power is an integer
if (!power1[0].isRational()) return false;
if (!power1[0].getRational().isInteger()) return false;
return true;
}
int TheoryArithOld::termDegree(const Expr& e) {
if (isLeaf(e)) return 1;
if (isPow(e)) return termDegree(e[1]) * e[0].getRational().getInt();
if (isMult(e)) {
int degree = 0;
for (int i = 0; i < e.arity(); i ++) degree += termDegree(e[i]);
return degree;
}
return 0;
}
bool TheoryArithOld::canPickEqMonomial(const Expr& right)
{
DebugAssert(right.arity() > 1, "TheoryArithOld::canPickEqMonomial, expecting > 1 child, got " + right.arity());
Expr::iterator istart = right.begin();
Expr::iterator iend = right.end();
// Skip the first one
istart++;
for(Expr::iterator i = istart; i != iend; ++i) {
Expr leaf;
Rational coeff;
// Check if linear term
if (isLeaf(*i)) {
leaf = *i;
coeff = 1;
} else if (isMult(*i) && (*i).arity() == 2 && (*i)[0].isRational() && isLeaf((*i)[1])) {
leaf = (*i)[1];
coeff = abs((*i)[0].getRational());
} else
continue;
// If integer, must be coeff 1/-1
if (!isIntegerThm(leaf).isNull())
if (coeff != 1 && coeff != -1)
continue;
// Check if a leaf in other ones
Expr::iterator j;
for (j = istart; j != iend; ++j)
if (j != i && isLeafIn(leaf, *j))
break;
if (j == iend)
return true;
}
return false;
}
bool TheoryArithOld::isBounded(const Expr& t, BoundsQueryType queryType) {
TRACE("arith shared", "isBounded(", t.toString(), ")");
return hasUpperBound(t, queryType) && hasLowerBound(t, queryType);
}
TheoryArithOld::DifferenceLogicGraph::EpsRational TheoryArithOld::getUpperBound(const Expr& t, BoundsQueryType queryType)
{
TRACE("arith shared", "getUpperBound(", t.toString(), ")");
// If t is a constant it's bounded
if (t.isRational()) {
TRACE("arith shared", "getUpperBound(", t.toString(), ") ==> " + t.getRational().toString());
return t.getRational();
}
// If buffered, just return it
CDMap::iterator find_t = termUpperBounded.find(t);
if (find_t != termUpperBounded.end()) {
TRACE("arith shared", "getUpperBound(", t.toString(), ") ==> " + (*find_t).second.toString());
return (*find_t).second;
} else if (queryType == QueryWithCacheAll) {
// Asked for cache query, so no bound is found
TRACE("arith shared", "getUpperBound(", t.toString(), ") ==> +inf");
return DifferenceLogicGraph::EpsRational::PlusInfinity;
}
// Assume it's not bounded
DifferenceLogicGraph::EpsRational upperBound = DifferenceLogicGraph::EpsRational::PlusInfinity;
// We always buffer the leaves, so all that's left are the terms
if (!isLeaf(t)) {
if (isMult(t)) {
// We only handle linear terms
if (!isNonlinearSumTerm(t)) {
// Separate the multiplication
Expr c, v;
separateMonomial(t, c, v);
// Get the upper-bound for the variable
if (c.getRational() > 0) upperBound = getUpperBound(v);
else upperBound = getLowerBound(v);
if (upperBound.isFinite()) upperBound = upperBound * c.getRational();
else upperBound = DifferenceLogicGraph::EpsRational::PlusInfinity;
}
} else if (isPlus(t)) {
// If one of them is unconstrained then the term itself is unconstrained
upperBound = DifferenceLogicGraph::EpsRational::Zero;
for (int i = 0; i < t.arity(); i ++) {
Expr t_i = t[i];
DifferenceLogicGraph::EpsRational t_i_upperBound = getUpperBound(t_i, queryType);
if (t_i_upperBound.isFinite()) upperBound = upperBound + t_i_upperBound;
else {
upperBound = DifferenceLogicGraph::EpsRational::PlusInfinity;
// Not-bounded, check for constrained
if (queryType == QueryWithCacheLeavesAndConstrainedComputation) {
for(; i < t.arity() && isConstrainedAbove(t[i], QueryWithCacheLeaves); i ++);
if (i == t.arity()) {
TRACE("arith shared", "getUpperBound(", t.toString(), ") ==> constrained");
termConstrainedAbove[t] = true;
}
break;
} else break;
}
}
}
}
// Buffer it
if (upperBound.isFinite()) {
termUpperBounded[t] = upperBound;
termConstrainedAbove[t] = true;
}
// Return if bounded or not
TRACE("arith shared", "getUpperBound(", t.toString(), ") ==> " + upperBound.toString());
return upperBound;
}
TheoryArithOld::DifferenceLogicGraph::EpsRational TheoryArithOld::getLowerBound(const Expr& t, BoundsQueryType queryType)
{
TRACE("arith shared", "getLowerBound(", t.toString(), ")");
// If t is a constant it's bounded
if (t.isRational()) {
TRACE("arith shared", "getLowerBound(", t.toString(), ") ==> " + t.getRational().toString());
return t.getRational();
}
// If buffered, just return it
CDMap::iterator t_find = termLowerBounded.find(t);
if (t_find != termLowerBounded.end()) {
TRACE("arith shared", "getLowerBound(", t.toString(), ") ==> " + (*t_find).second.toString());
return (*t_find).second;
} else if (queryType == QueryWithCacheAll) {
// Asked for cache query, so no bound is found
TRACE("arith shared", "getLowerBound(", t.toString(), ") ==> -inf");
return DifferenceLogicGraph::EpsRational::MinusInfinity;
}
// Assume it's not bounded
DifferenceLogicGraph::EpsRational lowerBound = DifferenceLogicGraph::EpsRational::MinusInfinity;
// Leaves are always buffered
if (!isLeaf(t)) {
if (isMult(t)) {
// We only handle linear terms
if (!isNonlinearSumTerm(t)) {
// Separate the multiplication
Expr c, v;
separateMonomial(t, c, v);
// Get the upper-bound for the variable
if (c.getRational() > 0) lowerBound = getLowerBound(v);
else lowerBound = getUpperBound(v);
if (lowerBound.isFinite()) lowerBound = lowerBound * c.getRational();
else lowerBound = DifferenceLogicGraph::EpsRational::MinusInfinity;
}
} else if (isPlus(t)) {
// If one of them is unconstrained then the term itself is unconstrained
lowerBound = DifferenceLogicGraph::EpsRational::Zero;
for (int i = 0; i < t.arity(); i ++) {
Expr t_i = t[i];
DifferenceLogicGraph::EpsRational t_i_lowerBound = getLowerBound(t_i, queryType);
if (t_i_lowerBound.isFinite()) lowerBound = lowerBound + t_i_lowerBound;
else {
lowerBound = DifferenceLogicGraph::EpsRational::MinusInfinity;
// Not-bounded, check for constrained
if (queryType == QueryWithCacheLeavesAndConstrainedComputation) {
for(; i < t.arity() && isConstrainedBelow(t[i], QueryWithCacheLeaves); i ++);
if (i == t.arity()) {
TRACE("arith shared", "getLowerBound(", t.toString(), ") ==> constrained");
termConstrainedBelow[t] = true;
}
break;
} else break;
}
}
}
}
// Buffer it
if (lowerBound.isFinite()) {
termLowerBounded[t] = lowerBound;
termConstrainedBelow[t] = true;
}
// Return if bounded or not
TRACE("arith shared", "getLowerBound(", t.toString(), ") ==> " + lowerBound.toString());
return lowerBound;
}
int TheoryArithOld::computeTermBounds()
{
int computeTermBoundsConstrainedCount = 0;
vector sorted_vars;
// Get the variables in the topological order
if (!diffLogicOnly) d_graph.getVerticesTopological(sorted_vars);
// Or if difference logic only, just get them
else {
diffLogicGraph.getVariables(sorted_vars);
IF_DEBUG(
diffLogicGraph.writeGraph(cerr);
)
}
// Go in the reverse topological order and try to see if the vats are constrained/bounded
for (int i = sorted_vars.size() - 1; i >= 0; i --)
{
// Get the variable
Expr v = sorted_vars[i];
// If the find is not identity, skip it
if (v.hasFind() && find(v).getRHS() != v) continue;
TRACE("arith shared", "processing: ", v.toString(), "");
// If the variable is not an integer, it's unconstrained, unless we are in model generation
if (isIntegerThm(v).isNull() && !d_inModelCreation) continue;
// We only do the computation if the variable is not already constrained
if (!isConstrained(v, QueryWithCacheAll)) {
// Recall if we already computed the constraint
bool constrainedAbove = isConstrained(v, QueryWithCacheAll);
// See if it's bounded from above in the difference graph
DifferenceLogicGraph::EpsRational upperBound = diffLogicGraph.getEdgeWeight(v, zero);
if (!constrainedAbove) constrainedAbove = upperBound.isFinite();
// Try to refine the bound by checking projected inequalities
if (!diffLogicOnly) {
ExprMap *>::iterator v_left_find = d_inequalitiesLeftDB.find(v);
// If not constraint from one side, it's unconstrained
if (v_left_find != d_inequalitiesLeftDB.end()) {
// Check right hand side for an unconstrained variable
CDList*& left_list = (*v_left_find).second;
if (left_list && left_list->size() > 0) {
for (unsigned ineq_i = 0; ineq_i < left_list->size(); ineq_i ++) {
// Get the inequality
Ineq ineq = (*left_list)[ineq_i];
// Get the right-hand side (v <= rhs)
Expr rhs = ineq.ineq().getExpr()[1];
// If rhs changed, skip it
if (rhs.hasFind() && find(rhs).getRHS() != rhs) continue;
// Compute the upper bound while
DifferenceLogicGraph::EpsRational currentUpperBound = getUpperBound(rhs, (constrainedAbove ? QueryWithCacheLeaves : QueryWithCacheLeavesAndConstrainedComputation));
if (currentUpperBound.isFinite() && (!upperBound.isFinite() || currentUpperBound < upperBound)) {
upperBound = currentUpperBound;
constrainedAbove = true;
}
// If not constrained, check if right-hand-side is constrained
if (!constrainedAbove) constrainedAbove = isConstrainedAbove(rhs, QueryWithCacheAll);
}
}
}
}
// Difference logic case (no projections)
else if (!constrainedAbove) {
// If there is no incoming edges, then the variable is not constrained
if (!diffLogicGraph.hasIncoming(v)) constrainedAbove = false;
// If there is a cycle from t to t, all the variables
// in the graph are constrained by each-other (we could
// choose one, but it's too complicated)
else if (diffLogicGraph.inCycle(v)) constrainedAbove = true;
// Otherwise, since there is no bounds, and the cycles
// can be shifted (since one of them can be taken as
// unconstrained), we can assume that the variables is
// not constrained. Conundrum here is that when in model-generation
// we actually should take it as constrained so that it's
// split on and we are on the safe side
else constrainedAbove = d_inModelCreation;
}
// Cache the upper bound and upper constrained computation
if (constrainedAbove) termConstrainedAbove[v] = true;
if (upperBound.isFinite()) termUpperBounded[v] = upperBound;
// Recall the below computation if it's there
bool constrainedBelow = isConstrainedBelow(v, QueryWithCacheAll);
// See if it's bounded from below in the difference graph
DifferenceLogicGraph::EpsRational lowerBound = diffLogicGraph.getEdgeWeight(zero, v);
if (lowerBound.isFinite()) lowerBound = -lowerBound;
else lowerBound = DifferenceLogicGraph::EpsRational::MinusInfinity;
if (!constrainedBelow) constrainedBelow = lowerBound.isFinite();
// Try to refine the bound by checking projected inequalities
if (!diffLogicOnly) {
ExprMap *>::iterator v_right_find = d_inequalitiesRightDB.find(v);
// If not constraint from one side, it's unconstrained
if (v_right_find != d_inequalitiesRightDB.end()) {
// Check right hand side for an unconstrained variable
CDList*& right_list = (*v_right_find).second;
if (right_list && right_list->size() > 0) {
for (unsigned ineq_i = 0; ineq_i < right_list->size(); ineq_i ++) {
// Get the inequality
Ineq ineq = (*right_list)[ineq_i];
// Get the right-hand side (lhs <= 0)
Expr lhs = ineq.ineq().getExpr()[0];
// If lhs has changed, skip it
if (lhs.hasFind() && find(lhs).getRHS() != lhs) continue;
// Compute the lower bound
DifferenceLogicGraph::EpsRational currentLowerBound = getLowerBound(lhs, (constrainedBelow ? QueryWithCacheLeaves : QueryWithCacheLeavesAndConstrainedComputation));
if (currentLowerBound.isFinite() && (!lowerBound.isFinite() || currentLowerBound > lowerBound)) {
lowerBound = currentLowerBound;
constrainedBelow = true;
}
// If not constrained, check if right-hand-side is constrained
if (!constrainedBelow) constrainedBelow = isConstrainedBelow(lhs, QueryWithCacheAll);
}
}
}
}
// Difference logic case (no projections)
else if (!constrainedBelow) {
// If there is no incoming edges, then the variable is not constrained
if (!diffLogicGraph.hasOutgoing(v)) constrainedBelow = false;
// If there is a cycle from t to t, all the variables
// in the graph are constrained by each-other (we could
// choose one, but it's too complicated)
else if (diffLogicGraph.inCycle(v)) constrainedBelow = true;
// Otherwise, since there is no bounds, and the cycles
// can be shifted (since one of them can be taken as
// unconstrained), we can assume that the variables is
// not constrained. Conundrum here is that when in model-generation
// we actually should take it as constrained so that it's
// split on and we are on the safe side
else constrainedBelow = d_inModelCreation;
}
// Cache the lower bound and lower constrained computation
if (constrainedBelow) termConstrainedBelow[v] = true;
if (lowerBound.isFinite()) termLowerBounded[v] = lowerBound;
// Is this variable constrained
if (constrainedAbove && constrainedBelow) computeTermBoundsConstrainedCount ++;
TRACE("arith shared", (constrainedAbove && constrainedBelow ? "constrained " : "unconstrained "), "", "");
} else
computeTermBoundsConstrainedCount ++;
}
TRACE("arith shared", "number of constrained variables : ", int2string(computeTermBoundsConstrainedCount), " of " + int2string(sorted_vars.size()));
return computeTermBoundsConstrainedCount;
}
bool TheoryArithOld::isConstrainedAbove(const Expr& t, BoundsQueryType queryType)
{
TRACE("arith shared", "isConstrainedAbove(", t.toString(), ")");
// Rational numbers are constrained
if (t.isRational()) {
TRACE("arith shared", "isConstrainedAbove() ==> true", "", "");
return true;
}
// Look it up in the cache
CDMap::iterator t_find = termConstrainedAbove.find(t);
if (t_find != termConstrainedAbove.end()) {
TRACE("arith shared", "isConstrainedAbove() ==> true", "", "");
return true;
}
else if (queryType == QueryWithCacheAll) {
TRACE("arith shared", "isConstrainedAbove() ==> false", "", "");
return false;
}
bool constrainedAbove = true;
if (isLeaf(t)) {
// Leaves are always cached
constrainedAbove = false;
} else {
if (isMult(t)) {
// Non-linear terms are constrained by default
// we only deal with the linear stuff
if (!isNonlinearSumTerm(t)) {
// Separate the multiplication
Expr c, v;
separateMonomial(t, c, v);
// Check if the variable is constrained
if (c.getRational() > 0) constrainedAbove = isConstrainedAbove(v, queryType);
else constrainedAbove = isConstrainedBelow(v, queryType);
}
} else if (isPlus(t)) {
// If one of them is unconstrained then the term itself is unconstrained
for (int i = 0; i < t.arity() && constrainedAbove; i ++)
if (!isConstrainedAbove(t[i])) constrainedAbove = false;
}
}
// Remember it
if (constrainedAbove) termConstrainedAbove[t] = true;
TRACE("arith shared", "isConstrainedAbove() ==> ", constrainedAbove ? "true" : "false", "");
// Return in
return constrainedAbove;
}
bool TheoryArithOld::isConstrainedBelow(const Expr& t, BoundsQueryType queryType)
{
TRACE("arith shared", "isConstrainedBelow(", t.toString(), ")");
// Rational numbers are constrained
if (t.isRational()) return true;
// Look it up in the cache
CDMap::iterator t_find = termConstrainedBelow.find(t);
if (t_find != termConstrainedBelow.end()) {
TRACE("arith shared", "isConstrainedBelow() ==> true", "", "");
return true;
}
else if (queryType == QueryWithCacheAll) {
TRACE("arith shared", "isConstrainedBelow() ==> false", "", "");
return false;
}
bool constrainedBelow = true;
if (isLeaf(t)) {
// Leaves are always cached
constrainedBelow = false;
} else {
if (isMult(t)) {
// Non-linear terms are constrained by default
// we only deal with the linear stuff
if (!isNonlinearSumTerm(t)) {
// Separate the multiplication
Expr c, v;
separateMonomial(t, c, v);
// Check if the variable is constrained
if (c.getRational() > 0) constrainedBelow = isConstrainedBelow(v, queryType);
else constrainedBelow = isConstrainedAbove(v, queryType);
}
} else if (isPlus(t)) {
// If one of them is unconstrained then the term itself is unconstrained
constrainedBelow = true;
for (int i = 0; i < t.arity() && constrainedBelow; i ++)
if (!isConstrainedBelow(t[i]))
constrainedBelow = false;
}
}
// Cache it
if (constrainedBelow) termConstrainedBelow[t] = true;
TRACE("arith shared", "isConstrainedBelow() ==> ", constrainedBelow ? "true" : "false", "");
// Return it
return constrainedBelow;
}
bool TheoryArithOld::isConstrained(const Expr& t, bool intOnly, BoundsQueryType queryType)
{
TRACE("arith shared", "isConstrained(", t.toString(), ")");
// For the reals we consider them unconstrained if not asked for full check
if (intOnly && isIntegerThm(t).isNull()) return false;
bool result = (isConstrainedAbove(t, queryType) && isConstrainedBelow(t, queryType));
TRACE("arith shared", "isConstrained(", t.toString(), (result ? ") ==> true " : ") ==> false ") );
return result;
}
bool TheoryArithOld::DifferenceLogicGraph::hasIncoming(const Expr& x)
{
EdgesList::iterator find_x = incomingEdges.find(x);
// No edges at all meaning no incoming
if (find_x == incomingEdges.end()) return false;
// The pointer being null, also no incoming
CDList*& list = (*find_x).second;
if (!list) return false;
// If in model creation, source vertex goes to all vertices
if (sourceVertex.isNull())
return list->size() > 0;
else
return list->size() > 1;
}
bool TheoryArithOld::DifferenceLogicGraph::hasOutgoing(const Expr& x)
{
EdgesList::iterator find_x = outgoingEdges.find(x);
// No edges at all meaning no incoming
if (find_x == outgoingEdges.end()) return false;
// The pointer being null, also no incoming
CDList*& list = (*find_x).second;
if (!list) return false;
// If the list is not empty we have outgoing edges
return list->size() > 0;
}
void TheoryArithOld::DifferenceLogicGraph::getVariables(vector& variables)
{
set vars_set;
EdgesList::iterator incoming_it = incomingEdges.begin();
EdgesList::iterator incoming_it_end = incomingEdges.end();
while (incoming_it != incoming_it_end) {
Expr var = (*incoming_it).first;
if (var != sourceVertex)
vars_set.insert(var);
incoming_it ++;
}
EdgesList::iterator outgoing_it = outgoingEdges.begin();
EdgesList::iterator outgoing_it_end = outgoingEdges.end();
while (outgoing_it != outgoing_it_end) {
Expr var = (*outgoing_it).first;
if (var != sourceVertex)
vars_set.insert(var);
outgoing_it ++;
}
set::iterator set_it = vars_set.begin();
set::iterator set_it_end = vars_set.end();
while (set_it != set_it_end) {
variables.push_back(*set_it);
set_it ++;
}
}
void TheoryArithOld::DifferenceLogicGraph::writeGraph(ostream& out) {
return;
out << "digraph G {" << endl;
EdgesList::iterator incoming_it = incomingEdges.begin();
EdgesList::iterator incoming_it_end = incomingEdges.end();
while (incoming_it != incoming_it_end) {
Expr var_u = (*incoming_it).first;
CDList* edges = (*incoming_it).second;
if (edges)
for (unsigned edge_i = 0; edge_i < edges->size(); edge_i ++) {
Expr var_v = (*edges)[edge_i];
out << var_u.toString() << " -> " << var_v.toString() << endl;
}
incoming_it ++;
}
out << "}" << endl;
}
bool TheoryArithOld::isUnconstrained(const Expr& t) {
if (isPlus(t)) {
for (int i = 0; i < t.arity(); ++ i) {
if (isUnconstrained(t[i])) {
TRACE("arith::unconstrained", "isUnconstrained(", t, ") => true (subterm)");
return true;
}
}
} else {
Expr c, var;
separateMonomial(t, c, var);
if (var.isRational()) {
TRACE("arith::unconstrained", "isUnconstrained(", t, ") => false (rational)");
return false;
}
if (isMult(var)) {
TRACE("arith::unconstrained", "isUnconstrained(", t, ") => false (multiplication)");
return false;
}
if (diffLogicOnly) {
if (!diffLogicGraph.hasIncoming(var) || !diffLogicGraph.hasOutgoing(var)) {
return true;
}
} else if (d_varConstrainedPlus.find(var) == d_varConstrainedPlus.end() || d_varConstrainedMinus.find(var) == d_varConstrainedMinus.end()) {
return true;
}
}
TRACE("arith::unconstrained", "isUnconstrained(", t, ") => false");
return false;
}
void TheoryArithOld::updateConstrained(const Expr& t) {
TRACE("arith::unconstrained", "updateConstrained(", t, ")");
if (isIneq(t)) {
updateConstrained(t[1]);
} else if (isPlus(t)) {
for (int i = 0; i < t.arity(); ++ i) {
updateConstrained(t[i]);
}
} else {
Expr c, var;
separateMonomial(t, c, var);
if (var.isRational() || isMult(var)) {
return;
}
if (c.getRational() < 0) {
d_varConstrainedMinus[var] = true;
} else {
d_varConstrainedPlus[var] = true;
}
}
}