GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/util/result.cpp Lines: 124 198 62.6 %
Date: 2021-03-22 Branches: 79 228 34.6 %

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