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.

diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index eda736b8a7ce2a802e4089735386b3c2943c1ae6..f2401041ecc9573c4d17bbb994d6f9e4d590e5f8 100644 (file)
--- 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 6cc10d878dd46a3fd292db789e6874532c3f76e7..661108dd0b50a8c9f6d6cfe1992db896b29607c5 100644 (file)
--- 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 eb607e9018735fd4c5137a98811fb06edd472421..6cdf17f30aa0339d72994136d2deeec55ee9db95 100644 (file)
--- 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 c02015931f177e44c7cdeb347c4808f5d40f396c..f966def2662540aba93e19f6dcdcd483774f4324 100644 (file)
--- 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 6e8f1fbbf97b971b9ec3547db9349a894b4ec2ae..5f5eac73374003afb2198fe84b05ed87e586050f 100644 (file)
--- 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;
         }

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 0ec55a5e65ee9063f3aaf036c98722b1600c7360..0aaf602e3b35164202d7280bda6f2437210d75e4 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -83,35 +83,8 @@ theory::LemmaStatus TheoryEngine::EngineOutputChannel::lemma(TNode lemma,
   ++ d_statistics.lemmas;
   d_engine->d_outputChannelUsed = true;
 
-  LemmaProofRecipe* proofRecipe = NULL;
   PROOF({
-      // Theory lemmas have one step that proves the empty clause
-      proofRecipe = new LemmaProofRecipe;
-
-      Node emptyNode;
-      LemmaProofRecipe::ProofStep proofStep(d_theory, emptyNode);
-
-      proofRecipe->setOriginalLemma(lemma);
-
-      Node rewritten;
-      if (lemma.getKind() == kind::OR) {
-        for (unsigned i = 0; i < lemma.getNumChildren(); ++i) {
-          rewritten = theory::Rewriter::rewrite(lemma[i]);
-          if (rewritten != lemma[i]) {
-            proofRecipe->addRewriteRule(lemma[i].negate(), rewritten.negate());
-          }
-          proofStep.addAssertion(lemma[i]);
-          proofRecipe->addBaseAssertion(rewritten);
-        }
-      } else {
-        rewritten = theory::Rewriter::rewrite(lemma);
-        if (rewritten != lemma) {
-          proofRecipe->addRewriteRule(lemma.negate(), rewritten.negate());
-        }
-        proofStep.addAssertion(lemma);
-        proofRecipe->addBaseAssertion(rewritten);
-      }
-      proofRecipe->addStep(proofStep);
+      registerLemmaRecipe(lemma, lemma, d_theory);
     });
 
   theory::LemmaStatus result = d_engine->lemma(lemma,
@@ -119,22 +92,59 @@ theory::LemmaStatus TheoryEngine::EngineOutputChannel::lemma(TNode lemma,
                                                false,
                                                removable,
                                                preprocess,
-                                               sendAtoms ? d_theory : theory::THEORY_LAST,
-                                               proofRecipe);
-  PROOF(delete proofRecipe;);
+                                               sendAtoms ? d_theory : theory::THEORY_LAST);
+  // PROOF(delete proofRecipe;);
   return result;
 }
 
