Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/util/result.h	Lines:	14	14	100.0 %
Date:	2021-09-13	Branches:	9	12	75.0 %


/******************************************************************************
 * Top contributors (to current version):
 *   Morgan Deters, Tim King, Aina Niemetz
 *
 * 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 "cvc5_public.h"

#ifndef CVC5__RESULT_H
#define CVC5__RESULT_H

#include <iosfwd>
#include <string>

#include "options/language.h"

namespace cvc5 {

class Result;

std::ostream& operator<<(std::ostream& out, const Result& r);

/**
 * Three-valued SMT result, with optional explanation.
 */
class Result
{
 public:
  enum Sat { UNSAT = 0, SAT = 1, SAT_UNKNOWN = 2 };

  enum Entailment
  {
    NOT_ENTAILED = 0,
    ENTAILED = 1,
    ENTAILMENT_UNKNOWN = 2
  };

  enum Type
  {
    TYPE_SAT,
    TYPE_ENTAILMENT,
    TYPE_NONE
  };

  enum UnknownExplanation
  {
    REQUIRES_FULL_CHECK,
    INCOMPLETE,
    TIMEOUT,
    RESOURCEOUT,
    MEMOUT,
    INTERRUPTED,
    NO_STATUS,
    UNSUPPORTED,
    OTHER,
    UNKNOWN_REASON
  };

 private:
  enum Sat d_sat;
  enum Entailment d_entailment;
  enum Type d_which;
  enum UnknownExplanation d_unknownExplanation;
  std::string d_inputName;

 public:
  Result();

  Result(enum Sat s, std::string inputName = "");

  Result(enum Entailment v, std::string inputName = "");

  Result(enum Sat s, enum UnknownExplanation unknownExplanation,
         std::string inputName = "");

  Result(enum Entailment v,
         enum UnknownExplanation unknownExplanation,
         std::string inputName = "");

  Result(const std::string& s, std::string inputName = "");

  Result(const Result& r, std::string inputName) {
    *this = r;
    d_inputName = inputName;
  }

  enum Sat isSat() const { return d_which == TYPE_SAT ? d_sat : SAT_UNKNOWN; }

  enum Entailment isEntailed() const
  {
    return d_which == TYPE_ENTAILMENT ? d_entailment : ENTAILMENT_UNKNOWN;
  }

  bool isUnknown() const {
    return isSat() == SAT_UNKNOWN && isEntailed() == ENTAILMENT_UNKNOWN;
  }

  Type getType() const { return d_which; }

  bool isNull() const { return d_which == TYPE_NONE; }

  enum UnknownExplanation whyUnknown() const;

  bool operator==(const Result& r) const;
  inline bool operator!=(const Result& r) const;
  Result asSatisfiabilityResult() const;
  Result asEntailmentResult() const;

  std::string toString() const;

  std::string getInputName() const { return d_inputName; }

  /**
   * Write a Result out to a stream in this language.
   */
  void toStream(std::ostream& out, Language language) const;

  /**
   * This is mostly the same the default
   * If getType() == Result::TYPE_SAT && isSat() == Result::SAT_UNKNOWN,
   *
   */
  void toStreamSmt2(std::ostream& out) const;

  /**
   * Write a Result out to a stream in the Tptp format
   */
  void toStreamTptp(std::ostream& out) const;

  /**
   * Write a Result out to a stream.
   *
   * The default implementation writes a reasonable string in lowercase
   * for sat, unsat, entailed, not entailed, or unknown results.  This behavior
   * is overridable by each Printer, since sometimes an output language
   * has a particular preference for how results should appear.
   */
  void toStreamDefault(std::ostream& out) const;
}; /* class Result */

inline bool Result::operator!=(const Result& r) const { return !(*this == r); }

std::ostream& operator<<(std::ostream& out, enum Result::Sat s);
std::ostream& operator<<(std::ostream& out, enum Result::Entailment e);
std::ostream& operator<<(std::ostream& out, enum Result::UnknownExplanation e);

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

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

}  // namespace cvc5

