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
,
54 size_t dag
) const = 0;
56 /** Write a CommandStatus out to a stream with this Printer. */
57 virtual void toStream(std::ostream
& out
, const CommandStatus
* s
) const = 0;
59 /** Write a Model out to a stream with this Printer. */
60 virtual void toStream(std::ostream
& out
, const smt::Model
& m
) const;
62 /** Write an UnsatCore out to a stream with this Printer. */
63 virtual void toStream(std::ostream
& out
, const UnsatCore
& core
) const;
65 /** Print empty command */
66 virtual void toStreamCmdEmpty(std::ostream
& out
,
67 const std::string
& name
) const;
69 /** Print echo command */
70 virtual void toStreamCmdEcho(std::ostream
& out
,
71 const std::string
& output
) const;
73 /** Print assert command */
74 virtual void toStreamCmdAssert(std::ostream
& out
, Node n
) const;
76 /** Print push command */
77 virtual void toStreamCmdPush(std::ostream
& out
) const;
79 /** Print pop command */
80 virtual void toStreamCmdPop(std::ostream
& out
) const;
82 /** Print declare-fun command */
83 virtual void toStreamCmdDeclareFunction(std::ostream
& out
,
84 const std::string
& id
,
87 /** Print declare-sort command */
88 virtual void toStreamCmdDeclareType(std::ostream
& out
,
89 const std::string
& id
,
93 /** Print define-sort command */
94 virtual void toStreamCmdDefineType(std::ostream
& out
,
95 const std::string
& id
,
96 const std::vector
<TypeNode
>& params
,
99 /** Print define-fun command */
100 virtual void toStreamCmdDefineFunction(std::ostream
& out
,
101 const std::string
& id
,
102 const std::vector
<Node
>& formals
,
106 /** Print define-fun-rec command */
107 virtual void toStreamCmdDefineFunctionRec(
109 const std::vector
<Node
>& funcs
,
110 const std::vector
<std::vector
<Node
>>& formals
,
111 const std::vector
<Node
>& formulas
) const;
113 /** Print set-user-attribute command */
114 void toStreamCmdSetUserAttribute(std::ostream
& out
,
115 const std::string
& attr
,
118 /** Print check-sat command */
119 virtual void toStreamCmdCheckSat(std::ostream
& out
,
120 Node n
= Node::null()) const;
122 /** Print check-sat-assuming command */
123 virtual void toStreamCmdCheckSatAssuming(
124 std::ostream
& out
, const std::vector
<Node
>& nodes
) const;
126 /** Print query command */
127 virtual void toStreamCmdQuery(std::ostream
& out
, Node n
) const;
129 /** Print declare-var command */
130 virtual void toStreamCmdDeclareVar(std::ostream
& out
,
132 TypeNode type
) const;
134 /** Print synth-fun command */
135 virtual void toStreamCmdSynthFun(std::ostream
& out
,
136 const std::string
& sym
,
137 const std::vector
<Node
>& vars
,
140 TypeNode sygusType
) const;
142 /** Print constraint command */
143 virtual void toStreamCmdConstraint(std::ostream
& out
, Node n
) const;
145 /** Print inv-constraint command */
146 virtual void toStreamCmdInvConstraint(
147 std::ostream
& out
, Node inv
, Node pre
, Node trans
, Node post
) const;
149 /** Print check-synth command */
150 virtual void toStreamCmdCheckSynth(std::ostream
& out
) const;
152 /** Print simplify command */
153 virtual void toStreamCmdSimplify(std::ostream
& out
, Node n
) const;
155 /** Print get-value command */
156 virtual void toStreamCmdGetValue(std::ostream
& out
,
157 const std::vector
<Node
>& nodes
) const;
159 /** Print get-assignment command */
160 virtual void toStreamCmdGetAssignment(std::ostream
& out
) const;
162 /** Print get-model command */
163 virtual void toStreamCmdGetModel(std::ostream
& out
) const;
165 /** Print block-model command */
166 void toStreamCmdBlockModel(std::ostream
& out
) const;
168 /** Print block-model-values command */
169 void toStreamCmdBlockModelValues(std::ostream
& out
,
170 const std::vector
<Node
>& nodes
) const;
172 /** Print get-proof command */
173 virtual void toStreamCmdGetProof(std::ostream
& out
) const;
175 /** Print get-instantiations command */
176 void toStreamCmdGetInstantiations(std::ostream
& out
) const;
178 /** Print get-synth-solution command */
179 void toStreamCmdGetSynthSolution(std::ostream
& out
) const;
181 /** Print get-interpol command */
182 void toStreamCmdGetInterpol(std::ostream
& out
,
183 const std::string
& name
,
185 TypeNode sygusType
) const;
187 /** Print get-abduct command */
188 virtual void toStreamCmdGetAbduct(std::ostream
& out
,
189 const std::string
& name
,
191 TypeNode sygusType
) const;
193 /** Print get-quantifier-elimination command */
194 void toStreamCmdGetQuantifierElimination(std::ostream
& out
, Node n
) const;
196 /** Print get-unsat-assumptions command */
197 virtual void toStreamCmdGetUnsatAssumptions(std::ostream
& out
) const;
199 /** Print get-unsat-core command */
200 virtual void toStreamCmdGetUnsatCore(std::ostream
& out
) const;
202 /** Print get-assertions command */
203 virtual void toStreamCmdGetAssertions(std::ostream
& out
) const;
205 /** Print set-info :status command */
206 virtual void toStreamCmdSetBenchmarkStatus(std::ostream
& out
,
207 Result::Sat status
) const;
209 /** Print set-logic command */
210 virtual void toStreamCmdSetBenchmarkLogic(std::ostream
& out
,
211 const std::string
& logic
) const;
213 /** Print set-info command */
214 virtual void toStreamCmdSetInfo(std::ostream
& out
,
215 const std::string
& flag
,
218 /** Print get-info command */
219 virtual void toStreamCmdGetInfo(std::ostream
& out
,
220 const std::string
& flag
) const;
222 /** Print set-option command */
223 virtual void toStreamCmdSetOption(std::ostream
& out
,
224 const std::string
& flag
,
227 /** Print get-option command */
228 virtual void toStreamCmdGetOption(std::ostream
& out
,
229 const std::string
& flag
) const;
231 /** Print set-expression-name command */
232 void toStreamCmdSetExpressionName(std::ostream
& out
,
234 const std::string
& name
) const;
236 /** Print declare-datatype(s) command */
237 virtual void toStreamCmdDatatypeDeclaration(
238 std::ostream
& out
, const std::vector
<TypeNode
>& datatypes
) const;
240 /** Print reset command */
241 virtual void toStreamCmdReset(std::ostream
& out
) const;
243 /** Print reset-assertions command */
244 virtual void toStreamCmdResetAssertions(std::ostream
& out
) const;
246 /** Print quit command */
247 virtual void toStreamCmdQuit(std::ostream
& out
) const;
249 /** Print comment command */
250 virtual void toStreamCmdComment(std::ostream
& out
,
251 const std::string
& comment
) const;
252 /** Declare heap command */
253 virtual void toStreamCmdDeclareHeap(std::ostream
& out
,
255 TypeNode dataType
) const;
257 /** Print command sequence command */
258 virtual void toStreamCmdCommandSequence(
259 std::ostream
& out
, const std::vector
<Command
*>& sequence
) const;
261 /** Print declaration sequence command */
262 virtual void toStreamCmdDeclarationSequence(
263 std::ostream
& out
, const std::vector
<Command
*>& sequence
) const;
266 /** Derived classes can construct, but no one else. */
269 /** write model response to command */
270 virtual void toStream(std::ostream
& out
,
272 const NodeCommand
* c
) const = 0;
274 /** write model response to command using another language printer */
275 void toStreamUsing(OutputLanguage lang
,
278 const NodeCommand
* c
) const
280 getPrinter(lang
)->toStream(out
, m
, c
);
284 * Write an error to `out` stating that command `name` is not supported by
287 void printUnknownCommand(std::ostream
& out
, const std::string
& name
) const;
290 /** Disallow copy, assignment */
291 Printer(const Printer
&) = delete;
292 Printer
& operator=(const Printer
&) = delete;
294 /** Make a Printer for a given OutputLanguage */
295 static std::unique_ptr
<Printer
> makePrinter(OutputLanguage lang
);
297 /** Printers for each OutputLanguage */
298 static std::unique_ptr
<Printer
> d_printers
[language::output::LANG_MAX
];
300 }; /* class Printer */
304 #endif /* CVC4__PRINTER__PRINTER_H */