1 /********************* */
4 ** Top contributors (to current version):
5 ** Tim King, Andrew Reynolds, Aina Niemetz
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2020 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.\endverbatim
12 ** \brief Base of the pretty-printer interface
14 ** Base of the pretty-printer interface.
17 #include "cvc4_private.h"
19 #ifndef CVC4__PRINTER__PRINTER_H
20 #define CVC4__PRINTER__PRINTER_H
25 #include "expr/node.h"
26 #include "options/language.h"
27 #include "smt/command.h"
28 #include "smt/model.h"
29 #include "util/sexpr.h"
39 * Since the printers are managed as unique_ptr, we need public acces to
40 * the virtual destructor.
44 /** Get the Printer for a given OutputLanguage */
45 static Printer
* getPrinter(OutputLanguage lang
);
47 /** Write a Node out to a stream with this Printer. */
48 virtual void toStream(std::ostream
& out
,
52 size_t dag
) const = 0;
54 /** Write a CommandStatus out to a stream with this Printer. */
55 virtual void toStream(std::ostream
& out
, const CommandStatus
* s
) const = 0;
57 /** Write a Model out to a stream with this Printer. */
58 virtual void toStream(std::ostream
& out
, const Model
& m
) const;
60 /** Write an UnsatCore out to a stream with this Printer. */
61 virtual void toStream(std::ostream
& out
, const UnsatCore
& core
) const;
63 /** Print empty command */
64 virtual void toStreamCmdEmpty(std::ostream
& out
,
65 const std::string
& name
) const;
67 /** Print echo command */
68 virtual void toStreamCmdEcho(std::ostream
& out
,
69 const std::string
& output
) const;
71 /** Print assert command */
72 virtual void toStreamCmdAssert(std::ostream
& out
, Node n
) const;
74 /** Print push command */
75 virtual void toStreamCmdPush(std::ostream
& out
) const;
77 /** Print pop command */
78 virtual void toStreamCmdPop(std::ostream
& out
) const;
80 /** Print declare-fun command */
81 virtual void toStreamCmdDeclareFunction(std::ostream
& out
,
82 const std::string
& id
,
85 /** Print declare-sort command */
86 virtual void toStreamCmdDeclareType(std::ostream
& out
,
87 const std::string
& id
,
91 /** Print define-sort command */
92 virtual void toStreamCmdDefineType(std::ostream
& out
,
93 const std::string
& id
,
94 const std::vector
<TypeNode
>& params
,
97 /** Print define-fun command */
98 virtual void toStreamCmdDefineFunction(std::ostream
& out
,
99 const std::string
& id
,
100 const std::vector
<Node
>& formals
,
104 /** Print define-named-fun command */
105 virtual void toStreamCmdDefineNamedFunction(std::ostream
& out
,
106 const std::string
& id
,
107 const std::vector
<Node
>& formals
,
111 /** Print define-fun-rec command */
112 virtual void toStreamCmdDefineFunctionRec(
114 const std::vector
<Node
>& funcs
,
115 const std::vector
<std::vector
<Node
>>& formals
,
116 const std::vector
<Node
>& formulas
) const;
118 /** Print set-user-attribute command */
119 void toStreamCmdSetUserAttribute(std::ostream
& out
,
120 const std::string
& attr
,
123 /** Print check-sat command */
124 virtual void toStreamCmdCheckSat(std::ostream
& out
,
125 Node n
= Node::null()) const;
127 /** Print check-sat-assuming command */
128 virtual void toStreamCmdCheckSatAssuming(
129 std::ostream
& out
, const std::vector
<Node
>& nodes
) const;
131 /** Print query command */
132 virtual void toStreamCmdQuery(std::ostream
& out
, Node n
) const;
134 /** Print declare-var command */
135 virtual void toStreamCmdDeclareVar(std::ostream
& out
,
137 TypeNode type
) const;
139 /** Print synth-fun command */
140 virtual void toStreamCmdSynthFun(std::ostream
& out
,
141 const std::string
& sym
,
142 const std::vector
<Node
>& vars
,
145 TypeNode sygusType
) const;
147 /** Print constraint command */
148 virtual void toStreamCmdConstraint(std::ostream
& out
, Node n
) const;
150 /** Print inv-constraint command */
151 virtual void toStreamCmdInvConstraint(
152 std::ostream
& out
, Node inv
, Node pre
, Node trans
, Node post
) const;
154 /** Print check-synth command */
155 virtual void toStreamCmdCheckSynth(std::ostream
& out
) const;
157 /** Print simplify command */
158 virtual void toStreamCmdSimplify(std::ostream
& out
, Node n
) const;
160 /** Print expand-definitions command */
161 void toStreamCmdExpandDefinitions(std::ostream
& out
, Node n
) const;
163 /** Print get-value command */
164 virtual void toStreamCmdGetValue(std::ostream
& out
,
165 const std::vector
<Node
>& nodes
) const;
167 /** Print get-assignment command */
168 virtual void toStreamCmdGetAssignment(std::ostream
& out
) const;
170 /** Print get-model command */
171 virtual void toStreamCmdGetModel(std::ostream
& out
) const;
173 /** Print block-model command */
174 void toStreamCmdBlockModel(std::ostream
& out
) const;
176 /** Print block-model-values command */
177 void toStreamCmdBlockModelValues(std::ostream
& out
,
178 const std::vector
<Node
>& nodes
) const;
180 /** Print get-proof command */
181 virtual void toStreamCmdGetProof(std::ostream
& out
) const;
183 /** Print get-instantiations command */
184 void toStreamCmdGetInstantiations(std::ostream
& out
) const;
186 /** Print get-synth-solution command */
187 void toStreamCmdGetSynthSolution(std::ostream
& out
) const;
189 /** Print get-interpol command */
190 void toStreamCmdGetInterpol(std::ostream
& out
,
191 const std::string
& name
,
193 TypeNode sygusType
) const;
195 /** Print get-abduct command */
196 virtual void toStreamCmdGetAbduct(std::ostream
& out
,
197 const std::string
& name
,
199 TypeNode sygusType
) const;
201 /** Print get-quantifier-elimination command */
202 void toStreamCmdGetQuantifierElimination(std::ostream
& out
, Node n
) const;
204 /** Print get-unsat-assumptions command */
205 virtual void toStreamCmdGetUnsatAssumptions(std::ostream
& out
) const;
207 /** Print get-unsat-core command */
208 virtual void toStreamCmdGetUnsatCore(std::ostream
& out
) const;
210 /** Print get-assertions command */
211 virtual void toStreamCmdGetAssertions(std::ostream
& out
) const;
213 /** Print set-info :status command */
214 virtual void toStreamCmdSetBenchmarkStatus(std::ostream
& out
,
215 BenchmarkStatus status
) const;
217 /** Print set-logic command */
218 virtual void toStreamCmdSetBenchmarkLogic(std::ostream
& out
,
219 const std::string
& logic
) const;
221 /** Print set-info command */
222 virtual void toStreamCmdSetInfo(std::ostream
& out
,
223 const std::string
& flag
,
226 /** Print get-info command */
227 virtual void toStreamCmdGetInfo(std::ostream
& out
,
228 const std::string
& flag
) const;
230 /** Print set-option command */
231 virtual void toStreamCmdSetOption(std::ostream
& out
,
232 const std::string
& flag
,
235 /** Print get-option command */
236 virtual void toStreamCmdGetOption(std::ostream
& out
,
237 const std::string
& flag
) const;
239 /** Print set-expression-name command */
240 void toStreamCmdSetExpressionName(std::ostream
& out
,
242 const std::string
& name
) const;
244 /** Print declare-datatype(s) command */
245 virtual void toStreamCmdDatatypeDeclaration(
246 std::ostream
& out
, const std::vector
<TypeNode
>& datatypes
) const;
248 /** Print reset command */
249 virtual void toStreamCmdReset(std::ostream
& out
) const;
251 /** Print reset-assertions command */
252 virtual void toStreamCmdResetAssertions(std::ostream
& out
) const;
254 /** Print quit command */
255 virtual void toStreamCmdQuit(std::ostream
& out
) const;
257 /** Print comment command */
258 virtual void toStreamCmdComment(std::ostream
& out
,
259 const std::string
& comment
) const;
261 /** Print command sequence command */
262 virtual void toStreamCmdCommandSequence(
263 std::ostream
& out
, const std::vector
<Command
*>& sequence
) const;
265 /** Print declaration sequence command */
266 virtual void toStreamCmdDeclarationSequence(
267 std::ostream
& out
, const std::vector
<Command
*>& sequence
) const;
270 /** Derived classes can construct, but no one else. */
273 /** write model response to command */
274 virtual void toStream(std::ostream
& out
,
276 const NodeCommand
* c
) const = 0;
278 /** write model response to command using another language printer */
279 void toStreamUsing(OutputLanguage lang
,
282 const NodeCommand
* c
) const
284 getPrinter(lang
)->toStream(out
, m
, c
);
288 * Write an error to `out` stating that command `name` is not supported by
291 void printUnknownCommand(std::ostream
& out
, const std::string
& name
) const;
294 /** Disallow copy, assignment */
295 Printer(const Printer
&) = delete;
296 Printer
& operator=(const Printer
&) = delete;
298 /** Make a Printer for a given OutputLanguage */
299 static std::unique_ptr
<Printer
> makePrinter(OutputLanguage lang
);
301 /** Printers for each OutputLanguage */
302 static std::unique_ptr
<Printer
> d_printers
[language::output::LANG_MAX
];
304 }; /* class Printer */
308 #endif /* CVC4__PRINTER__PRINTER_H */