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 pretty-printer interface for the SMT2 output language.
11 : : */
12 : :
13 : : #include "cvc5_private.h"
14 : :
15 : : #ifndef CVC5__PRINTER__SMT2_PRINTER_H
16 : : #define CVC5__PRINTER__SMT2_PRINTER_H
17 : :
18 : : #include <cvc5/cvc5_skolem_id.h>
19 : :
20 : : #include "printer/printer.h"
21 : :
22 : : namespace cvc5::internal {
23 : :
24 : : class LetBinding;
25 : : class DType;
26 : :
27 : : namespace printer {
28 : : namespace smt2 {
29 : :
30 : : enum class Variant
31 : : {
32 : : no_variant,
33 : : // A variant used for printing commands in the preamble of Eunoia proofs.
34 : : // This is used by the Eunoia printer.
35 : : eo_variant
36 : : };
37 : :
38 : : class Smt2Printer : public cvc5::internal::Printer
39 : : {
40 : : public:
41 : 22310 : Smt2Printer(Variant variant = Variant::no_variant) : d_variant(variant) {}
42 : : using cvc5::internal::Printer::toStream;
43 : : void toStream(std::ostream& out, TNode n) const override;
44 : : void toStream(std::ostream& out, TNode n, int toDepth, size_t dag) const;
45 : : void toStream(std::ostream& out,
46 : : TNode n,
47 : : const LetBinding* lbind,
48 : : bool lbindTop) const override;
49 : : void toStream(std::ostream& out, Kind k) const override;
50 : : void toStream(std::ostream& out, const smt::Model& m) const override;
51 : : /**
52 : : * Writes the unsat core to the stream out.
53 : : * We use the expression names that are associated with the core
54 : : * (UnsatCore::getCoreNames) for printing named assertions.
55 : : */
56 : : void toStream(std::ostream& out, const UnsatCore& core) const override;
57 : :
58 : : void toStreamCmdSuccess(std::ostream& out) const override;
59 : : void toStreamCmdInterrupted(std::ostream& out) const override;
60 : : void toStreamCmdUnsupported(std::ostream& out) const override;
61 : : void toStreamCmdFailure(std::ostream& out,
62 : : const std::string& message) const override;
63 : : void toStreamCmdRecoverableFailure(std::ostream& out,
64 : : const std::string& message) const override;
65 : :
66 : : /** Print empty command */
67 : : void toStreamCmdEmpty(std::ostream& out,
68 : : const std::string& name) const override;
69 : :
70 : : /** Print echo command */
71 : : void toStreamCmdEcho(std::ostream& out,
72 : : const std::string& output) const override;
73 : :
74 : : /** Print assert command */
75 : : void toStreamCmdAssert(std::ostream& out, Node n) const override;
76 : :
77 : : /** Print push command */
78 : : void toStreamCmdPush(std::ostream& out, uint32_t nscopes) const override;
79 : :
80 : : /** Print pop command */
81 : : void toStreamCmdPop(std::ostream& out, uint32_t nscopes) const override;
82 : :
83 : : /** Print declare-fun command */
84 : : void toStreamCmdDeclareFunction(std::ostream& out,
85 : : const std::string& id,
86 : : const std::vector<TypeNode>& argTypes,
87 : : TypeNode type) const override;
88 : :
89 : : /** Print declare-oracle-fun command */
90 : : void toStreamCmdDeclareOracleFun(std::ostream& out,
91 : : const std::string& id,
92 : : const std::vector<TypeNode>& argTypes,
93 : : TypeNode type,
94 : : const std::string& binName) const override;
95 : :
96 : : /** Print declare-pool command */
97 : : void toStreamCmdDeclarePool(
98 : : std::ostream& out,
99 : : const std::string& id,
100 : : TypeNode type,
101 : : const std::vector<Node>& initValue) const override;
102 : :
103 : : /** Print declare-sort command */
104 : : void toStreamCmdDeclareType(std::ostream& out,
105 : : const std::string& id,
106 : : size_t arity) const override;
107 : :
108 : : /** Print define-sort command */
109 : : void toStreamCmdDefineType(std::ostream& out,
110 : : const std::string& id,
111 : : const std::vector<TypeNode>& params,
112 : : TypeNode t) const override;
113 : :
114 : : /** Print define-fun command */
115 : : void toStreamCmdDefineFunction(std::ostream& out,
116 : : const std::string& id,
117 : : const std::vector<Node>& formals,
118 : : TypeNode range,
119 : : Node formula) const override;
120 : :
121 : : /** Print define-fun-rec command */
122 : : void toStreamCmdDefineFunctionRec(
123 : : std::ostream& out,
124 : : const std::vector<Node>& funcs,
125 : : const std::vector<std::vector<Node>>& formals,
126 : : const std::vector<Node>& formulas) const override;
127 : :
128 : : /** Print check-sat command */
129 : : void toStreamCmdCheckSat(std::ostream& out) const override;
130 : :
131 : : /** Print check-sat-assuming command */
132 : : void toStreamCmdCheckSatAssuming(
133 : : std::ostream& out, const std::vector<Node>& nodes) const override;
134 : :
135 : : /** Print query command */
136 : : void toStreamCmdQuery(std::ostream& out, Node n) const override;
137 : :
138 : : /** Print declare-var command */
139 : : void toStreamCmdDeclareVar(std::ostream& out,
140 : : const std::string& id,
141 : : TypeNode type) const override;
142 : :
143 : : /** Print synth-fun command */
144 : : void toStreamCmdSynthFun(std::ostream& out,
145 : : const std::string& id,
146 : : const std::vector<Node>& vars,
147 : : TypeNode rangeType,
148 : : TypeNode sygusType) const override;
149 : :
150 : : /** Print constraint command */
151 : : void toStreamCmdConstraint(std::ostream& out, Node n) const override;
152 : :
153 : : /** Print assume command */
154 : : void toStreamCmdAssume(std::ostream& out, Node n) const override;
155 : :
156 : : /** Print inv-constraint command */
157 : : void toStreamCmdInvConstraint(std::ostream& out,
158 : : Node inv,
159 : : Node pre,
160 : : Node trans,
161 : : Node post) const override;
162 : :
163 : : /** Print check-synth command */
164 : : void toStreamCmdCheckSynth(std::ostream& out) const override;
165 : :
166 : : /** Print check-synth-next command */
167 : : void toStreamCmdCheckSynthNext(std::ostream& out) const override;
168 : :
169 : : /** Print find-synth command */
170 : : void toStreamCmdFindSynth(std::ostream& out,
171 : : modes::FindSynthTarget fst,
172 : : TypeNode sygusType) const override;
173 : :
174 : : /** Print find-synth-next command */
175 : : void toStreamCmdFindSynthNext(std::ostream& out) const override;
176 : :
177 : : /** Print simplify command */
178 : : void toStreamCmdSimplify(std::ostream& out, Node nodes) const override;
179 : :
180 : : /** Print get-value command */
181 : : void toStreamCmdGetValue(std::ostream& out,
182 : : const std::vector<Node>& n) const override;
183 : :
184 : : /** Print get-model-domain-elements command */
185 : : void toStreamCmdGetModelDomainElements(std::ostream& out,
186 : : TypeNode type) const override;
187 : :
188 : : /** Print get-assignment command */
189 : : void toStreamCmdGetAssignment(std::ostream& out) const override;
190 : :
191 : : /** Print get-model command */
192 : : void toStreamCmdGetModel(std::ostream& out) const override;
193 : :
194 : : /** Print block-model command */
195 : : void toStreamCmdBlockModel(std::ostream& out,
196 : : modes::BlockModelsMode mode) const override;
197 : :
198 : : /** Print block-model-values command */
199 : : void toStreamCmdBlockModelValues(
200 : : std::ostream& out, const std::vector<Node>& nodes) const override;
201 : :
202 : : /** Print get-proof command */
203 : : void toStreamCmdGetProof(std::ostream& out,
204 : : modes::ProofComponent c) const override;
205 : :
206 : : /** Print get-interpolant command */
207 : : void toStreamCmdGetInterpol(std::ostream& out,
208 : : const std::string& name,
209 : : Node conj,
210 : : TypeNode sygusType) const override;
211 : :
212 : : /** Print get-interpolant-next command */
213 : : void toStreamCmdGetInterpolNext(std::ostream& out) const override;
214 : :
215 : : /** Print get-abduct command */
216 : : void toStreamCmdGetAbduct(std::ostream& out,
217 : : const std::string& name,
218 : : Node conj,
219 : : TypeNode sygusType) const override;
220 : :
221 : : /** Print get-abduct-next command */
222 : : void toStreamCmdGetAbductNext(std::ostream& out) const override;
223 : :
224 : : /** Print get-quantifier-elimination command */
225 : : void toStreamCmdGetQuantifierElimination(std::ostream& out,
226 : : Node n,
227 : : bool doFull) const override;
228 : :
229 : : /** Print get-unsat-assumptions command */
230 : : void toStreamCmdGetUnsatAssumptions(std::ostream& out) const override;
231 : :
232 : : /** Print get-unsat-core command */
233 : : void toStreamCmdGetUnsatCore(std::ostream& out) const override;
234 : :
235 : : /** Print get-difficulty command */
236 : : void toStreamCmdGetDifficulty(std::ostream& out) const override;
237 : :
238 : : /** Print get-timeout-core command */
239 : : void toStreamCmdGetTimeoutCore(std::ostream& out) const override;
240 : :
241 : : /** Print get-timeout-core-assuming command */
242 : : void toStreamCmdGetTimeoutCoreAssuming(
243 : : std::ostream& out, const std::vector<Node>& assumptions) const override;
244 : :
245 : : /** Print get-learned-literals command */
246 : : void toStreamCmdGetLearnedLiterals(std::ostream& out,
247 : : modes::LearnedLitType t) const override;
248 : :
249 : : /** Print get-assertions command */
250 : : void toStreamCmdGetAssertions(std::ostream& out) const override;
251 : :
252 : : /** Print set-logic command */
253 : : void toStreamCmdSetBenchmarkLogic(std::ostream& out,
254 : : const std::string& logic) const override;
255 : :
256 : : /** Print set-info command */
257 : : void toStreamCmdSetInfo(std::ostream& out,
258 : : const std::string& flag,
259 : : const std::string& value) const override;
260 : :
261 : : /** Print get-info command */
262 : : void toStreamCmdGetInfo(std::ostream& out,
263 : : const std::string& flag) const override;
264 : :
265 : : /** Print set-option command */
266 : : void toStreamCmdSetOption(std::ostream& out,
267 : : const std::string& flag,
268 : : const std::string& value) const override;
269 : :
270 : : /** Print get-option command */
271 : : void toStreamCmdGetOption(std::ostream& out,
272 : : const std::string& flag) const override;
273 : :
274 : : /** Print declare-datatype(s) command */
275 : : void toStreamCmdDatatypeDeclaration(
276 : : std::ostream& out, const std::vector<TypeNode>& datatypes) const override;
277 : :
278 : : /** Print reset command */
279 : : void toStreamCmdReset(std::ostream& out) const override;
280 : :
281 : : /** Print reset-assertions command */
282 : : void toStreamCmdResetAssertions(std::ostream& out) const override;
283 : :
284 : : /** Print quit command */
285 : : void toStreamCmdQuit(std::ostream& out) const override;
286 : :
287 : : /** Print declare-heap command */
288 : : void toStreamCmdDeclareHeap(std::ostream& out,
289 : : TypeNode locType,
290 : : TypeNode dataType) const override;
291 : :
292 : : /** Print skolems.
293 : : * @param out The stream to print to
294 : : * @param cacheVal The cache value of the skolem
295 : : * @param id The skolem id
296 : : * @param isApplied Whether the skolem is applied as an APPLY_UF
297 : : */
298 : : void toStreamSkolem(std::ostream& out,
299 : : Node cacheVal,
300 : : SkolemId id,
301 : : bool isApplied,
302 : : int toDepth,
303 : : const LetBinding* lbind) const;
304 : :
305 : : /**
306 : : * Get the string for a kind k, which returns how the kind k is printed in
307 : : * the SMT-LIB format.
308 : : */
309 : : static std::string smtKindString(Kind k);
310 : : /**
311 : : * Same as above, but also takes into account the type of the node, which
312 : : * makes a difference for printing sequences.
313 : : */
314 : : static std::string smtKindStringOf(const Node& n);
315 : : /**
316 : : * Get the string corresponding to the sygus datatype t printed as a grammar.
317 : : */
318 : : static std::string sygusGrammarString(const TypeNode& t);
319 : :
320 : : private:
321 : : /**
322 : : * Base print method.
323 : : *
324 : : * This prints n when n is atomic (metakind::CONSTANT or metakind::VARIABLE),
325 : : * or when we require a special method for printing n (i.e. for match terms
326 : : * or quantifiers).
327 : : *
328 : : * Otherwise, print the operator of n, followed by a space.
329 : : *
330 : : * Returns false if we need to print the children of n.
331 : : */
332 : : bool toStreamBase(std::ostream& out,
333 : : TNode n,
334 : : const LetBinding* lbind,
335 : : int toDepth) const;
336 : : /**
337 : : * The main printing method for nodes n.
338 : : */
339 : : void toStream(std::ostream& out,
340 : : TNode n,
341 : : const LetBinding* lbind,
342 : : int toDepth,
343 : : bool lbindTop = true) const;
344 : : /**
345 : : * Prints the vector as a sorted variable list
346 : : */
347 : : void toStreamSortedVarList(std::ostream& out,
348 : : const std::vector<Node>& vars) const;
349 : : /**
350 : : * Prints a type as part of e.g. a declare-fun command. This prints either
351 : : * `() T` if the type T is not a function, or `(T1 ... Tn) Tr` if T is
352 : : * a function type with argument types T1 ... Tn and return Tr.
353 : : */
354 : : void toStreamDeclareType(std::ostream& out,
355 : : const std::vector<TypeNode>& argTypes,
356 : : TypeNode tn) const;
357 : : /** To stream type node, which ensures tn is printed in smt2 format */
358 : : void toStreamType(std::ostream& out, TypeNode tn) const;
359 : : /** To stream datatype */
360 : : void toStream(std::ostream& out, const DType& dt) const;
361 : : /**
362 : : * To stream model sort. This prints the appropriate output for type
363 : : * tn declared via declare-sort or declare-datatype.
364 : : */
365 : : void toStreamModelSort(std::ostream& out,
366 : : TypeNode tn,
367 : : const std::vector<Node>& elements) const override;
368 : :
369 : : /**
370 : : * To stream model term. This prints the appropriate output for term
371 : : * n declared via declare-fun.
372 : : */
373 : : void toStreamModelTerm(std::ostream& out,
374 : : const Node& n,
375 : : const Node& value) const override;
376 : :
377 : : /**
378 : : * To stream with let binding. This prints n, possibly in the scope
379 : : * of letification generated by this method based on lbind.
380 : : */
381 : : void toStreamWithLetify(std::ostream& out,
382 : : Node n,
383 : : int toDepth,
384 : : LetBinding* lbind) const;
385 : : Variant d_variant;
386 : : }; /* class Smt2Printer */
387 : :
388 : : } // namespace smt2
389 : : } // namespace printer
390 : : } // namespace cvc5::internal
391 : :
392 : : #endif /* CVC5__PRINTER__SMT2_PRINTER_H */
|
