diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2020-03-31 18:12:16 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-03-31 18:12:16 -0700 |
commit | cfeaf40ed6a9d4d7fec925352e30d2470a1ca567 (patch) | |
tree | e69411603787d99cea12d729ec0a0a2ae8889f20 /src/util/result.h | |
parent | 186b3872a3de454d0f30224dc2e0a396163c3fdc (diff) |
Rename checkValid/query to checkEntailed. (#4191)
This renames api::Solver::checkValidAssuming to checkEntailed and
removes api::Solver::checkValid. Internally, SmtEngine::query is renamed
to SmtEngine::checkEntailed, and these changes are further propagated to
the Result class.
Diffstat (limited to 'src/util/result.h')
-rw-r--r-- | src/util/result.h | 38 |
1 files changed, 25 insertions, 13 deletions
diff --git a/src/util/result.h b/src/util/result.h index f34a9bb5a..10df05388 100644 --- a/src/util/result.h +++ b/src/util/result.h @@ -38,9 +38,19 @@ class CVC4_PUBLIC Result { public: enum Sat { UNSAT = 0, SAT = 1, SAT_UNKNOWN = 2 }; - enum Validity { INVALID = 0, VALID = 1, VALIDITY_UNKNOWN = 2 }; + enum Entailment + { + NOT_ENTAILED = 0, + ENTAILED = 1, + ENTAILMENT_UNKNOWN = 2 + }; - enum Type { TYPE_SAT, TYPE_VALIDITY, TYPE_NONE }; + enum Type + { + TYPE_SAT, + TYPE_ENTAILMENT, + TYPE_NONE + }; enum UnknownExplanation { REQUIRES_FULL_CHECK, @@ -57,7 +67,7 @@ class CVC4_PUBLIC Result { private: enum Sat d_sat; - enum Validity d_validity; + enum Entailment d_entailment; enum Type d_which; enum UnknownExplanation d_unknownExplanation; std::string d_inputName; @@ -67,12 +77,13 @@ class CVC4_PUBLIC Result { Result(enum Sat s, std::string inputName = ""); - Result(enum Validity v, std::string inputName = ""); + Result(enum Entailment v, std::string inputName = ""); Result(enum Sat s, enum UnknownExplanation unknownExplanation, std::string inputName = ""); - Result(enum Validity v, enum UnknownExplanation unknownExplanation, + Result(enum Entailment v, + enum UnknownExplanation unknownExplanation, std::string inputName = ""); Result(const std::string& s, std::string inputName = ""); @@ -84,12 +95,13 @@ class CVC4_PUBLIC Result { enum Sat isSat() const { return d_which == TYPE_SAT ? d_sat : SAT_UNKNOWN; } - enum Validity isValid() const { - return d_which == TYPE_VALIDITY ? d_validity : VALIDITY_UNKNOWN; + enum Entailment isEntailed() const + { + return d_which == TYPE_ENTAILMENT ? d_entailment : ENTAILMENT_UNKNOWN; } bool isUnknown() const { - return isSat() == SAT_UNKNOWN && isValid() == VALIDITY_UNKNOWN; + return isSat() == SAT_UNKNOWN && isEntailed() == ENTAILMENT_UNKNOWN; } Type getType() const { return d_which; } @@ -101,7 +113,7 @@ class CVC4_PUBLIC Result { bool operator==(const Result& r) const; inline bool operator!=(const Result& r) const; Result asSatisfiabilityResult() const; - Result asValidityResult() const; + Result asEntailmentResult() const; std::string toString() const; @@ -128,7 +140,7 @@ class CVC4_PUBLIC Result { * Write a Result out to a stream. * * The default implementation writes a reasonable string in lowercase - * for sat, unsat, valid, invalid, or unknown results. This behavior + * 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. */ @@ -139,15 +151,15 @@ inline bool Result::operator!=(const Result& r) const { return !(*this == r); } std::ostream& operator<<(std::ostream& out, enum Result::Sat s) CVC4_PUBLIC; std::ostream& operator<<(std::ostream& out, - enum Result::Validity v) CVC4_PUBLIC; + enum Result::Entailment e) CVC4_PUBLIC; std::ostream& operator<<(std::ostream& out, enum Result::UnknownExplanation e) CVC4_PUBLIC; bool operator==(enum Result::Sat s, const Result& r) CVC4_PUBLIC; -bool operator==(enum Result::Validity v, const Result& r) CVC4_PUBLIC; +bool operator==(enum Result::Entailment e, const Result& r) CVC4_PUBLIC; bool operator!=(enum Result::Sat s, const Result& r) CVC4_PUBLIC; -bool operator!=(enum Result::Validity v, const Result& r) CVC4_PUBLIC; +bool operator!=(enum Result::Entailment e, const Result& r) CVC4_PUBLIC; } /* CVC4 namespace */ |