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