(proof-new) Updates to assertions pipeline and preprocess generator (#5300)

This updates and improves assertions pipeline and preprocess generator so that they avoid cyclic proofs and have better infrastructure for catching pedantic failures.

This is in preparation for making the non-clausal-simplification pass proof producing.

diff --git a/src/preprocessing/assertion_pipeline.cpp b/src/preprocessing/assertion_pipeline.cpp
index 4529ad5e1ab3458ccb80a8d73072dcd5bb4bb49d..78c459cb7b5249eaea6c77639e07373d443a9946 100644 (file)
--- a/src/preprocessing/assertion_pipeline.cpp
+++ b/src/preprocessing/assertion_pipeline.cpp
@@ -62,6 +62,8 @@ void AssertionPipeline::push_back(Node n,
     Assert(d_assumptionsStart + d_numAssumptions == d_nodes.size() - 1);
     d_numAssumptions++;
   }
+  Trace("assert-pipeline") << "Assertions: ...new assertion " << n
+                           << ", isInput=" << isInput << std::endl;
   if (isProofEnabled())
   {
     if (!isInput)
@@ -71,7 +73,9 @@ void AssertionPipeline::push_back(Node n,
     }
     else
     {
-      Trace("smt-pppg") << "...input assertion " << n << std::endl;
+      Assert(pgen == nullptr);
+      // n is an input assertion, whose proof should be ASSUME.
+      d_pppg->notifyInput(n);
     }
   }
 }
@@ -90,8 +94,8 @@ void AssertionPipeline::replace(size_t i, Node n, ProofGenerator* pgen)
     // no change, skip
     return;
   }
-  Trace("smt-pppg-repl") << "Replace " << d_nodes[i] << " with " << n
-                         << std::endl;
+  Trace("assert-pipeline") << "Assertions: Replace " << d_nodes[i] << " with "
+                           << n << std::endl;
   if (options::unsatCores())
   {
     ProofManager::currentPM()->addDependence(n, d_nodes[i]);
@@ -111,6 +115,7 @@ void AssertionPipeline::replaceTrusted(size_t i, theory::TrustNode trn)
     return;
   }
   Assert(trn.getKind() == theory::TrustNodeKind::REWRITE);
+  Assert(trn.getProven()[0] == d_nodes[i]);
   replace(i, trn.getNode(), trn.getGenerator());
 }
 
@@ -145,6 +150,10 @@ void AssertionPipeline::conjoin(size_t i, Node n, ProofGenerator* pg)
   NodeManager* nm = NodeManager::currentNM();
   Node newConj = nm->mkNode(kind::AND, d_nodes[i], n);
   Node newConjr = theory::Rewriter::rewrite(newConj);
