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.

diff --git a/src/smt/preprocess_proof_generator.cpp b/src/smt/preprocess_proof_generator.cpp
index 12a802f14af21eadc72372a3fc85d1c35cbac12b..5511800a13340cba87c34468229145ccf656d3e0 100644 (file)
--- 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});

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 39fa83311dc235494496a1dd097b745347fa2cef..205729553f4437012732fe67474b25ab2fa04481 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -827,6 +827,7 @@ set(regress_0_tests
   regress0/printer/let_shadowing.smt2
   regress0/printer/symbol_starting_w_digit.smt2
   regress0/printer/tuples_and_records.cvc
+  regress0/proofs/cyclic-ucp.smt2
   regress0/proofs/issue277-circuit-propagator.smt2
   regress0/proofs/open-pf-if-unordered-iff.smt2
   regress0/proofs/scope.smt2

diff --git a/test/regress/regress0/proofs/cyclic-ucp.smt2 b/test/regress/regress0/proofs/cyclic-ucp.smt2
new file mode 100644 (file)
index 0000000..1fe29c2
--- /dev/null
+++ b/test/regress/regress0/proofs/cyclic-ucp.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: -i
+; EXPECT: unsat
+; EXPECT: unsat
+(set-logic ALL)
+(push)
+(assert (= "A" ""))
+(check-sat)
+(pop)
+(assert (= "" "A"))
+(check-sat)