diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-08-17 15:20:19 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-08-17 15:20:19 +0000 |
commit | 32e1d3558f17d12f2631175776209a5f8cabbdd9 (patch) | |
tree | ebc20658d5375b17f13b5c83d3dc7ee078029f96 /src/theory/theory_engine.h | |
parent | 41dc1b3685b9258660dab571f8f8b56deb0fb095 (diff) |
new implementation of lemmas on demand
comparison <http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=2673&&p=5&reference_id=2637>
Diffstat (limited to 'src/theory/theory_engine.h')
-rw-r--r-- | src/theory/theory_engine.h | 53 |
1 files changed, 35 insertions, 18 deletions
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 3507723f9..1e5653564 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -98,7 +98,7 @@ class TheoryEngine { TheoryEngine* d_engine; context::Context* d_context; - context::CDO<Node> d_conflictNode; + context::CDO<bool> d_inConflict; context::CDO<Node> d_explanationNode; /** @@ -113,12 +113,29 @@ class TheoryEngine { d_newFactTimer, "theory::newFactTimer"); + /** + * Check if the node is in conflict for debug purposes + */ + bool isProperConflict(TNode conflictNode) { + bool value; + if (conflictNode.getKind() == kind::AND) { + for (unsigned i = 0; i < conflictNode.getNumChildren(); ++ i) { + if (!d_engine->getPropEngine()->hasValue(conflictNode[i], value)) return false; + if (!value) return false; + } + } else { + if (!d_engine->getPropEngine()->hasValue(conflictNode, value)) return false; + return value; + } + return true; + } + public: EngineOutputChannel(TheoryEngine* engine, context::Context* context) : d_engine(engine), d_context(context), - d_conflictNode(context), + d_inConflict(context, false), d_explanationNode(context) { } @@ -126,10 +143,15 @@ class TheoryEngine { void conflict(TNode conflictNode, bool safe) throw(theory::Interrupted, AssertionException) { - Trace("theory") << "EngineOutputChannel::conflict(" - << conflictNode << ")" << std::endl; - d_conflictNode = conflictNode; + Trace("theory") << "EngineOutputChannel::conflict(" << conflictNode << ")" << std::endl; + d_inConflict = true; + ++(d_engine->d_statistics.d_statConflicts); + + // Construct the lemma (note that no CNF caching should happen as all the literals already exists) + Assert(isProperConflict(conflictNode)); + d_engine->newLemma(conflictNode, true, true); + if(safe) { throw theory::Interrupted(); } @@ -143,12 +165,13 @@ class TheoryEngine { ++(d_engine->d_statistics.d_statPropagate); } - void lemma(TNode node, bool) + void lemma(TNode node, bool removable = false) throw(theory::Interrupted, AssertionException) { Trace("theory") << "EngineOutputChannel::lemma(" << node << ")" << std::endl; ++(d_engine->d_statistics.d_statLemma); - d_engine->newLemma(node); + + d_engine->newLemma(node, false, removable); } void explanation(TNode explanationNode, bool) @@ -387,7 +410,7 @@ public: * Check all (currently-active) theories for conflicts. * @param effort the effort level to use */ - bool check(theory::Theory::Effort effort); + void check(theory::Theory::Effort effort); /** * Calls staticLearning() on all theories, accumulating their @@ -414,23 +437,17 @@ public: d_theoryOut.d_propagatedLiterals.clear(); } - inline void newLemma(TNode node) { + inline void newLemma(TNode node, bool negated, bool removable) { // Remove the ITEs and assert to prop engine std::vector<Node> additionalLemmas; additionalLemmas.push_back(node); RemoveITE::run(additionalLemmas); - for (unsigned i = 0; i < additionalLemmas.size(); ++ i) { - d_propEngine->assertLemma(theory::Rewriter::rewrite(additionalLemmas[i])); + d_propEngine->assertLemma(theory::Rewriter::rewrite(additionalLemmas[0]), negated, removable); + for (unsigned i = 1; i < additionalLemmas.size(); ++ i) { + d_propEngine->assertLemma(theory::Rewriter::rewrite(additionalLemmas[i]), false, removable); } } - /** - * Returns the last conflict (if any). - */ - inline Node getConflict() { - return d_theoryOut.d_conflictNode; - } - void propagate(); inline Node getExplanation(TNode node, theory::Theory* theory) { |