+void TheoryEngine::EngineOutputChannel::registerLemmaRecipe(Node lemma, Node originalLemma, theory::TheoryId theoryId) {
+  // During CNF conversion, conjunctions will be broken down into
+  // multiple lemmas. In order for the recipes to match, we have to do
+  // the same here.
+  if (lemma.getKind() == kind::AND) {
+    for (unsigned i = 0; i < lemma.getNumChildren(); ++i)
+      registerLemmaRecipe(lemma[i], originalLemma, theoryId);
+  }
+
+  // Theory lemmas have one step that proves the empty clause
+  LemmaProofRecipe proofRecipe;
+  Node emptyNode;
+  LemmaProofRecipe::ProofStep proofStep(theoryId, emptyNode);
+
+  // Remember the original lemma, so we can report this later when asked to
+  proofRecipe.setOriginalLemma(originalLemma);
+
+  // Record the assertions and rewrites
+  Node rewritten;
+  if (lemma.getKind() == kind::OR) {
+    for (unsigned i = 0; i < lemma.getNumChildren(); ++i) {
+      rewritten = theory::Rewriter::rewrite(lemma[i]);
+      if (rewritten != lemma[i]) {
+        proofRecipe.addRewriteRule(lemma[i].negate(), rewritten.negate());
+      }
+      proofStep.addAssertion(lemma[i]);
+      proofRecipe.addBaseAssertion(rewritten);
+    }
+  } else {
+    rewritten = theory::Rewriter::rewrite(lemma);
+    if (rewritten != lemma) {
+      proofRecipe.addRewriteRule(lemma.negate(), rewritten.negate());
+    }
+    proofStep.addAssertion(lemma);
+    proofRecipe.addBaseAssertion(rewritten);
+  }
+  proofRecipe.addStep(proofStep);
+  ProofManager::getCnfProof()->setProofRecipe(&proofRecipe);
+}
+
 theory::LemmaStatus TheoryEngine::EngineOutputChannel::splitLemma(TNode lemma, bool removable)
   throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) {
   Debug("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma(" << lemma << ")" << std::endl;
   ++ d_statistics.lemmas;
   d_engine->d_outputChannelUsed = true;
 
-
-  LemmaProofRecipe* proofRecipe = NULL;
   Debug("pf::explain") << "TheoryEngine::EngineOutputChannel::splitLemma( " << lemma << " )" << std::endl;
-  theory::LemmaStatus result = d_engine->lemma(lemma, RULE_SPLIT, false, removable, false, d_theory, proofRecipe);
+  theory::LemmaStatus result = d_engine->lemma(lemma, RULE_SPLIT, false, removable, false, d_theory);
   return result;
 }
 
@@ -629,8 +639,7 @@ void TheoryEngine::combineTheories() {
     // We need to split on it
     Debug("combineTheories") << "TheoryEngine::combineTheories(): requesting a split " << endl;
 
-    LemmaProofRecipe* proofRecipe = NULL;
-    lemma(equality.orNode(equality.notNode()), RULE_INVALID, false, false, false, carePair.theory, proofRecipe);
+    lemma(equality.orNode(equality.notNode()), RULE_INVALID, false, false, false, carePair.theory);
 
     // This code is supposed to force preference to follow what the theory models already have
     // but it doesn't seem to make a big difference - need to explore more -Clark
@@ -1616,8 +1625,7 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node,
                                         bool negated,
                                         bool removable,
                                         bool preprocess,
-                                        theory::TheoryId atomsTo,
-                                        LemmaProofRecipe* proofRecipe) {
+                                        theory::TheoryId atomsTo) {
   // For resource-limiting (also does a time check).
   // spendResource();
 
@@ -1667,10 +1675,10 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node,
   }
 
   // assert to prop engine
-  d_propEngine->assertLemma(additionalLemmas[0], negated, removable, rule, proofRecipe, node);
+  d_propEngine->assertLemma(additionalLemmas[0], negated, removable, rule, node);
   for (unsigned i = 1; i < additionalLemmas.size(); ++ i) {
     additionalLemmas[i] = theory::Rewriter::rewrite(additionalLemmas[i]);
-    d_propEngine->assertLemma(additionalLemmas[i], false, removable, rule, proofRecipe, node);
+    d_propEngine->assertLemma(additionalLemmas[i], false, removable, rule, node);
   }
 
   // WARNING: Below this point don't assume additionalLemmas[0] to be not negated.
@@ -1729,10 +1737,11 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) {
 
     // Process the explanation
     getExplanation(explanationVector, proofRecipe);
+    PROOF(ProofManager::getCnfProof()->setProofRecipe(proofRecipe));
     Node fullConflict = mkExplanation(explanationVector);
     Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << "): full = " << fullConflict << endl;
     Assert(properConflict(fullConflict));
-    lemma(fullConflict, RULE_CONFLICT, true, true, false, THEORY_LAST, proofRecipe);
+    lemma(fullConflict, RULE_CONFLICT, true, true, false, THEORY_LAST);
 
   } else {
     // When only one theory, the conflict should need no processing
@@ -1758,9 +1767,11 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) {
           proofRecipe->getStep(0)->addAssertion(conflict.negate());
           proofRecipe->addBaseAssertion(conflict.negate());
         }
+
+        ProofManager::getCnfProof()->setProofRecipe(proofRecipe);
       });
 
-    lemma(conflict, RULE_CONFLICT, true, true, false, THEORY_LAST, proofRecipe);
+    lemma(conflict, RULE_CONFLICT, true, true, false, THEORY_LAST);
   }
 
   PROOF({

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index eed58864a40ed2f527fb7cbc0d729fdf80a44006..ea8628f9c028370048d29c58d2ff97213eeec43f 100644 (file)
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -322,6 +322,13 @@ class TheoryEngine {
     void handleUserAttribute( const char* attr, theory::Theory* t ){
       d_engine->handleUserAttribute( attr, t );
     }
+
+  private:
+
+    /**
+     * A helper function for registering lemma recipes with the proof engine
+     */
+    void registerLemmaRecipe(Node lemma, Node originalLemma, theory::TheoryId theoryId);
   };/* class TheoryEngine::EngineOutputChannel */
 
   /**
@@ -429,8 +436,7 @@ class TheoryEngine {
                             bool negated,
                             bool removable,
                             bool preprocess,
-                            theory::TheoryId atomsTo,
-                            LemmaProofRecipe* proofRecipe);
+                            theory::TheoryId atomsTo);
 
   /** Enusre that the given atoms are send to the given theory */
   void ensureLemmaAtoms(const std::vector<TNode>& atoms, theory::TheoryId theory);