From 54eac4f9781d9c07446453697128c4bd036c110d Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 14 Jul 2021 16:15:28 -0500
Subject: Fix for context on input proof generator (#6873)

The preprocess proof generator uses a dummy CDProof to mark input assertions that do not need justification. This CDProof should be user-context dependent to avoid rare cases where an input assertion was the symmetric equality of another, it was previously context independent.

This also refactors the debugging traces in this class.
---
 src/smt/preprocess_proof_generator.cpp | 37 +++++++++++++++++++++++-----------
 1 file changed, 25 insertions(+), 12 deletions(-)

(limited to 'src')

diff --git a/src/smt/preprocess_proof_generator.cpp b/src/smt/preprocess_proof_generator.cpp
index 12a802f14..5511800a1 100644
--- a/src/smt/preprocess_proof_generator.cpp
+++ b/src/smt/preprocess_proof_generator.cpp
@@ -36,7 +36,7 @@ PreprocessProofGenerator::PreprocessProofGenerator(ProofNodeManager* pnm,
       d_ctx(c ? c : &d_context),
       d_src(d_ctx),
       d_helperProofs(pnm, d_ctx),
-      d_inputPf(pnm, nullptr),
+      d_inputPf(pnm, c, "InputProof"),
       d_name(name),
       d_ra(ra),
       d_rpp(rpp)
@@ -50,12 +50,18 @@ void PreprocessProofGenerator::notifyInput(Node n)
 
 void PreprocessProofGenerator::notifyNewAssert(Node n, ProofGenerator* pg)
 {
+  if (n.isConst() && n.getConst<bool>())
+  {
+    // ignore true assertions
+    return;
+  }
   Trace("smt-proof-pp-debug")
-      << "PreprocessProofGenerator::notifyNewAssert: " << n << std::endl;
+      << "PreprocessProofGenerator::notifyNewAssert: " << identify() << " " << n
+      << " from " << (pg == nullptr ? "null" : pg->identify()) << 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>()))
+    if (pg == nullptr)
     {
       checkEagerPedantic(d_ra);
     }
@@ -95,8 +101,7 @@ void PreprocessProofGenerator::notifyTrustedPreprocessed(TrustNode tnp)
   Assert(tnp.getKind() == TrustNodeKind::REWRITE);
   Node np = tnp.getNode();
   Trace("smt-proof-pp-debug")
-      << "PreprocessProofGenerator::notifyPreprocessed: " << tnp.getProven()
-      << std::endl;
+      << "PreprocessProofGenerator::notifyPreprocessed: " << tnp << std::endl;
   if (d_src.find(np) == d_src.end())
   {
     if (tnp.getGenerator() == nullptr)
@@ -113,17 +118,19 @@ void PreprocessProofGenerator::notifyTrustedPreprocessed(TrustNode tnp)
 
 std::shared_ptr<ProofNode> PreprocessProofGenerator::getProofFor(Node f)
 {
+  Trace("smt-pppg") << "PreprocessProofGenerator::getProofFor: (" << d_name
+                    << ") input " << f << std::endl;
   NodeTrustNodeMap::iterator it = d_src.find(f);
   if (it == d_src.end())
   {
+    Trace("smt-pppg") << "...no proof for " << identify() << " " << f
+                      << std::endl;
     // could be an assumption, return nullptr
     return nullptr;
   }
   // make CDProof to construct the proof below
   CDProof cdp(d_pnm);
 
-  Trace("smt-pppg") << "PreprocessProofGenerator::getProofFor: (" << d_name
-                    << ") input " << f << std::endl;
   Node curr = f;
   std::vector<Node> transChildren;
   std::unordered_set<Node> processed;
@@ -150,27 +157,30 @@ std::shared_ptr<ProofNode> PreprocessProofGenerator::getProofFor(Node f)
       bool proofStepProcessed = false;
 
       // if a generator for the step was provided, it is stored in the proof
-      Trace("smt-pppg") << "...get provided proof" << std::endl;
+      Trace("smt-pppg-debug")
+          << "...get provided proof " << (*it).second << std::endl;
       std::shared_ptr<ProofNode> pfr = (*it).second.toProofNode();
       if (pfr != nullptr)
       {
-        Trace("smt-pppg") << "...add provided" << std::endl;
+        Trace("smt-pppg-debug") << "...add provided " << *pfr << std::endl;
         Assert(pfr->getResult() == proven);
         cdp.addProof(pfr);
         proofStepProcessed = true;
       }
 
-      Trace("smt-pppg") << "...update" << std::endl;
+      Trace("smt-pppg-debug") << "...update" << std::endl;
       TrustNodeKind tnk = (*it).second.getKind();
       if (tnk == TrustNodeKind::REWRITE)
       {
-        Trace("smt-pppg") << "...rewritten from " << proven[0] << std::endl;
+        Trace("smt-pppg-debug")
+            << "...rewritten from " << proven[0] << std::endl;
         Assert(proven.getKind() == kind::EQUAL);
         if (!proofStepProcessed)
         {
           // maybe its just a simple rewrite?
           if (proven[1] == theory::Rewriter::rewrite(proven[0]))
           {
+            Trace("smt-pppg-debug") << "...add simple rewrite" << std::endl;
             cdp.addStep(proven, PfRule::REWRITE, {}, {proven[0]});
             proofStepProcessed = true;
           }
@@ -180,6 +190,7 @@ std::shared_ptr<ProofNode> PreprocessProofGenerator::getProofFor(Node f)
         curr = proven[0];
         success = true;
         // find the next node
+        Trace("smt-pppg") << "...continue " << curr << std::endl;
         it = d_src.find(curr);
       }
       else
@@ -190,7 +201,9 @@ std::shared_ptr<ProofNode> PreprocessProofGenerator::getProofFor(Node f)
 
       if (!proofStepProcessed)
       {
-        Trace("smt-pppg") << "...add missing step" << std::endl;
+        Trace("smt-pppg-debug")
+            << "...justify missing step with "
+            << (tnk == TrustNodeKind::LEMMA ? d_ra : d_rpp) << std::endl;
         // add trusted step, the rule depends on the kind of trust node
         cdp.addStep(
             proven, tnk == TrustNodeKind::LEMMA ? d_ra : d_rpp, {}, {proven});
-- 
cgit v1.2.3