diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-10-12 21:10:36 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-10-12 21:10:36 +0000 |
commit | 3d97646be5eb3f2b50028875f4d899698228e8c7 (patch) | |
tree | 691e57f07b76c3413cebabb7ece4536eb309de16 /src/theory/output_channel.h | |
parent | 2bc4c351bbf89103577fa9f33ebb395f5d61826a (diff) |
hooked up "we are incomplete" flag after conversation with Tim (a theory notifies the theory engine through its output channel); some cleanup; add a regression for bug #216
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 */ |