From 7667b8e139cba6024ebb5e25e280cb15ce1af51a Mon Sep 17 00:00:00 2001 From: Tim King Date: Sat, 29 Sep 2012 07:19:28 +0000 Subject: [PATCH] This commit add interpretation by lemma for INTS_DIVISION, INTS_MODULUS, and DIVISION. Improves support for non-linear monomials in getEqualityStatus(). Fixes bug 405. --- src/theory/arith/arith_utilities.h | 6 + src/theory/arith/normal_form.cpp | 11 ++ src/theory/arith/normal_form.h | 15 ++- src/theory/arith/theory_arith.cpp | 176 +++++++++++++++++++++++++++-- src/theory/arith/theory_arith.h | 7 ++ 5 files changed, 200 insertions(+), 15 deletions(-) diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h index 6ac2338f3..427ebbbd3 100644 --- a/src/theory/arith/arith_utilities.h +++ b/src/theory/arith/arith_utilities.h @@ -45,7 +45,13 @@ inline Node mkBoolNode(bool b){ return NodeManager::currentNM()->mkConst(b); } +inline Node mkIntSkolem(const std::string& name){ + return NodeManager::currentNM()->mkSkolem(name, NodeManager::currentNM()->integerType()); +} +inline Node mkRealSkolem(const std::string& name){ + return NodeManager::currentNM()->mkSkolem(name, NodeManager::currentNM()->realType()); +} /** \f$ k \in {LT, LEQ, EQ, GEQ, GT} \f$ */ inline bool isRelationOperator(Kind k){ diff --git a/src/theory/arith/normal_form.cpp b/src/theory/arith/normal_form.cpp index c90be63b9..39618d498 100644 --- a/src/theory/arith/normal_form.cpp +++ b/src/theory/arith/normal_form.cpp @@ -27,6 +27,17 @@ namespace CVC4 { namespace theory{ namespace arith { +bool Variable::isDivMember(Node n){ + switch(n.getKind()){ + case kind::DIVISION: + case kind::INTS_DIVISION: + case kind::INTS_MODULUS: + return Polynomial::isMember(n[0]) && Polynomial::isMember(n[1]); + default: + return false; + } +} + bool VarList::isSorted(iterator start, iterator end) { return __gnu_cxx::is_sorted(start, end); } diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h index 33fc42cea..3184deec5 100644 --- a/src/theory/arith/normal_form.h +++ b/src/theory/arith/normal_form.h @@ -211,7 +211,6 @@ namespace arith { * | (+ [monomial]) -> [monomial] */ - /** * A NodeWrapper is a class that is a thinly veiled container of a Node object. */ @@ -232,9 +231,17 @@ public: // TODO: check if it's a theory leaf also static bool isMember(Node n) { - if (n.getKind() == kind::CONST_RATIONAL) return false; - if (isRelationOperator(n.getKind())) return false; - return Theory::isLeafOf(n, theory::THEORY_ARITH); + Kind k = n.getKind(); + if (k == kind::CONST_RATIONAL) return false; + if (isRelationOperator(k)) return false; + if (Theory::isLeafOf(n, theory::THEORY_ARITH)) return true; + if (k == kind::INTS_DIVISION || k == kind::INTS_MODULUS || k == kind::DIVISION) return isDivMember(n); + return false; + } + + static bool isDivMember(Node n); + bool isDivLike() const{ + return isDivMember(getNode()); } bool isNormalForm() { return isMember(getNode()); } diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index e159c0e42..e552ae5a0 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -58,6 +58,7 @@ const uint32_t RESET_START = 2; TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe) : Theory(THEORY_ARITH, c, u, out, valuation, logicInfo, qe), + d_nlIncomplete(u, false), d_qflraStatus(Result::SAT_UNKNOWN), d_unknownsInARow(0), d_hasDoneWorkSinceCut(false), @@ -653,6 +654,7 @@ Node TheoryArith::ppRewrite(TNode atom) { << a << endl; } + if (a.getKind() == kind::EQUAL && options::arithRewriteEq()) { Node leq = NodeBuilder<2>(kind::LEQ) << a[0] << a[1]; Node geq = NodeBuilder<2>(kind::GEQ) << a[0] << a[1]; @@ -792,6 +794,12 @@ void TheoryArith::setupVariable(const Variable& x){ setupInitialValue(varN); markSetup(n); + + + if(x.isDivLike()){ + interpretDivLike(x); + } + } void TheoryArith::setupVariableList(const VarList& vl){ @@ -813,6 +821,7 @@ void TheoryArith::setupVariableList(const VarList& vl){ // vl is the product of at least 2 variables // vl : (* v1 v2 ...) d_out->setIncomplete(); + d_nlIncomplete = true; ++(d_statistics.d_statUserVariables); ArithVar av = requestArithVar(vlNode, false); @@ -826,6 +835,68 @@ void TheoryArith::setupVariableList(const VarList& vl){ * See the comment in setupPolynomail for more. */ } +void TheoryArith::interpretDivLike(const Variable& v){ + Assert(v.isDivLike()); + Node vnode = v.getNode(); + Assert(isSetup(vnode)); // Otherwise there is some invariant breaking recursion + Polynomial m = Polynomial::parsePolynomial(vnode[0]); + Polynomial n = Polynomial::parsePolynomial(vnode[1]); + + NodeManager* currNM = NodeManager::currentNM(); + + Node nNeq0 = currNM->mkNode(EQUAL, n.getNode(), mkRationalNode(0)).notNode(); + if(vnode.getKind() == INTS_DIVISION || vnode.getKind() == INTS_MODULUS){ + // (for all ((m Int) (n Int)) + // (=> (distinct n 0) + // (let ((q (div m n)) (r (mod m n))) + // (and (= m (+ (* n q) r)) + // (<= 0 r (- (abs n) 1)))))) + + Node q = (vnode.getKind() == INTS_DIVISION) ? vnode : currNM->mkNode(INTS_DIVISION, m.getNode(), n.getNode()); + Node r = (vnode.getKind() == INTS_MODULUS) ? vnode : currNM->mkNode(INTS_MODULUS, m.getNode(), n.getNode()); + + + Polynomial rp = Polynomial::parsePolynomial(r); + Polynomial qp = Polynomial::parsePolynomial(q); + + Node abs_n; + Node zero = mkRationalNode(0); + + if(n.isConstant()){ + abs_n = n.getHead().getConstant().abs().getNode(); + }else{ + abs_n = mkIntSkolem("abs_$$"); + Polynomial abs_np = Polynomial::parsePolynomial(abs_n); + Node absCnd = currNM->mkNode(ITE, + currNM->mkNode(LEQ, n.getNode(), zero), + Comparison::mkComparison(EQUAL, abs_np, -rp).getNode(), + Comparison::mkComparison(EQUAL, abs_np, rp).getNode()); + + d_out->lemma(absCnd); + } + + Node eq = Comparison::mkComparison(EQUAL, m, n * qp + rp).getNode(); + Node leq0 = currNM->mkNode(LEQ, zero, r); + Node leq1 = currNM->mkNode(LT, r, abs_n); + + Node andE = currNM->mkNode(AND, eq, leq0, leq1); + Node nNeq0ImpliesandE = currNM->mkNode(IMPLIES, nNeq0, andE); + + d_out->lemma(nNeq0ImpliesandE); + }else{ + // DIVISION (/ q r) + // (=> (distinct 0 n) (= m (* d n))) + + Assert(vnode.getKind() == DIVISION); + Node d = mkRealSkolem("division_$$"); + + Node eq = Comparison::mkComparison(EQUAL, m, n * Polynomial::parsePolynomial(d)).getNode(); + Node nNeq0ImpliesEq = currNM->mkNode(IMPLIES, nNeq0, eq); + + d_out->lemma(nNeq0ImpliesEq); + } + +} void TheoryArith::setupPolynomial(const Polynomial& poly) { Assert(!poly.containsConstant()); @@ -923,7 +994,9 @@ void TheoryArith::preRegisterTerm(TNode n) { ArithVar TheoryArith::requestArithVar(TNode x, bool slack){ - Assert(isLeaf(x) || x.getKind() == PLUS); + //TODO : The VarList trick is good enough? + Assert(isLeaf(x) || VarList::isMember(x) || x.getKind() == PLUS); + Assert(!Variable::isDivMember(x) || !getLogicInfo().isLinear()); Assert(!d_arithvarNodeMap.hasArithVar(x)); Assert(x.getType().isReal());// real or integer @@ -966,20 +1039,23 @@ void TheoryArith::asVectors(const Polynomial& p, std::vector& coeffs, Debug("rewriter") << "should be var: " << n << endl; - Assert(isLeaf(n)); + // TODO: This VarList::isMember(n) can be stronger + Assert(isLeaf(n) || VarList::isMember(n)); Assert(theoryOf(n) != THEORY_ARITH || d_arithvarNodeMap.hasArithVar(n)); Assert(d_arithvarNodeMap.hasArithVar(n)); ArithVar av; - if (theoryOf(n) != THEORY_ARITH && !d_arithvarNodeMap.hasArithVar(n)) { - // The only way not to get it through pre-register is if it's a foreign term - ++(d_statistics.d_statUserVariables); - av = requestArithVar(n,false); - setupInitialValue(av); - } else { - // Otherwise, we already have it's variable - av = d_arithvarNodeMap.asArithVar(n); - } + // The first if is likely dead is likely dead code: + // if (theoryOf(n) != THEORY_ARITH && !d_arithvarNodeMap.hasArithVar(n)) { + // // The only way not to get it through pre-register is if it's a foreign term + // ++(d_statistics.d_statUserVariables); + // av = requestArithVar(n,false); + // setupInitialValue(av); + // } else { + // // Otherwise, we already have it's variable + // av = d_arithvarNodeMap.asArithVar(n); + // } + av = d_arithvarNodeMap.asArithVar(n); coeffs.push_back(constant.getValue()); variables.push_back(av); @@ -1870,6 +1946,7 @@ bool TheoryArith::getDeltaAtomValue(TNode n) { DeltaRational TheoryArith::getDeltaValue(TNode n) { Assert(d_qflraStatus != Result::SAT_UNKNOWN); + Assert(!d_nlIncomplete); Debug("arith::value") << n << std::endl; switch(n.getKind()) { @@ -1925,8 +2002,76 @@ DeltaRational TheoryArith::getDeltaValue(TNode n) { } } +DeltaRational TheoryArith::getDeltaValueWithNonlinear(TNode n, bool& failed) { + Assert(d_qflraStatus != Result::SAT_UNKNOWN); + Assert(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(); + } + } + } +} + void TheoryArith::collectModelInfo( TheoryModel* m, bool fullModel ){ Assert(d_qflraStatus == Result::SAT); + Assert(!d_nlIncomplete); Debug("arith::collectModelInfo") << "collectModelInfo() begin " << endl; @@ -2110,6 +2255,15 @@ 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){ + 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 { diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index c98c759f7..1c2c942fd 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -64,6 +64,8 @@ class InstantiatorTheoryArith; class TheoryArith : public Theory { friend class InstantiatorTheoryArith; private: + context::CDO d_nlIncomplete; + enum Result::Sat d_qflraStatus; // check() // !done() -> d_qflraStatus = Unknown @@ -105,6 +107,8 @@ private: d_setupNodes.insert(n); } + void interpretDivLike(const Variable& x); + void setupVariable(const Variable& x); void setupVariableList(const VarList& vl); void setupPolynomial(const Polynomial& poly); @@ -310,6 +314,9 @@ private: /** Internal model value for the node */ DeltaRational getDeltaValue(TNode n); + /** TODO : get rid of this. */ + DeltaRational getDeltaValueWithNonlinear(TNode n, bool& failed); + public: TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe); virtual ~TheoryArith(); -- 2.30.2