Revert "Merging proof branch"

This reverts commit 89ba584531115b7f6d47088d7614368ea05ab9d8.

1 files changed, 11 insertions, 10 deletions

diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index 6cc10d878..cf9d519a7 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -36,9 +36,6 @@
 #include "smt_util/lemma_channels.h"
 
 namespace CVC4 {
-
-class LemmaProofRecipe;
-
 namespace prop {
 
 class PropEngine;
@@ -177,7 +174,7 @@ protected:
    * structure in this expression.  Assumed to not be in the
    * translation cache.
    */
-  SatLiteral convertAtom(TNode node, bool noPreprocessing = false);
+  SatLiteral convertAtom(TNode node);
 
 public:
 
@@ -210,10 +207,14 @@ public:
    * @param node node to convert and assert
    * @param removable whether the sat solver can choose to remove the clauses
    * @param negated whether we are asserting the node negated
-   * @param proofRecipe contains the proof recipe for proving this node
+   * @param ownerTheory indicates the theory that should invoked to prove the formula.
    */
-  virtual void convertAndAssert(TNode node, bool removable, bool negated, ProofRule proof_id, TNode from = TNode::null(), LemmaProofRecipe* proofRecipe = NULL) = 0;
-
+  virtual void convertAndAssert(TNode node,
+                                bool removable,
+                                bool negated,
+                                ProofRule proof_id,
+                                TNode from = TNode::null(),
+                                theory::TheoryId ownerTheory = theory::THEORY_LAST) = 0;
   /**
    * Get the node that is represented by the given SatLiteral.
    * @param literal the literal from the sat solver
@@ -234,7 +235,7 @@ public:
    * this is like a "convert-but-don't-assert" version of
    * convertAndAssert().
    */
-  virtual void ensureLiteral(TNode n, bool noPreregistration = false) = 0;
+  virtual void ensureLiteral(TNode n) = 0;
 
   /**
    * Returns the literal that represents the given node in the SAT CNF
@@ -283,7 +284,7 @@ public:
    */
   void convertAndAssert(TNode node, bool removable,
                         bool negated, ProofRule rule, TNode from = TNode::null(),
-                        LemmaProofRecipe* proofRecipe = NULL);
+                        theory::TheoryId ownerTheory = theory::THEORY_LAST);
 
   /**
    * Constructs the stream to use the given sat solver.
@@ -336,7 +337,7 @@ private:
    */
   SatLiteral toCNF(TNode node, bool negated = false);
 
-  void ensureLiteral(TNode n, bool noPreregistration = false);
+  void ensureLiteral(TNode n);
 
 };/* class TseitinCnfStream */