summaryrefslogtreecommitdiff
path: root/test/unit/theory
diff options
context:
space:
mode:
Diffstat (limited to 'test/unit/theory')
-rw-r--r--test/unit/theory/theory_arith_white.h96
1 files changed, 47 insertions, 49 deletions
diff --git a/test/unit/theory/theory_arith_white.h b/test/unit/theory/theory_arith_white.h
index 41d370aac..c6d6e3e2e 100644
--- a/test/unit/theory/theory_arith_white.h
+++ b/test/unit/theory/theory_arith_white.h
@@ -125,7 +125,8 @@ public:
Node x = d_nm->mkVar(*d_realType);
Node c = d_nm->mkConst<Rational>(d_zero);
- Node leq = d_nm->mkNode(LEQ, x, c);
+ Node gt = d_nm->mkNode(GT, x, c);
+ Node leq = gt.notNode();
fakeTheoryEnginePreprocess(leq);
d_arith->assertFact(leq, true);
@@ -149,37 +150,36 @@ public:
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 gt0 = d_nm->mkNode(GT, x, c0);
+ Node gt1 = d_nm->mkNode(GT, 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);
+ Node leq0 = gt0.notNode();
+ Node leq1 = gt1.notNode();
+ Node lt1 = geq1.notNode();
fakeTheoryEnginePreprocess(leq0);
fakeTheoryEnginePreprocess(leq1);
fakeTheoryEnginePreprocess(geq1);
+ d_arith->presolve();
d_arith->assertFact(lt1, true);
-
-
d_arith->check(d_level);
d_arith->propagate(d_level);
- Node gt1ThenGt0 = NodeBuilder<2>(IMPLIES) << gt1 << gt0;
- Node geq1ThenGt0 = NodeBuilder<2>(IMPLIES) << geq1 << gt0;
- Node lt1ThenLeq1 = NodeBuilder<2>(IMPLIES) << lt1 << leq1;
- TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 3u);
+ 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;
+
+ TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 2u);
TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(0), LEMMA);
- TS_ASSERT_EQUALS(d_outputChannel.getIthNode(0), gt1ThenGt0);
+ TS_ASSERT_EQUALS(d_outputChannel.getIthNode(0), gt0Orlt1);
TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(1), LEMMA);
- TS_ASSERT_EQUALS(d_outputChannel.getIthNode(1), geq1ThenGt0);
-
- TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(2), LEMMA);
- TS_ASSERT_EQUALS(d_outputChannel.getIthNode(2), lt1ThenLeq1);
+ TS_ASSERT_EQUALS(d_outputChannel.getIthNode(1), geq0OrLeq1);
}
@@ -188,72 +188,70 @@ public:
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 gt0 = d_nm->mkNode(GT, x, c0);
+ Node gt1 = d_nm->mkNode(GT, 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);
+ Node leq0 = gt0.notNode();
+ Node leq1 = gt1.notNode();
+ Node lt1 = geq1.notNode();
fakeTheoryEnginePreprocess(leq0);
fakeTheoryEnginePreprocess(leq1);
fakeTheoryEnginePreprocess(geq1);
+ d_arith->presolve();
d_arith->assertFact(leq0, true);
-
-
d_arith->check(d_level);
+ d_arith->propagate(d_level);
- Node gt1ThenGt0 = NodeBuilder<2>(IMPLIES) << gt1 << gt0;
- Node geq1ThenGt0 = NodeBuilder<2>(IMPLIES) << geq1 << gt0;
- Node lt1ThenLeq1 = NodeBuilder<2>(IMPLIES) << lt1 << leq1;
+ Node gt0Orlt1 = NodeBuilder<2>(OR) << gt0 << lt1;
+ Node geq0OrLeq1 = NodeBuilder<2>(OR) << geq1 << leq1;
- TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 3u);
+ cout << d_outputChannel.getIthNode(0) << endl;
+ cout << d_outputChannel.getIthNode(1) << endl;
+
+ TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 2u);
TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(0), LEMMA);
- TS_ASSERT_EQUALS(d_outputChannel.getIthNode(0), gt1ThenGt0);
+ TS_ASSERT_EQUALS(d_outputChannel.getIthNode(0), gt0Orlt1);
TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(1), LEMMA);
- TS_ASSERT_EQUALS(d_outputChannel.getIthNode(1), geq1ThenGt0);
-
- TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(2), LEMMA);
- TS_ASSERT_EQUALS(d_outputChannel.getIthNode(2), lt1ThenLeq1);
+ TS_ASSERT_EQUALS(d_outputChannel.getIthNode(1), geq0OrLeq1);
}
+
void testTPLeq1() {
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 gt0 = d_nm->mkNode(GT, x, c0);
+ Node gt1 = d_nm->mkNode(GT, 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);
+ Node leq0 = gt0.notNode();
+ Node leq1 = gt1.notNode();
+ Node lt1 = geq1.notNode();
fakeTheoryEnginePreprocess(leq0);
fakeTheoryEnginePreprocess(leq1);
fakeTheoryEnginePreprocess(geq1);
+ d_arith->presolve();
d_arith->assertFact(leq1, true);
-
-
d_arith->check(d_level);
d_arith->propagate(d_level);
- Node gt1ThenGt0 = NodeBuilder<2>(IMPLIES) << gt1 << gt0;
- Node geq1ThenGt0 = NodeBuilder<2>(IMPLIES) << geq1 << gt0;
- Node lt1ThenLeq1 = NodeBuilder<2>(IMPLIES) << lt1 << leq1;
+ 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;
- TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 3u);
+ TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 2u);
TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(0), LEMMA);
- TS_ASSERT_EQUALS(d_outputChannel.getIthNode(0), gt1ThenGt0);
+ TS_ASSERT_EQUALS(d_outputChannel.getIthNode(0), gt0Orlt1);
TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(1), LEMMA);
- TS_ASSERT_EQUALS(d_outputChannel.getIthNode(1), geq1ThenGt0);
-
- TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(2), LEMMA);
- TS_ASSERT_EQUALS(d_outputChannel.getIthNode(2), lt1ThenLeq1);
+ TS_ASSERT_EQUALS(d_outputChannel.getIthNode(1), geq0OrLeq1);
}
};
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback