Merge remote-tracking branch 'origin/master'

5 files changed, 6 insertions, 20 deletions

diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index eda736b8a..f2401041e 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -678,8 +678,7 @@ void TseitinCnfStream::convertAndAssert(TNode node,
                                         bool removable,
                                         bool negated,
                                         ProofRule proof_id,
-                                        TNode from,
-                                        LemmaProofRecipe* proofRecipe) {
+                                        TNode from) {
   Debug("cnf") << "convertAndAssert(" << node
                << ", removable = " << (removable ? "true" : "false")
                << ", negated = " << (negated ? "true" : "false") << ")" << endl;
@@ -689,12 +688,6 @@ void TseitinCnfStream::convertAndAssert(TNode node,
       Node assertion = negated ? node.notNode() : (Node)node;
       Node from_assertion = negated? from.notNode() : (Node) from;
 
-      if (proofRecipe) {
-        Debug("pf::sat") << "TseitinCnfStream::convertAndAssert: setting proof recipe" << std::endl;
-        proofRecipe->dump("pf::sat");
-        d_cnfProof->setProofRecipe(proofRecipe);
-      }
-
       if (proof_id != RULE_INVALID) {
         d_cnfProof->pushCurrentAssertion(from.isNull() ? assertion : from_assertion);
         d_cnfProof->registerAssertion(from.isNull() ? assertion : from_assertion, proof_id);
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index 6cc10d878..661108dd0 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -37,8 +37,6 @@
 
 namespace CVC4 {
 
-class LemmaProofRecipe;
-
 namespace prop {
 
 class PropEngine;
@@ -210,9 +208,8 @@ 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
    */
-  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()) = 0;
 
   /**
    * Get the node that is represented by the given SatLiteral.
@@ -282,8 +279,7 @@ public:
    * @param negated true if negated
    */
   void convertAndAssert(TNode node, bool removable,
-                        bool negated, ProofRule rule, TNode from = TNode::null(),
-                        LemmaProofRecipe* proofRecipe = NULL);
+                        bool negated, ProofRule rule, TNode from = TNode::null());
 
   /**
    * Constructs the stream to use the given sat solver.
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index eb607e901..6cdf17f30 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -132,13 +132,12 @@ void PropEngine::assertFormula(TNode node) {
 void PropEngine::assertLemma(TNode node, bool negated,
                              bool removable,
                              ProofRule rule,
-                             LemmaProofRecipe* proofRecipe,
                              TNode from) {
   //Assert(d_inCheckSat, "Sat solver should be in solve()!");
   Debug("prop::lemmas") << "assertLemma(" << node << ")" << endl;
 
   // Assert as (possibly) removable
-  d_cnfStream->convertAndAssert(node, removable, negated, rule, from, proofRecipe);
+  d_cnfStream->convertAndAssert(node, removable, negated, rule, from);
 }
 
 void PropEngine::requirePhase(TNode n, bool phase) {
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index c02015931..f966def26 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -37,7 +37,6 @@ namespace CVC4 {
 class ResourceManager;
 class DecisionEngine;
 class TheoryEngine;
-class LemmaProofRecipe;
 
 namespace theory {
   class TheoryRegistrar;
@@ -135,7 +134,7 @@ public:
    * @param removable whether this lemma can be quietly removed based
    * on an activity heuristic (or not)
    */
-  void assertLemma(TNode node, bool negated, bool removable, ProofRule rule, LemmaProofRecipe* proofRecipe, TNode from = TNode::null());
+  void assertLemma(TNode node, bool negated, bool removable, ProofRule rule, TNode from = TNode::null());
 
   /**
    * If ever n is decided upon, it must be in the given phase.  This
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index 6e8f1fbbf..5f5eac733 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -181,8 +181,7 @@ void TheoryProxy::notifyRestart() {
             Debug("shared") << "=) " << asNode << std::endl;
           }
 
-          LemmaProofRecipe* noProofRecipe = NULL;
-          d_propEngine->assertLemma(d_theoryEngine->preprocess(asNode), false, true, RULE_INVALID, noProofRecipe);
+          d_propEngine->assertLemma(d_theoryEngine->preprocess(asNode), false, true, RULE_INVALID);
         } else {
           Debug("shared") << "=(" << asNode << std::endl;
         }