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