diff options
author | Tim King <taking@cs.nyu.edu> | 2013-05-09 14:33:35 -0400 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2013-05-09 16:31:11 -0400 |
commit | 588468e4800d790aecd35725c123d21f3e7a86ae (patch) | |
tree | 3732e3bb7a6d7a8cad818651b3b18a15a55256ff /test/unit/theory | |
parent | 85377f73a331b334437aa0d50d15c81e905869c1 (diff) |
Changing the integer normal form to increase matching.
Diffstat (limited to 'test/unit/theory')
-rw-r--r-- | test/unit/theory/theory_arith_white.h | 36 |
1 files changed, 36 insertions, 0 deletions
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())); + } }; |