diff options
| author | Tim King <taking@cs.nyu.edu> | 2010-05-27 20:34:18 +0000 |
|---|---|---|
| committer | Tim King <taking@cs.nyu.edu> | 2010-05-27 20:34:18 +0000 |
| commit | d1acfe81a013d1f8960bd0267dcd685185ffc785 (patch) | |
| tree | 70870c5ccbea9fff7edf5ba26c5f8e68fe16c20e /src/theory/output_channel.h | |
| parent | e5c77b0674a9cb698e6012ccc1950fef9bee4f8d (diff) | |
Preregistration has been turned on. Highly experimental eager splitting support has been added. Also a few bug fixes to Tableau.
Diffstat (limited to 'src/theory/output_channel.h')
| -rw-r--r-- | src/theory/output_channel.h | 20 |
1 files changed, 15 insertions, 5 deletions
diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index 54fa71808..08a3353e6 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -18,6 +18,7 @@ #ifndef __CVC4__THEORY__OUTPUT_CHANNEL_H #define __CVC4__THEORY__OUTPUT_CHANNEL_H +#include "util/Assert.h" #include "theory/interrupted.h" namespace CVC4 { @@ -53,7 +54,7 @@ public: * With safePoint(), the theory signals that it is at a safe point * and can be interrupted. */ - virtual void safePoint() throw(Interrupted) { + virtual void safePoint() throw(Interrupted, AssertionException) { } /** @@ -66,7 +67,7 @@ public: * * @param safe - whether it is safe to be interrupted */ - virtual void conflict(TNode n, bool safe = false) throw(Interrupted) = 0; + virtual void conflict(TNode n, bool safe = false) throw(Interrupted, AssertionException) = 0; /** * Propagate a theory literal. @@ -75,7 +76,7 @@ public: * * @param safe - whether it is safe to be interrupted */ - virtual void propagate(TNode n, bool safe = false) throw(Interrupted) = 0; + virtual void propagate(TNode n, bool safe = false) throw(Interrupted, AssertionException) = 0; /** * Tell the core that a valid theory lemma at decision level 0 has @@ -84,7 +85,16 @@ public: * @param n - a theory lemma valid at decision level 0 * @param safe - whether it is safe to be interrupted */ - virtual void lemma(TNode n, bool safe = false) throw(Interrupted) = 0; + virtual void lemma(TNode n, bool safe = false) throw(Interrupted, AssertionException) = 0; + + /** + * Tell the core to add the following valid lemma as if it were a user assertion. + * This should NOT be called during solving, only preprocessing. + * + * @param n - a theory lemma valid to be asserted + * @param safe - whether it is safe to be interrupted + */ + virtual void augmentingLemma(TNode n, bool safe = false) throw(Interrupted, AssertionException) = 0; /** * Provide an explanation in response to an explanation request. @@ -92,7 +102,7 @@ public: * @param n - an explanation * @param safe - whether it is safe to be interrupted */ - virtual void explanation(TNode n, bool safe = false) throw(Interrupted) = 0; + virtual void explanation(TNode n, bool safe = false) throw(Interrupted, AssertionException) = 0; };/* class OutputChannel */ |