1 /********************* */
2 /*! \file cvc_printer.h
4 ** Top contributors (to current version):
5 ** Abdalrhman Mohamed, Andrew Reynolds, Tim King
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 The pretty-printer interface for the CVC output language
14 ** The pretty-printer interface for the CVC output language.
17 #include "cvc4_private.h"
19 #ifndef CVC4__PRINTER__CVC_PRINTER_H
20 #define CVC4__PRINTER__CVC_PRINTER_H
24 #include "printer/printer.h"
33 class CvcPrinter
: public CVC4::Printer
36 using CVC4::Printer::toStream
;
37 CvcPrinter(bool cvc3Mode
= false) : d_cvc3Mode(cvc3Mode
) {}
38 void toStream(std::ostream
& out
,
41 size_t dag
) const override
;
42 void toStream(std::ostream
& out
, const CommandStatus
* s
) const override
;
43 void toStream(std::ostream
& out
, const smt::Model
& m
) const override
;
45 /** Print empty command */
46 void toStreamCmdEmpty(std::ostream
& out
,
47 const std::string
& name
) const override
;
49 /** Print echo command */
50 void toStreamCmdEcho(std::ostream
& out
,
51 const std::string
& output
) const override
;
53 /** Print assert command */
54 void toStreamCmdAssert(std::ostream
& out
, Node n
) const override
;
56 /** Print push command */
57 void toStreamCmdPush(std::ostream
& out
) const override
;
59 /** Print pop command */
60 void toStreamCmdPop(std::ostream
& out
) const override
;
62 /** Print declare-fun command */
63 void toStreamCmdDeclareFunction(std::ostream
& out
,
64 const std::string
& id
,
65 TypeNode type
) const override
;
67 /** Print declare-sort command */
68 void toStreamCmdDeclareType(std::ostream
& out
,
69 TypeNode type
) const override
;
71 /** Print define-sort command */
72 void toStreamCmdDefineType(std::ostream
& out
,
73 const std::string
& id
,
74 const std::vector
<TypeNode
>& params
,
75 TypeNode t
) const override
;
77 /** Print define-fun command */
78 void toStreamCmdDefineFunction(std::ostream
& out
,
79 const std::string
& id
,
80 const std::vector
<Node
>& formals
,
82 Node formula
) const override
;
84 /** Print check-sat command */
85 void toStreamCmdCheckSat(std::ostream
& out
,
86 Node n
= Node::null()) const override
;
88 /** Print check-sat-assuming command */
89 void toStreamCmdCheckSatAssuming(
90 std::ostream
& out
, const std::vector
<Node
>& nodes
) const override
;
92 /** Print query command */
93 void toStreamCmdQuery(std::ostream
& out
, Node n
) const override
;
95 /** Print simplify command */
96 void toStreamCmdSimplify(std::ostream
& out
, Node nodes
) const override
;
98 /** Print get-value command */
99 void toStreamCmdGetValue(std::ostream
& out
,
100 const std::vector
<Node
>& n
) const override
;
102 /** Print get-assignment command */
103 void toStreamCmdGetAssignment(std::ostream
& out
) const override
;
105 /** Print get-model command */
106 void toStreamCmdGetModel(std::ostream
& out
) const override
;
108 /** Print get-proof command */
109 void toStreamCmdGetProof(std::ostream
& out
) const override
;
111 /** Print get-unsat-core command */
112 void toStreamCmdGetUnsatCore(std::ostream
& out
) const override
;
114 /** Print get-assertions command */
115 void toStreamCmdGetAssertions(std::ostream
& out
) const override
;
117 /** Print set-info :status command */
118 void toStreamCmdSetBenchmarkStatus(std::ostream
& out
,
119 Result::Sat status
) const override
;
121 /** Print set-logic command */
122 void toStreamCmdSetBenchmarkLogic(std::ostream
& out
,
123 const std::string
& logic
) const override
;
125 /** Print set-info command */
126 void toStreamCmdSetInfo(std::ostream
& out
,
127 const std::string
& flag
,
128 SExpr sexpr
) const override
;
130 /** Print get-info command */
131 void toStreamCmdGetInfo(std::ostream
& out
,
132 const std::string
& flag
) const override
;
134 /** Print set-option command */
135 void toStreamCmdSetOption(std::ostream
& out
,
136 const std::string
& flag
,
137 SExpr sexpr
) const override
;
139 /** Print get-option command */
140 void toStreamCmdGetOption(std::ostream
& out
,
141 const std::string
& flag
) const override
;
143 /** Print declare-datatype(s) command */
144 void toStreamCmdDatatypeDeclaration(
145 std::ostream
& out
, const std::vector
<TypeNode
>& datatypes
) const override
;
147 /** Print reset command */
148 void toStreamCmdReset(std::ostream
& out
) const override
;
150 /** Print reset-assertions command */
151 void toStreamCmdResetAssertions(std::ostream
& out
) const override
;
153 /** Print quit command */
154 void toStreamCmdQuit(std::ostream
& out
) const override
;
156 /** Print comment command */
157 void toStreamCmdComment(std::ostream
& out
,
158 const std::string
& comment
) const override
;
160 /** Print command sequence command */
161 void toStreamCmdCommandSequence(
162 std::ostream
& out
, const std::vector
<Command
*>& sequence
) const override
;
164 /** Print declaration sequence command */
165 void toStreamCmdDeclarationSequence(
166 std::ostream
& out
, const std::vector
<Command
*>& sequence
) const override
;
170 * The main method for printing Nodes.
172 void toStreamNode(std::ostream
& out
,
176 LetBinding
* lbind
) const;
178 * To stream model sort. This prints the appropriate output for type
179 * tn declared via declare-sort or declare-datatype.
181 void toStreamModelSort(std::ostream
& out
,
183 TypeNode tn
) const override
;
186 * To stream model term. This prints the appropriate output for term
187 * n declared via declare-fun.
189 void toStreamModelTerm(std::ostream
& out
,
191 Node n
) const override
;
193 * To stream with let binding. This prints n, possibly in the scope
194 * of letification generated by this method based on lbind.
196 void toStreamNodeWithLetify(std::ostream
& out
,
200 LetBinding
* lbind
) const;
203 }; /* class CvcPrinter */
206 } // namespace printer
209 #endif /* CVC4__PRINTER__CVC_PRINTER_H */