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 | |
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')
-rw-r--r-- | src/theory/theory_engine.cpp | 15 | ||||
-rw-r--r-- | src/theory/theory_engine.h | 53 |
2 files changed, 41 insertions, 27 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 28d7ab2c0..b1b4d67dd 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -235,8 +235,8 @@ void TheoryEngine::preRegister(TNode preprocessed) { * Check all (currently-active) theories for conflicts. * @param effort the effort level to use */ -bool TheoryEngine::check(theory::Theory::Effort effort) { - d_theoryOut.d_conflictNode = Node::null(); +void TheoryEngine::check(theory::Theory::Effort effort) { + d_theoryOut.d_propagatedLiterals.clear(); #ifdef CVC4_FOR_EACH_THEORY_STATEMENT @@ -245,8 +245,8 @@ bool TheoryEngine::check(theory::Theory::Effort effort) { #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ if (theory::TheoryTraits<THEORY>::hasCheck && d_theoryIsActive[THEORY]) { \ reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(d_theoryTable[THEORY])->check(effort); \ - if (!d_theoryOut.d_conflictNode.get().isNull()) { \ - return false; \ + if (d_theoryOut.d_inConflict) { \ + return; \ } \ } @@ -256,8 +256,6 @@ bool TheoryEngine::check(theory::Theory::Effort effort) { } catch(const theory::Interrupted&) { Trace("theory") << "TheoryEngine::check() => conflict" << std::endl; } - - return true; } void TheoryEngine::propagate() { @@ -296,7 +294,6 @@ bool TheoryEngine::presolve() { // at doing something with the input formula, even if it wouldn't // otherwise be active. - d_theoryOut.d_conflictNode = Node::null(); d_theoryOut.d_propagatedLiterals.clear(); try { @@ -307,7 +304,7 @@ bool TheoryEngine::presolve() { #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ if (theory::TheoryTraits<THEORY>::hasPresolve) { \ reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(d_theoryTable[THEORY])->presolve(); \ - if(!d_theoryOut.d_conflictNode.get().isNull()) { \ + if(d_theoryOut.d_inConflict) { \ return true; \ } \ } @@ -318,7 +315,7 @@ bool TheoryEngine::presolve() { Trace("theory") << "TheoryEngine::presolve() => interrupted" << endl; } // return whether we have a conflict - return !d_theoryOut.d_conflictNode.get().isNull(); + return false; } 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) { |