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 */