summaryrefslogtreecommitdiff
path: root/test
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@gmail.com>2010-10-12 21:10:36 +0000
committerMorgan Deters <mdeters@gmail.com>2010-10-12 21:10:36 +0000
commit3d97646be5eb3f2b50028875f4d899698228e8c7 (patch)
tree691e57f07b76c3413cebabb7ece4536eb309de16 /test
parent2bc4c351bbf89103577fa9f33ebb395f5d61826a (diff)
hooked up "we are incomplete" flag after conversation with Tim (a theory notifies the theory engine through its output channel); some cleanup; add a regression for bug #216
Diffstat (limited to 'test')
-rw-r--r--test/regress/regress0/bug216.smt28
-rw-r--r--test/unit/expr/node_self_iterator_black.h1
-rw-r--r--test/unit/theory/theory_black.h20
-rw-r--r--test/unit/theory/theory_engine_white.h3
4 files changed, 27 insertions, 5 deletions
diff --git a/test/regress/regress0/bug216.smt2 b/test/regress/regress0/bug216.smt2
new file mode 100644
index 000000000..78e0f716c
--- /dev/null
+++ b/test/regress/regress0/bug216.smt2
@@ -0,0 +1,8 @@
+(set-logic QF_UF)
+(declare-fun x () Bool)
+(declare-fun y () Bool)
+(assert (=> x y))
+(check-sat) ; returns sat
+(assert (=> y x))
+(assert (and x (not y)))
+(check-sat) ; returns sat --> ERROR
diff --git a/test/unit/expr/node_self_iterator_black.h b/test/unit/expr/node_self_iterator_black.h
index 5627a9db5..4e7c198ee 100644
--- a/test/unit/expr/node_self_iterator_black.h
+++ b/test/unit/expr/node_self_iterator_black.h
@@ -71,6 +71,7 @@ public:
TS_ASSERT(j == NodeSelfIterator::selfEnd(x_and_y));
TS_ASSERT(i == x_and_y.end());
TS_ASSERT(j == x_and_y.end());
+
i = x_and_y.begin();
TS_ASSERT(i != x_and_y.end());
TS_ASSERT(*i == x);
diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h
index 57ce0c78e..f0da885c7 100644
--- a/test/unit/theory/theory_black.h
+++ b/test/unit/theory/theory_black.h
@@ -52,25 +52,35 @@ public:
void safePoint() throw(Interrupted, AssertionException) {}
- void conflict(TNode n, bool safe = false) throw(Interrupted, AssertionException) {
+ void conflict(TNode n, bool safe = false)
+ throw(Interrupted, AssertionException) {
push(CONFLICT, n);
}
- void propagate(TNode n, bool safe = false) throw(Interrupted, AssertionException) {
+ void propagate(TNode n, bool safe = false)
+ throw(Interrupted, AssertionException) {
push(PROPAGATE, n);
}
- void lemma(TNode n, bool safe = false) throw(Interrupted, AssertionException){
+ void lemma(TNode n, bool safe = false)
+ throw(Interrupted, AssertionException) {
push(LEMMA, n);
}
- void augmentingLemma(TNode n, bool safe = false) throw(Interrupted, AssertionException){
+ void augmentingLemma(TNode n, bool safe = false)
+ throw(Interrupted, AssertionException) {
Unreachable();
}
- void explanation(TNode n, bool safe = false) throw(Interrupted, AssertionException) {
+ void explanation(TNode n, bool safe = false)
+ throw(Interrupted, AssertionException) {
push(EXPLANATION, n);
}
+ void setIncomplete()
+ throw(Interrupted, AssertionException) {
+ Unreachable();
+ }
+
void clear() {
d_callHistory.clear();
}
diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h
index 965857684..6adbba207 100644
--- a/test/unit/theory/theory_engine_white.h
+++ b/test/unit/theory/theory_engine_white.h
@@ -62,6 +62,9 @@ class FakeOutputChannel : public OutputChannel {
void explanation(TNode n, bool safe) throw(AssertionException) {
Unimplemented();
}
+ void setIncomplete() throw(AssertionException) {
+ Unimplemented()
+ }
};/* class FakeOutputChannel */
class FakeTheory;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback