[proofs] Alethe: Implementation of AletheProofPostprocessCallback (#7212)

Implementation of addAletheStep and addAletheStepFromOr. Added stub for AletheProofPostprocessCallback update function that will be populated by subsequent PRs.

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

diff --git a/src/proof/alethe/alethe_post_processor.cpp b/src/proof/alethe/alethe_post_processor.cpp
new file mode 100644 (file)
index 0000000..738497e
--- /dev/null
+++ b/src/proof/alethe/alethe_post_processor.cpp
@@ -0,0 +1,111 @@
+/******************************************************************************
+ * 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
+ */
+
+#include "proof/alethe/alethe_post_processor.h"
+
+#include "expr/node_algorithm.h"
+#include "proof/proof.h"
+#include "proof/proof_checker.h"
+#include "util/rational.h"
+
+namespace cvc5 {
+
+namespace proof {
+
+AletheProofPostprocessCallback::AletheProofPostprocessCallback(
+    ProofNodeManager* pnm, AletheNodeConverter& anc)
+    : d_pnm(pnm), d_anc(anc)
+{
+  NodeManager* nm = NodeManager::currentNM();
+  d_cl = nm->mkBoundVar("cl", nm->sExprType());
+}
+
+bool AletheProofPostprocessCallback::shouldUpdate(std::shared_ptr<ProofNode> pn,
+                                                  const std::vector<Node>& fa,
+                                                  bool& continueUpdate)
+{
+  return pn->getRule() != PfRule::ALETHE_RULE;
+}
+
+bool AletheProofPostprocessCallback::update(Node res,
+                                            PfRule id,
+                                            const std::vector<Node>& children,
+                                            const std::vector<Node>& args,
+                                            CDProof* cdp,
+                                            bool& continueUpdate)
+{
+  Trace("alethe-proof") << "- Alethe post process callback " << res << " " << id
+                        << " " << children << " / " << args << std::endl;
+
+  NodeManager* nm = NodeManager::currentNM();
+  std::vector<Node> new_args = std::vector<Node>();
+
+  switch (id)
+  {
+    default:
+    {
+      return addAletheStep(AletheRule::UNDEFINED,
+                           res,
+                           nm->mkNode(kind::SEXPR, d_cl, res),
+                           children,
+                           args,
+                           *cdp);
+    }
+  }
+}
+
+bool AletheProofPostprocessCallback::addAletheStep(
+    AletheRule rule,
+    Node res,
+    Node conclusion,
+    const std::vector<Node>& children,
+    const std::vector<Node>& args,
+    CDProof& cdp)
+{
+  // delete attributes
+  Node sanitized_conclusion = conclusion;
+  if (expr::hasClosure(conclusion))
+  {
+    sanitized_conclusion = d_anc.convert(conclusion);
+  }
+
+  std::vector<Node> new_args = std::vector<Node>();
+  new_args.push_back(
+      NodeManager::currentNM()->mkConst<Rational>(static_cast<unsigned>(rule)));
+  new_args.push_back(res);
+  new_args.push_back(sanitized_conclusion);
+  new_args.insert(new_args.end(), args.begin(), args.end());
+  Trace("alethe-proof") << "... add Alethe step " << res << " / " << conclusion
+                        << " " << rule << " " << children << " / " << new_args
+                        << std::endl;
+  return cdp.addStep(res, PfRule::ALETHE_RULE, children, new_args);
+}
+
+bool AletheProofPostprocessCallback::addAletheStepFromOr(
+    Node res,
+    AletheRule rule,
+    const std::vector<Node>& children,
+    const std::vector<Node>& args,
+    CDProof& cdp)
+{
+  std::vector<Node> subterms = {d_cl};
+  subterms.insert(subterms.end(), res.begin(), res.end());
+  Node conclusion = NodeManager::currentNM()->mkNode(kind::SEXPR, subterms);
+  return addAletheStep(rule, res, conclusion, children, args, cdp);
+}
+
+}  // namespace proof
+
+}  // namespace cvc5

diff --git a/src/proof/alethe/alethe_post_processor.h b/src/proof/alethe/alethe_post_processor.h
index a19903f12e9c14c77bee4a3b731d166a401b9bc5..d8fae8a5543de68a5a7534ce5d5ff8c05ab26d15 100644 (file)
--- a/src/proof/alethe/alethe_post_processor.h
+++ b/src/proof/alethe/alethe_post_processor.h
@@ -16,8 +16,9 @@
 #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"
+#include "proof/alethe/alethe_node_converter.h"
+#include "proof/alethe/alethe_proof_rule.h"
 
 namespace cvc5 {
 
@@ -30,7 +31,8 @@ namespace proof {
 class AletheProofPostprocessCallback : public ProofNodeUpdaterCallback
 {
  public:
-  AletheProofPostprocessCallback(ProofNodeManager* pnm);
+  AletheProofPostprocessCallback(ProofNodeManager* pnm,
+                                 AletheNodeConverter& anc);
   ~AletheProofPostprocessCallback() {}
   /** Should proof pn be updated? Only if its top-level proof rule is not an
    *  Alethe proof rule.
@@ -52,6 +54,8 @@ class AletheProofPostprocessCallback : public ProofNodeUpdaterCallback
  private:
   /** The proof node manager */
   ProofNodeManager* d_pnm;
+  /** The Alethe node converter */
+  AletheNodeConverter& d_anc;
   /** 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
@@ -114,7 +118,8 @@ class AletheProofPostprocessCallback : public ProofNodeUpdaterCallback
 class AletheProofPostprocessFinalCallback : public ProofNodeUpdaterCallback
 {
  public:
-  AletheProofPostprocessFinalCallback(ProofNodeManager* pnm);
+   AletheProofPostprocessFinalCallback(ProofNodeManager* pnm,
+                                       AletheNodeConverter& anc);
   ~AletheProofPostprocessFinalCallback() {}
   /** Should proof pn be updated? It should, if the last step is printed as (cl
    * false) or if it is an assumption (in that case it is printed as false).
@@ -139,6 +144,8 @@ class AletheProofPostprocessFinalCallback : public ProofNodeUpdaterCallback
  private:
   /** The proof node manager */
   ProofNodeManager* d_pnm;
+  /** The Alethe node converter */
+  AletheNodeConverter& d_anc;
   /** The cl operator is defined as described in the
    * AletheProofPostprocessCallback class above
    **/
@@ -152,7 +159,7 @@ class AletheProofPostprocessFinalCallback : public ProofNodeUpdaterCallback
 class AletheProofPostprocess
 {
  public:
-  AletheProofPostprocess(ProofNodeManager* pnm);
+   AletheProofPostprocess(ProofNodeManager* pnm, AletheNodeConverter& anc);
   ~AletheProofPostprocess();
   /** post-process */
   void process(std::shared_ptr<ProofNode> pf);