diff options
Diffstat (limited to 'src/theory/arith/theory_arith.cpp')
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 176 |
1 files changed, 165 insertions, 11 deletions
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<Rational>& 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<Rational>(); + + 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<Rational>(); + }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<Rational>(); + }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 { |