1 /********************* */
2 /*! \file result.cpp
3 ** \verbatim
4 ** Top contributors (to current version):
5 ** Tim King, Morgan Deters, Andrew Reynolds
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2019 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 Encapsulation of the result of a query.
13 **
14 ** Encapsulation of the result of a query.
15 **/
16 #include "util/result.h"
17
18 #include <algorithm>
19 #include <cctype>
20 #include <iostream>
21 #include <string>
22
23 #include "base/cvc4_assert.h"
24 #include "options/set_language.h"
25
26 using namespace std;
27
28 namespace CVC4 {
29
Result()30 Result::Result()
31 : d_sat(SAT_UNKNOWN),
32 d_validity(VALIDITY_UNKNOWN),
33 d_which(TYPE_NONE),
34 d_unknownExplanation(UNKNOWN_REASON),
35 d_inputName("") {}
36
Result(enum Sat s,std::string inputName)37 Result::Result(enum Sat s, std::string inputName)
38 : d_sat(s),
39 d_validity(VALIDITY_UNKNOWN),
40 d_which(TYPE_SAT),
41 d_unknownExplanation(UNKNOWN_REASON),
42 d_inputName(inputName) {
43 PrettyCheckArgument(s != SAT_UNKNOWN,
44 "Must provide a reason for satisfiability being unknown");
45 }
46
Result(enum Validity v,std::string inputName)47 Result::Result(enum Validity v, std::string inputName)
48 : d_sat(SAT_UNKNOWN),
49 d_validity(v),
50 d_which(TYPE_VALIDITY),
51 d_unknownExplanation(UNKNOWN_REASON),
52 d_inputName(inputName) {
53 PrettyCheckArgument(v != VALIDITY_UNKNOWN,
54 "Must provide a reason for validity being unknown");
55 }
56
Result(enum Sat s,enum UnknownExplanation unknownExplanation,std::string inputName)57 Result::Result(enum Sat s, enum UnknownExplanation unknownExplanation,
58 std::string inputName)
59 : d_sat(s),
60 d_validity(VALIDITY_UNKNOWN),
61 d_which(TYPE_SAT),
62 d_unknownExplanation(unknownExplanation),
63 d_inputName(inputName) {
64 PrettyCheckArgument(s == SAT_UNKNOWN,
65 "improper use of unknown-result constructor");
66 }
67
Result(enum Validity v,enum UnknownExplanation unknownExplanation,std::string inputName)68 Result::Result(enum Validity v, enum UnknownExplanation unknownExplanation,
69 std::string inputName)
70 : d_sat(SAT_UNKNOWN),
71 d_validity(v),
72 d_which(TYPE_VALIDITY),
73 d_unknownExplanation(unknownExplanation),
74 d_inputName(inputName) {
75 PrettyCheckArgument(v == VALIDITY_UNKNOWN,
76 "improper use of unknown-result constructor");
77 }
78
Result(const std::string & instr,std::string inputName)79 Result::Result(const std::string& instr, std::string inputName)
80 : d_sat(SAT_UNKNOWN),
81 d_validity(VALIDITY_UNKNOWN),
82 d_which(TYPE_NONE),
83 d_unknownExplanation(UNKNOWN_REASON),
84 d_inputName(inputName) {
85 string s = instr;
86 transform(s.begin(), s.end(), s.begin(), ::tolower);
87 if (s == "sat" || s == "satisfiable") {
88 d_which = TYPE_SAT;
89 d_sat = SAT;
90 } else if (s == "unsat" || s == "unsatisfiable") {
91 d_which = TYPE_SAT;
92 d_sat = UNSAT;
93 } else if (s == "valid") {
94 d_which = TYPE_VALIDITY;
95 d_validity = VALID;
96 } else if (s == "invalid") {
97 d_which = TYPE_VALIDITY;
98 d_validity = INVALID;
99 } else if (s == "incomplete") {
100 d_which = TYPE_SAT;
101 d_sat = SAT_UNKNOWN;
102 d_unknownExplanation = INCOMPLETE;
103 } else if (s == "timeout") {
104 d_which = TYPE_SAT;
105 d_sat = SAT_UNKNOWN;
106 d_unknownExplanation = TIMEOUT;
107 } else if (s == "resourceout") {
108 d_which = TYPE_SAT;
109 d_sat = SAT_UNKNOWN;
110 d_unknownExplanation = RESOURCEOUT;
111 } else if (s == "memout") {
112 d_which = TYPE_SAT;
113 d_sat = SAT_UNKNOWN;
114 d_unknownExplanation = MEMOUT;
115 } else if (s == "interrupted") {
116 d_which = TYPE_SAT;
117 d_sat = SAT_UNKNOWN;
118 d_unknownExplanation = INTERRUPTED;
119 } else if (s.size() >= 7 && s.compare(0, 7, "unknown") == 0) {
120 d_which = TYPE_SAT;
121 d_sat = SAT_UNKNOWN;
122 } else {
123 IllegalArgument(s,
124 "expected satisfiability/validity result, "
125 "instead got `%s'",
126 s.c_str());
127 }
128 }
129
whyUnknown() const130 Result::UnknownExplanation Result::whyUnknown() const {
131 PrettyCheckArgument(isUnknown(), this,
132 "This result is not unknown, so the reason for "
133 "being unknown cannot be inquired of it");
134 return d_unknownExplanation;
135 }
136
operator ==(const Result & r) const137 bool Result::operator==(const Result& r) const {
138 if (d_which != r.d_which) {
139 return false;
140 }
141 if (d_which == TYPE_SAT) {
142 return d_sat == r.d_sat && (d_sat != SAT_UNKNOWN ||
143 d_unknownExplanation == r.d_unknownExplanation);
144 }
145 if (d_which == TYPE_VALIDITY) {
146 return d_validity == r.d_validity &&
147 (d_validity != VALIDITY_UNKNOWN ||
148 d_unknownExplanation == r.d_unknownExplanation);
149 }
150 return false;
151 }
152
operator ==(enum Result::Sat sr,const Result & r)153 bool operator==(enum Result::Sat sr, const Result& r) { return r == sr; }
154
operator ==(enum Result::Validity vr,const Result & r)155 bool operator==(enum Result::Validity vr, const Result& r) { return r == vr; }
operator !=(enum Result::Sat s,const Result & r)156 bool operator!=(enum Result::Sat s, const Result& r) { return !(s == r); }
operator !=(enum Result::Validity v,const Result & r)157 bool operator!=(enum Result::Validity v, const Result& r) { return !(v == r); }
158
asSatisfiabilityResult() const159 Result Result::asSatisfiabilityResult() const {
160 if (d_which == TYPE_SAT) {
161 return *this;
162 }
163
164 if (d_which == TYPE_VALIDITY) {
165 switch (d_validity) {
166 case INVALID:
167 return Result(SAT, d_inputName);
168
169 case VALID:
170 return Result(UNSAT, d_inputName);
171
172 case VALIDITY_UNKNOWN:
173 return Result(SAT_UNKNOWN, d_unknownExplanation, d_inputName);
174
175 default:
176 Unhandled(d_validity);
177 }
178 }
179
180 // TYPE_NONE
181 return Result(SAT_UNKNOWN, NO_STATUS, d_inputName);
182 }
183
asValidityResult() const184 Result Result::asValidityResult() const {
185 if (d_which == TYPE_VALIDITY) {
186 return *this;
187 }
188
189 if (d_which == TYPE_SAT) {
190 switch (d_sat) {
191 case SAT:
192 return Result(INVALID, d_inputName);
193
194 case UNSAT:
195 return Result(VALID, d_inputName);
196
197 case SAT_UNKNOWN:
198 return Result(VALIDITY_UNKNOWN, d_unknownExplanation, d_inputName);
199
200 default:
201 Unhandled(d_sat);
202 }
203 }
204
205 // TYPE_NONE
206 return Result(VALIDITY_UNKNOWN, NO_STATUS, d_inputName);
207 }
208
toString() const209 string Result::toString() const {
210 stringstream ss;
211 ss << *this;
212 return ss.str();
213 }
214
operator <<(ostream & out,enum Result::Sat s)215 ostream& operator<<(ostream& out, enum Result::Sat s) {
216 switch (s) {
217 case Result::UNSAT:
218 out << "UNSAT";
219 break;
220 case Result::SAT:
221 out << "SAT";
222 break;
223 case Result::SAT_UNKNOWN:
224 out << "SAT_UNKNOWN";
225 break;
226 default:
227 Unhandled(s);
228 }
229 return out;
230 }
231
operator <<(ostream & out,enum Result::Validity v)232 ostream& operator<<(ostream& out, enum Result::Validity v) {
233 switch (v) {
234 case Result::INVALID:
235 out << "INVALID";
236 break;
237 case Result::VALID:
238 out << "VALID";
239 break;
240 case Result::VALIDITY_UNKNOWN:
241 out << "VALIDITY_UNKNOWN";
242 break;
243 default:
244 Unhandled(v);
245 }
246 return out;
247 }
248
operator <<(ostream & out,enum Result::UnknownExplanation e)249 ostream& operator<<(ostream& out, enum Result::UnknownExplanation e) {
250 switch (e) {
251 case Result::REQUIRES_FULL_CHECK:
252 out << "REQUIRES_FULL_CHECK";
253 break;
254 case Result::INCOMPLETE:
255 out << "INCOMPLETE";
256 break;
257 case Result::TIMEOUT:
258 out << "TIMEOUT";
259 break;
260 case Result::RESOURCEOUT:
261 out << "RESOURCEOUT";
262 break;
263 case Result::MEMOUT:
264 out << "MEMOUT";
265 break;
266 case Result::INTERRUPTED:
267 out << "INTERRUPTED";
268 break;
269 case Result::NO_STATUS:
270 out << "NO_STATUS";
271 break;
272 case Result::UNSUPPORTED:
273 out << "UNSUPPORTED";
274 break;
275 case Result::OTHER:
276 out << "OTHER";
277 break;
278 case Result::UNKNOWN_REASON:
279 out << "UNKNOWN_REASON";
280 break;
281 default:
282 Unhandled(e);
283 }
284 return out;
285 }
286
operator <<(ostream & out,const Result & r)287 ostream& operator<<(ostream& out, const Result& r) {
288 r.toStream(out, language::SetLanguage::getLanguage(out));
289 return out;
290 } /* operator<<(ostream&, const Result&) */
291
toStreamDefault(std::ostream & out) const292 void Result::toStreamDefault(std::ostream& out) const {
293 if (getType() == Result::TYPE_SAT) {
294 switch (isSat()) {
295 case Result::UNSAT:
296 out << "unsat";
297 break;
298 case Result::SAT:
299 out << "sat";
300 break;
301 case Result::SAT_UNKNOWN:
302 out << "unknown";
303 if (whyUnknown() != Result::UNKNOWN_REASON) {
304 out << " (" << whyUnknown() << ")";
305 }
306 break;
307 }
308 } else {
309 switch (isValid()) {
310 case Result::INVALID:
311 out << "invalid";
312 break;
313 case Result::VALID:
314 out << "valid";
315 break;
316 case Result::VALIDITY_UNKNOWN:
317 out << "unknown";
318 if (whyUnknown() != Result::UNKNOWN_REASON) {
319 out << " (" << whyUnknown() << ")";
320 }
321 break;
322 }
323 }
324 } /* Result::toStreamDefault() */
325
toStreamSmt2(ostream & out) const326 void Result::toStreamSmt2(ostream& out) const {
327 if (getType() == Result::TYPE_SAT && isSat() == Result::SAT_UNKNOWN) {
328 out << "unknown";
329 } else {
330 toStreamDefault(out);
331 }
332 }
333
toStreamTptp(std::ostream & out) const334 void Result::toStreamTptp(std::ostream& out) const {
335 out << "% SZS status ";
336 if (isSat() == Result::SAT) {
337 out << "Satisfiable";
338 } else if (isSat() == Result::UNSAT) {
339 out << "Unsatisfiable";
340 } else if (isValid() == Result::VALID) {
341 out << "Theorem";
342 } else if (isValid() == Result::INVALID) {
343 out << "CounterSatisfiable";
344 } else {
345 out << "GaveUp";
346 }
347 out << " for " << getInputName();
348 }
349
toStream(std::ostream & out,OutputLanguage language) const350 void Result::toStream(std::ostream& out, OutputLanguage language) const {
351 switch (language) {
352 case language::output::LANG_SYGUS:
353 toStreamSmt2(out);
354 break;
355 case language::output::LANG_TPTP:
356 toStreamTptp(out);
357 break;
358 default:
359 if (language::isOutputLang_smt2(language))
360 {
361 toStreamSmt2(out);
362 }
363 else
364 {
365 toStreamDefault(out);
366 }
367 break;
368 };
369 }
370
371 } /* CVC4 namespace */
372