Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * The printer for LFSC proofs
11 : : */
12 : :
13 : : #include <functional>
14 : :
15 : : #include "cvc5_private.h"
16 : :
17 : : #ifndef CVC5__PROOF__LFSC__LFSC_PRINTER_H
18 : : #define CVC5__PROOF__LFSC__LFSC_PRINTER_H
19 : :
20 : : #include <iosfwd>
21 : : #include <map>
22 : :
23 : : #include "expr/node.h"
24 : : #include "printer/let_binding.h"
25 : : #include "proof/lfsc/lfsc_node_converter.h"
26 : : #include "proof/lfsc/lfsc_util.h"
27 : : #include "proof/print_expr.h"
28 : : #include "proof/proof_node.h"
29 : : #include "rewriter/rewrite_db.h"
30 : : #include "smt/env_obj.h"
31 : :
32 : : namespace cvc5::internal {
33 : : namespace proof {
34 : :
35 : : class LfscPrintChannel;
36 : :
37 : : /**
38 : : * The LFSC printer, which prints proof nodes in a proof that is checkable
39 : : * by LFSC using the signature, currently located at:
40 : : * https://github.com/CVC4/signatures/tree/master/lfsc/new.
41 : : *
42 : : * It expects to print proof nodes that have been processed by the LFSC
43 : : * proof post processor.
44 : : */
45 : : class LfscPrinter : protected EnvObj
46 : : {
47 : : public:
48 : : LfscPrinter(Env& env, LfscNodeConverter& ltp, rewriter::RewriteDb* rdb);
49 : 1715 : ~LfscPrinter() {}
50 : :
51 : : /**
52 : : * Print the full proof of false by pn on output stream out.
53 : : */
54 : : void print(std::ostream& out, const ProofNode* pn);
55 : :
56 : : /**
57 : : * Print node to stream in the expected format of LFSC.
58 : : */
59 : : void print(std::ostream& out, Node n);
60 : : /**
61 : : * Print type node to stream in the expected format of LFSC.
62 : : */
63 : : void printType(std::ostream& out, TypeNode n);
64 : :
65 : : private:
66 : : /**
67 : : * This ensures that the type definition of type tn has been
68 : : * printed, which ensures that all of its component types, and the
69 : : * user-defined subfields of datatype types among those are declared. This
70 : : * furthermore includes running to a fixed point in the case that tn contains
71 : : * subfield types that are themselves datatypes.
72 : : * Notice that type definitions do not include printing the symbols of the
73 : : * datatype.
74 : : *
75 : : * @param os The stream to print to
76 : : * @param tn The type to ensure the definition(s) are printed for
77 : : * @param processed The types whose definitions we have already printed
78 : : * @param tupleArityProcessed The arity of tuples that we have declared.
79 : : * Note this is only required until we have a more robust treatment of
80 : : * tuples in the LFSC signature
81 : : */
82 : : void ensureTypeDefinitionPrinted(
83 : : std::ostream& os,
84 : : TypeNode tn,
85 : : std::unordered_set<TypeNode>& processed,
86 : : std::unordered_set<size_t>& tupleArityProcessed);
87 : : /**
88 : : * print type definition, which is the same as above, but does not process
89 : : * component types.
90 : : */
91 : : void printTypeDefinition(std::ostream& os,
92 : : TypeNode tn,
93 : : std::unordered_set<TypeNode>& processed,
94 : : std::unordered_set<size_t>& tupleArityProcessed);
95 : : /**
96 : : * Print node to stream in the expected format of LFSC.
97 : : */
98 : : void printLetify(std::ostream& out, Node n);
99 : : /**
100 : : * Print node to stream in the expected format of LFSC, where n has been
101 : : * processed by the LFSC node converter.
102 : : */
103 : : void printInternal(std::ostream& out, Node n);
104 : : /**
105 : : * Print node n to stream in the expected format of LFSC, with let binding,
106 : : * where n has been processed by the LFSC node converter.
107 : : *
108 : : * @param out The output stream
109 : : * @param n The node to print
110 : : * @param lbind The let binding to consider
111 : : * @param letTop Whether we should consider the top-most application in n
112 : : * for the let binding (see LetBinding::convert).
113 : : */
114 : : void printInternal(std::ostream& out,
115 : : Node n,
116 : : LetBinding& lbind,
117 : : bool letTop = true);
118 : : /**
119 : : * print let list, prints definitions of lbind on out in order, and closing
120 : : * parentheses on cparen. If asDefs is true, then the definition is printed
121 : : * as a standalone define statement on out.
122 : : */
123 : : void printLetList(std::ostream& out,
124 : : std::ostream& cparen,
125 : : LetBinding& lbind,
126 : : bool asDefs = false);
127 : :
128 : : //------------------------------ printing proofs
129 : : /**
130 : : * Print proof internal, after term lets and proofs for assumptions have
131 : : * been computed.
132 : : */
133 : : void printProofLetify(LfscPrintChannel* out,
134 : : const ProofNode* pn,
135 : : const LetBinding& lbind,
136 : : const std::vector<const ProofNode*>& pletList,
137 : : std::map<const ProofNode*, size_t>& pletMap,
138 : : std::map<Node, size_t>& passumeMap);
139 : : /**
140 : : * Print proof internal, after all mappings have been computed.
141 : : */
142 : : void printProofInternal(LfscPrintChannel* out,
143 : : const ProofNode* pn,
144 : : const LetBinding& lbind,
145 : : const std::map<const ProofNode*, size_t>& pletMap,
146 : : std::map<Node, size_t>& passumeMap);
147 : : /**
148 : : * Print a plet proof on output channel out, where p is the letified
149 : : * proof and pid is its identifier for the given name prefix.
150 : : * The remaining arguments are used for printing p.
151 : : */
152 : : void printPLet(LfscPrintChannel* out,
153 : : const ProofNode* p,
154 : : size_t pid,
155 : : const std::string& prefix,
156 : : const LetBinding& lbind,
157 : : const std::map<const ProofNode*, size_t>& pletMap,
158 : : std::map<Node, size_t>& passumeMap);
159 : : /**
160 : : * Get the arguments for the proof node application. This adds the arguments
161 : : * of the given proof to the vector pargs.
162 : : *
163 : : * @return false if the proof cannot be printed in LFSC format.
164 : : */
165 : : bool computeProofArgs(const ProofNode* pn, std::vector<PExpr>& pargs);
166 : : /**
167 : : * Compute proof letification for proof node pn.
168 : : */
169 : : void computeProofLetification(const ProofNode* pn,
170 : : std::vector<const ProofNode*>& pletList,
171 : : std::map<const ProofNode*, size_t>& pletMap);
172 : : /** Print DSL rule */
173 : : void printDslRule(std::ostream& out,
174 : : ProofRewriteRule id,
175 : : std::vector<Node>& format);
176 : : //------------------------------ end printing proofs
177 : : /** The term processor */
178 : : LfscNodeConverter& d_tproc;
179 : : /** The proof traversal callback */
180 : : LfscProofLetifyTraverseCallback d_lpltc;
181 : : /** true and false nodes */
182 : : Node d_tt;
183 : : Node d_ff;
184 : : /** Boolean type */
185 : : TypeNode d_boolType;
186 : : /** assumption counter */
187 : : size_t d_assumpCounter;
188 : : /** Counter for plet definitions for children of trust steps */
189 : : size_t d_trustChildPletCounter;
190 : : /** term prefix */
191 : : std::string d_termLetPrefix;
192 : : /** assumption prefix */
193 : : std::string d_assumpPrefix;
194 : : /** proof letified prefix */
195 : : std::string d_pletPrefix;
196 : : /** proof letified trust child prefix */
197 : : std::string d_pletTrustChildPrefix;
198 : : /** for debugging the open rules, the set of ProofRule we have warned about */
199 : : std::unordered_set<ProofRule, std::hash<ProofRule>> d_trustWarned;
200 : : /** Pointer to the rewrite database */
201 : : rewriter::RewriteDb* d_rdb;
202 : : /**
203 : : * Mapping rewrite rules to format for conditions.
204 : : * The output of a DslRule is thus listing the term arguments, then
205 : : * a list of ( holes | child proofs ) based on this list.
206 : : * Each rule is mapped to a list of terms, where Node::null signifies
207 : : * positions of holes, non-null nodes are child proofs to print.
208 : : */
209 : : std::map<ProofRewriteRule, std::vector<Node>> d_dslFormat;
210 : : };
211 : :
212 : : } // namespace proof
213 : : } // namespace cvc5::internal
214 : :
215 : : #endif
|
