Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/util/result.cpp	Lines:	122	196	62.2 %
Date:	2021-09-07	Branches:	79	228	34.6 %


/******************************************************************************
 * Top contributors (to current version):
 *   Aina Niemetz, Morgan Deters, Tim King
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * Encapsulation of the result of a query.
 */
#include "util/result.h"

#include <algorithm>
#include <cctype>
#include <iostream>
#include <sstream>
#include <string>

#include "base/check.h"
#include "options/set_language.h"

using namespace std;

namespace cvc5 {

Result::Result()
    : d_sat(SAT_UNKNOWN),
      d_entailment(ENTAILMENT_UNKNOWN),
      d_which(TYPE_NONE),
      d_unknownExplanation(UNKNOWN_REASON),
      d_inputName("")
{
}

Result::Result(enum Sat s, std::string inputName)
    : d_sat(s),
      d_entailment(ENTAILMENT_UNKNOWN),
      d_which(TYPE_SAT),
      d_unknownExplanation(UNKNOWN_REASON),
      d_inputName(inputName)
{
  PrettyCheckArgument(s != SAT_UNKNOWN,
                      "Must provide a reason for satisfiability being unknown");
}

Result::Result(enum Entailment e, std::string inputName)
    : d_sat(SAT_UNKNOWN),
      d_entailment(e),
      d_which(TYPE_ENTAILMENT),
      d_unknownExplanation(UNKNOWN_REASON),
      d_inputName(inputName)
{
  PrettyCheckArgument(e != ENTAILMENT_UNKNOWN,
                      "Must provide a reason for entailment being unknown");
}

Result::Result(enum Sat s,
               enum UnknownExplanation unknownExplanation,
               std::string inputName)
    : d_sat(s),
      d_entailment(ENTAILMENT_UNKNOWN),
      d_which(TYPE_SAT),
      d_unknownExplanation(unknownExplanation),
      d_inputName(inputName)
{
  PrettyCheckArgument(s == SAT_UNKNOWN,
                      "improper use of unknown-result constructor");
}

Result::Result(enum Entailment e,
               enum UnknownExplanation unknownExplanation,
               std::string inputName)
    : d_sat(SAT_UNKNOWN),
      d_entailment(e),
      d_which(TYPE_ENTAILMENT),
      d_unknownExplanation(unknownExplanation),
      d_inputName(inputName)
{
  PrettyCheckArgument(e == ENTAILMENT_UNKNOWN,
                      "improper use of unknown-result constructor");
}

Result::Result(const std::string& instr, std::string inputName)
    : d_sat(SAT_UNKNOWN),
      d_entailment(ENTAILMENT_UNKNOWN),
      d_which(TYPE_NONE),
      d_unknownExplanation(UNKNOWN_REASON),
      d_inputName(inputName)
{
  string s = instr;
  transform(s.begin(), s.end(), s.begin(), ::tolower);
  if (s == "sat" || s == "satisfiable") {
    d_which = TYPE_SAT;
    d_sat = SAT;
  } else if (s == "unsat" || s == "unsatisfiable") {
    d_which = TYPE_SAT;
    d_sat = UNSAT;
  }
  else if (s == "entailed")
  {
    d_which = TYPE_ENTAILMENT;
    d_entailment = ENTAILED;
  }
  else if (s == "not_entailed")
  {
    d_which = TYPE_ENTAILMENT;
    d_entailment = NOT_ENTAILED;
  }
  else if (s == "incomplete")
  {
    d_which = TYPE_SAT;
    d_sat = SAT_UNKNOWN;
    d_unknownExplanation = INCOMPLETE;
  }
  else if (s == "timeout")
  {
    d_which = TYPE_SAT;
    d_sat = SAT_UNKNOWN;
    d_unknownExplanation = TIMEOUT;
  }
  else if (s == "resourceout")
  {
    d_which = TYPE_SAT;
    d_sat = SAT_UNKNOWN;
    d_unknownExplanation = RESOURCEOUT;
  }
  else if (s == "memout")
  {
    d_which = TYPE_SAT;
    d_sat = SAT_UNKNOWN;
    d_unknownExplanation = MEMOUT;
  }
  else if (s == "interrupted")
  {
    d_which = TYPE_SAT;
    d_sat = SAT_UNKNOWN;
    d_unknownExplanation = INTERRUPTED;
  }
  else if (s.size() >= 7 && s.compare(0, 7, "unknown") == 0)
  {
    d_which = TYPE_SAT;
    d_sat = SAT_UNKNOWN;
  }
  else
  {
    IllegalArgument(s,
                    "expected satisfiability/entailment result, "
                    "instead got `%s'",
                    s.c_str());
  }
}

Result::UnknownExplanation Result::whyUnknown() const {
  PrettyCheckArgument(isUnknown(), this,
                      "This result is not unknown, so the reason for "
                      "being unknown cannot be inquired of it");
  return d_unknownExplanation;
}

bool Result::operator==(const Result& r) const {
  if (d_which != r.d_which) {
    return false;
  }
  if (d_which == TYPE_SAT) {
    return d_sat == r.d_sat && (d_sat != SAT_UNKNOWN ||
                                d_unknownExplanation == r.d_unknownExplanation);
  }
  if (d_which == TYPE_ENTAILMENT)
  {
    return d_entailment == r.d_entailment
           && (d_entailment != ENTAILMENT_UNKNOWN
               || d_unknownExplanation == r.d_unknownExplanation);
  }
  return false;
}

bool operator==(enum Result::Sat sr, const Result& r) { return r == sr; }

bool operator==(enum Result::Entailment e, const Result& r) { return r == e; }
bool operator!=(enum Result::Sat s, const Result& r) { return !(s == r); }
bool operator!=(enum Result::Entailment e, const Result& r)
{
  return !(e == r);
}

Result Result::asSatisfiabilityResult() const {
  if (d_which == TYPE_SAT) {
    return *this;
  }

  if (d_which == TYPE_ENTAILMENT)
  {
    switch (d_entailment)
    {
      case NOT_ENTAILED: return Result(SAT, d_inputName);

      case ENTAILED: return Result(UNSAT, d_inputName);

      case ENTAILMENT_UNKNOWN:
        return Result(SAT_UNKNOWN, d_unknownExplanation, d_inputName);

      default: Unhandled() << d_entailment;
    }
  }

  // TYPE_NONE
  return Result(SAT_UNKNOWN, NO_STATUS, d_inputName);
}

Result Result::asEntailmentResult() const
{
  if (d_which == TYPE_ENTAILMENT)
  {
    return *this;
  }

  if (d_which == TYPE_SAT) {
    switch (d_sat) {
      case SAT: return Result(NOT_ENTAILED, d_inputName);

      case UNSAT: return Result(ENTAILED, d_inputName);

      case SAT_UNKNOWN:
        return Result(ENTAILMENT_UNKNOWN, d_unknownExplanation, d_inputName);

      default: Unhandled() << d_sat;
    }
  }

  // TYPE_NONE
  return Result(ENTAILMENT_UNKNOWN, NO_STATUS, d_inputName);
}

string Result::toString() const {
  stringstream ss;
  ss << *this;
  return ss.str();
}

ostream& operator<<(ostream& out, enum Result::Sat s) {
  switch (s) {
    case Result::UNSAT:
      out << "UNSAT";
      break;
    case Result::SAT:
      out << "SAT";
      break;
    case Result::SAT_UNKNOWN:
      out << "SAT_UNKNOWN";
      break;
    default: Unhandled() << s;
  }
  return out;
}

ostream& operator<<(ostream& out, enum Result::Entailment e)
{
  switch (e)
  {
    case Result::NOT_ENTAILED: out << "NOT_ENTAILED"; break;
    case Result::ENTAILED: out << "ENTAILED"; break;
    case Result::ENTAILMENT_UNKNOWN: out << "ENTAILMENT_UNKNOWN"; break;
    default: Unhandled() << e;
  }
  return out;
}

ostream& operator<<(ostream& out, enum Result::UnknownExplanation e)
{
  switch (e)
  {
    case Result::REQUIRES_FULL_CHECK: out << "REQUIRES_FULL_CHECK"; break;
    case Result::INCOMPLETE: out << "INCOMPLETE"; break;
    case Result::TIMEOUT: out << "TIMEOUT"; break;
    case Result::RESOURCEOUT: out << "RESOURCEOUT"; break;
    case Result::MEMOUT: out << "MEMOUT"; break;
    case Result::INTERRUPTED: out << "INTERRUPTED"; break;
    case Result::NO_STATUS: out << "NO_STATUS"; break;
    case Result::UNSUPPORTED: out << "UNSUPPORTED"; break;
    case Result::OTHER: out << "OTHER"; break;
    case Result::UNKNOWN_REASON: out << "UNKNOWN_REASON"; break;
    default: Unhandled() << e;
  }
  return out;
}

ostream& operator<<(ostream& out, const Result& r) {
  r.toStream(out, language::SetLanguage::getLanguage(out));
  return out;
} /* operator<<(ostream&, const Result&) */

void Result::toStreamDefault(std::ostream& out) const {
  if (getType() == Result::TYPE_SAT) {
    switch (isSat()) {
      case Result::UNSAT:
        out << "unsat";
        break;
      case Result::SAT:
        out << "sat";
        break;
      case Result::SAT_UNKNOWN:
        out << "unknown";
        if (whyUnknown() != Result::UNKNOWN_REASON) {
          out << " (" << whyUnknown() << ")";
        }
        break;
    }
  } else {
    switch (isEntailed())
    {
      case Result::NOT_ENTAILED: out << "not_entailed"; break;
      case Result::ENTAILED: out << "entailed"; break;
      case Result::ENTAILMENT_UNKNOWN:
        out << "unknown";
        if (whyUnknown() != Result::UNKNOWN_REASON) {
          out << " (" << whyUnknown() << ")";
        }
        break;
    }
  }
} /* Result::toStreamDefault() */

void Result::toStreamSmt2(ostream& out) const {
  if (getType() == Result::TYPE_SAT && isSat() == Result::SAT_UNKNOWN) {
    out << "unknown";
  } else {
    toStreamDefault(out);
  }
}

void Result::toStreamTptp(std::ostream& out) const {
  out << "% SZS status ";
  if (isSat() == Result::SAT) {
    out << "Satisfiable";
  } else if (isSat() == Result::UNSAT) {
    out << "Unsatisfiable";
  }
  else if (isEntailed() == Result::ENTAILED)
  {
    out << "Theorem";
  }
  else if (isEntailed() == Result::NOT_ENTAILED)
  {
    out << "CounterSatisfiable";
  }
  else
  {
    out << "GaveUp";
  }
  out << " for " << getInputName();
}

void Result::toStream(std::ostream& out, Language language) const
{
  switch (language) {
    case Language::LANG_SYGUS_V2: toStreamSmt2(out); break;
    case Language::LANG_TPTP: toStreamTptp(out); break;
    default:
      if (language::isLangSmt2(language))
      {
        toStreamSmt2(out);
      }
      else
      {
        toStreamDefault(out);
      }
      break;
  };
}

}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

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