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.

1 files changed, 5 insertions, 4 deletions

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;
 }