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.

3 files changed, 10 insertions, 9 deletions

diff --git a/test/system/boilerplate.cpp b/test/system/boilerplate.cpp
index 141db4eea..2ce50949b 100644
--- a/test/system/boilerplate.cpp
+++ b/test/system/boilerplate.cpp
@@ -29,8 +29,8 @@ int main() {
   ExprManager em;
   Options opts;
   SmtEngine smt(&em);
-  Result r = smt.query(em.mkConst(true));
+  Result r = smt.checkEntailed(em.mkConst(true));
 
-  return (Result::VALID == r) ? 0 : 1;
+  return (Result::ENTAILED == r) ? 0 : 1;
 }
 
diff --git a/test/system/statistics.cpp b/test/system/statistics.cpp
index fb9714d4b..2924359e8 100644
--- a/test/system/statistics.cpp
+++ b/test/system/statistics.cpp
@@ -35,9 +35,10 @@ int main() {
   Expr y = em.mkVar("y", em.integerType());
   smt.assertFormula(em.mkExpr(kind::GT, em.mkExpr(kind::PLUS, x, y), em.mkConst(Rational(5))));
   Expr q = em.mkExpr(kind::GT, x, em.mkConst(Rational(0)));
-  Result r = smt.query(q);
+  Result r = smt.checkEntailed(q);
 
-  if(r != Result::INVALID) {
+  if (r != Result::NOT_ENTAILED)
+  {
     exit(1);
   }
 
@@ -47,7 +48,7 @@ int main() {
   }
 
   smt.assertFormula(em.mkExpr(kind::LT, y, em.mkConst(Rational(5))));
-  r = smt.query(q);
+  r = smt.checkEntailed(q);
   Statistics stats2 = smt.getStatistics();
   bool different = false;
   for(Statistics::iterator i = stats2.begin(); i != stats2.end(); ++i) {
@@ -68,5 +69,5 @@ int main() {
   }
 #endif /* CVC4_STATISTICS_ON */
 
-  return r == Result::VALID ? 0 : 1;
+  return r == Result::ENTAILED ? 0 : 1;
 }
diff --git a/test/system/two_smt_engines.cpp b/test/system/two_smt_engines.cpp
index a7266e0b0..8698fde0e 100644
--- a/test/system/two_smt_engines.cpp
+++ b/test/system/two_smt_engines.cpp
@@ -28,9 +28,9 @@ int main() {
   Options opts;
   SmtEngine smt(&em);
   SmtEngine smt2(&em);
-  Result r = smt.query(em.mkConst(true));
-  Result r2 = smt2.query(em.mkConst(true));
+  Result r = smt.checkEntailed(em.mkConst(true));
+  Result r2 = smt2.checkEntailed(em.mkConst(true));
 
-  return r == Result::VALID && r2 == Result::VALID ? 0 : 1;
+  return r == Result::ENTAILED && r2 == Result::ENTAILED ? 0 : 1;
 }