[proof-new] Optionally print conclusion in the AST proof (#5954)

Adds an option to optionally print conclusion in the AST proof.

diff --git a/src/expr/proof_node_to_sexpr.cpp b/src/expr/proof_node_to_sexpr.cpp
index 2dbb2a873b0bacb833e397872707744d0c61a248..71c75ceaec46e2cae7edc0cda147cf094143742d 100644 (file)
--- a/src/expr/proof_node_to_sexpr.cpp
+++ b/src/expr/proof_node_to_sexpr.cpp
@@ -16,6 +16,8 @@
 
 #include <iostream>
 
+#include "options/proof_options.h"
+
 using namespace CVC4::kind;
 
 namespace CVC4 {
@@ -24,6 +26,7 @@ ProofNodeToSExpr::ProofNodeToSExpr()
 {
   NodeManager* nm = NodeManager::currentNM();
   std::vector<TypeNode> types;
+  d_conclusionMarker = nm->mkBoundVar(":conclusion", nm->mkSExprType(types));
   d_argsMarker = nm->mkBoundVar(":args", nm->mkSExprType(types));
 }
 
@@ -67,6 +70,11 @@ Node ProofNodeToSExpr::convertToSExpr(const ProofNode* pn)
       std::vector<Node> children;
       // add proof rule
       children.push_back(getOrMkPfRuleVariable(cur->getRule()));
+      if (options::proofPrintConclusion())
+      {
+        children.push_back(d_conclusionMarker);
+        children.push_back(cur->getResult());
+      }
       const std::vector<std::shared_ptr<ProofNode>>& pc = cur->getChildren();
       for (const std::shared_ptr<ProofNode>& cp : pc)
       {

diff --git a/src/expr/proof_node_to_sexpr.h b/src/expr/proof_node_to_sexpr.h
index 16a60e2526d9af0ab489f8cad148611d83c146e5..3e0d42a7d62afe0cd236edf992aff4019a278777 100644 (file)
--- a/src/expr/proof_node_to_sexpr.h
+++ b/src/expr/proof_node_to_sexpr.h
@@ -47,6 +47,8 @@ class ProofNodeToSExpr
   std::map<PfRule, Node> d_pfrMap;
   /** Dummy ":args" marker */
   Node d_argsMarker;
+  /** Dummy ":conclusion" marker */
+  Node d_conclusionMarker;
   /** map proof nodes to their s-expression */
   std::map<const ProofNode*, Node> d_pnMap;
   /**

diff --git a/src/options/proof_options.toml b/src/options/proof_options.toml
index 9db541e27237e4ba4d3eaf0480e721def70c2264..c744b237bd725a69b5bceb69b65fb79c8c6d3dec 100644 (file)
--- a/src/options/proof_options.toml
+++ b/src/options/proof_options.toml
@@ -1,3 +1,12 @@
 id     = "PROOF"
 name   = "Proof"
 header = "options/proof_options.h"
+
+[[option]]
+  name       = "proofPrintConclusion"
+  category   = "regular"
+  long       = "proof-print-conclusion"
+  type       = "bool"
+  default    = "false"
+  read_only  = true
+  help       = "Print conclusion of proof steps when printing AST"