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/output_channel.h | |
parent | d8da3b13bc9df7750723cf3da38edc8cb6f67d3d (diff) |
Resource-limiting work.
Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
Diffstat (limited to 'src/theory/output_channel.h')
-rw-r--r-- | src/theory/output_channel.h | 23 |
1 files changed, 12 insertions, 11 deletions
diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index 40eba6ff5..fdf253d3f 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -21,6 +21,7 @@ #include "util/cvc4_assert.h" #include "theory/interrupted.h" +#include "util/resource_manager.h" namespace CVC4 { namespace theory { @@ -84,7 +85,7 @@ public: * With safePoint(), the theory signals that it is at a safe point * and can be interrupted. */ - virtual void safePoint() throw(Interrupted, AssertionException) { + virtual void safePoint() throw(Interrupted, UnsafeInterruptException, AssertionException) { } /** @@ -97,7 +98,7 @@ public: * unit conflict) which is assigned TRUE (and T-conflicting) in the * current assignment. */ - virtual void conflict(TNode n) throw(AssertionException) = 0; + virtual void conflict(TNode n) throw(AssertionException, UnsafeInterruptException) = 0; /** * Propagate a theory literal. @@ -105,7 +106,7 @@ public: * @param n - a theory consequence at the current decision level * @return false if an immediate conflict was encountered */ - virtual bool propagate(TNode n) throw(AssertionException) = 0; + virtual bool propagate(TNode n) throw(AssertionException, UnsafeInterruptException) = 0; /** * Tell the core that a valid theory lemma at decision level 0 has @@ -119,7 +120,7 @@ public: */ virtual LemmaStatus lemma(TNode n, bool removable = false, bool preprocess = false) - throw(TypeCheckingExceptionPrivate, AssertionException) = 0; + throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) = 0; /** * Request a split on a new theory atom. This is equivalent to @@ -128,12 +129,12 @@ public: * @param n - a theory atom; must be of Boolean type */ LemmaStatus split(TNode n) - throw(TypeCheckingExceptionPrivate, AssertionException) { + throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) { return splitLemma(n.orNode(n.notNode())); } virtual LemmaStatus splitLemma(TNode n, bool removable = false) - throw(TypeCheckingExceptionPrivate, AssertionException) = 0; + throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) = 0; /** * If a decision is made on n, it must be in the phase specified. @@ -148,7 +149,7 @@ public: * @param phase - the phase to decide on n */ virtual void requirePhase(TNode n, bool phase) - throw(Interrupted, TypeCheckingExceptionPrivate, AssertionException) = 0; + throw(Interrupted, TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) = 0; /** * Flips the most recent unflipped decision to the other phase and @@ -191,14 +192,14 @@ public: * could be flipped, or if the root decision was re-flipped */ virtual bool flipDecision() - throw(Interrupted, TypeCheckingExceptionPrivate, AssertionException) = 0; + throw(Interrupted, TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) = 0; /** * Notification from a theory that it realizes it is incomplete at * this context level. If SAT is later determined by the * TheoryEngine, it should actually return an UNKNOWN result. */ - virtual void setIncomplete() throw(AssertionException) = 0; + virtual void setIncomplete() throw(AssertionException, UnsafeInterruptException) = 0; /** * "Spend" a "resource." The meaning is specific to the context in @@ -211,7 +212,7 @@ public: * long-running operations, they cannot rely on resource() to break * out of infinite or intractable computations. */ - virtual void spendResource() throw() {} + virtual void spendResource() throw(UnsafeInterruptException) {} /** * Handle user attribute. @@ -226,7 +227,7 @@ public: * Using this leads to non-termination issues. * It is appropriate for prototyping for theories. */ - virtual void demandRestart() throw(TypeCheckingExceptionPrivate, AssertionException) {} + virtual void demandRestart() throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) {} };/* class OutputChannel */ |