[proof-new] Fixing SMT post-processor's handling of assumptions (#6277)

Previously the SMT post-processor would update any assumption as long as it
had a proof for it. This can be a problem when one as assumption introduced in a
scope that should not be expanded. This commit fixes the issue by adding the
option of configuring a proof node updater to track scopes and the assumptions
they introduce, which can be used to determine the prood nodes which should be
updated. It also changes the SMT post-processor to only update assumptions that
have not been introduced in some scope.

This commit fixes an issue found by @Lachnitt during the integration of CVC4 and Isabelle.

10 files changed, 147 insertions, 36 deletions

diff --git a/src/expr/proof_node_updater.cpp b/src/expr/proof_node_updater.cpp
index 933e5b999..cbd457cd7 100644
--- a/src/expr/proof_node_updater.cpp
+++ b/src/expr/proof_node_updater.cpp
@@ -125,28 +125,21 @@ void ProofNodeUpdater::processInternal(
       }
       traversing.push_back(cur);
       visit.push_back(cur);
-      if (d_mergeSubproofs)
+      // If we are not the top-level proof, we were a scope, or became a scope
+      // after updating, we do a separate recursive call to this method. This
+      // allows us to properly track the assumptions in scope, which is
+      // important for example to merge or to determine updates based on free
+      // assumptions.
+      if (cur->getRule() == PfRule::SCOPE && cur != pf)
       {
-        // If we are not the top-level proof, we were a scope, or became a
-        // scope after updating, we need to make a separate recursive call to
-        // this method. This is not necessary if we are not merging subproofs.
-        if (cur->getRule() == PfRule::SCOPE && cur != pf)
-        {
-          std::vector<Node> nfa;
-          // if we are debugging free assumptions, update the set
-          if (d_debugFreeAssumps)
-          {
-            nfa.insert(nfa.end(), fa.begin(), fa.end());
-            const std::vector<Node>& args = cur->getArguments();
-            nfa.insert(nfa.end(), args.begin(), args.end());
-            Trace("pfnu-debug2")
-                << "Process new scope with " << args << std::endl;
-          }
-          // Process in new call separately, since we should not cache
-          // the results of proofs that have a different scope.
-          processInternal(cur, nfa, traversing);
-          continue;
-        }
+        std::vector<Node> nfa;
+        nfa.insert(nfa.end(), fa.begin(), fa.end());
+        const std::vector<Node>& args = cur->getArguments();
+        nfa.insert(nfa.end(), args.begin(), args.end());
+        Trace("pfnu-debug2") << "Process new scope with " << args << std::endl;
+        // Process in new call separately
+        processInternal(cur, nfa, traversing);
+        continue;
       }
       const std::vector<std::shared_ptr<ProofNode>>& ccp = cur->getChildren();
       // now, process children
