From: Lachnitt <lachnitt@stanford.edu>
Date: Wed, 15 Sep 2021 18:19:53 +0000 (-0700)
Subject: [proofs] Alethe: Added Callback Function to alethe_proof_processor (#7186)
X-Git-Tag: cvc5-1.0.0~1205
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c6e663987150cab74d0e75393eef36595f9764b9;p=cvc5.git

[proofs] Alethe: Added Callback Function to alethe_proof_processor (#7186)

Added alethe_proof_processor header file and introduced callback class.

Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
---

diff --git a/src/proof/alethe/alethe_post_processor.h b/src/proof/alethe/alethe_post_processor.h
new file mode 100644
index 000000000..6b5ab04d7
--- /dev/null
+++ b/src/proof/alethe/alethe_post_processor.h
@@ -0,0 +1,106 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Hanna Lachnitt, Haniel Barbosa
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * The module for processing proof nodes into Alethe proof nodes
+ */
+
+#ifndef CVC4__PROOF__ALETHE_PROOF_PROCESSOR_H
+#define CVC4__PROOF__ALETHE_PROOF_PROCESSOR_H
+
+#include "proof/alethe/alethe_proof_rule.h"
+#include "proof/proof_node_updater.h"
+
+namespace cvc5 {
+
+namespace proof {
+
+/**
+ * A callback class used by the Alethe converter for post-processing proof nodes
+ * by replacing internal rules by the rules in the Alethe calculus.
+ */
+class AletheProofPostprocessCallback : public ProofNodeUpdaterCallback
+{
+ public:
+  AletheProofPostprocessCallback(ProofNodeManager* pnm);
+  ~AletheProofPostprocessCallback() {}
+  /** Should proof pn be updated? Only if its top-level proof rule is not an
+   *  Alethe proof rule.
+   */
+  bool shouldUpdate(std::shared_ptr<ProofNode> pn,
+                    const std::vector<Node>& fa,
+                    bool& continueUpdate) override;
+  /**
+   * This method updates the proof rule application depending on the given
+   * rule and translating it into a proof node in terms of the Alethe rules.
+   */
+  bool update(Node res,
+              PfRule id,
+              const std::vector<Node>& children,
+              const std::vector<Node>& args,
+              CDProof* cdp,
+              bool& continueUpdate) override;
+
+ private:
+  /** The proof node manager */
+  ProofNodeManager* d_pnm;
+  /** The cl operator
+   * For every step the conclusion is a clause. But since the or operator
+   *requires at least two arguments it is extended by the cl operator. In case
+   *of more than one argument it corresponds to or otherwise it is the identity.
+   **/
+  Node d_cl;
+  /**
+   * This method adds a new ALETHE_RULE step to the proof, with `rule` as the
+   * first argument, the original conclusion `res` as the second and
+   * `conclusion`, the result to be printed (which may or may not differ from
+   * `res`), as the third.
+   *
+   * @param rule The id of the Alethe rule,
+   * @param res The expected result of the application,
+   * @param conclusion The conclusion to be printed for the step
+   * @param children The children of the application,
+   * @param args The arguments of the application
+   * @param cdp The proof to add to
+   * @return True if the step could be added, or false if not.
+   */
+  bool addAletheStep(AletheRule rule,
+                     Node res,
+                     Node conclusion,
+                     const std::vector<Node>& children,
+                     const std::vector<Node>& args,
+                     CDProof& cdp);
+  /**
+   * As above, but for proof nodes with original conclusions of the form `(or F1
+   * ... Fn)` whose conclusion-to-be-printed must be `(cl F1 ... Fn)`.
+   *
+   * This method internally calls addAletheStep. The kind of the given Node has
+   * to be OR.
+   *
+   * @param res The expected result of the application in form (or F1 ... Fn),
+   * @param rule The id of the Alethe rule,
+   * @param children The children of the application,
+   * @param args The arguments of the application
+   * @param cdp The proof to add to
+   * @return True if the step could be added, or false if not.
+   */
+  bool addAletheStepFromOr(Node res,
+                           AletheRule rule,
+                           const std::vector<Node>& children,
+                           const std::vector<Node>& args,
+                           CDProof& cdp);
+};
+
+}  // namespace proof
+
+}  // namespace cvc5
+
+#endif