diff options
author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2021-02-22 16:03:22 -0300 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-02-22 16:03:22 -0300 |
commit | a2d72a1fafccbeaeafec32f85776b03077dbb0fe (patch) | |
tree | bea016dc86d286d498e33c2a3f728ba746681fed /src | |
parent | dea7a1fc8360735f90618f005509306c7c45bd30 (diff) |
[proof-new] Optionally print conclusion in the AST proof (#5954)
Adds an option to optionally print conclusion in the AST proof.
Diffstat (limited to 'src')
-rw-r--r-- | src/expr/proof_node_to_sexpr.cpp | 8 | ||||
-rw-r--r-- | src/expr/proof_node_to_sexpr.h | 2 | ||||
-rw-r--r-- | src/options/proof_options.toml | 9 |
3 files changed, 19 insertions, 0 deletions
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" |