From 213c2c4a7d5f6d90f2bf169fb38c998808c05978 Mon Sep 17 00:00:00 2001 From: Tim King Date: Thu, 13 Apr 2017 00:21:30 -0700 Subject: [PATCH] Updating TheoryArithPrivate::getDeltaValue() to eagerly use the partial model value if exists. --- src/theory/arith/theory_arith_private.cpp | 138 +++++++++------------- src/theory/arith/theory_arith_private.h | 16 ++- 2 files changed, 73 insertions(+), 81 deletions(-) diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 34529007d..4f62f4451 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -1314,9 +1314,9 @@ void TheoryArithPrivate::addSharedTerm(TNode n){ Node TheoryArithPrivate::getModelValue(TNode term) { try{ - DeltaRational drv = getDeltaValue(term); + const DeltaRational drv = getDeltaValue(term); const Rational& delta = d_partialModel.getDelta(); - Rational qmodel = drv.substituteDelta( delta ); + const Rational qmodel = drv.substituteDelta( delta ); return mkRationalNode( qmodel ); } catch (DeltaRationalException& dr) { return Node::null(); @@ -1529,7 +1529,8 @@ ArithVar TheoryArithPrivate::findShortestBasicRow(ArithVar variable){ bestRowLength = rowLength; } } - Assert(bestBasic == ARITHVAR_SENTINEL || bestRowLength < std::numeric_limits::max()); + Assert(bestBasic == ARITHVAR_SENTINEL || + bestRowLength < std::numeric_limits::max()); return bestBasic; } @@ -1545,7 +1546,6 @@ void TheoryArithPrivate::setupVariable(const Variable& x){ markSetup(n); - if(x.isDivLike()){ setupDivLike(x); } @@ -1610,7 +1610,11 @@ void TheoryArithPrivate::setupDivLike(const Variable& v){ Assert(v.isDivLike()); if(getLogicInfo().isLinear()){ - throw LogicException("A non-linear fact (involving div/mod/divisibility) was asserted to arithmetic in a linear logic;\nif you only use division (or modulus) by a constant value, or if you only use the divisibility-by-k predicate, try using the --rewrite-divk option."); + throw LogicException( + "A non-linear fact (involving div/mod/divisibility) was asserted to " + "arithmetic in a linear logic;\nif you only use division (or modulus) " + "by a constant value, or if you only use the divisibility-by-k " + "predicate, try using the --rewrite-divk option."); } Node vnode = v.getNode(); @@ -4271,95 +4275,71 @@ void TheoryArithPrivate::propagate(Theory::Effort e) { } } -DeltaRational TheoryArithPrivate::getDeltaValue(TNode n) const throw (DeltaRationalException, ModelException) { +DeltaRational TheoryArithPrivate::getDeltaValue(TNode term) const + throw(DeltaRationalException, ModelException) { AlwaysAssert(d_qflraStatus != Result::SAT_UNKNOWN); - Debug("arith::value") << n << std::endl; + Debug("arith::value") << term << std::endl; - switch(n.getKind()) { + if (d_partialModel.hasArithVar(term)) { + ArithVar var = d_partialModel.asArithVar(term); + return d_partialModel.getAssignment(var); + } - case kind::CONST_RATIONAL: - return n.getConst(); + switch (Kind kind = term.getKind()) { + case kind::CONST_RATIONAL: + return term.getConst(); - case kind::PLUS: { // 2+ args - DeltaRational value(0); - for(TNode::iterator i = n.begin(), iend = n.end(); i != iend; ++i) { - value = value + getDeltaValue(*i); + case kind::PLUS: { // 2+ args + DeltaRational value(0); + for (TNode::iterator i = term.begin(), iend = term.end(); i != iend; + ++i) { + value = value + getDeltaValue(*i); + } + return value; } - return value; - } - case kind::MULT: { // 2+ args - 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; + case kind::NONLINEAR_MULT: + case kind::MULT: { // 2+ args + Assert(!isSetup(term)); + DeltaRational value(1); + for (TNode::iterator i = term.begin(), iend = term.end(); i != iend; + ++i) { + value = value * getDeltaValue(*i); } + return value; } - // TODO: This is a bit of a weak check - if(isSetup(n)){ - ArithVar var = d_partialModel.asArithVar(n); - const DeltaRational& assign = d_partialModel.getAssignment(var); - if(assign != value){ - throw ModelException(n, "Model disagrees on non-linear term."); - } + case kind::MINUS: { // 2 args + return getDeltaValue(term[0]) - getDeltaValue(term[1]); + } + case kind::UMINUS: { // 1 arg + return (-getDeltaValue(term[0])); } - return value; - } - case kind::MINUS:{ // 2 args - return getDeltaValue(n[0]) - getDeltaValue(n[1]); - } - - case kind::UMINUS:{ // 1 arg - return (- getDeltaValue(n[0])); - } - case kind::DIVISION:{ // 2 args - DeltaRational res = getDeltaValue(n[0]) / getDeltaValue(n[1]); - if(isSetup(n)){ - ArithVar var = d_partialModel.asArithVar(n); - if(d_partialModel.getAssignment(var) != res){ - throw ModelException(n, "Model disagrees on non-linear term."); - } + case kind::DIVISION: { // 2 args + Assert(!isSetup(term)); + return getDeltaValue(term[0]) / getDeltaValue(term[1]); } - 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 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.euclidianDivideQuotient(denom)); - }else{ - Assert(n.getKind() == kind::INTS_MODULUS_TOTAL); - res = Rational(numer.euclidianDivideRemainder(denom)); + case kind::DIVISION_TOTAL: + case kind::INTS_DIVISION_TOTAL: + case kind::INTS_MODULUS_TOTAL: { // 2 args + Assert(!isSetup(term)); + DeltaRational denominator = getDeltaValue(term[1]); + if (denominator.isZero()) { + return DeltaRational(0, 0); } - if(isSetup(n)){ - ArithVar var = d_partialModel.asArithVar(n); - if(d_partialModel.getAssignment(var) != res){ - throw ModelException(n, "Model disagrees on non-linear term."); - } + DeltaRational numerator = getDeltaValue(term[0]); + if (kind == kind::DIVISION_TOTAL) { + return numerator / denominator; + } else if (kind == kind::INTS_DIVISION_TOTAL) { + return Rational(numerator.euclidianDivideQuotient(denominator)); + } else { + Assert(kind == kind::INTS_MODULUS_TOTAL); + return Rational(numerator.euclidianDivideRemainder(denominator)); } - return res; } - } - default: - if(isSetup(n)){ - ArithVar var = d_partialModel.asArithVar(n); - return d_partialModel.getAssignment(var); - }else{ - throw ModelException(n, "Expected a setup node."); - } + default: + throw ModelException(term, "No model assignment."); } } diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index 79e7a77bc..9d27aac7a 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -401,8 +401,20 @@ private: virtual ~ModelException() throw (); }; - /** Internal model value for the node */ - DeltaRational getDeltaValue(TNode n) const throw (DeltaRationalException, ModelException); + /** + * Computes the delta rational value of a term from the current partial + * model. This returns the delta value assignment to the term if it is in the + * partial model. Otherwise, this is computed recursively for arithmetic terms + * from each subterm. + * + * This throws a DeltaRationalException if the value cannot be represented as + * a DeltaRational. This throws a ModelException if there is a term is not in + * the partial model and is not a theory of arithmetic term. + * + * precondition: The linear abstraction of the nodes must be satisfiable. + */ + DeltaRational getDeltaValue(TNode term) const + throw(DeltaRationalException, ModelException); /** Uninterpretted function symbol for use when interpreting * division by zero. -- 2.30.2