[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.

1 files changed, 16 insertions, 2 deletions

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);