diff options
| author | Tim King <taking@cs.nyu.edu> | 2012-05-22 15:09:03 +0000 |
|---|---|---|
| committer | Tim King <taking@cs.nyu.edu> | 2012-05-22 15:09:03 +0000 |
| commit | 52c5c282f47448856e0dec8a7d4e5de612a8dcc3 (patch) | |
| tree | b6eac07d1c91aeab8fbfa4d6bd03981939614e77 /test/unit | |
| parent | 6ce8f5cc5d7767d5ff9e74bc08d3c8a364ad8bf1 (diff) | |
This commit merges in the branch arithmetic/cprop.
Diffstat (limited to 'test/unit')
| -rw-r--r-- | test/unit/theory/theory_arith_white.h | 20 |
1 files changed, 16 insertions, 4 deletions
diff --git a/test/unit/theory/theory_arith_white.h b/test/unit/theory/theory_arith_white.h index 161329c06..b4d5c0086 100644 --- a/test/unit/theory/theory_arith_white.h +++ b/test/unit/theory/theory_arith_white.h @@ -171,16 +171,20 @@ public: Node gt0Orlt1 = NodeBuilder<2>(OR) << gt0 << lt1; Node geq0OrLeq1 = NodeBuilder<2>(OR) << geq1 << leq1; - cout << d_outputChannel.getIthNode(0) << endl; - cout << d_outputChannel.getIthNode(1) << endl; + cout << d_outputChannel.getIthNode(0) << endl << endl; + cout << d_outputChannel.getIthNode(1) << endl << endl; + cout << d_outputChannel.getIthNode(2) << endl << endl; - TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 2u); + TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 3u); TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(0), LEMMA); TS_ASSERT_EQUALS(d_outputChannel.getIthNode(0), gt0Orlt1); TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(1), LEMMA); TS_ASSERT_EQUALS(d_outputChannel.getIthNode(1), geq0OrLeq1); + + TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(2), PROPAGATE); + TS_ASSERT_EQUALS(d_outputChannel.getIthNode(2), leq1); } @@ -210,14 +214,22 @@ public: cout << d_outputChannel.getIthNode(0) << endl; cout << d_outputChannel.getIthNode(1) << endl; + cout << d_outputChannel.getIthNode(2) << endl; + cout << d_outputChannel.getIthNode(3) << endl; - TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 2u); + TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 4u); TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(0), LEMMA); TS_ASSERT_EQUALS(d_outputChannel.getIthNode(0), gt0Orlt1); TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(1), LEMMA); TS_ASSERT_EQUALS(d_outputChannel.getIthNode(1), geq0OrLeq1); + + TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(2), PROPAGATE); + TS_ASSERT_EQUALS(d_outputChannel.getIthNode(2), lt1 ); + + TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(3), PROPAGATE); + TS_ASSERT_EQUALS(d_outputChannel.getIthNode(3), leq1); } void testTPLeq1() { |