+  Trace("assert-pipeline") << "Assertions: conjoin " << n << " to "
+                           << d_nodes[i] << std::endl;
+  Trace("assert-pipeline-debug") << "conjoin " << n << " to " << d_nodes[i]
+                                 << ", got " << newConjr << std::endl;
   if (newConjr == d_nodes[i])
   {
     // trivial, skip
@@ -152,29 +161,45 @@ void AssertionPipeline::conjoin(size_t i, Node n, ProofGenerator* pg)
   }
   if (isProofEnabled())
   {
-    // ---------- from pppg   --------- from pg
-    // d_nodes[i]                n
-    // -------------------------------- AND_INTRO
-    //      d_nodes[i] ^ n
-    // -------------------------------- MACRO_SR_PRED_TRANSFORM
-    //   rewrite( d_nodes[i] ^ n )
-    // allocate a fresh proof which will act as the proof generator
-    LazyCDProof* lcp = d_pppg->allocateHelperProof();
-    lcp->addLazyStep(d_nodes[i], d_pppg, false);
-    lcp->addLazyStep(
-        n, pg, false, "AssertionPipeline::conjoin", false, PfRule::PREPROCESS);
-    lcp->addStep(newConj, PfRule::AND_INTRO, {d_nodes[i], n}, {});
-    if (newConjr != newConj)
+    if (newConjr == n)
     {
-      lcp->addStep(
-          newConjr, PfRule::MACRO_SR_PRED_TRANSFORM, {newConj}, {newConjr});
+      // don't care about the previous proof and can simply plug in the
+      // proof from pg if the resulting assertion is the same as n.
+      d_pppg->notifyNewAssert(newConjr, pg);
+    }
+    else
+    {
+      // ---------- from pppg   --------- from pg
+      // d_nodes[i]                n
+      // -------------------------------- AND_INTRO
+      //      d_nodes[i] ^ n
+      // -------------------------------- MACRO_SR_PRED_TRANSFORM
+      //   rewrite( d_nodes[i] ^ n )
+      // allocate a fresh proof which will act as the proof generator
+      LazyCDProof* lcp = d_pppg->allocateHelperProof();
+      lcp->addLazyStep(n, pg, false);
+      if (d_nodes[i].isConst() && d_nodes[i].getConst<bool>())
+      {
+        // skip the AND_INTRO if the previous d_nodes[i] was true
+        newConj = n;
+      }
+      else
+      {
+        lcp->addLazyStep(d_nodes[i], d_pppg);
+        lcp->addStep(newConj, PfRule::AND_INTRO, {d_nodes[i], n}, {});
+      }
+      if (newConjr != newConj)
+      {
+        lcp->addStep(
+            newConjr, PfRule::MACRO_SR_PRED_TRANSFORM, {newConj}, {newConjr});
+      }
+      // Notice we have constructed a proof of a new assertion, where d_pppg
+      // is referenced in the lazy proof above. If alternatively we had
+      // constructed a proof of d_nodes[i] = rewrite( d_nodes[i] ^ n ), we would
+      // have used notifyPreprocessed. However, it is simpler to make the
+      // above proof.
+      d_pppg->notifyNewAssert(newConjr, lcp);
     }
-    // Notice we have constructed a proof of a new assertion, where d_pppg
-    // is referenced in the lazy proof above. If alternatively we had
-    // constructed a proof of d_nodes[i] = rewrite( d_nodes[i] ^ n ), we would
-    // have used notifyPreprocessed. However, it is simpler to make the
-    // above proof.
-    d_pppg->notifyNewAssert(newConjr, lcp);
   }
   if (options::unsatCores())
   {

diff --git a/src/preprocessing/assertion_pipeline.h b/src/preprocessing/assertion_pipeline.h
index 5c50903c5bae39b61cd4d8cf549ed753af0545e2..75f3704501f18eafc92314f8f471a0d098dfea9e 100644 (file)
--- a/src/preprocessing/assertion_pipeline.h
+++ b/src/preprocessing/assertion_pipeline.h
@@ -88,7 +88,10 @@ class AssertionPipeline
    * where d_nodes[i] is the assertion at position i prior to this call.
    */
   void replace(size_t i, Node n, ProofGenerator* pg = nullptr);
-  /** Same as above, with TrustNode */
+  /**
+   * Same as above, with TrustNode trn, which is of kind REWRITE and proves
+   * d_nodes[i] = n for some n.
+   */
   void replaceTrusted(size_t i, theory::TrustNode trn);
 
   IteSkolemMap& getIteSkolemMap() { return d_iteSkolemMap; }

diff --git a/src/smt/preprocess_proof_generator.cpp b/src/smt/preprocess_proof_generator.cpp
index 7bd10e0b089dc4621d898a168577663b8b311df9..465e7a471117dc26bb07c0c50a9ddd228ebf061d 100644 (file)
--- a/src/smt/preprocess_proof_generator.cpp
+++ b/src/smt/preprocess_proof_generator.cpp
@@ -16,6 +16,7 @@
 #include "smt/preprocess_proof_generator.h"
 
 #include "expr/proof.h"
+#include "options/smt_options.h"
 #include "theory/rewriter.h"
 
 namespace CVC4 {
@@ -23,20 +24,35 @@ namespace smt {
 
 PreprocessProofGenerator::PreprocessProofGenerator(ProofNodeManager* pnm,
                                                    context::Context* c,
-                                                   std::string name)
+                                                   std::string name,
+                                                   PfRule ra,
+                                                   PfRule rpp)
     : d_pnm(pnm),
       d_src(c ? c : &d_context),
       d_helperProofs(pnm, c ? c : &d_context),
-      d_name(name)
+      d_inputPf(pnm, nullptr),
+      d_name(name),
+      d_ra(ra),
+      d_rpp(rpp)
 {
 }
 
+void PreprocessProofGenerator::notifyInput(Node n)
+{
+  notifyNewAssert(n, &d_inputPf);
+}
+
 void PreprocessProofGenerator::notifyNewAssert(Node n, ProofGenerator* pg)
 {
   Trace("smt-proof-pp-debug")
       << "PreprocessProofGenerator::notifyNewAssert: " << n << std::endl;
   if (d_src.find(n) == d_src.end())
   {
+    // if no proof generator provided for (non-true) assertion
+    if (pg == nullptr && (!n.isConst() || !n.getConst<bool>()))
+    {
+      checkEagerPedantic(d_ra);
+    }
     d_src[n] = theory::TrustNode::mkTrustLemma(n, pg);
   }
   else
@@ -77,6 +93,10 @@ void PreprocessProofGenerator::notifyTrustedPreprocessed(theory::TrustNode tnp)
       << std::endl;
   if (d_src.find(np) == d_src.end())
   {
+    if (tnp.getGenerator() == nullptr)
+    {
+      checkEagerPedantic(d_rpp);
+    }
     d_src[np] = tnp;
   }
   else
@@ -167,9 +187,7 @@ std::shared_ptr<ProofNode> PreprocessProofGenerator::getProofFor(Node f)
         Trace("smt-pppg") << "...add missing step" << std::endl;
         // add trusted step, the rule depends on the kind of trust node
         cdp.addStep(proven,
-                    tnk == theory::TrustNodeKind::LEMMA
-                        ? PfRule::PREPROCESS_LEMMA
-                        : PfRule::PREPROCESS,
+                    tnk == theory::TrustNodeKind::LEMMA ? d_ra : d_rpp,
                     {},
                     {proven});
       }
@@ -214,5 +232,21 @@ LazyCDProof* PreprocessProofGenerator::allocateHelperProof()
 
 std::string PreprocessProofGenerator::identify() const { return d_name; }
 
+void PreprocessProofGenerator::checkEagerPedantic(PfRule r)
+{
+  if (options::proofNewEagerChecking())
+  {
+    // catch a pedantic failure now, which otherwise would not be
+    // triggered since we are doing lazy proof generation
+    ProofChecker* pc = d_pnm->getChecker();
+    std::stringstream serr;
+    if (pc->isPedanticFailure(r, serr))
+    {
+      Unhandled() << "PreprocessProofGenerator::checkEagerPedantic: "
+                  << serr.str();
+    }
+  }
+}
+
 }  // namespace smt
 }  // namespace CVC4

