cvc4-1.4
result.h
Go to the documentation of this file.
1 /********************* */
17 #include "cvc4_public.h"
18 
19 #ifndef __CVC4__RESULT_H
20 #define __CVC4__RESULT_H
21 
22 #include <iostream>
23 #include <string>
24 
25 #include "util/exception.h"
26 
27 namespace CVC4 {
28 
29 class Result;
30 
31 std::ostream& operator<<(std::ostream& out, const Result& r) CVC4_PUBLIC;
32 
36 class CVC4_PUBLIC Result {
37 public:
38  enum Sat {
39  UNSAT = 0,
40  SAT = 1,
41  SAT_UNKNOWN = 2
42  };
43 
44  enum Validity {
45  INVALID = 0,
46  VALID = 1,
47  VALIDITY_UNKNOWN = 2
48  };
49 
50  enum Type {
53  TYPE_NONE
54  };
55 
66  UNKNOWN_REASON
67  };
68 
69 private:
70  enum Sat d_sat;
71  enum Validity d_validity;
72  enum Type d_which;
73  enum UnknownExplanation d_unknownExplanation;
74  std::string d_inputName;
75 
76 public:
77  Result() :
78  d_sat(SAT_UNKNOWN),
79  d_validity(VALIDITY_UNKNOWN),
80  d_which(TYPE_NONE),
81  d_unknownExplanation(UNKNOWN_REASON),
82  d_inputName("") {
83  }
84  Result(enum Sat s, std::string inputName = "") :
85  d_sat(s),
86  d_validity(VALIDITY_UNKNOWN),
87  d_which(TYPE_SAT),
88  d_unknownExplanation(UNKNOWN_REASON),
89  d_inputName(inputName) {
90  CheckArgument(s != SAT_UNKNOWN,
91  "Must provide a reason for satisfiability being unknown");
92  }
93  Result(enum Validity v, std::string inputName = "") :
94  d_sat(SAT_UNKNOWN),
95  d_validity(v),
96  d_which(TYPE_VALIDITY),
97  d_unknownExplanation(UNKNOWN_REASON),
98  d_inputName(inputName) {
99  CheckArgument(v != VALIDITY_UNKNOWN,
100  "Must provide a reason for validity being unknown");
101  }
102  Result(enum Sat s, enum UnknownExplanation unknownExplanation, std::string inputName = "") :
103  d_sat(s),
104  d_validity(VALIDITY_UNKNOWN),
105  d_which(TYPE_SAT),
106  d_unknownExplanation(unknownExplanation),
107  d_inputName(inputName) {
108  CheckArgument(s == SAT_UNKNOWN,
109  "improper use of unknown-result constructor");
110  }
111  Result(enum Validity v, enum UnknownExplanation unknownExplanation, std::string inputName = "") :
112  d_sat(SAT_UNKNOWN),
113  d_validity(v),
114  d_which(TYPE_VALIDITY),
115  d_unknownExplanation(unknownExplanation),
116  d_inputName(inputName) {
117  CheckArgument(v == VALIDITY_UNKNOWN,
118  "improper use of unknown-result constructor");
119  }
120  Result(const std::string& s, std::string inputName = "");
121 
122  Result(const Result& r, std::string inputName) {
123  *this = r;
124  d_inputName = inputName;
125  }
126 
127  enum Sat isSat() const {
128  return d_which == TYPE_SAT ? d_sat : SAT_UNKNOWN;
129  }
130  enum Validity isValid() const {
131  return d_which == TYPE_VALIDITY ? d_validity : VALIDITY_UNKNOWN;
132  }
133  bool isUnknown() const {
134  return isSat() == SAT_UNKNOWN && isValid() == VALIDITY_UNKNOWN;
135  }
136  Type getType() const {
137  return d_which;
138  }
139  bool isNull() const {
140  return d_which == TYPE_NONE;
141  }
142  enum UnknownExplanation whyUnknown() const {
143  CheckArgument( isUnknown(), this,
144  "This result is not unknown, so the reason for "
145  "being unknown cannot be inquired of it" );
146  return d_unknownExplanation;
147  }
148 
149  bool operator==(const Result& r) const throw();
150  inline bool operator!=(const Result& r) const throw();
151  Result asSatisfiabilityResult() const throw();
152  Result asValidityResult() const throw();
153 
154  std::string toString() const;
155 
156  std::string getInputName() const { return d_inputName; }
157 
158 };/* class Result */
159 
160 inline bool Result::operator!=(const Result& r) const throw() {
161  return !(*this == r);
162 }
163 
164 std::ostream& operator<<(std::ostream& out,
165  enum Result::Sat s) CVC4_PUBLIC;
166 std::ostream& operator<<(std::ostream& out,
168 std::ostream& operator<<(std::ostream& out,
170 
171 bool operator==(enum Result::Sat s, const Result& r) throw() CVC4_PUBLIC;
172 bool operator==(enum Result::Validity v, const Result& r) throw() CVC4_PUBLIC;
173 
174 bool operator!=(enum Result::Sat s, const Result& r) throw() CVC4_PUBLIC;
175 bool operator!=(enum Result::Validity v, const Result& r) throw() CVC4_PUBLIC;
176 
177 }/* CVC4 namespace */
178 
179 #endif /* __CVC4__RESULT_H */
Definition: modes.h:25
bool isNull() const
Definition: result.h:139
Result(const Result &r, std::string inputName)
Definition: result.h:122
void CheckArgument(bool cond, const T &arg, const char *fmt,...)
Definition: exception.h:140
Type getType() const
Definition: result.h:136
CVC4&#39;s exception base class and some associated utilities.
std::string getInputName() const
Definition: result.h:156
bool operator!=(const Result &r) const
Definition: result.h:160
#define CVC4_PUBLIC
Definition: cvc4_public.h:30
Macros that should be defined everywhere during the building of the libraries and driver binary...
Three-valued SMT result, with optional explanation.
Definition: result.h:36
Result(enum Validity v, std::string inputName="")
Definition: result.h:93
Result(enum Sat s, std::string inputName="")
Definition: result.h:84
Result(enum Sat s, enum UnknownExplanation unknownExplanation, std::string inputName="")
Definition: result.h:102
bool isUnknown() const
Definition: result.h:133
std::ostream & operator<<(std::ostream &out, ModelFormatMode mode)
struct CVC4::options::out__option_t out
bool operator!=(enum Result::Sat s, const Result &r)
bool operator==(enum Result::Sat s, const Result &r)
Result(enum Validity v, enum UnknownExplanation unknownExplanation, std::string inputName="")
Definition: result.h:111
UnknownExplanation
Definition: result.h:56