GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/smt/dump.cpp Lines: 51 73 69.9 %
Date: 2021-03-22 Branches: 47 130 36.2 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file dump.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andres Noetzli, Morgan Deters, 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 Dump utility classes and functions
13
 **
14
 ** Dump utility classes and functions.
15
 **/
16
17
#include "smt/dump.h"
18
19
#include "base/configuration.h"
20
#include "base/output.h"
21
#include "lib/strtok_r.h"
22
#include "preprocessing/preprocessing_pass_registry.h"
23
#include "smt/command.h"
24
#include "smt/node_command.h"
25
26
namespace CVC4 {
27
28
#if defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE)
29
30
671
CVC4dumpstream& CVC4dumpstream::operator<<(const Command& c)
31
{
32
671
  if (d_os != nullptr)
33
  {
34
    (*d_os) << c;
35
  }
36
671
  return *this;
37
}
38
39
12
CVC4dumpstream& CVC4dumpstream::operator<<(const NodeCommand& nc)
40
{
41
12
  if (d_os != nullptr)
42
  {
43
12
    (*d_os) << nc;
44
  }
45
12
  return *this;
46
}
47
48
#else
49
50
CVC4dumpstream& CVC4dumpstream::operator<<(const Command& c) { return *this; }
51
CVC4dumpstream& CVC4dumpstream::operator<<(const NodeCommand& nc)
52
{
53
  return *this;
54
}
55
56
#endif /* CVC4_DUMPING && !CVC4_MUZZLE */
57
58
8892
DumpC DumpChannel;
59
60
std::ostream& DumpC::setStream(std::ostream* os) {
61
  ::CVC4::DumpOutChannel.setStream(os);
62
  return *os;
63
}
64
2711
std::ostream& DumpC::getStream() { return ::CVC4::DumpOutChannel.getStream(); }
65
9599
std::ostream* DumpC::getStreamPointer() { return ::CVC4::DumpOutChannel.getStreamPointer(); }
66
67
68
3
void DumpC::setDumpFromString(const std::string& optarg) {
69
3
  if (Configuration::isDumpingBuild())
70
  {
71
    // Make a copy of optarg for strtok_r to use.
72
6
    std::string optargCopy = optarg;
73
3
    char* optargPtr = const_cast<char*>(optargCopy.c_str());
74
3
    char* tokstr = optargPtr;
75
    char* toksave;
76
7
    while ((optargPtr = strtok_r(tokstr, ",", &toksave)) != NULL)
77
    {
78
3
      tokstr = NULL;
79
3
      if (!strcmp(optargPtr, "raw-benchmark"))
80
      {
81
      }
82
2
      else if (!strcmp(optargPtr, "benchmark"))
83
      {
84
      }
85
2
      else if (!strcmp(optargPtr, "declarations"))
86
      {
87
      }
88
2
      else if (!strcmp(optargPtr, "assertions"))
89
      {
90
        Dump.on("assertions:post-everything");
91
      }
92
2
      else if (!strncmp(optargPtr, "assertions:", 11))
93
      {
94
1
        const char* p = optargPtr + 11;
95
1
        if (!strncmp(p, "pre-", 4))
96
        {
97
          p += 4;
98
        }
99
1
        else if (!strncmp(p, "post-", 5))
100
        {
101
1
          p += 5;
102
        }
103
        else
104
        {
105
          throw OptionException(std::string("don't know how to dump `")
106
                                + optargPtr
107
                                + "'.  Please consult --dump help.");
108
        }
109
        // hard-coded cases
110
1
        if (!strcmp(p, "everything") || !strcmp(p, "definition-expansion")
111
1
            || !strcmp(p, "simplify") || !strcmp(p, "repeat-simplify"))
112
        {
113
        }
114
2
        else if (preprocessing::PreprocessingPassRegistry::getInstance()
115
1
                     .hasPass(p))
116
        {
117
        }
118
        else
119
        {
120
          throw OptionException(std::string("don't know how to dump `")
121
                                + optargPtr
122
                                + "'.  Please consult --dump help.");
123
        }
124
1
        Dump.on("assertions");
125
      }
126
1
      else if (!strcmp(optargPtr, "skolems"))
127
      {
128
      }
129
1
      else if (!strcmp(optargPtr, "clauses"))
130
      {
131
      }
132
1
      else if (!strcmp(optargPtr, "t-conflicts")
133
1
               || !strcmp(optargPtr, "t-lemmas")
134
1
               || !strcmp(optargPtr, "t-explanations")
135
1
               || !strcmp(optargPtr, "bv-rewrites")
136
1
               || !strcmp(optargPtr, "theory::fullcheck"))
137
      {
138
      }
139
1
      else if (!strcmp(optargPtr, "help"))
140
      {
141
        puts(s_dumpHelp.c_str());
142
143
        std::stringstream ss;
144
        ss << "Available preprocessing passes:\n";
145
        for (const std::string& pass :
146
             preprocessing::PreprocessingPassRegistry::getInstance()
147
                 .getAvailablePasses())
148
        {
149
          ss << "- " << pass << "\n";
150
        }
151
        puts(ss.str().c_str());
152
        exit(1);
153
      }
154
      else
155
      {
156
2
        throw OptionException(std::string("unknown option for --dump: `")
157
3
                              + optargPtr + "'.  Try --dump help.");
158
      }
159
160
2
      Dump.on(optargPtr);
161
2
      Dump.on("benchmark");
162
2
      if (strcmp(optargPtr, "benchmark"))
163
      {
164
2
        Dump.on("declarations");
165
2
        if (strcmp(optargPtr, "declarations")
166
2
            && strcmp(optargPtr, "raw-benchmark"))
167
        {
168
1
          Dump.on("skolems");
169
        }
170
      }
171
    }
172
  }
173
  else
174
  {
175
    throw OptionException(
176
        "The dumping feature was disabled in this build of CVC4.");
177
  }
178
2
}
179
180
8892
const std::string DumpC::s_dumpHelp =
181
    "\
182
Dump modes currently supported by the --dump option:\n\
183
\n\
184
benchmark\n\
185
+ Dump the benchmark structure (set-logic, push/pop, queries, etc.), but\n\
186
  does not include any declarations or assertions.  Implied by all following\n\
187
  modes.\n\
188
\n\
189
declarations\n\
190
+ Dump user declarations.  Implied by all following modes.\n\
191
\n\
192
raw-benchmark\n\
193
+ Dump all user-commands as they are received (including assertions) without\n\
194
  any preprocessing and without any internally-created commands.\n\
195
\n\
196
skolems\n\
197
+ Dump internally-created skolem variable declarations.  These can\n\
198
  arise from preprocessing simplifications, existential elimination,\n\
199
  and a number of other things.  Implied by all following modes.\n\
200
\n\
201
assertions\n\
202
+ Output the assertions after preprocessing and before clausification.\n\
203
  Can also specify \"assertions:pre-PASS\" or \"assertions:post-PASS\",\n\
204
  where PASS is one of the preprocessing passes: definition-expansion\n\
205
  boolean-terms constrain-subtypes substitution bv-to-bool bool-to-bv\n\
206
  strings-pp skolem-quant simplify static-learning ite-removal\n\
207
  repeat-simplify rewrite-apply-to-const theory-preprocessing.\n\
208
  PASS can also be the special value \"everything\", in which case the\n\
209
  assertions are printed before any preprocessing (with\n\
210
  \"assertions:pre-everything\") or after all preprocessing completes\n\
211
  (with \"assertions:post-everything\").\n\
212
\n\
213
clauses\n\
214
+ Do all the preprocessing outlined above, and dump the CNF-converted\n\
215
  output\n\
216
\n\
217
t-conflicts\n\
218
+ Output correctness queries for all theory conflicts\n\
219
\n\
220
t-lemmas\n\
221
+ Output correctness queries for all theory lemmas\n\
222
\n\
223
t-explanations\n\
224
+ Output correctness queries for all theory explanations\n\
225
\n\
226
bv-rewrites\n\
227
+ Output correctness queries for all bitvector rewrites\n\
228
\n\
229
theory::fullcheck\n\
230
+ Output completeness queries for all full-check effort-level theory checks\n\
231
\n\
232
Dump modes can be combined by concatenating the above values with \",\" in\n\
233
between them.  Generally you want raw-benchmark or, alternatively, one from\n\
234
the assertions category (either assertions or clauses), and perhaps one or more\n\
235
other modes for checking correctness and completeness of decision procedure\n\
236
implementations.\n\
237
\n\
238
The --output-language option controls the language used for dumping, and\n\
239
this allows you to connect CVC4 to another solver implementation via a UNIX\n\
240
pipe to perform on-line checking.  The --dump-to option can be used to dump\n\
241
to a file.\n\
242
";
243
244
26676
}/* CVC4 namespace */