diff --git a/src/smt/preprocess_proof_generator.h b/src/smt/preprocess_proof_generator.h
index e5a9d17f74b2c0d0cbe9302c9da913c99f0fd2a9..a0c090ad73e0d374d4638ceea12d06c114c15b1e 100644 (file)
--- a/src/smt/preprocess_proof_generator.h
+++ b/src/smt/preprocess_proof_generator.h
@@ -58,10 +58,25 @@ class PreprocessProofGenerator : public ProofGenerator
       NodeTrustNodeMap;
 
  public:
+  /**
+   * @param pnm The proof node manager
+   * @param c The context this class depends on
+   * @param name The name of this generator (for debugging)
+   * @param ra The proof rule to use when no generator is provided for new
+   * assertions
+   * @param rpp The proof rule to use when no generator is provided for
+   * preprocessing steps.
+   */
   PreprocessProofGenerator(ProofNodeManager* pnm,
                            context::Context* c = nullptr,
-                           std::string name = "PreprocessProofGenerator");
+                           std::string name = "PreprocessProofGenerator",
+                           PfRule ra = PfRule::PREPROCESS_LEMMA,
+                           PfRule rpp = PfRule::PREPROCESS);
   ~PreprocessProofGenerator() {}
+  /**
+   * Notify that n is an input (its proof is ASSUME).
+   */
+  void notifyInput(Node n);
   /**
    * Notify that n is a new assertion, where pg can provide a proof of n.
    */
@@ -94,6 +109,11 @@ class PreprocessProofGenerator : public ProofGenerator
   LazyCDProof* allocateHelperProof();
 
  private:
+  /**
+   * Possibly check pedantic failure for null proof generator provided
+   * to this class.
+   */
+  void checkEagerPedantic(PfRule r);
   /** The proof node manager */
   ProofNodeManager* d_pnm;
   /** A dummy context used by this class if none is provided */
@@ -108,8 +128,17 @@ class PreprocessProofGenerator : public ProofGenerator
   NodeTrustNodeMap d_src;
   /** A context-dependent list of LazyCDProof, allocated for conjoin steps */
   LazyCDProofSet d_helperProofs;
+  /**
+   * A cd proof for input assertions, this is an empty proof that intentionally
+   * returns (ASSUME f) for all f.
+   */
+  CDProof d_inputPf;
   /** Name for debugging */
   std::string d_name;
+  /** The trust rule for new assertions with no provided proof generator */
+  PfRule d_ra;
+  /** The trust rule for rewrites with no provided proof generator */
+  PfRule d_rpp;
 };
 
 }  // namespace smt