From a2cc0337aa53cfb686e26d68f98f2ae176ff1337 Mon Sep 17 00:00:00 2001 From: Tim King Date: Sat, 2 Apr 2011 21:05:47 +0000 Subject: Delayed the addition of unate propagation lemmas until propagation is called. The OutputChannel is now untouched by TheoryArith during preregistration. --- test/unit/theory/theory_arith_white.h | 32 ++++++++++++++++++++++++++++++++ 1 file changed, 32 insertions(+) (limited to 'test/unit/theory') 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(d_zero); + Node c1 = d_nm->mkConst(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); + } }; -- cgit v1.2.3