Changing the integer normal form to increase matching.

2 files changed, 42 insertions, 5 deletions

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()));
+  }
 };