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
,
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-fun-rec command */
105 virtual void toStreamCmdDefineFunctionRec(
107 const std::vector
<Node
>& funcs
,
108 const std::vector
<std::vector
<Node
>>& formals
,
109 const std::vector
<Node
>& formulas
) const;
111 /** Print set-user-attribute command */
112 void toStreamCmdSetUserAttribute(std::ostream
& out
,
113 const std::string
& attr
,
116 /** Print check-sat command */
117 virtual void toStreamCmdCheckSat(std::ostream
& out
,
118 Node n
= Node::null()) const;
120 /** Print check-sat-assuming command */
121 virtual void toStreamCmdCheckSatAssuming(
122 std::ostream
& out
, const std::vector
<Node
>& nodes
) const;
124 /** Print query command */
125 virtual void toStreamCmdQuery(std::ostream
& out
, Node n
) const;
127 /** Print declare-var command */
128 virtual void toStreamCmdDeclareVar(std::ostream
& out
,
130 TypeNode type
) const;
132 /** Print synth-fun command */
133 virtual void toStreamCmdSynthFun(std::ostream
& out
,
134 const std::string
& sym
,
135 const std::vector
<Node
>& vars
,
138 TypeNode sygusType
) const;
140 /** Print constraint command */
141 virtual void toStreamCmdConstraint(std::ostream
& out
, Node n
) const;
143 /** Print inv-constraint command */
144 virtual void toStreamCmdInvConstraint(
145 std::ostream
& out
, Node inv
, Node pre
, Node trans
, Node post
) const;
147 /** Print check-synth command */
148 virtual void toStreamCmdCheckSynth(std::ostream
& out
) const;
150 /** Print simplify command */
151 virtual void toStreamCmdSimplify(std::ostream
& out
, Node n
) const;
153 /** Print get-value command */
154 virtual void toStreamCmdGetValue(std::ostream
& out
,
155 const std::vector
<Node
>& nodes
) const;
157 /** Print get-assignment command */
158 virtual void toStreamCmdGetAssignment(std::ostream
& out
) const;
160 /** Print get-model command */
161 virtual void toStreamCmdGetModel(std::ostream
& out
) const;
163 /** Print block-model command */
164 void toStreamCmdBlockModel(std::ostream
& out
) const;
166 /** Print block-model-values command */
167 void toStreamCmdBlockModelValues(std::ostream
& out
,
168 const std::vector
<Node
>& nodes
) const;
170 /** Print get-proof command */
171 virtual void toStreamCmdGetProof(std::ostream
& out
) const;
173 /** Print get-instantiations command */
174 void toStreamCmdGetInstantiations(std::ostream
& out
) const;
176 /** Print get-synth-solution command */
177 void toStreamCmdGetSynthSolution(std::ostream
& out
) const;
179 /** Print get-interpol command */
180 void toStreamCmdGetInterpol(std::ostream
& out
,
181 const std::string
& name
,
183 TypeNode sygusType
) const;
185 /** Print get-abduct command */
186 virtual void toStreamCmdGetAbduct(std::ostream
& out
,
187 const std::string
& name
,
189 TypeNode sygusType
) const;
191 /** Print get-quantifier-elimination command */
192 void toStreamCmdGetQuantifierElimination(std::ostream
& out
, Node n
) const;
194 /** Print get-unsat-assumptions command */
195 virtual void toStreamCmdGetUnsatAssumptions(std::ostream
& out
) const;
197 /** Print get-unsat-core command */
198 virtual void toStreamCmdGetUnsatCore(std::ostream
& out
) const;
200 /** Print get-assertions command */
201 virtual void toStreamCmdGetAssertions(std::ostream
& out
) const;
203 /** Print set-info :status command */
204 virtual void toStreamCmdSetBenchmarkStatus(std::ostream
& out
,
205 Result::Sat status
) const;
207 /** Print set-logic command */
208 virtual void toStreamCmdSetBenchmarkLogic(std::ostream
& out
,
209 const std::string
& logic
) const;
211 /** Print set-info command */
212 virtual void toStreamCmdSetInfo(std::ostream
& out
,
213 const std::string
& flag
,
216 /** Print get-info command */
217 virtual void toStreamCmdGetInfo(std::ostream
& out
,
218 const std::string
& flag
) const;
220 /** Print set-option command */
221 virtual void toStreamCmdSetOption(std::ostream
& out
,
222 const std::string
& flag
,
225 /** Print get-option command */
226 virtual void toStreamCmdGetOption(std::ostream
& out
,
227 const std::string
& flag
) const;
229 /** Print set-expression-name command */
230 void toStreamCmdSetExpressionName(std::ostream
& out
,
232 const std::string
& name
) const;
234 /** Print declare-datatype(s) command */
235 virtual void toStreamCmdDatatypeDeclaration(
236 std::ostream
& out
, const std::vector
<TypeNode
>& datatypes
) const;
238 /** Print reset command */
239 virtual void toStreamCmdReset(std::ostream
& out
) const;
241 /** Print reset-assertions command */
242 virtual void toStreamCmdResetAssertions(std::ostream
& out
) const;
244 /** Print quit command */
245 virtual void toStreamCmdQuit(std::ostream
& out
) const;
247 /** Print comment command */
248 virtual void toStreamCmdComment(std::ostream
& out
,
249 const std::string
& comment
) const;
250 /** Declare heap command */
251 virtual void toStreamCmdDeclareHeap(std::ostream
& out
,
253 TypeNode dataType
) const;
255 /** Print command sequence command */
256 virtual void toStreamCmdCommandSequence(
257 std::ostream
& out
, const std::vector
<Command
*>& sequence
) const;
259 /** Print declaration sequence command */
260 virtual void toStreamCmdDeclarationSequence(
261 std::ostream
& out
, const std::vector
<Command
*>& sequence
) const;
264 /** Derived classes can construct, but no one else. */
268 * To stream model sort. This prints the appropriate output for type
269 * tn declared via declare-sort or declare-datatype.
271 virtual void toStreamModelSort(std::ostream
& out
,
273 TypeNode tn
) const = 0;
276 * To stream model term. This prints the appropriate output for term
277 * n declared via declare-fun.
279 virtual void toStreamModelTerm(std::ostream
& out
,
283 /** write model response to command using another language printer */
284 void toStreamUsing(OutputLanguage lang
,
286 const smt::Model
& m
) const;
289 * Write an error to `out` stating that command `name` is not supported by
292 void printUnknownCommand(std::ostream
& out
, const std::string
& name
) const;
295 /** Disallow copy, assignment */
296 Printer(const Printer
&) = delete;
297 Printer
& operator=(const Printer
&) = delete;
299 /** Make a Printer for a given OutputLanguage */
300 static std::unique_ptr
<Printer
> makePrinter(OutputLanguage lang
);
302 /** Printers for each OutputLanguage */
303 static std::unique_ptr
<Printer
> d_printers
[language::output::LANG_MAX
];
305 }; /* class Printer */
309 #endif /* CVC4__PRINTER__PRINTER_H */