Changing the integer normal form to increase matching.

4 files changed, 76 insertions, 13 deletions

diff --git a/src/theory/arith/normal_form.cpp b/src/theory/arith/normal_form.cpp
index 8454ca210..1ebbe49e0 100644
--- a/src/theory/arith/normal_form.cpp
+++ b/src/theory/arith/normal_form.cpp
@@ -745,9 +745,8 @@ bool Comparison::isNormalGEQ() const {
       return false;
     }else{
       if(left.isIntegral()){
-        return left.denominatorLCMIsOne() && left.numeratorGCDIsOne();
+        return left.signNormalizedReducedSum();
       }else{
-        Debug("nf::tmp") << "imme sdfhkdjfh "<< left.leadingCoefficientIsAbsOne() << endl;
         return left.leadingCoefficientIsAbsOne();
       }
     }
@@ -768,7 +767,7 @@ bool Comparison::isNormalLT() const {
       return false;
     }else{
       if(left.isIntegral()){
-        return left.denominatorLCMIsOne() && left.numeratorGCDIsOne();
+        return left.signNormalizedReducedSum();
       }else{
         return left.leadingCoefficientIsAbsOne();
       }
@@ -889,6 +888,7 @@ Node Comparison::mkIntInequality(Kind k, const Polynomial& p){
   Polynomial left = sp.getPolynomial();
   Rational right = - (sp.getConstant().getValue());
 
+
   Monomial m = left.getHead();
   Assert(!m.isConstant());
 
@@ -899,16 +899,31 @@ Node Comparison::mkIntInequality(Kind k, const Polynomial& p){
   Polynomial newLeft = left * mult;
   Rational rightMult = right * mult;
 
+  bool negateResult = false;
+  if(!newLeft.leadingCoefficientIsPositive()){
+    // multiply by -1
+    // a: left >= right or b: left > right
+    // becomes
+    // a: -left <= -right or b: -left < -right
+    // a: not (-left > -right) or b: (not -left >= -right)
+    newLeft = -newLeft;
+    rightMult = -rightMult;
+    k = (kind::GT == k) ? kind::GEQ : kind::GT;
+    negateResult = true;
+    // the later stages handle:
+    // a: not (-left >= -right + 1) or b: (not -left >= -right)
+  }
 
+  Node result = Node::null();
   if(rightMult.isIntegral()){
     if(k == kind::GT){
       // (> p z)
       // (>= p (+ z 1))
       Constant rightMultPlusOne = Constant::mkConstant(rightMult + 1);
-      return toNode(kind::GEQ, newLeft, rightMultPlusOne);
+      result = toNode(kind::GEQ, newLeft, rightMultPlusOne);
     }else{
       Constant newRight = Constant::mkConstant(rightMult);
-      return toNode(kind::GEQ, newLeft, newRight);
+      result = toNode(kind::GEQ, newLeft, newRight);
     }
   }else{
     //(>= l (/ n d))
@@ -916,7 +931,13 @@ Node Comparison::mkIntInequality(Kind k, const Polynomial& p){
     //This also hold for GT as (ceil (/ n d)) > (/ n d)
     Integer ceilr = rightMult.ceiling();
     Constant ceilRight = Constant::mkConstant(ceilr);
-    return toNode(kind::GEQ, newLeft, ceilRight);
+    result = toNode(kind::GEQ, newLeft, ceilRight);
+  }
+  Assert(!result.isNull());
+  if(negateResult){
+    return result.notNode();
+  }else{
+    return result;
   }
 }
 
diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h
index bcf9cbfa4..c6af7010f 100644
--- a/src/theory/arith/normal_form.h
+++ b/src/theory/arith/normal_form.h
@@ -76,12 +76,13 @@ namespace arith {
  *     (exists realMonomial (monomialList qpolynomial))
  *     abs(monomialCoefficient (head (monomialList qpolynomial))) == 1
  *
- * integer_cmp := (<= zpolynomial constant)
+ * integer_cmp := (>= zpolynomial constant)
  *   where
  *     not (exists constantMonomial (monomialList zpolynomial))
  *     (forall integerMonomial (monomialList zpolynomial))
  *     the gcd of all numerators of coefficients is 1
  *     the denominator of all coefficients and the constant is 1
+ *     the leading coefficient is positive
  *
  * rational_eq := (= qvarlist qpolynomial)
  *   where
@@ -939,6 +940,10 @@ public:
   bool denominatorLCMIsOne() const;
   bool numeratorGCDIsOne() const;
 
+  bool signNormalizedReducedSum() const {
+    return leadingCoefficientIsPositive() && denominatorLCMIsOne() && numeratorGCDIsOne();
+  }
+
   /**
    * Returns the Least Common Multiple of the denominators of the coefficients
    * of the monomials.
@@ -1265,7 +1270,7 @@ private:
    * Creates a comparison equivalent to (k l 0).
    * k is either GT or GEQ.
    * It is not the case that all variables in l are integral.
-   */  
+   */
   static Node mkRatInequality(Kind k, const Polynomial& l);
 
 public:
diff --git a/test/regress/regress0/arith/integers/Makefile.am b/test/regress/regress0/arith/integers/Makefile.am
index efd5aa909..c555ba413 100644
--- a/test/regress/regress0/arith/integers/Makefile.am
+++ b/test/regress/regress0/arith/integers/Makefile.am
@@ -20,9 +20,9 @@ MAKEFLAGS = -k
 
 TESTS =	\
 	arith-int-004.cvc \
-	arith-int-007.cvc \
 	arith-int-011.cvc \
 	arith-int-012.cvc \
+	arith-int-013.cvc \
 	arith-int-022.cvc \
 	arith-int-024.cvc \
 	arith-int-042.cvc \
@@ -34,7 +34,7 @@ TESTS =	\
 	arith-int-097.cvc \
 	arith-int-085.cvc
 
-EXTRA_DIST = $(TESTS)
+EXTRA_DIST = $(TESTS) \
 	arith-int-001.cvc \
 	arith-int-002.cvc \
 	arith-int-003.cvc \
@@ -105,7 +105,6 @@ EXTRA_DIST = $(TESTS)
 	arith-int-079.cvc \
 	arith-int-080.cvc \
 	arith-int-081.cvc \
-	arith-int-082.cvc \
 	arith-int-083.cvc \
 	arith-int-086.cvc \
 	arith-int-087.cvc \
@@ -122,9 +121,11 @@ EXTRA_DIST = $(TESTS)
 	arith-int-099.cvc \
 	arith-int-100.cvc
 
+
 FAILING_TESTS = \
-	arith-int-024.cvc \
-	arith-int-013.cvc
+	arith-int-007.cvc \
+	arith-int-082.cvc \
+	arith-int-098.cvc
 
 #if CVC4_BUILD_PROFILE_COMPETITION
 #else
diff --git a/test/unit/theory/theory_arith_white.h b/test/unit/theory/theory_arith_white.h
index 844fb57d1..3247b8c73 100644
--- a/test/unit/theory/theory_arith_white.h
+++ b/test/unit/theory/theory_arith_white.h
@@ -60,6 +60,7 @@ class TheoryArithWhite : public CxxTest::TestSuite {
 
   TypeNode* d_booleanType;
   TypeNode* d_realType;
+  TypeNode* d_intType;
 
   const Rational d_zero;
   const Rational d_one;
@@ -120,10 +121,12 @@ public:
 
     d_booleanType = new TypeNode(d_nm->booleanType());
     d_realType = new TypeNode(d_nm->realType());
+    d_intType = new TypeNode(d_nm->integerType());
 
   }
 
   void tearDown() {
+    delete d_intType;
     delete d_realType;
     delete d_booleanType;
 
@@ -281,4 +284,37 @@ public:
     TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(1), LEMMA);
     TS_ASSERT_EQUALS(d_outputChannel.getIthNode(1), geq0OrLeq1);
   }
+
+  void testIntNormalForm() {
+    Node x = d_nm->mkVar(*d_intType);
+    Node c0 = d_nm->mkConst<Rational>(d_zero);
+    Node c1 = d_nm->mkConst<Rational>(d_one);
+    Node c2 = d_nm->mkConst<Rational>(Rational(2));
+
+
+    Node geq0 = d_nm->mkNode(GEQ, x, c0);
+    Node geq1 = d_nm->mkNode(GEQ, x, c1);
+    Node geq2 = d_nm->mkNode(GEQ, x, c2);
+
+    TS_ASSERT_EQUALS(Rewriter::rewrite(geq0), geq0);
+    TS_ASSERT_EQUALS(Rewriter::rewrite(geq1), geq1);
+
+    Node gt0 = d_nm->mkNode(GT, x, c0);
+    Node gt1 = d_nm->mkNode(GT, x, c1);
+
+    TS_ASSERT_EQUALS(Rewriter::rewrite(gt0), Rewriter::rewrite(geq1));
+    TS_ASSERT_EQUALS(Rewriter::rewrite(gt1), Rewriter::rewrite(geq2));
+
+    Node lt0 = d_nm->mkNode(LT, x, c0);
+    Node lt1 = d_nm->mkNode(LT, x, c1);
+
+    TS_ASSERT_EQUALS(Rewriter::rewrite(lt0), Rewriter::rewrite(geq0.notNode()));
+    TS_ASSERT_EQUALS(Rewriter::rewrite(lt1), Rewriter::rewrite(geq1.notNode()));
+
+    Node leq0 = d_nm->mkNode(LEQ, x, c0);
+    Node leq1 = d_nm->mkNode(LEQ, x, c1);
+
+    TS_ASSERT_EQUALS(Rewriter::rewrite(leq0), Rewriter::rewrite(geq1.notNode()));
+    TS_ASSERT_EQUALS(Rewriter::rewrite(leq1), Rewriter::rewrite(geq2.notNode()));
+  }
 };