From 9fe111daad65bc1b6375cc5ed18d3c8eba65887f Mon Sep 17 00:00:00 2001 From: Tim King Date: Wed, 21 Nov 2012 18:46:23 +0000 Subject: [PATCH] - Removes getDeltaValueWithNonlinear() entirely - Changes the signature of getDeltaValue to throw DeltaRationalException and ModelException -- DeltaRationalExceptions can occur with non-linear arithmetic computations that cannot be done. (0 + delta) * (1 + delta) is not a DeltaRational. -- ModelExceptions occur if getDeltaValue() is going to return a value that disagrees with its value in the model (due to non-linear arithmetic) -- ModelExceptions also occur if getDeltaValue(n) is called on a variable arithmetic has never seen before. - getEqualityStatus() now wraps and catches both of these exceptions. If either occurs, the equality status is EQUALITY_UNKNOWN. This allows arithmetic to handle terms it has never seen before in getEqualityStatus. This resolves bug 453. - Removes the dead code rowImplication() entirely. --- src/theory/arith/theory_arith.cpp | 275 +++++++++--------------------- src/theory/arith/theory_arith.h | 13 +- 2 files changed, 82 insertions(+), 206 deletions(-) diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index c69c1e92e..27883abcb 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -144,6 +144,14 @@ Node TheoryArith::getIntModulusBy0Func(){ return d_intModulusBy0Func; } +TheoryArith::ModelException::ModelException(TNode n, const char* msg) throw (){ + stringstream ss; + ss << "Cannot construct a model for " << n << " as " << endl << msg; + setMessage(ss.str()); +} +TheoryArith::ModelException::~ModelException() throw (){ } + + TheoryArith::Statistics::Statistics(): d_statAssertUpperConflicts("theory::arith::AssertUpperConflicts", 0), d_statAssertLowerConflicts("theory::arith::AssertLowerConflicts", 0), @@ -1948,35 +1956,8 @@ void TheoryArith::propagate(Effort e) { } } -bool TheoryArith::getDeltaAtomValue(TNode n) const { - Assert(d_qflraStatus != Result::SAT_UNKNOWN); - - switch (n.getKind()) { - case kind::EQUAL: // 2 args - return getDeltaValue(n[0]) == getDeltaValue(n[1]); - case kind::LT: // 2 args - return getDeltaValue(n[0]) < getDeltaValue(n[1]); - case kind::LEQ: // 2 args - return getDeltaValue(n[0]) <= getDeltaValue(n[1]); - case kind::GT: // 2 args - return getDeltaValue(n[0]) > getDeltaValue(n[1]); - case kind::GEQ: // 2 args - return getDeltaValue(n[0]) >= getDeltaValue(n[1]); - default: - Unreachable(); - } -} - -Exception nlException(TNode t){ - stringstream ss; - ss << "Cannot generate a DeltaRational value for non-linear term: "; - ss << t; - return Exception(ss.str()); -} - -DeltaRational TheoryArith::getDeltaValue(TNode n) const { +DeltaRational TheoryArith::getDeltaValue(TNode n) const throw (DeltaRationalException, ModelException) { AlwaysAssert(d_qflraStatus != Result::SAT_UNKNOWN); - AlwaysAssert(!d_nlIncomplete); Debug("arith::value") << n << std::endl; switch(n.getKind()) { @@ -1986,150 +1967,83 @@ DeltaRational TheoryArith::getDeltaValue(TNode n) const { case kind::PLUS: { // 2+ args DeltaRational value(0); - for(TNode::iterator i = n.begin(), - iend = n.end(); - i != iend; - ++i) { + for(TNode::iterator i = n.begin(), iend = n.end(); i != iend; ++i) { value = value + getDeltaValue(*i); } return value; } case kind::MULT: { // 2+ args - if (n[0].getKind() == kind::CONST_RATIONAL && n.getNumChildren() == 2) { - return getDeltaValue(n[1]) * n[0].getConst(); - } else { - DeltaRational value(1,0); - for(TNode::iterator i = n.begin(), i_e = n.end(); i != i_e; ++i){ - DeltaRational curr = getDeltaValue(*i); - if(value.infinitesimalSgn() != 0 && curr.infinitesimalSgn() != 0){ - throw nlException(n); - }else if(curr.infinitesimalSgn() != 0){ - Rational q = value.getNoninfinitesimalPart(); - value = curr * q; - }else{ - Rational q = curr.getNoninfinitesimalPart(); - value = value * q; - } + DeltaRational value(1); + unsigned variableParts = 0; + for(TNode::iterator i = n.begin(), iend = n.end(); i != iend; ++i) { + TNode curr = *i; + value = value * getDeltaValue(curr); + if(!curr.isConst()){ + ++variableParts; + } + } + // TODO: This is a bit of a weak check + if(isSetup(n)){ + ArithVar var = d_arithvarNodeMap.asArithVar(n); + const DeltaRational& assign = d_partialModel.getAssignment(var); + if(assign != value){ + throw ModelException(n, "Model disagrees on non-linear term."); } - return value; } + return value; } - - case kind::MINUS: // 2 args + case kind::MINUS:{ // 2 args return getDeltaValue(n[0]) - getDeltaValue(n[1]); + } - case kind::UMINUS: // 1 arg + case kind::UMINUS:{ // 1 arg return (- getDeltaValue(n[0])); + } - case kind::DIVISION: // 2 args - case kind::INTS_DIVISION_TOTAL: - case kind::INTS_MODULUS_TOTAL: - case kind::DIVISION_TOTAL: + case kind::DIVISION:{ // 2 args + DeltaRational res = getDeltaValue(n[0]) / getDeltaValue(n[1]); if(isSetup(n)){ ArithVar var = d_arithvarNodeMap.asArithVar(n); - return d_partialModel.getAssignment(var); + if(d_partialModel.getAssignment(var) != res){ + throw ModelException(n, "Model disagrees on non-linear term."); + } + } + return res; + } + case kind::DIVISION_TOTAL: + case kind::INTS_DIVISION_TOTAL: + case kind::INTS_MODULUS_TOTAL: { // 2 args + DeltaRational denom = getDeltaValue(n[1]); + if(denom.isZero()){ + return DeltaRational(0,0); }else{ - DeltaRational den_dr = getDeltaValue(n[1]); - if(den_dr.infinitesimalSgn() == 0){ - Rational d = den_dr.getNoninfinitesimalPart(); - if(d.isZero()){ - return DeltaRational(0,0); - }else if(n.getKind() == kind::DIVISION_TOTAL){ - return getDeltaValue(n[0]) / d; - }else{ - DeltaRational num = getDeltaValue(n[0]); - if(num.isIntegral() && d.isIntegral()){ - Integer ni = num.getNoninfinitesimalPart().getNumerator(); - Integer di = d.getNumerator(); - - Integer res = (n.getKind() == kind::INTS_DIVISION_TOTAL) ? - ni.floorDivideQuotient(di) : ni.floorDivideRemainder(di); - return DeltaRational(res); - }else{ - throw nlException(n); - } - } + DeltaRational numer = getDeltaValue(n[0]); + DeltaRational res; + if(n.getKind() == kind::DIVISION_TOTAL){ + res = numer / denom; + }else if(n.getKind() == kind::INTS_DIVISION_TOTAL){ + res = Rational(numer.floorDivideQuotient(denom)); }else{ - throw nlException(n); + Assert(n.getKind() == kind::INTS_MODULUS_TOTAL); + res = Rational(numer.floorDivideRemainder(denom)); } - } - - default: - { if(isSetup(n)){ ArithVar var = d_arithvarNodeMap.asArithVar(n); - return d_partialModel.getAssignment(var); - }else{ - Unreachable(); + if(d_partialModel.getAssignment(var) != res){ + throw ModelException(n, "Model disagrees on non-linear term."); + } } + return res; } } -} - -DeltaRational TheoryArith::getDeltaValueWithNonlinear(TNode n, bool& failed) const { - AlwaysAssert(d_qflraStatus != Result::SAT_UNKNOWN); - AlwaysAssert(d_nlIncomplete); - - Debug("arith::value") << n << std::endl; - - switch(n.getKind()) { - - case kind::CONST_RATIONAL: - return n.getConst(); - - case kind::PLUS: { // 2+ args - DeltaRational value(0); - for(TNode::iterator i = n.begin(), - iend = n.end(); - i != iend && !failed; - ++i) { - value = value + getDeltaValueWithNonlinear(*i, failed); - } - return value; - } - - case kind::MULT: { // 2+ args - DeltaRational value(1); - if (n[0].getKind() == kind::CONST_RATIONAL) { - return getDeltaValueWithNonlinear(n[1], failed) * n[0].getConst(); - }else{ - failed = true; - return value; - } - } - - case kind::MINUS: // 2 args - // should have been rewritten - Unreachable(); - - case kind::UMINUS: // 1 arg - // should have been rewritten - Unreachable(); - - case kind::DIVISION: // 2 args - Assert(n[1].isConst()); - if (n[1].getKind() == kind::CONST_RATIONAL) { - return getDeltaValueWithNonlinear(n[0], failed) / n[0].getConst(); - }else{ - failed = true; - return DeltaRational(); - } - //fall through - case kind::INTS_DIVISION: - case kind::INTS_MODULUS: - //a bit strict - failed = true; - return DeltaRational(); default: - { - if(isSetup(n)){ - ArithVar var = d_arithvarNodeMap.asArithVar(n); - return d_partialModel.getAssignment(var); - }else{ - Unreachable(); - } + if(isSetup(n)){ + ArithVar var = d_arithvarNodeMap.asArithVar(n); + return d_partialModel.getAssignment(var); + }else{ + throw ModelException(n, "Expected a setup node."); } } } @@ -2151,15 +2065,10 @@ Rational TheoryArith::deltaValueForTotalOrder() const{ shared_end = shared_terms_end(); shared_iter != shared_end; ++shared_iter){ Node sharedCurr = *shared_iter; - try{ - DeltaRational val = getDeltaValue(sharedCurr); - relevantDeltaValues.insert(val); - }catch(Exception e){ - stringstream ss; - ss << "Cannot build a model due an exception: " << endl; - ss << e.getMessage(); - throw Exception(ss.str()); - } + // ModelException is fatal as this point. Don't catch! + // DeltaRationalException is fatal as this point. Don't catch! + DeltaRational val = getDeltaValue(sharedCurr); + relevantDeltaValues.insert(val); } for(ArithVar v = 0; v < d_variables.size(); ++v){ @@ -2185,32 +2094,7 @@ Rational TheoryArith::deltaValueForTotalOrder() const{ Assert(prev < curr); - const Rational& pinf = prev.getInfinitesimalPart(); - const Rational& cinf = curr.getInfinitesimalPart(); - - const Rational& pmaj = prev.getNoninfinitesimalPart(); - const Rational& cmaj = curr.getNoninfinitesimalPart(); - - if(pmaj == cmaj){ - Assert(pinf < cinf); - // any value of delta preserves the order - }else if(pinf == cinf){ - Assert(pmaj < cmaj); - // any value of delta preserves the order - }else{ - Assert(pinf != cinf && pmaj != cmaj); - Rational denDiffAbs = (cinf - pinf).abs(); - - Rational numDiff = (cmaj - pmaj); - Assert(numDiff.sgn() >= 0); - Assert(denDiffAbs.sgn() > 0); - Rational ratio = numDiff / denDiffAbs; - Assert(ratio.sgn() > 0); - - if(ratio < min){ - min = ratio; - } - } + DeltaRational::seperatingDelta(min, prev, curr); prev = curr; } } @@ -2411,26 +2295,19 @@ void TheoryArith::presolve(){ EqualityStatus TheoryArith::getEqualityStatus(TNode a, TNode b) { if(d_qflraStatus == Result::SAT_UNKNOWN){ return EQUALITY_UNKNOWN; - }else if(d_nlIncomplete){ - bool failed = false; - DeltaRational amod = getDeltaValueWithNonlinear(a, failed); - DeltaRational bmod = getDeltaValueWithNonlinear(b, failed); - if(failed){ + }else{ + try { + if (getDeltaValue(a) == getDeltaValue(b)) { + return EQUALITY_TRUE_IN_MODEL; + } else { + return EQUALITY_FALSE_IN_MODEL; + } + } catch (DeltaRationalException& dr) { + return EQUALITY_UNKNOWN; + } catch (ModelException& me) { return EQUALITY_UNKNOWN; - }else{ - return amod == bmod ? EQUALITY_TRUE_IN_MODEL : EQUALITY_FALSE_IN_MODEL; } - }else if (getDeltaValue(a) == getDeltaValue(b)) { - return EQUALITY_TRUE_IN_MODEL; - } else { - return EQUALITY_FALSE_IN_MODEL; } - -} - -bool TheoryArith::rowImplication(ArithVar v, bool upperBound, const DeltaRational& r){ - Unimplemented(); - return false; } bool TheoryArith::propagateCandidateBound(ArithVar basic, bool upperBound){ diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 8cd8a01b2..0773ab7ba 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -75,7 +75,6 @@ private: // if unknown, the simplex priority queue cannot be emptied int d_unknownsInARow; - bool rowImplication(ArithVar v, bool upperBound, const DeltaRational& r); /** * This counter is false if nothing has been done since the last cut. @@ -298,14 +297,14 @@ private: /** The constraint database associated with the theory. */ ConstraintDatabase d_constraintDatabase; - /** Internal model value for the atom */ - bool getDeltaAtomValue(TNode n) const; + class ModelException : public Exception { + public: + ModelException(TNode n, const char* msg) throw (); + virtual ~ModelException() throw (); + }; /** Internal model value for the node */ - DeltaRational getDeltaValue(TNode n) const; - - /** TODO : get rid of this. */ - DeltaRational getDeltaValueWithNonlinear(TNode n, bool& failed) const; + DeltaRational getDeltaValue(TNode n) const throw (DeltaRationalException, ModelException); /** Uninterpretted function symbol for use when interpreting * division by zero. -- 2.30.2