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/expr/proof_node_to_sexpr.h | |
| 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/expr/proof_node_to_sexpr.h')
| -rw-r--r-- | src/expr/proof_node_to_sexpr.h | 2 |
1 files changed, 2 insertions, 0 deletions
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; /** |