Revert "Merging proof branch"

This reverts commit 89ba584531115b7f6d47088d7614368ea05ab9d8.

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