diff options
author | Guy <katz911@gmail.com> | 2016-06-01 17:41:17 -0700 |
---|---|---|
committer | Guy <katz911@gmail.com> | 2016-06-01 17:41:17 -0700 |
commit | de0dd1dc966b05467f1a5443ff33094262f5076a (patch) | |
tree | 46a8539229fc31226b416755e6a88c18476ecffc /src/theory/theory_engine.h | |
parent | 89ba584531115b7f6d47088d7614368ea05ab9d8 (diff) |
Revert "Merging proof branch"
This reverts commit 89ba584531115b7f6d47088d7614368ea05ab9d8.
Diffstat (limited to 'src/theory/theory_engine.h')
-rw-r--r-- | src/theory/theory_engine.h | 46 |
1 files changed, 36 insertions, 10 deletions
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 53c4aac77..db94edd7c 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -50,7 +50,6 @@ namespace CVC4 { class ResourceManager; -class LemmaProofRecipe; /** * A pair of a theory and a node. This is used to mark the flow of @@ -271,18 +270,46 @@ class TheoryEngine { } } - void conflict(TNode conflictNode, Proof* pf = NULL) throw(AssertionException, UnsafeInterruptException); + void conflict(TNode conflictNode, Proof* pf = NULL) throw(AssertionException, UnsafeInterruptException) { + Trace("theory::conflict") << "EngineOutputChannel<" << d_theory << ">::conflict(" << conflictNode << ")" << std::endl; + Assert(pf == NULL); // theory shouldn't be producing proofs yet + ++ d_statistics.conflicts; + d_engine->d_outputChannelUsed = true; + d_engine->conflict(conflictNode, d_theory); + } - bool propagate(TNode literal) throw(AssertionException, UnsafeInterruptException); + bool propagate(TNode literal) throw(AssertionException, UnsafeInterruptException) { + Trace("theory::propagate") << "EngineOutputChannel<" << d_theory << ">::propagate(" << literal << ")" << std::endl; + ++ d_statistics.propagations; + d_engine->d_outputChannelUsed = true; + return d_engine->propagate(literal, d_theory); + } theory::LemmaStatus lemma(TNode lemma, ProofRule rule, bool removable = false, bool preprocess = false, bool sendAtoms = false) - throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException); + throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) { + Trace("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma(" << lemma << ")" << std::endl; + ++ d_statistics.lemmas; + d_engine->d_outputChannelUsed = true; + return d_engine->lemma(lemma, rule, false, removable, preprocess, sendAtoms ? d_theory : theory::THEORY_LAST, d_theory); + } - theory::LemmaStatus splitLemma(TNode lemma, bool removable = false) throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException); + /*theory::LemmaStatus preservedLemma(TNode lemma, bool removable = false, bool preprocess = false) throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException, LogicException) { + Trace("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::preservedLemma(" << lemma << ")" << std::endl; + ++ d_statistics.lemmas; + d_engine->d_outputChannelUsed = true; + return d_engine->lemma(lemma, false, removable, preprocess, d_theory); + }*/ + + theory::LemmaStatus splitLemma(TNode lemma, bool removable = false) throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) { + Trace("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::splitLemma(" << lemma << ")" << std::endl; + ++ d_statistics.lemmas; + d_engine->d_outputChannelUsed = true; + return d_engine->lemma(lemma, RULE_SPLIT, false, removable, false, d_theory, d_theory); + } void demandRestart() throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) { NodeManager* curr = NodeManager::currentNM(); @@ -429,7 +456,7 @@ class TheoryEngine { bool removable, bool preprocess, theory::TheoryId atomsTo, - LemmaProofRecipe* proofRecipe); + theory::TheoryId ownerTheory); /** Enusre that the given atoms are send to the given theory */ void ensureLemmaAtoms(const std::vector<TNode>& atoms, theory::TheoryId theory); @@ -579,10 +606,9 @@ private: * asking relevant theories to explain the propagations. Initially * the explanation vector should contain only the element (node, theory) * where the node is the one to be explained, and the theory is the - * theory that sent the literal. The lemmaProofRecipe will contain a list - * of the explanation steps required to produce the original node. + * theory that sent the literal. */ - void getExplanation(std::vector<NodeTheoryPair>& explanationVector, LemmaProofRecipe* lemmaProofRecipe); + void getExplanation(std::vector<NodeTheoryPair>& explanationVector); public: @@ -704,7 +730,7 @@ public: * Returns an explanation of the node propagated to the SAT solver and the theory * that propagated it. */ - Node getExplanationAndRecipe(TNode node, LemmaProofRecipe* proofRecipe); + NodeTheoryPair getExplanationAndExplainer(TNode node); /** * collect model info |