diff options
Diffstat (limited to 'src/theory/output_channel.h')
-rw-r--r-- | src/theory/output_channel.h | 30 |
1 files changed, 6 insertions, 24 deletions
diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index bf928cb62..f5bf620bf 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -69,59 +69,41 @@ public: * assigned false), or else a literal by itself (in the case of a * unit conflict) which is assigned TRUE (and T-conflicting) in the * current assignment. - * - * @param safe - whether it is safe to be interrupted */ - virtual void conflict(TNode n, bool safe = false) - throw(Interrupted, AssertionException) = 0; + virtual void conflict(TNode n) throw(AssertionException) = 0; /** * Propagate a theory literal. * * @param n - a theory consequence at the current decision level - * @param safe - whether it is safe to be interrupted */ - virtual void propagate(TNode n, bool safe = false) - throw(Interrupted, AssertionException) = 0; + virtual void propagate(TNode n) throw(AssertionException) = 0; /** * Tell the core that a valid theory lemma at decision level 0 has * been detected. (This requests a split.) * * @param n - a theory lemma valid at decision level 0 - * @param safe - whether it is safe to be interrupted + * @param removable - whether the lemma can be removed at any point */ - virtual void lemma(TNode n, bool safe = false) - throw(Interrupted, TypeCheckingExceptionPrivate, AssertionException) = 0; + virtual void lemma(TNode n, bool removable = false) throw(TypeCheckingExceptionPrivate, AssertionException) = 0; /** * Request a split on a new theory atom. This is equivalent to * calling lemma({OR n (NOT n)}). * * @param n - a theory atom; must be of Boolean type - * @param safe - whether it is safe to be interrupted */ - void split(TNode n, bool safe = false) - throw(Interrupted, TypeCheckingExceptionPrivate, AssertionException) { + void split(TNode n) throw(TypeCheckingExceptionPrivate, AssertionException) { lemma(n.orNode(n.notNode())); } /** - * Provide an explanation in response to an explanation request. - * - * @param n - an explanation - * @param safe - whether it is safe to be interrupted - */ - virtual void explanation(TNode n, bool safe = false) - throw(Interrupted, AssertionException) = 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(Interrupted, AssertionException) = 0; + virtual void setIncomplete() throw(AssertionException) = 0; };/* class OutputChannel */ |