diff options
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/regress0/arith/integers/Makefile.am | 11 | ||||
-rw-r--r-- | test/unit/theory/theory_arith_white.h | 36 |
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())); + } }; |