#endif /* CVC5__RESULT_H */


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Morgan Deters, Tim King, Aina Niemetz
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
16		#include "cvc5_public.h"
17
18		#ifndef CVC5__RESULT_H
19		#define CVC5__RESULT_H
20
21		#include <iosfwd>
22		#include <string>
23
24		#include "options/language.h"
25
26		namespace cvc5 {
27
28		class Result;
29
30		std::ostream& operator<<(std::ostream& out, const Result& r);
31
32		/**
33		* Three-valued SMT result, with optional explanation.
34		*/
35	910632	class Result
36		{
37		public:
38		enum Sat { UNSAT = 0, SAT = 1, SAT_UNKNOWN = 2 };
39
40		enum Entailment
41		{
42		NOT_ENTAILED = 0,
43		ENTAILED = 1,
44		ENTAILMENT_UNKNOWN = 2
45		};
46
47		enum Type
48		{
49		TYPE_SAT,
50		TYPE_ENTAILMENT,
51		TYPE_NONE
52		};
53
54		enum UnknownExplanation
55		{
56		REQUIRES_FULL_CHECK,
57		INCOMPLETE,
58		TIMEOUT,
59		RESOURCEOUT,
60		MEMOUT,
61		INTERRUPTED,
62		NO_STATUS,
63		UNSUPPORTED,
64		OTHER,
65		UNKNOWN_REASON
66		};
67
68		private:
69		enum Sat d_sat;
70		enum Entailment d_entailment;
71		enum Type d_which;
72		enum UnknownExplanation d_unknownExplanation;
73		std::string d_inputName;
74
75		public:
76		Result();
77
78		Result(enum Sat s, std::string inputName = "");
79
80		Result(enum Entailment v, std::string inputName = "");
81
82		Result(enum Sat s, enum UnknownExplanation unknownExplanation,
83		std::string inputName = "");
84
85		Result(enum Entailment v,
86		enum UnknownExplanation unknownExplanation,
87		std::string inputName = "");
88
89		Result(const std::string& s, std::string inputName = "");
90
91	15225	Result(const Result& r, std::string inputName) {
92	15225	*this = r;
93	15225	d_inputName = inputName;
94	15225	}
95
96	92400	enum Sat isSat() const { return d_which == TYPE_SAT ? d_sat : SAT_UNKNOWN; }
97
98	13935	enum Entailment isEntailed() const
99		{
100	13935	return d_which == TYPE_ENTAILMENT ? d_entailment : ENTAILMENT_UNKNOWN;
101		}
102
103	21228	bool isUnknown() const {
104	21228	return isSat() == SAT_UNKNOWN && isEntailed() == ENTAILMENT_UNKNOWN;
105		}
106
107	1205397	Type getType() const { return d_which; }
108
109	9	bool isNull() const { return d_which == TYPE_NONE; }
110
111		enum UnknownExplanation whyUnknown() const;
112
113		bool operator==(const Result& r) const;
114		inline bool operator!=(const Result& r) const;
115		Result asSatisfiabilityResult() const;
116		Result asEntailmentResult() const;
117
118		std::string toString() const;
119
120	40	std::string getInputName() const { return d_inputName; }
121
122		/**
123		* Write a Result out to a stream in this language.
124		*/
125		void toStream(std::ostream& out, Language language) const;
126
127		/**
128		* This is mostly the same the default
129		* If getType() == Result::TYPE_SAT && isSat() == Result::SAT_UNKNOWN,
130		*
131		*/
132		void toStreamSmt2(std::ostream& out) const;
133
134		/**
135		* Write a Result out to a stream in the Tptp format
136		*/
137		void toStreamTptp(std::ostream& out) const;
138
139		/**
140		* Write a Result out to a stream.
141		*
142		* The default implementation writes a reasonable string in lowercase
143		* for sat, unsat, entailed, not entailed, or unknown results. This behavior
144		* is overridable by each Printer, since sometimes an output language
145		* has a particular preference for how results should appear.
146		*/
147		void toStreamDefault(std::ostream& out) const;
148		}; /* class Result */
149
150	3618	inline bool Result::operator!=(const Result& r) const { return !(*this == r); }
151
152		std::ostream& operator<<(std::ostream& out, enum Result::Sat s);
153		std::ostream& operator<<(std::ostream& out, enum Result::Entailment e);
154		std::ostream& operator<<(std::ostream& out, enum Result::UnknownExplanation e);
155
156		bool operator==(enum Result::Sat s, const Result& r);
157		bool operator==(enum Result::Entailment e, const Result& r);
158
159		bool operator!=(enum Result::Sat s, const Result& r);
160		bool operator!=(enum Result::Entailment e, const Result& r);
161
162		} // namespace cvc5
163
164		#endif /* CVC5__RESULT_H */