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/theory_engine.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/theory_engine.h')
-rw-r--r-- | src/theory/theory_engine.h | 36 |
1 files changed, 30 insertions, 6 deletions
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 85e6d2cfc..ca39001fe 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -83,8 +83,10 @@ class TheoryEngine { void newFact(TNode n); - void conflict(TNode conflictNode, bool safe) throw(theory::Interrupted, AssertionException) { - Debug("theory") << "EngineOutputChannel::conflict(" << conflictNode << ")" << std::endl; + void conflict(TNode conflictNode, bool safe) + throw(theory::Interrupted, AssertionException) { + Debug("theory") << "EngineOutputChannel::conflict(" + << conflictNode << ")" << std::endl; d_conflictNode = conflictNode; ++(d_engine->d_statistics.d_statConflicts); if(safe) { @@ -92,23 +94,32 @@ class TheoryEngine { } } - void propagate(TNode lit, bool) throw(theory::Interrupted, AssertionException) { + void propagate(TNode lit, bool) + throw(theory::Interrupted, AssertionException) { d_propagatedLiterals.push_back(lit); ++(d_engine->d_statistics.d_statPropagate); } - void lemma(TNode node, bool) throw(theory::Interrupted, AssertionException) { + void lemma(TNode node, bool) + throw(theory::Interrupted, AssertionException) { ++(d_engine->d_statistics.d_statLemma); d_engine->newLemma(node); } - void augmentingLemma(TNode node, bool) throw(theory::Interrupted, AssertionException) { + void augmentingLemma(TNode node, bool) + throw(theory::Interrupted, AssertionException) { ++(d_engine->d_statistics.d_statAugLemma); d_engine->newAugmentingLemma(node); } - void explanation(TNode explanationNode, bool) throw(theory::Interrupted, AssertionException) { + void explanation(TNode explanationNode, bool) + throw(theory::Interrupted, AssertionException) { d_explanationNode = explanationNode; ++(d_engine->d_statistics.d_statExplanation); } + + void setIncomplete() + throw(theory::Interrupted, AssertionException) { + d_engine->d_incomplete = true; + } };/* class EngineOutputChannel */ EngineOutputChannel d_theoryOut; @@ -130,6 +141,12 @@ class TheoryEngine { bool d_hasShutDown; /** + * True if a theory has notified us of incompleteness (at this + * context level or below). + */ + context::CDO<bool> d_incomplete; + + /** * Check whether a node is in the pre-rewrite cache or not. */ static bool inPreRewriteCache(TNode n, bool topLevel) throw() { @@ -206,6 +223,13 @@ public: } /** + * Return whether or not we are incomplete (in the current context). + */ + bool isIncomplete() { + return d_incomplete; + } + + /** * This is called at shutdown time by the SmtEngine, just before * destruction. It is important because there are destruction * ordering issues between PropEngine and Theory. |