@@ -180,7 +173,7 @@ bool ProofNodeUpdater::runUpdate(std::shared_ptr<ProofNode> cur,
                                  bool& continueUpdate)
 {
   // should it be updated?
-  if (!d_cb.shouldUpdate(cur, continueUpdate))
+  if (!d_cb.shouldUpdate(cur, fa, continueUpdate))
   {
     return false;
   }
@@ -196,9 +189,9 @@ bool ProofNodeUpdater::runUpdate(std::shared_ptr<ProofNode> cur,
     // store in the proof
     cpf.addProof(cp);
   }
-  Trace("pf-process-debug")
-      << "Updating (" << cur->getRule() << ")..." << std::endl;
   Node res = cur->getResult();
+  Trace("pf-process-debug")
+      << "Updating (" << cur->getRule() << "): " << res << std::endl;
   // only if the callback updated the node
   if (d_cb.update(res, id, ccn, cur->getArguments(), &cpf, continueUpdate))
   {
diff --git a/src/expr/proof_node_updater.h b/src/expr/proof_node_updater.h
index 8e30f14d2..268fcda5e 100644
--- a/src/expr/proof_node_updater.h
+++ b/src/expr/proof_node_updater.h
@@ -41,10 +41,12 @@ class ProofNodeUpdaterCallback
   /** Should proof pn be updated?
    *
    * @param pn the proof node that maybe should be updated
+   * @param fa the assumptions in scope
    * @param continueUpdate whether we should continue recursively updating pn
    * @return whether we should run the update method on pn
    */
   virtual bool shouldUpdate(std::shared_ptr<ProofNode> pn,
+                            const std::vector<Node>& fa,
                             bool& continueUpdate) = 0;
   /**
    * Update the proof rule application, store steps in cdp. Return true if
diff --git a/src/options/proof_options.toml b/src/options/proof_options.toml
index ff03e70f5..f6a39e0fe 100644
--- a/src/options/proof_options.toml
+++ b/src/options/proof_options.toml
@@ -16,7 +16,10 @@ header = "options/proof_options.h"
 [[option.mode.DOT]]
   name       = "dot"
   help       = "Output DOT proof"
-  
+[[option.mode.VERIT]]
+  name       = "verit"
+  help       = "Output veriT proof"
+
 [[option]]
   name       = "proofPrintConclusion"
   category   = "regular"
diff --git a/src/prop/proof_post_processor.cpp b/src/prop/proof_post_processor.cpp
index 6b31e6053..10bf53aa1 100644
--- a/src/prop/proof_post_processor.cpp
+++ b/src/prop/proof_post_processor.cpp
@@ -29,6 +29,7 @@ ProofPostprocessCallback::ProofPostprocessCallback(
 void ProofPostprocessCallback::initializeUpdate() { d_assumpToProof.clear(); }
 
 bool ProofPostprocessCallback::shouldUpdate(std::shared_ptr<ProofNode> pn,
+                                            const std::vector<Node>& fa,
                                             bool& continueUpdate)
 {
   bool result = pn->getRule() == PfRule::ASSUME
diff --git a/src/prop/proof_post_processor.h b/src/prop/proof_post_processor.h
index 363970117..906faaafd 100644
--- a/src/prop/proof_post_processor.h
+++ b/src/prop/proof_post_processor.h
@@ -54,6 +54,7 @@ class ProofPostprocessCallback : public ProofNodeUpdaterCallback
    * cancelled, i.e., continueUpdate is set to false.
    */
   bool shouldUpdate(std::shared_ptr<ProofNode> pn,
+                    const std::vector<Node>& fa,
                     bool& continueUpdate) override;
   /** Update the proof rule application.
    *
diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp
index b651e390c..846df7e41 100644
--- a/src/smt/proof_manager.cpp
+++ b/src/smt/proof_manager.cpp
@@ -34,7 +34,27 @@ PfManager::PfManager(context::UserContext* u, SmtEngine* smte)
       d_pnm(new ProofNodeManager(d_pchecker.get())),
       d_pppg(new PreprocessProofGenerator(
           d_pnm.get(), u, "smt::PreprocessProofGenerator")),
-      d_pfpp(new ProofPostproccess(d_pnm.get(), smte, d_pppg.get())),
+      d_pfpp(new ProofPostproccess(
+          d_pnm.get(),
+          smte,
+          d_pppg.get(),
+          // by default the post-processor will update all assumptions, which
+          // can lead to SCOPE subproofs of the form
+          //   A
+          //  ...
+          //   B1    B2
+          //  ...   ...
+          // ------------
+          //      C
+          // ------------- SCOPE [B1, B2]
+          // B1 ^ B2 => C
+          //
+          // where A is an available assumption from outside the scope (note
+          // that B1 was an assumption of this SCOPE subproof but since it could
+          // be inferred from A, it was updated). This shape is problematic for
+          // the veriT reconstruction, so we disable the update of scoped
+          // assumptions (which would disable the update of B1 in this case).
+          options::proofFormatMode() != options::ProofFormatMode::VERIT)),
       d_finalProof(nullptr)
 {
   // add rules to eliminate here
@@ -131,7 +151,7 @@ void PfManager::printProof(std::ostream& out,
   }
   // TODO (proj #37) according to the proof format, post process the proof node
   // TODO (proj #37) according to the proof format, print the proof node
-  
+
   if (options::proofFormatMode() == options::ProofFormatMode::DOT)
   {
     proof::DotPrinter::print(out, fp.get());
diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp
index dedb686c3..a27a5697e 100644
--- a/src/smt/proof_post_processor.cpp
+++ b/src/smt/proof_post_processor.cpp
@@ -33,12 +33,15 @@ namespace smt {
 
 ProofPostprocessCallback::ProofPostprocessCallback(ProofNodeManager* pnm,
                                                    SmtEngine* smte,
-                                                   ProofGenerator* pppg)
-    : d_pnm(pnm), d_smte(smte), d_pppg(pppg), d_wfpm(pnm)
+                                                   ProofGenerator* pppg,
+                                                   bool updateScopedAssumptions)
+    : d_pnm(pnm),
+      d_smte(smte),
+      d_pppg(pppg),
+      d_wfpm(pnm),
+      d_updateScopedAssumptions(updateScopedAssumptions)
 {
   d_true = NodeManager::currentNM()->mkConst(true);
-  // always check whether to update ASSUME
-  d_elimRules.insert(PfRule::ASSUME);
 }
 
 void ProofPostprocessCallback::initializeUpdate()
@@ -53,9 +56,26 @@ void ProofPostprocessCallback::setEliminateRule(PfRule rule)
 }
 
 bool ProofPostprocessCallback::shouldUpdate(std::shared_ptr<ProofNode> pn,
+                                            const std::vector<Node>& fa,
                                             bool& continueUpdate)
 {
-  return d_elimRules.find(pn->getRule()) != d_elimRules.end();
+  PfRule id = pn->getRule();
+  if (d_elimRules.find(id) != d_elimRules.end())
+  {
+    return true;
+  }
+  // other than elimination rules, we always update assumptions as long as
+  // d_updateScopedAssumptions is true or they are *not* in scope, i.e., not in
+  // fa
+  if (id != PfRule::ASSUME
+      || (!d_updateScopedAssumptions
+          && std::find(fa.begin(), fa.end(), pn->getResult()) != fa.end()))
+  {
+    Trace("smt-proof-pp-debug")
+        << "... not updating in-scope assumption " << pn->getResult() << "\n";
+    return false;
+  }
+  return true;
 }
 
 bool ProofPostprocessCallback::update(Node res,
@@ -1108,6 +1128,7 @@ void ProofPostprocessFinalCallback::initializeUpdate()
 }
 
 bool ProofPostprocessFinalCallback::shouldUpdate(std::shared_ptr<ProofNode> pn,
+                                                 const std::vector<Node>& fa,
                                                  bool& continueUpdate)
 {
   PfRule r = pn->getRule();
@@ -1146,9 +1167,10 @@ bool ProofPostprocessFinalCallback::wasPedanticFailure(std::ostream& out) const
 
 ProofPostproccess::ProofPostproccess(ProofNodeManager* pnm,
                                      SmtEngine* smte,
-                                     ProofGenerator* pppg)
+                                     ProofGenerator* pppg,
+                                     bool updateScopedAssumptions)
     : d_pnm(pnm),
-      d_cb(pnm, smte, pppg),
+      d_cb(pnm, smte, pppg, updateScopedAssumptions),
       // the update merges subproofs
       d_updater(d_pnm, d_cb, true),
       d_finalCb(pnm),
diff --git a/src/smt/proof_post_processor.h b/src/smt/proof_post_processor.h
index 9f3e7e55b..4111e83de 100644
--- a/src/smt/proof_post_processor.h
+++ b/src/smt/proof_post_processor.h
@@ -40,7 +40,8 @@ class ProofPostprocessCallback : public ProofNodeUpdaterCallback
  public:
   ProofPostprocessCallback(ProofNodeManager* pnm,
                            SmtEngine* smte,
-                           ProofGenerator* pppg);
+                           ProofGenerator* pppg,
+                           bool updateScopedAssumptions);
   ~ProofPostprocessCallback() {}
   /**
    * Initialize, called once for each new ProofNode to process. This initializes
@@ -56,6 +57,7 @@ class ProofPostprocessCallback : public ProofNodeUpdaterCallback
   void setEliminateRule(PfRule rule);
   /** Should proof pn be updated? */
   bool shouldUpdate(std::shared_ptr<ProofNode> pn,
+                    const std::vector<Node>& fa,
                     bool& continueUpdate) override;
   /** Update the proof rule application. */
   bool update(Node res,
@@ -80,6 +82,8 @@ class ProofPostprocessCallback : public ProofNodeUpdaterCallback
   std::vector<Node> d_wfAssumptions;
   /** Kinds of proof rules we are eliminating */
   std::unordered_set<PfRule, PfRuleHashFunction> d_elimRules;
+  /** Whether we post-process assumptions in scope. */
+  bool d_updateScopedAssumptions;
   //---------------------------------reset at the begining of each update
   /** Mapping assumptions to their proof from preprocessing */
   std::map<Node, std::shared_ptr<ProofNode> > d_assumpToProof;
@@ -244,6 +248,7 @@ class ProofPostprocessFinalCallback : public ProofNodeUpdaterCallback
   void initializeUpdate();
   /** Should proof pn be updated? Returns false, adds to stats. */
   bool shouldUpdate(std::shared_ptr<ProofNode> pn,
+                    const std::vector<Node>& fa,
                     bool& continueUpdate) override;
   /** was pedantic failure */
   bool wasPedanticFailure(std::ostream& out) const;
@@ -274,9 +279,18 @@ class ProofPostprocessFinalCallback : public ProofNodeUpdaterCallback
 class ProofPostproccess
 {
  public:
+  /**
+   * @param pnm The proof node manager we are using
+   * @param smte The SMT engine whose proofs are being post-processed
+   * @param pppg The proof generator for pre-processing proofs
+   * @param updateScopedAssumptions Whether we post-process assumptions in
+   * scope. Since doing so is sound and only problematic depending on who is
+   * consuming the proof, it's true by default.
+   */
   ProofPostproccess(ProofNodeManager* pnm,
                     SmtEngine* smte,
-                    ProofGenerator* pppg);
+                    ProofGenerator* pppg,
+                    bool updateScopedAssumptions = true);
   ~ProofPostproccess();
   /** post-process */
   void process(std::shared_ptr<ProofNode> pf);
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 967b027de..f3f31edbf 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -774,6 +774,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/scope.smt2
   regress0/push-pop/boolean/fuzz_12.smt2
   regress0/push-pop/boolean/fuzz_13.smt2
   regress0/push-pop/boolean/fuzz_14.smt2
diff --git a/test/regress/regress0/proofs/scope.smt2 b/test/regress/regress0/proofs/scope.smt2
new file mode 100644
index 000000000..7a324952e
--- /dev/null
+++ b/test/regress/regress0/proofs/scope.smt2
@@ -0,0 +1,54 @@
+; COMMAND-LINE: --produce-proofs
+; EXIT: 0
+; SCRUBBER: grep -v -E '.*'
+(set-logic AUFLIA)
+(declare-sort A$ 0)
+(declare-sort B$ 0)
+(declare-sort C$ 0)
+(declare-sort D$ 0)
+(declare-sort E$ 0)
+(declare-sort F$ 0)
+(declare-sort G$ 0)
+(declare-sort H$ 0)
+(declare-sort I$ 0)
+(declare-sort J$ 0)
+(declare-sort K$ 0)
+(declare-sort L$ 0)
+(declare-sort M$ 0)
+(declare-sort N$ 0)
+(declare-sort O$ 0)
+(declare-sort P$ 0)
+(declare-fun f1$ (M$ J$) L$)
+(declare-fun f2$ (N$ C$) L$)
+(declare-fun f3$ (C$ A$) B$)
+(declare-fun f4$ (D$ E$) B$)
+(declare-fun f5$ (F$ G$) D$)
+(declare-fun f6$ (A$) F$)
+(declare-fun f7$ (A$) G$)
+(declare-fun f8$ (A$) E$)
+(declare-fun f9$ (A$) E$)
+(declare-fun x1$ () M$)
+(declare-fun x2$ () N$)
+(declare-fun x3$ () C$)
+(declare-fun x4$ () C$)
+(declare-fun x5$ () D$)
+(declare-fun x6$ () J$)
+(declare-fun x7$ () J$)
+(declare-fun x8$ () M$)
+(declare-fun x9$ () O$)
+(declare-fun f10$ (H$ A$) K$)
+(declare-fun f3a$ (E$ H$) I$)
+(declare-fun f3b$ (J$ K$) I$)
+(declare-fun f5a$ (O$ P$) N$)
+(declare-fun x10$ () P$)
+(assert (! (forall ((?v0 A$)) (not (= (f3$ x3$ ?v0) (f4$ (f5$ (f6$ ?v0) (f7$ ?v0)) (f8$ ?v0))))) :named a0))
+(assert (! (forall ((?v0 A$)) (not (= (f3$ x4$ ?v0) (f4$ x5$ (f9$ ?v0))))) :named a1))
+(assert (! (forall ((?v0 A$) (?v1 H$)) (not (= (f3a$ (f8$ ?v0) ?v1) (f3b$ x6$ (f10$ ?v1 ?v0))))) :named a2))
+(assert (! (forall ((?v0 A$) (?v1 H$)) (not (= (f3a$ (f9$ ?v0) ?v1) (f3b$ x7$ (f10$ ?v1 ?v0))))) :named a3))
+(assert (! (not (= (f1$ x8$ x6$) (f2$ (f5a$ x9$ x10$) x3$))) :named a4))
+(assert (! (= (f1$ x1$ x7$) (f1$ x8$ x6$)) :named a5))
+(assert (! (= (f1$ x1$ x7$) (f2$ x2$ x4$)) :named a6))
+(assert (! (= (f2$ x2$ x4$) (f2$ (f5a$ x9$ x10$) x3$)) :named a7))
+(assert (! (not false) :named a8))
+(check-sat)
+(get-proof)
\ No newline at end of file