Proper handling for lemmas that are conjuncts:

Record a separate recipe for each conjunct, but have as the "original lemma" in this recipe the complete conjunction, so that we can report this to the theory solver later, if asked.

Refactoring: instead of propagating the proof recipes from the theory engine to the prop engine and cnf stream to be registered there, just register them at the theory engine - as the prop engine and cnf stream don't change them.

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;
         }