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.

4 files changed, 11 insertions, 11 deletions

diff --git a/examples/api/java/BitVectors.java b/examples/api/java/BitVectors.java
index 17111b63a..bb2245a6f 100644
--- a/examples/api/java/BitVectors.java
+++ b/examples/api/java/BitVectors.java
@@ -86,8 +86,8 @@ public class BitVectors {
     Expr new_x_eq_new_x_ = em.mkExpr(Kind.EQUAL, new_x, new_x_);
 
     System.out.println(" Querying: " + new_x_eq_new_x_);
-    System.out.println(" Expect valid. ");
-    System.out.println(" CVC4: " + smt.query(new_x_eq_new_x_));
+    System.out.println(" Expect entailed. ");
+    System.out.println(" CVC4: " + smt.checkEntailed(new_x_eq_new_x_));
     System.out.println(" Popping context. ");
     smt.pop();
 
@@ -102,7 +102,7 @@ public class BitVectors {
     smt.assertFormula(assignment2);
 
     System.out.println(" Querying: " + new_x_eq_new_x_);
-    System.out.println(" Expect valid. ");
-    System.out.println(" CVC4: " + smt.query(new_x_eq_new_x_));
+    System.out.println(" Expect entailed. ");
+    System.out.println(" CVC4: " + smt.checkEntailed(new_x_eq_new_x_));
   }
 }
diff --git a/examples/api/java/Combination.java b/examples/api/java/Combination.java
index 0c9ca84d6..53b1fa92d 100644
--- a/examples/api/java/Combination.java
+++ b/examples/api/java/Combination.java
@@ -83,10 +83,9 @@ public class Combination {
 
     System.out.println("Given the following assumptions:");
     System.out.println(assumptions);
-    System.out.println("Prove x /= y is valid. " +
-                       "CVC4 says: " + smt.query(em.mkExpr(Kind.DISTINCT, x, y)) +
-                       ".");
-
+    System.out.println("Prove x /= y is entailed. "
+        + "CVC4 says: " + smt.checkEntailed(em.mkExpr(Kind.DISTINCT, x, y))
+        + ".");
 
     System.out.println("Now we call checksat on a trivial query to show that");
     System.out.println("the assumptions are satisfiable: " +
diff --git a/examples/api/java/HelloWorld.java b/examples/api/java/HelloWorld.java
index 393ce40f0..a08f3d452 100644
--- a/examples/api/java/HelloWorld.java
+++ b/examples/api/java/HelloWorld.java
@@ -30,6 +30,6 @@ public class HelloWorld {
     Expr helloworld = em.mkVar("Hello World!", em.booleanType());
     SmtEngine smt = new SmtEngine(em);
 
-    System.out.println(helloworld + " is " + smt.query(helloworld));
+    System.out.println(helloworld + " is " + smt.checkEntailed(helloworld));
   }
 }
diff --git a/examples/api/java/LinearArith.java b/examples/api/java/LinearArith.java
index 2ddf92584..e060263b4 100644
--- a/examples/api/java/LinearArith.java
+++ b/examples/api/java/LinearArith.java
@@ -61,8 +61,9 @@ public class LinearArith {
     smt.push();
     Expr diff_leq_two_thirds = em.mkExpr(Kind.LEQ, diff, two_thirds);
     System.out.println("Prove that " + diff_leq_two_thirds + " with CVC4.");
-    System.out.println("CVC4 should report VALID.");
-    System.out.println("Result from CVC4 is: " + smt.query(diff_leq_two_thirds));
+    System.out.println("CVC4 should report ENTAILED.");
+    System.out.println(
+        "Result from CVC4 is: " + smt.checkEntailed(diff_leq_two_thirds));
     smt.pop();
 
     System.out.println();