1 /********************* */
4 ** Top contributors (to current version):
5 ** Abdalrhman Mohamed, Tim King, 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/model.h"
28 #include "util/result.h"
29 #include "util/sexpr.h"
42 * Since the printers are managed as unique_ptr, we need public acces to
43 * the virtual destructor.
47 /** Get the Printer for a given OutputLanguage */
48 static Printer
* getPrinter(OutputLanguage lang
);
50 /** Write a Node out to a stream with this Printer. */
51 virtual void toStream(std::ostream
& out
,
55 size_t dag
) const = 0;
57 /** Write a CommandStatus out to a stream with this Printer. */
58 virtual void toStream(std::ostream
& out
, const CommandStatus
* s
) const = 0;
60 /** Write a Model out to a stream with this Printer. */
61 virtual void toStream(std::ostream
& out
, const smt::Model
& m
) const;
63 /** Write an UnsatCore out to a stream with this Printer. */
64 virtual void toStream(std::ostream
& out
, const UnsatCore
& core
) const;
66 /** Print empty command */
67 virtual void toStreamCmdEmpty(std::ostream
& out
,
68 const std::string
& name
) const;
70 /** Print echo command */
71 virtual void toStreamCmdEcho(std::ostream
& out
,
72 const std::string
& output
) const;
74 /** Print assert command */
75 virtual void toStreamCmdAssert(std::ostream
& out
, Node n
) const;
77 /** Print push command */
78 virtual void toStreamCmdPush(std::ostream
& out
) const;
80 /** Print pop command */
81 virtual void toStreamCmdPop(std::ostream
& out
) const;
83 /** Print declare-fun command */
84 virtual void toStreamCmdDeclareFunction(std::ostream
& out
,
85 const std::string
& id
,
88 /** Print declare-sort command */
89 virtual void toStreamCmdDeclareType(std::ostream
& out
,
90 const std::string
& id
,
94 /** Print define-sort command */
95 virtual void toStreamCmdDefineType(std::ostream
& out
,
96 const std::string
& id
,
97 const std::vector
<TypeNode
>& params
,
100 /** Print define-fun command */
101 virtual void toStreamCmdDefineFunction(std::ostream
& out
,
102 const std::string
& id
,
103 const std::vector
<Node
>& formals
,
107 /** Print define-named-fun command */
108 virtual void toStreamCmdDefineNamedFunction(std::ostream
& out
,
109 const std::string
& id
,
110 const std::vector
<Node
>& formals
,
114 /** Print define-fun-rec command */
115 virtual void toStreamCmdDefineFunctionRec(
117 const std::vector
<Node
>& funcs
,
118 const std::vector
<std::vector
<Node
>>& formals
,
119 const std::vector
<Node
>& formulas
) const;
121 /** Print set-user-attribute command */
122 void toStreamCmdSetUserAttribute(std::ostream
& out
,
123 const std::string
& attr
,
126 /** Print check-sat command */
127 virtual void toStreamCmdCheckSat(std::ostream
& out
,
128 Node n
= Node::null()) const;
130 /** Print check-sat-assuming command */
131 virtual void toStreamCmdCheckSatAssuming(
132 std::ostream
& out
, const std::vector
<Node
>& nodes
) const;
134 /** Print query command */
135 virtual void toStreamCmdQuery(std::ostream
& out
, Node n
) const;
137 /** Print declare-var command */
138 virtual void toStreamCmdDeclareVar(std::ostream
& out
,
140 TypeNode type
) const;
142 /** Print synth-fun command */
143 virtual void toStreamCmdSynthFun(std::ostream
& out
,
144 const std::string
& sym
,
145 const std::vector
<Node
>& vars
,
148 TypeNode sygusType
) const;
150 /** Print constraint command */
151 virtual void toStreamCmdConstraint(std::ostream
& out
, Node n
) const;
153 /** Print inv-constraint command */
154 virtual void toStreamCmdInvConstraint(
155 std::ostream
& out
, Node inv
, Node pre
, Node trans
, Node post
) const;
157 /** Print check-synth command */
158 virtual void toStreamCmdCheckSynth(std::ostream
& out
) const;
160 /** Print simplify command */
161 virtual void toStreamCmdSimplify(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 Result::Sat 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 */