From c3c4a6fc6062e17bf92a5657c168034a33cf94b8 Mon Sep 17 00:00:00 2001 From: Tim King Date: Wed, 7 Nov 2012 19:43:34 +0000 Subject: [PATCH] Fix to a bug in integer mod lemmas. --- src/theory/arith/normal_form.cpp | 13 +++ src/theory/arith/normal_form.h | 12 ++- src/theory/arith/theory_arith.cpp | 107 ++++++++++++------------ test/regress/regress0/arith/Makefile.am | 3 +- test/regress/regress0/arith/mod.01.smt2 | 10 +++ 5 files changed, 88 insertions(+), 57 deletions(-) create mode 100644 test/regress/regress0/arith/mod.01.smt2 diff --git a/src/theory/arith/normal_form.cpp b/src/theory/arith/normal_form.cpp index 2e1d7fd5c..de5f801f0 100644 --- a/src/theory/arith/normal_form.cpp +++ b/src/theory/arith/normal_form.cpp @@ -1047,6 +1047,19 @@ Kind Comparison::comparisonKind(TNode literal){ } } + +Node Polynomial::makeAbsCondition(Variable v, Polynomial p){ + Polynomial zerop = Polynomial::mkZero(); + + Polynomial varp = Polynomial::mkPolynomial(v); + Comparison pLeq0 = Comparison::mkComparison(kind::LEQ, p, zerop); + Comparison negP = Comparison::mkComparison(kind::EQUAL, varp, -p); + Comparison posP = Comparison::mkComparison(kind::EQUAL, varp, p); + + Node absCnd = (pLeq0.getNode()).iteNode(negP.getNode(), posP.getNode()); + return absCnd; +} + } //namespace arith } //namespace theory } //namespace CVC4 diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h index bdaaf1918..31f8e138e 100644 --- a/src/theory/arith/normal_form.h +++ b/src/theory/arith/normal_form.h @@ -992,7 +992,7 @@ public: }else{ uint32_t max = (*i).coefficientLength(); ++i; - for(; i!=e; ++i){ + for(; i!=e; ++i){ uint32_t curr = (*i).coefficientLength(); if(curr > max){ max = curr; @@ -1032,7 +1032,15 @@ public: } friend class SumPair; - friend class Comparison;; + friend class Comparison; + + /** Returns a node that if asserted ensures v is the abs of this polynomial.*/ + Node makeAbsCondition(Variable v){ + return makeAbsCondition(v, *this); + } + + /** Returns a node that if asserted ensures v is the abs of p.*/ + static Node makeAbsCondition(Variable v, Polynomial p); };/* class Polynomial */ diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 65d9551ac..5bd4c166d 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -819,63 +819,62 @@ 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); - } + 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)))))) + + // Updated for div 0 functions + // (for all ((m Int) (n Int)) + // (let ((q (div m n)) (r (mod m n))) + // (ite (= n 0) + // (and (= q (div_0_func m)) (= r (mod_0_func m))) + // (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_$$"); + Node absCnd = n.makeAbsCondition(Variable(abs_n)); + 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 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); + 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); + } - 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) { diff --git a/test/regress/regress0/arith/Makefile.am b/test/regress/regress0/arith/Makefile.am index dfeede365..d0b787f20 100644 --- a/test/regress/regress0/arith/Makefile.am +++ b/test/regress/regress0/arith/Makefile.am @@ -24,7 +24,8 @@ TESTS = \ fuzz_3-eq.smt \ leq.01.smt \ miplibtrick.smt \ - DTP_k2_n35_c175_s15.smt2 + DTP_k2_n35_c175_s15.smt2 \ + mod.01.smt2 # problem__003.smt2 EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/arith/mod.01.smt2 b/test/regress/regress0/arith/mod.01.smt2 new file mode 100644 index 000000000..2e3f1d834 --- /dev/null +++ b/test/regress/regress0/arith/mod.01.smt2 @@ -0,0 +1,10 @@ +(set-logic QF_NIA) +(set-info :smt-lib-version 2.0) +(set-info :status unknown) +(declare-fun n () Int) +(declare-fun x () Int) + +(assert (>= n 1)) +(assert (< (mod x n) n)) + +(check-sat) \ No newline at end of file -- 2.30.2