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

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