1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Abdalrhman Mohamed, Andrew Reynolds, Tim King |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
7 |
|
* Copyright (c) 2009-2021 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. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* The pretty-printer interface for the CVC output language. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "cvc5_private.h" |
17 |
|
|
18 |
|
#ifndef CVC5__PRINTER__CVC_PRINTER_H |
19 |
|
#define CVC5__PRINTER__CVC_PRINTER_H |
20 |
|
|
21 |
|
#include <iostream> |
22 |
|
|
23 |
|
#include "printer/printer.h" |
24 |
|
|
25 |
|
namespace cvc5 { |
26 |
|
|
27 |
|
class LetBinding; |
28 |
|
|
29 |
|
namespace printer { |
30 |
|
namespace cvc { |
31 |
|
|
32 |
1612 |
class CvcPrinter : public cvc5::Printer |
33 |
|
{ |
34 |
|
public: |
35 |
|
using cvc5::Printer::toStream; |
36 |
806 |
CvcPrinter(bool cvc3Mode = false) : d_cvc3Mode(cvc3Mode) {} |
37 |
|
void toStream(std::ostream& out, |
38 |
|
TNode n, |
39 |
|
int toDepth, |
40 |
|
size_t dag) const override; |
41 |
|
void toStream(std::ostream& out, const CommandStatus* s) const override; |
42 |
|
void toStream(std::ostream& out, const smt::Model& m) const override; |
43 |
|
|
44 |
|
/** Print empty command */ |
45 |
|
void toStreamCmdEmpty(std::ostream& out, |
46 |
|
const std::string& name) const override; |
47 |
|
|
48 |
|
/** Print echo command */ |
49 |
|
void toStreamCmdEcho(std::ostream& out, |
50 |
|
const std::string& output) const override; |
51 |
|
|
52 |
|
/** Print assert command */ |
53 |
|
void toStreamCmdAssert(std::ostream& out, Node n) const override; |
54 |
|
|
55 |
|
/** Print push command */ |
56 |
|
void toStreamCmdPush(std::ostream& out) const override; |
57 |
|
|
58 |
|
/** Print pop command */ |
59 |
|
void toStreamCmdPop(std::ostream& out) const override; |
60 |
|
|
61 |
|
/** Print declare-fun command */ |
62 |
|
void toStreamCmdDeclareFunction(std::ostream& out, |
63 |
|
const std::string& id, |
64 |
|
TypeNode type) const override; |
65 |
|
|
66 |
|
/** Print declare-sort command */ |
67 |
|
void toStreamCmdDeclareType(std::ostream& out, |
68 |
|
TypeNode type) const override; |
69 |
|
|
70 |
|
/** Print define-sort command */ |
71 |
|
void toStreamCmdDefineType(std::ostream& out, |
72 |
|
const std::string& id, |
73 |
|
const std::vector<TypeNode>& params, |
74 |
|
TypeNode t) const override; |
75 |
|
|
76 |
|
/** Print define-fun command */ |
77 |
|
void toStreamCmdDefineFunction(std::ostream& out, |
78 |
|
const std::string& id, |
79 |
|
const std::vector<Node>& formals, |
80 |
|
TypeNode range, |
81 |
|
Node formula) const override; |
82 |
|
|
83 |
|
/** Print check-sat command */ |
84 |
|
void toStreamCmdCheckSat(std::ostream& out, |
85 |
|
Node n = Node::null()) const override; |
86 |
|
|
87 |
|
/** Print check-sat-assuming command */ |
88 |
|
void toStreamCmdCheckSatAssuming( |
89 |
|
std::ostream& out, const std::vector<Node>& nodes) const override; |
90 |
|
|
91 |
|
/** Print query command */ |
92 |
|
void toStreamCmdQuery(std::ostream& out, Node n) const override; |
93 |
|
|
94 |
|
/** Print simplify command */ |
95 |
|
void toStreamCmdSimplify(std::ostream& out, Node nodes) const override; |
96 |
|
|
97 |
|
/** Print get-value command */ |
98 |
|
void toStreamCmdGetValue(std::ostream& out, |
99 |
|
const std::vector<Node>& n) const override; |
100 |
|
|
101 |
|
/** Print get-assignment command */ |
102 |
|
void toStreamCmdGetAssignment(std::ostream& out) const override; |
103 |
|
|
104 |
|
/** Print get-model command */ |
105 |
|
void toStreamCmdGetModel(std::ostream& out) const override; |
106 |
|
|
107 |
|
/** Print get-proof command */ |
108 |
|
void toStreamCmdGetProof(std::ostream& out) const override; |
109 |
|
|
110 |
|
/** Print get-unsat-core command */ |
111 |
|
void toStreamCmdGetUnsatCore(std::ostream& out) const override; |
112 |
|
|
113 |
|
/** Print get-assertions command */ |
114 |
|
void toStreamCmdGetAssertions(std::ostream& out) const override; |
115 |
|
|
116 |
|
/** Print set-info :status command */ |
117 |
|
void toStreamCmdSetBenchmarkStatus(std::ostream& out, |
118 |
|
Result::Sat status) const override; |
119 |
|
|
120 |
|
/** Print set-logic command */ |
121 |
|
void toStreamCmdSetBenchmarkLogic(std::ostream& out, |
122 |
|
const std::string& logic) const override; |
123 |
|
|
124 |
|
/** Print set-info command */ |
125 |
|
void toStreamCmdSetInfo(std::ostream& out, |
126 |
|
const std::string& flag, |
127 |
|
const std::string& value) const override; |
128 |
|
|
129 |
|
/** Print get-info command */ |
130 |
|
void toStreamCmdGetInfo(std::ostream& out, |
131 |
|
const std::string& flag) const override; |
132 |
|
|
133 |
|
/** Print set-option command */ |
134 |
|
void toStreamCmdSetOption(std::ostream& out, |
135 |
|
const std::string& flag, |
136 |
|
const std::string& value) const override; |
137 |
|
|
138 |
|
/** Print get-option command */ |
139 |
|
void toStreamCmdGetOption(std::ostream& out, |
140 |
|
const std::string& flag) const override; |
141 |
|
|
142 |
|
/** Print declare-datatype(s) command */ |
143 |
|
void toStreamCmdDatatypeDeclaration( |
144 |
|
std::ostream& out, const std::vector<TypeNode>& datatypes) const override; |
145 |
|
|
146 |
|
/** Print reset command */ |
147 |
|
void toStreamCmdReset(std::ostream& out) const override; |
148 |
|
|
149 |
|
/** Print reset-assertions command */ |
150 |
|
void toStreamCmdResetAssertions(std::ostream& out) const override; |
151 |
|
|
152 |
|
/** Print quit command */ |
153 |
|
void toStreamCmdQuit(std::ostream& out) const override; |
154 |
|
|
155 |
|
/** Print comment command */ |
156 |
|
void toStreamCmdComment(std::ostream& out, |
157 |
|
const std::string& comment) const override; |
158 |
|
|
159 |
|
/** Print command sequence command */ |
160 |
|
void toStreamCmdCommandSequence( |
161 |
|
std::ostream& out, const std::vector<Command*>& sequence) const override; |
162 |
|
|
163 |
|
/** Print declaration sequence command */ |
164 |
|
void toStreamCmdDeclarationSequence( |
165 |
|
std::ostream& out, const std::vector<Command*>& sequence) const override; |
166 |
|
|
167 |
|
private: |
168 |
|
/** |
169 |
|
* The main method for printing Nodes. |
170 |
|
*/ |
171 |
|
void toStreamNode(std::ostream& out, |
172 |
|
TNode n, |
173 |
|
int toDepth, |
174 |
|
bool bracket, |
175 |
|
LetBinding* lbind) const; |
176 |
|
/** |
177 |
|
* To stream model sort. This prints the appropriate output for type |
178 |
|
* tn declared via declare-sort or declare-datatype. |
179 |
|
*/ |
180 |
|
void toStreamModelSort(std::ostream& out, |
181 |
|
const smt::Model& m, |
182 |
|
TypeNode tn) const override; |
183 |
|
|
184 |
|
/** |
185 |
|
* To stream model term. This prints the appropriate output for term |
186 |
|
* n declared via declare-fun. |
187 |
|
*/ |
188 |
|
void toStreamModelTerm(std::ostream& out, |
189 |
|
const smt::Model& m, |
190 |
|
Node n) const override; |
191 |
|
/** |
192 |
|
* To stream with let binding. This prints n, possibly in the scope |
193 |
|
* of letification generated by this method based on lbind. |
194 |
|
*/ |
195 |
|
void toStreamNodeWithLetify(std::ostream& out, |
196 |
|
Node n, |
197 |
|
int toDepth, |
198 |
|
bool bracket, |
199 |
|
LetBinding* lbind) const; |
200 |
|
|
201 |
|
bool d_cvc3Mode; |
202 |
|
}; /* class CvcPrinter */ |
203 |
|
|
204 |
|
} // namespace cvc |
205 |
|
} // namespace printer |
206 |
|
} // namespace cvc5 |
207 |
|
|
208 |
|
#endif /* CVC5__PRINTER__CVC_PRINTER_H */ |