cvc4-1.3
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 
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 */
bool isNull() const
Definition: result.h:139
Class encapsulating CVC4 expression types.
Definition: type.h:88
Result(const Result &r, std::string inputName)
Definition: result.h:122
std::ostream & operator<<(std::ostream &, const Command &)
void CheckArgument(bool cond, const T &arg, const char *fmt,...)
Definition: exception.h:140
Type getType() const
Definition: result.h:136
CVC4's exception base class and some associated utilities.
This is CVC4 release version For build and installation please see the INSTALL file included with this distribution This first official release of CVC4 is the result of more than three years of efforts by researchers at New York University and The University of Iowa The project leaders are Clark please refer to the AUTHORS file in the source distribution CVC4 is a tool for determining the satisfiability of a first order formula modulo a first order CVC CVC3 but does not directly incorporate code from any previous version CVC4 is intended to be an open and extensible SMT engine It can be used as a stand alone tool or as a library It has been designed to increase the performance and reduce the memory overhead of its predecessors It is written entirely in C and is released under a free software see the INSTALL file that comes with this distribution We recommend that you visit our CVC4 tutorials online please write to the cvc users cs nyu edu mailing list *if you need to report a bug with CVC4
Definition: README:39
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
struct CVC4::options::out__option_t out
Result(enum Sat s, enum UnknownExplanation unknownExplanation, std::string inputName="")
Definition: result.h:102
bool isUnknown() const
Definition: result.h:133
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