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