diff options
author | Liana Hadarean <lianah@cs.nyu.edu> | 2014-11-17 15:26:42 -0500 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-11-17 15:26:42 -0500 |
commit | 3ba7ed6b1b09739385ae2ffb77a5c7ccd18b40a5 (patch) | |
tree | 845ae47600ffff9c68fa654c0f78d3474e406beb /src/theory/theory_test_utils.h | |
parent | d8da3b13bc9df7750723cf3da38edc8cb6f67d3d (diff) |
Resource-limiting work.
Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
Diffstat (limited to 'src/theory/theory_test_utils.h')
-rw-r--r-- | src/theory/theory_test_utils.h | 24 |
1 files changed, 13 insertions, 11 deletions
diff --git a/src/theory/theory_test_utils.h b/src/theory/theory_test_utils.h index 6d1275c20..46a717cc5 100644 --- a/src/theory/theory_test_utils.h +++ b/src/theory/theory_test_utils.h @@ -23,13 +23,13 @@ #include "expr/node.h" #include "theory/output_channel.h" #include "theory/interrupted.h" +#include "util/unsafe_interrupt_exception.h" #include <vector> #include <utility> #include <iostream> namespace CVC4 { - namespace theory { /** @@ -72,42 +72,44 @@ public: void safePoint() throw(Interrupted, AssertionException) {} void conflict(TNode n) - throw(AssertionException) { + throw(AssertionException, UnsafeInterruptException) { push(CONFLICT, n); } bool propagate(TNode n) - throw(AssertionException) { + throw(AssertionException, UnsafeInterruptException) { push(PROPAGATE, n); return true; } void propagateAsDecision(TNode n) - throw(AssertionException) { + throw(AssertionException, UnsafeInterruptException) { push(PROPAGATE_AS_DECISION, n); } - LemmaStatus lemma(TNode n, bool removable, bool preprocess) throw(AssertionException) { + LemmaStatus lemma(TNode n, bool removable, bool preprocess) throw(AssertionException, UnsafeInterruptException) { push(LEMMA, n); return LemmaStatus(Node::null(), 0); } - void requirePhase(TNode, bool) throw(Interrupted, AssertionException) { + void requirePhase(TNode, bool) throw(Interrupted, AssertionException, UnsafeInterruptException) { } - bool flipDecision() throw(Interrupted, AssertionException) { + bool flipDecision() throw(Interrupted, AssertionException, UnsafeInterruptException) { return true; } - void setIncomplete() throw(AssertionException) {} + void setIncomplete() throw(AssertionException, UnsafeInterruptException) { + } - void handleUserAttribute( const char* attr, theory::Theory* t ){} + void handleUserAttribute( const char* attr, theory::Theory* t ) { + } void clear() { d_callHistory.clear(); } - LemmaStatus splitLemma(TNode n, bool removable = false) throw(TypeCheckingExceptionPrivate, AssertionException){ + LemmaStatus splitLemma(TNode n, bool removable = false) throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) { push(LEMMA, n); return LemmaStatus(Node::null(), 0); } @@ -125,7 +127,7 @@ public: return d_callHistory.size(); } - void printIth(std::ostream& os, int i){ + void printIth(std::ostream& os, int i) { os << "[TestOutputChannel " << i; os << " " << getIthCallType(i); os << " " << getIthNode(i) << "]"; |