diff options
author | Tim King <taking@cs.nyu.edu> | 2010-06-29 20:53:47 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2010-06-29 20:53:47 +0000 |
commit | e792bb8628ea7010fa9c452bf1aa7ba1b60291a3 (patch) | |
tree | ddc12f92092627b7aee2a63dca8dd66279b2970e /src/theory/theory_engine.h | |
parent | e7e9c10006b5b243a73832ed97c5dec79df6c90a (diff) |
Merging the unate-propagator branch into the trunk. This is a big update so expect a little turbulence. This commit will not compile. There will be a second commit that fixes this in a moment. I am delaying a change to avoid svn whining about a conflict.
Diffstat (limited to 'src/theory/theory_engine.h')
-rw-r--r-- | src/theory/theory_engine.h | 46 |
1 files changed, 43 insertions, 3 deletions
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index c2511f4e6..15b406cdd 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -64,13 +64,22 @@ class TheoryEngine { TheoryEngine* d_engine; context::Context* d_context; context::CDO<Node> d_conflictNode; + context::CDO<Node> d_explanationNode; + + /** + * Literals that are propagated by the theory. Note that these are TNodes. + * The theory can only propagate nodes that have an assigned literal in the + * sat solver and are hence referenced in the SAT solver. + */ + std::vector<TNode> d_propagatedLiterals; public: EngineOutputChannel(TheoryEngine* engine, context::Context* context) : d_engine(engine), d_context(context), - d_conflictNode(context) { + d_conflictNode(context), + d_explanationNode(context){ } void conflict(TNode conflictNode, bool safe) throw(theory::Interrupted, AssertionException) { @@ -82,7 +91,9 @@ class TheoryEngine { } } - void propagate(TNode, 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); ++(d_engine->d_statistics.d_statPropagate); } @@ -94,7 +105,9 @@ class TheoryEngine { ++(d_engine->d_statistics.d_statAugLemma); d_engine->newAugmentingLemma(node); } - void explanation(TNode, bool) throw(theory::Interrupted, AssertionException) { + void explanation(TNode explanationNode, bool) throw(theory::Interrupted, AssertionException) { + d_explanationNode = explanationNode; + ++(d_engine->d_statistics.d_statExplanatation); ++(d_engine->d_statistics.d_statExplanatation); } }; @@ -302,6 +315,7 @@ public: inline bool check(theory::Theory::Effort effort) { d_theoryOut.d_conflictNode = Node::null(); + d_theoryOut.d_propagatedLiterals.clear(); // Do the checking try { //d_bool.check(effort); @@ -316,13 +330,23 @@ public: return d_theoryOut.d_conflictNode.get().isNull(); } + inline const std::vector<TNode>& getPropagatedLiterals() const { + return d_theoryOut.d_propagatedLiterals; + } + + void clearPropagatedLiterals() { + d_theoryOut.d_propagatedLiterals.clear(); + } + inline void newLemma(TNode node) { d_propEngine->assertLemma(node); } + inline void newAugmentingLemma(TNode node) { Node preprocessed = preprocess(node); d_propEngine->assertFormula(preprocessed); } + /** * Returns the last conflict (if any). */ @@ -330,6 +354,21 @@ public: return d_theoryOut.d_conflictNode; } + inline void propagate() { + d_theoryOut.d_propagatedLiterals.clear(); + // Do the propagation + d_uf.propagate(theory::Theory::FULL_EFFORT); + d_arith.propagate(theory::Theory::FULL_EFFORT); + } + + inline Node getExplanation(TNode node){ + d_theoryOut.d_explanationNode = Node::null(); + theory::Theory* theory = + node.getKind() == kind::NOT ? theoryOf(node[0]) : theoryOf(node); + theory->explain(node); + return d_theoryOut.d_explanationNode; + } + private: class Statistics { public: @@ -350,6 +389,7 @@ private: }; Statistics d_statistics; + };/* class TheoryEngine */ }/* CVC4 namespace */ |