From a2d72a1fafccbeaeafec32f85776b03077dbb0fe Mon Sep 17 00:00:00 2001
From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Mon, 22 Feb 2021 16:03:22 -0300
Subject: [PATCH] [proof-new] Optionally print conclusion in the AST proof
 (#5954)

Adds an option to optionally print conclusion in the AST proof.
---
 src/expr/proof_node_to_sexpr.cpp | 8 ++++++++
 src/expr/proof_node_to_sexpr.h   | 2 ++
 src/options/proof_options.toml   | 9 +++++++++
 3 files changed, 19 insertions(+)

diff --git a/src/expr/proof_node_to_sexpr.cpp b/src/expr/proof_node_to_sexpr.cpp
index 2dbb2a873..71c75ceae 100644
--- 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 16a60e252..3e0d42a7d 100644
--- 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 9db541e27..c744b237b 100644
--- 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"
-- 
2.30.2