Fix to a bug in integer mod lemmas.

diff --git a/src/theory/arith/normal_form.cpp b/src/theory/arith/normal_form.cpp
index 2e1d7fd5c59d0dded4cecb0aa52afb46e57e1888..de5f801f0749ac8f563b8dadd3a21a5a0295cbfa 100644 (file)
--- 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 bdaaf19186a3d40e7ab647fd4102fb2482e7b7ed..31f8e138e6bbb186705291b1183c02e02e18e9a8 100644 (file)
--- 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 65d9551acc7ca868b4dc231701bc7f6f5a254111..5bd4c166d05a78a4120f417c1b88d21f2466e63b 100644 (file)
--- 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 dfeede3658c595302aeae5c8ec72a4d45fc56f98..d0b787f20c6ec6aeeff2a5c1f9167ddc4eaa715c 100644 (file)
--- 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 (file)
index 0000000..2e3f1d8
--- /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