From 72f552ead344b13d90832222157b970ae3dec8ff Mon Sep 17 00:00:00 2001 From: Dejan Jovanović Date: Thu, 15 Sep 2011 06:53:33 +0000 Subject: additional stuff for sharing, --- src/theory/theory_test_utils.h | 18 ++++++------------ 1 file changed, 6 insertions(+), 12 deletions(-) (limited to 'src/theory/theory_test_utils.h') diff --git a/src/theory/theory_test_utils.h b/src/theory/theory_test_utils.h index ec2405295..bcb1c46d7 100644 --- a/src/theory/theory_test_utils.h +++ b/src/theory/theory_test_utils.h @@ -71,27 +71,21 @@ public: void safePoint() throw(Interrupted, AssertionException) {} - void conflict(TNode n, bool safe = false) - throw(Interrupted, AssertionException) { + void conflict(TNode n) + throw(AssertionException) { push(CONFLICT, n); } - void propagate(TNode n, bool safe = false) - throw(Interrupted, AssertionException) { + void propagate(TNode n) + throw(AssertionException) { push(PROPAGATE, n); } - void lemma(TNode n, bool safe = false) throw(Interrupted, AssertionException) { + void lemma(TNode n, bool removable) throw(AssertionException) { push(LEMMA, n); } - void augmentingLemma(TNode n, bool safe = false) throw(Interrupted, AssertionException){ - push(AUG_LEMMA, n); - } - void explanation(TNode n, bool safe = false) throw(Interrupted, AssertionException) { - push(EXPLANATION, n); - } - void setIncomplete() throw(Interrupted, AssertionException) {} + void setIncomplete() throw(AssertionException) {} void clear() { d_callHistory.clear(); -- cgit v1.2.3