diff options
author | Tim King <taking@cs.nyu.edu> | 2011-04-18 16:48:52 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2011-04-18 16:48:52 +0000 |
commit | abe849b486ea3707fd51a612c7982554f3d6581f (patch) | |
tree | 8f3967f644f9098079c778dd60cf9feb36e1ab2b /test/unit/theory | |
parent | b90081962840584bb9eeda368ea232a7d42a292b (diff) |
This commit merges the branch arithmetic/propagation-again into trunk.
- This adds code for bounds refinement, and conflict weakening.
- This adds util/boolean_simplification.h.
- This adds a propagation manager to theory of arithmetic.
- Propagation is disabled by default.
- Propagation can be enabled by the command line flag "--enable-arithmetic-propagation"
- Propagation interacts *heavily* with rewriting equalities, and will work best if the command line flag "--rewrite-arithmetic-equalities" is enabled.
Diffstat (limited to 'test/unit/theory')
-rw-r--r-- | test/unit/theory/theory_arith_white.h | 36 |
1 files changed, 21 insertions, 15 deletions
diff --git a/test/unit/theory/theory_arith_white.h b/test/unit/theory/theory_arith_white.h index 060c3036d..fb82a7ac9 100644 --- a/test/unit/theory/theory_arith_white.h +++ b/test/unit/theory/theory_arith_white.h @@ -150,6 +150,8 @@ public: Node leq1 = d_nm->mkNode(LEQ, x, c1); Node geq1 = d_nm->mkNode(GEQ, x, c1); Node lt1 = d_nm->mkNode(NOT, geq1); + Node gt0 = d_nm->mkNode(NOT, leq0); + Node gt1 = d_nm->mkNode(NOT, leq1); fakeTheoryEnginePreprocess(leq0); fakeTheoryEnginePreprocess(leq1); @@ -161,20 +163,20 @@ public: d_arith->check(d_level); d_arith->propagate(d_level); - Node leq0ThenLeq1 = NodeBuilder<2>(IMPLIES) << leq0 << (leq1); + Node gt1ThenGt0 = NodeBuilder<2>(IMPLIES) << gt1 << gt0; + Node geq1ThenGt0 = NodeBuilder<2>(IMPLIES) << geq1 << gt0; Node lt1ThenLeq1 = NodeBuilder<2>(IMPLIES) << lt1 << leq1; - Node leq0ThenLt1 = NodeBuilder<2>(IMPLIES) << leq0 << lt1; TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 3u); TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(0), LEMMA); - TS_ASSERT_EQUALS(d_outputChannel.getIthNode(0), leq0ThenLeq1); + TS_ASSERT_EQUALS(d_outputChannel.getIthNode(0), gt1ThenGt0); TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(1), LEMMA); - TS_ASSERT_EQUALS(d_outputChannel.getIthNode(1), lt1ThenLeq1); + TS_ASSERT_EQUALS(d_outputChannel.getIthNode(1), geq1ThenGt0); TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(2), LEMMA); - TS_ASSERT_EQUALS(d_outputChannel.getIthNode(2), leq0ThenLt1); + TS_ASSERT_EQUALS(d_outputChannel.getIthNode(2), lt1ThenLeq1); } @@ -187,6 +189,8 @@ public: Node leq1 = d_nm->mkNode(LEQ, x, c1); Node geq1 = d_nm->mkNode(GEQ, x, c1); Node lt1 = d_nm->mkNode(NOT, geq1); + Node gt0 = d_nm->mkNode(NOT, leq0); + Node gt1 = d_nm->mkNode(NOT, leq1); fakeTheoryEnginePreprocess(leq0); fakeTheoryEnginePreprocess(leq1); @@ -197,20 +201,20 @@ public: d_arith->check(d_level); - Node leq0ThenLeq1 = NodeBuilder<2>(IMPLIES) << leq0 << (leq1); + Node gt1ThenGt0 = NodeBuilder<2>(IMPLIES) << gt1 << gt0; + Node geq1ThenGt0 = NodeBuilder<2>(IMPLIES) << geq1 << gt0; Node lt1ThenLeq1 = NodeBuilder<2>(IMPLIES) << lt1 << leq1; - Node leq0ThenLt1 = NodeBuilder<2>(IMPLIES) << leq0 << lt1; TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 3u); TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(0), LEMMA); - TS_ASSERT_EQUALS(d_outputChannel.getIthNode(0), leq0ThenLeq1); + TS_ASSERT_EQUALS(d_outputChannel.getIthNode(0), gt1ThenGt0); TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(1), LEMMA); - TS_ASSERT_EQUALS(d_outputChannel.getIthNode(1), lt1ThenLeq1); + TS_ASSERT_EQUALS(d_outputChannel.getIthNode(1), geq1ThenGt0); TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(2), LEMMA); - TS_ASSERT_EQUALS(d_outputChannel.getIthNode(2), leq0ThenLt1); + TS_ASSERT_EQUALS(d_outputChannel.getIthNode(2), lt1ThenLeq1); } void testTPLeq1() { Node x = d_nm->mkVar(*d_realType); @@ -221,6 +225,8 @@ public: Node leq1 = d_nm->mkNode(LEQ, x, c1); Node geq1 = d_nm->mkNode(GEQ, x, c1); Node lt1 = d_nm->mkNode(NOT, geq1); + Node gt0 = d_nm->mkNode(NOT, leq0); + Node gt1 = d_nm->mkNode(NOT, leq1); fakeTheoryEnginePreprocess(leq0); fakeTheoryEnginePreprocess(leq1); @@ -232,19 +238,19 @@ public: d_arith->check(d_level); d_arith->propagate(d_level); - Node leq0ThenLeq1 = NodeBuilder<2>(IMPLIES) << leq0 << (leq1); + Node gt1ThenGt0 = NodeBuilder<2>(IMPLIES) << gt1 << gt0; + Node geq1ThenGt0 = NodeBuilder<2>(IMPLIES) << geq1 << gt0; Node lt1ThenLeq1 = NodeBuilder<2>(IMPLIES) << lt1 << leq1; - Node leq0ThenLt1 = NodeBuilder<2>(IMPLIES) << leq0 << lt1; TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 3u); TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(0), LEMMA); - TS_ASSERT_EQUALS(d_outputChannel.getIthNode(0), leq0ThenLeq1); + TS_ASSERT_EQUALS(d_outputChannel.getIthNode(0), gt1ThenGt0); TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(1), LEMMA); - TS_ASSERT_EQUALS(d_outputChannel.getIthNode(1), lt1ThenLeq1); + TS_ASSERT_EQUALS(d_outputChannel.getIthNode(1), geq1ThenGt0); TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(2), LEMMA); - TS_ASSERT_EQUALS(d_outputChannel.getIthNode(2), leq0ThenLt1); + TS_ASSERT_EQUALS(d_outputChannel.getIthNode(2), lt1ThenLeq1); } }; |