diff options
Diffstat (limited to 'src/theory/output_channel.h')
-rw-r--r-- | src/theory/output_channel.h | 28 |
1 files changed, 21 insertions, 7 deletions
diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index cdc1e1cc2..cc51c7a7c 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -76,7 +76,8 @@ public: * * @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, bool safe = false) + throw(Interrupted, AssertionException) = 0; /** * Propagate a theory literal. @@ -85,7 +86,8 @@ public: * * @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, bool safe = false) + throw(Interrupted, AssertionException) = 0; /** * Tell the core that a valid theory lemma at decision level 0 has @@ -94,16 +96,19 @@ 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, AssertionException) = 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. + * 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; + virtual void augmentingLemma(TNode n, bool safe = false) + throw(Interrupted, AssertionException) = 0; /** * Provide an explanation in response to an explanation request. @@ -111,7 +116,16 @@ public: * @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; + 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; };/* class OutputChannel */ |