From 2935af06e3fae46418c10450df9e02465f0a8038 Mon Sep 17 00:00:00 2001 From: Tim King Date: Mon, 4 Apr 2011 20:18:11 +0000 Subject: Reverts previous commit r1636. --- test/unit/theory/theory_arith_white.h | 32 -------------------------------- 1 file changed, 32 deletions(-) (limited to 'test/unit') diff --git a/test/unit/theory/theory_arith_white.h b/test/unit/theory/theory_arith_white.h index 65437ba0e..9de8f94b4 100644 --- a/test/unit/theory/theory_arith_white.h +++ b/test/unit/theory/theory_arith_white.h @@ -159,8 +159,6 @@ 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); @@ -198,9 +196,6 @@ 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; @@ -235,8 +230,6 @@ 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); @@ -254,29 +247,4 @@ 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