From 89c5d4ac65f45f24a7dc0ab76bb2bdb447bdfcda Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 17 Sep 2020 21:38:42 -0500
Subject: (proof-new) Updates to proof node updater algorithm (#5088)

This updates the proof node updater so that we apply updates to a fixed point, stopping if the proof node is not updated or if the callback explicitly tells us not to continue. This also fixes an issue where proof nodes would be updated to SCOPE and incorrectly traversed after updating.

This additionally adds debugging feature to proof node updater to track the moment at which an unexpected free assumption is introduced by an update.
---
 src/expr/proof_node_updater.h | 37 ++++++++++++++++++++++++++++++++++---
 1 file changed, 34 insertions(+), 3 deletions(-)

(limited to 'src/expr/proof_node_updater.h')

diff --git a/src/expr/proof_node_updater.h b/src/expr/proof_node_updater.h
index 061a12310..d5c0a884f 100644
--- a/src/expr/proof_node_updater.h
+++ b/src/expr/proof_node_updater.h
@@ -41,12 +41,20 @@ class ProofNodeUpdaterCallback
    * Update the proof rule application, store steps in cdp. Return true if
    * the proof changed. It can be assumed that cdp contains proofs of each
    * fact in children.
+   *
+   * If continueUpdate is set to false in this method, then the resulting
+   * proof (the proof of res in cdp) is *not* called back to update by the
+   * proof node updater, nor are its children recursed. Otherwise, by default,
+   * the proof node updater will continue updating the resulting proof and will
+   * recursively update its children. This is analogous to marking REWRITE_DONE
+   * in a rewrite response.
    */
   virtual bool update(Node res,
                       PfRule id,
                       const std::vector<Node>& children,
                       const std::vector<Node>& args,
-                      CDProof* cdp);
+                      CDProof* cdp,
+                      bool& continueUpdate);
 };
 
 /**
@@ -68,17 +76,40 @@ class ProofNodeUpdater
    */
   void process(std::shared_ptr<ProofNode> pf);
 
+  /**
+   * Set free assumptions to freeAssumps. This indicates that we expect
+   * the proof we are processing to have free assumptions that are in
+   * freeAssumps. This enables checking when this is violated, which is
+   * expensive in general. It is not recommended that this method is called
+   * by default.
+   */
+  void setDebugFreeAssumptions(const std::vector<Node>& freeAssumps);
+
  private:
   /** The proof node manager */
   ProofNodeManager* d_pnm;
   /** The callback */
   ProofNodeUpdaterCallback& d_cb;
+  /**
+   * Post-process, which performs the main post-processing technique described
+   * above.
+   */
+  void processInternal(std::shared_ptr<ProofNode> pf,
+                       const std::vector<Node>& fa);
   /**
    * Update proof node cur based on the callback. This modifies curr using
    * ProofNodeManager::updateNode based on the proof node constructed to
-   * replace it by the callback.
+   * replace it by the callback. Return true if cur was updated. If
+   * continueUpdate is updated to false, then cur is not updated further
+   * and its children are not traversed.
    */
-  void runUpdate(ProofNode* cur);
+  bool runUpdate(std::shared_ptr<ProofNode> cur,
+                 const std::vector<Node>& fa,
+                 bool& continueUpdate);
+  /** Are we debugging free assumptions? */
+  bool d_debugFreeAssumps;
+  /** The initial free assumptions */
+  std::vector<Node> d_freeAssumps;
 };
 
 }  // namespace CVC4
-- 
cgit v1.2.3