GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/printer/smt2/smt2_printer.h Lines: 2 2 100.0 %
Date: 2021-03-23 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file smt2_printer.h
3
 ** \verbatim
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-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.\endverbatim
11
 **
12
 ** \brief The pretty-printer interface for the SMT2 output language
13
 **
14
 ** The pretty-printer interface for the SMT2 output language.
15
 **/
16
17
#include "cvc4_private.h"
18
19
#ifndef CVC4__PRINTER__SMT2_PRINTER_H
20
#define CVC4__PRINTER__SMT2_PRINTER_H
21
22
#include "printer/printer.h"
23
24
namespace CVC4 {
25
26
class LetBinding;
27
28
namespace printer {
29
namespace smt2 {
30
31
enum Variant
32
{
33
  no_variant,
34
  smt2_6_variant,  // new-style 2.6 syntax, when it makes a difference, with
35
                   // support for the string standard
36
};                 /* enum Variant */
37
38
10556
class Smt2Printer : public CVC4::Printer
39
{
40
 public:
41
5278
  Smt2Printer(Variant variant = no_variant) : d_variant(variant) {}
42
  using CVC4::Printer::toStream;
43
  void toStream(std::ostream& out,
44
                TNode n,
45
                int toDepth,
46
                size_t dag) const override;
47
  void toStream(std::ostream& out, const CommandStatus* s) const override;
48
  void toStream(std::ostream& out, const smt::Model& m) const override;
49
  /**
50
   * Writes the unsat core to the stream out.
51
   * We use the expression names that are stored in the SMT engine associated
52
   * with the core (UnsatCore::getSmtEngine) for printing named assertions.
53
   */
54
  void toStream(std::ostream& out, const UnsatCore& core) const override;
55
56
  /** Print empty command */
57
  void toStreamCmdEmpty(std::ostream& out,
58
                        const std::string& name) const override;
59
60
  /** Print echo command */
61
  void toStreamCmdEcho(std::ostream& out,
62
                       const std::string& output) const override;
63
64
  /** Print assert command */
65
  void toStreamCmdAssert(std::ostream& out, Node n) const override;
66
67
  /** Print push command */
68
  void toStreamCmdPush(std::ostream& out) const override;
69
70
  /** Print pop command */
71
  void toStreamCmdPop(std::ostream& out) const override;
72
73
  /** Print declare-fun command */
74
  void toStreamCmdDeclareFunction(std::ostream& out,
75
                                  const std::string& id,
76
                                  TypeNode type) const override;
77
78
  /** Print declare-sort command */
79
  void toStreamCmdDeclareType(std::ostream& out,
80
                              TypeNode type) const override;
81
82
  /** Print define-sort command */
83
  void toStreamCmdDefineType(std::ostream& out,
84
                             const std::string& id,
85
                             const std::vector<TypeNode>& params,
86
                             TypeNode t) const override;
87
88
  /** Print define-fun command */
89
  void toStreamCmdDefineFunction(std::ostream& out,
90
                                 const std::string& id,
91
                                 const std::vector<Node>& formals,
92
                                 TypeNode range,
93
                                 Node formula) const override;
94
95
  /** Print define-fun-rec command */
96
  void toStreamCmdDefineFunctionRec(
97
      std::ostream& out,
98
      const std::vector<Node>& funcs,
99
      const std::vector<std::vector<Node>>& formals,
100
      const std::vector<Node>& formulas) const override;
101
102
  /** Print check-sat command */
103
  void toStreamCmdCheckSat(std::ostream& out,
104
                           Node n = Node::null()) const override;
105
106
  /** Print check-sat-assuming command */
107
  void toStreamCmdCheckSatAssuming(
108
      std::ostream& out, const std::vector<Node>& nodes) const override;
109
110
  /** Print query command */
111
  void toStreamCmdQuery(std::ostream& out, Node n) const override;
112
113
  /** Print declare-var command */
114
  void toStreamCmdDeclareVar(std::ostream& out,
115
                             Node var,
116
                             TypeNode type) const override;
117
118
  /** Print synth-fun command */
119
  void toStreamCmdSynthFun(std::ostream& out,
120
                           Node f,
121
                           const std::vector<Node>& vars,
122
                           bool isInv,
123
                           TypeNode sygusType = TypeNode::null()) const override;
124
125
  /** Print constraint command */
126
  void toStreamCmdConstraint(std::ostream& out, Node n) const override;
127
128
  /** Print inv-constraint command */
129
  void toStreamCmdInvConstraint(std::ostream& out,
130
                                Node inv,
131
                                Node pre,
132
                                Node trans,
133
                                Node post) const override;
134
135
  /** Print check-synth command */
136
  void toStreamCmdCheckSynth(std::ostream& out) const override;
137
138
  /** Print simplify command */
139
  void toStreamCmdSimplify(std::ostream& out, Node nodes) const override;
140
141
  /** Print get-value command */
142
  void toStreamCmdGetValue(std::ostream& out,
143
                           const std::vector<Node>& n) const override;
144
145
  /** Print get-assignment command */
146
  void toStreamCmdGetAssignment(std::ostream& out) const override;
147
148
  /** Print get-model command */
149
  void toStreamCmdGetModel(std::ostream& out) const override;
150
151
  /** Print get-proof command */
152
  void toStreamCmdGetProof(std::ostream& out) const override;
153
154
  /** Print get-abduct command */
155
  void toStreamCmdGetAbduct(std::ostream& out,
156
                            const std::string& name,
157
                            Node conj,
158
                            TypeNode sygusType) const override;
159
160
  /** Print get-unsat-assumptions command */
161
  void toStreamCmdGetUnsatAssumptions(std::ostream& out) const override;
162
163
  /** Print get-unsat-core command */
164
  void toStreamCmdGetUnsatCore(std::ostream& out) const override;
165
166
  /** Print get-assertions command */
167
  void toStreamCmdGetAssertions(std::ostream& out) const override;
168
169
  /** Print set-info :status command */
170
  void toStreamCmdSetBenchmarkStatus(std::ostream& out,
171
                                     Result::Sat status) const override;
172
173
  /** Print set-logic command */
174
  void toStreamCmdSetBenchmarkLogic(std::ostream& out,
175
                                    const std::string& logic) const override;
176
177
  /** Print set-info command */
178
  void toStreamCmdSetInfo(std::ostream& out,
179
                          const std::string& flag,
180
                          const std::string& value) const override;
181
182
  /** Print get-info command */
183
  void toStreamCmdGetInfo(std::ostream& out,
184
                          const std::string& flag) const override;
185
186
  /** Print set-option command */
187
  void toStreamCmdSetOption(std::ostream& out,
188
                            const std::string& flag,
189
                            const std::string& value) const override;
190
191
  /** Print get-option command */
192
  void toStreamCmdGetOption(std::ostream& out,
193
                            const std::string& flag) const override;
194
195
  /** Print declare-datatype(s) command */
196
  void toStreamCmdDatatypeDeclaration(
197
      std::ostream& out, const std::vector<TypeNode>& datatypes) const override;
198
199
  /** Print reset command */
200
  void toStreamCmdReset(std::ostream& out) const override;
201
202
  /** Print reset-assertions command */
203
  void toStreamCmdResetAssertions(std::ostream& out) const override;
204
205
  /** Print quit command */
206
  void toStreamCmdQuit(std::ostream& out) const override;
207
208
  /** Print comment command */
209
  void toStreamCmdComment(std::ostream& out,
210
                          const std::string& comment) const override;
211
212
  /** Print declare-heap command */
213
  void toStreamCmdDeclareHeap(std::ostream& out,
214
                              TypeNode locType,
215
                              TypeNode dataType) const override;
216
217
  /** Print command sequence command */
218
  void toStreamCmdCommandSequence(
219
      std::ostream& out, const std::vector<Command*>& sequence) const override;
220
221
  /** Print declaration sequence command */
222
  void toStreamCmdDeclarationSequence(
223
      std::ostream& out, const std::vector<Command*>& sequence) const override;
224
225
  /**
226
   * Get the string for a kind k, which returns how the kind k is printed in
227
   * the SMT-LIB format (with variant v).
228
   */
229
  static std::string smtKindString(Kind k, Variant v = smt2_6_variant);
230
231
 private:
232
  /**
233
   * The main printing method for nodes n.
234
   */
235
  void toStream(std::ostream& out,
236
                TNode n,
237
                int toDepth,
238
                LetBinding* lbind = nullptr) const;
239
  /**
240
   * To stream, with a forced type. This method is used in some corner cases
241
   * to force a node n to be printed as if it had type tn. This is used e.g.
242
   * for the body of define-fun commands and arguments of singleton terms.
243
   */
244
  void toStreamCastToType(std::ostream& out,
245
                          TNode n,
246
                          int toDepth,
247
                          TypeNode tn) const;
248
  void toStream(std::ostream& out, const DType& dt) const;
249
  /**
250
   * To stream model sort. This prints the appropriate output for type
251
   * tn declared via declare-sort or declare-datatype.
252
   */
253
  void toStreamModelSort(std::ostream& out,
254
                         const smt::Model& m,
255
                         TypeNode tn) const override;
256
257
  /**
258
   * To stream model term. This prints the appropriate output for term
259
   * n declared via declare-fun.
260
   */
261
  void toStreamModelTerm(std::ostream& out,
262
                         const smt::Model& m,
263
                         Node n) const override;
264
265
  /**
266
   * To stream with let binding. This prints n, possibly in the scope
267
   * of letification generated by this method based on lbind.
268
   */
269
  void toStreamWithLetify(std::ostream& out,
270
                          Node n,
271
                          int toDepth,
272
                          LetBinding* lbind) const;
273
  Variant d_variant;
274
}; /* class Smt2Printer */
275
276
}  // namespace smt2
277
}  // namespace printer
278
}  // namespace CVC4
279
280
#endif /* CVC4__PRINTER__SMT2_PRINTER_H */