Implement lazy proof checking modes (#7106)

[cvc5.git] / src / proof / proof_node_manager.h

diff --git a/src/proof/proof_node_manager.h b/src/proof/proof_node_manager.h
index 541686a30643da0314932fe98f7ec003a796b9df..928aabb7678de49b156b3b545f27d897aeccb5ab 100644 (file)
--- a/src/proof/proof_node_manager.h
+++ b/src/proof/proof_node_manager.h
@@ -163,6 +163,10 @@ class ProofNodeManager
    * unchanged.
    */
   bool updateNode(ProofNode* pn, ProofNode* pnr);
+  /**
+   * Ensure that pn is checked, regardless of the proof check format.
+   */
+  void ensureChecked(ProofNode* pn);
   /** Get the underlying proof checker */
   ProofChecker* getChecker() const;
   /**
@@ -193,11 +197,15 @@ class ProofNodeManager
    * This throws an assertion error if we fail to check such a proof node, or
    * if expected is provided (non-null) and is different what is proven by the
    * other arguments.
+   *
+   * The flag didCheck is set to true if the underlying proof checker was
+   * invoked. This may be false if e.g. the proof checking mode is lazy.
    */
   Node checkInternal(PfRule id,
                      const std::vector<std::shared_ptr<ProofNode>>& children,
                      const std::vector<Node>& args,
-                     Node expected);
+                     Node expected,
+                     bool& didCheck);
   /**
    * Update node internal, return true if successful. This is called by
    * the update node methods above. The argument needsCheck is whether we