diff options
| author | Tim King <taking@cs.nyu.edu> | 2011-04-02 21:05:47 +0000 |
|---|---|---|
| committer | Tim King <taking@cs.nyu.edu> | 2011-04-02 21:05:47 +0000 |
| commit | a2cc0337aa53cfb686e26d68f98f2ae176ff1337 (patch) | |
| tree | 73dbd73b52511d7575b925acd9ea18414b92ff4e /test | |
| parent | 41362e76ebc0073c1801700da574b6265dcbc6a9 (diff) | |
Delayed the addition of unate propagation lemmas until propagation is called. The OutputChannel is now untouched by TheoryArith during preregistration.
Diffstat (limited to 'test')
| -rw-r--r-- | test/unit/theory/theory_arith_white.h | 32 |
1 files changed, 32 insertions, 0 deletions
diff --git a/test/unit/theory/theory_arith_white.h b/test/unit/theory/theory_arith_white.h index 9de8f94b4..65437ba0e 100644 --- a/test/unit/theory/theory_arith_white.h +++ b/test/unit/theory/theory_arith_white.h @@ -159,6 +159,8 @@ public: d_arith->check(d_level); + TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 0u); + d_arith->propagate(d_level); Node leq0ThenLeq1 = NodeBuilder<2>(IMPLIES) << leq0 << (leq1); @@ -196,6 +198,9 @@ public: d_arith->check(d_level); + TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 0u); + + d_arith->propagate(d_level); Node leq0ThenLeq1 = NodeBuilder<2>(IMPLIES) << leq0 << (leq1); Node lt1ThenLeq1 = NodeBuilder<2>(IMPLIES) << lt1 << leq1; @@ -230,6 +235,8 @@ public: d_arith->check(d_level); + TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 0u); + d_arith->propagate(d_level); Node leq0ThenLeq1 = NodeBuilder<2>(IMPLIES) << leq0 << (leq1); @@ -247,4 +254,29 @@ public: TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(2), LEMMA); TS_ASSERT_EQUALS(d_outputChannel.getIthNode(2), leq0ThenLt1); } + + void testConflict() { + Node x = d_nm->mkVar(*d_realType); + Node c0 = d_nm->mkConst<Rational>(d_zero); + Node c1 = d_nm->mkConst<Rational>(d_one); + + Node leq0 = d_nm->mkNode(LEQ, x, c0); + Node leq1 = d_nm->mkNode(LEQ, x, c1); + Node gt1 = d_nm->mkNode(NOT, leq1); + + fakeTheoryEnginePreprocess(leq0); + fakeTheoryEnginePreprocess(leq1); + + d_arith->assertFact(leq0); + d_arith->assertFact(gt1); + + d_arith->check(d_level); + + + Node conf = d_nm->mkNode(AND, leq0, gt1); + TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 1u); + + TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(0), CONFLICT); + TS_ASSERT_EQUALS(d_outputChannel.getIthNode(0), conf); + } }; |