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, 22 insertions, 46 deletions

diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h
index 0eefde700..9fd1b7789 100644
--- a/test/unit/api/solver_black.h
+++ b/test/unit/api/solver_black.h
@@ -95,10 +95,9 @@ class SolverBlack : public CxxTest::TestSuite
   void testPop3();
 
   void testSimplify();
-  void testCheckValid1();
-  void testCheckValid2();
-  void testCheckValidAssuming1();
-  void testCheckValidAssuming2();
+  void testCheckEntailed();
+  void testCheckEntailed1();
+  void testCheckEntailed2();
 
   void testSetInfo();
   void testSetLogic();
@@ -1104,51 +1103,28 @@ void SolverBlack::testSimplify()
   TS_ASSERT_THROWS_NOTHING(d_solver->simplify(f2));
 }
 
-void SolverBlack::testCheckValid1()
+void SolverBlack::testCheckEntailed()
 {
   d_solver->setOption("incremental", "false");
-  TS_ASSERT_THROWS_NOTHING(d_solver->checkValid());
-  TS_ASSERT_THROWS(d_solver->checkValid(), CVC4ApiException&);
+  TS_ASSERT_THROWS_NOTHING(d_solver->checkEntailed(d_solver->mkTrue()));
+  TS_ASSERT_THROWS(d_solver->checkEntailed(d_solver->mkTrue()),
+                   CVC4ApiException&);
 }
 
-void SolverBlack::testCheckValid2()
+void SolverBlack::testCheckEntailed1()
 {
+  Sort boolSort = d_solver->getBooleanSort();
+  Term x = d_solver->mkConst(boolSort, "x");
+  Term y = d_solver->mkConst(boolSort, "y");
+  Term z = d_solver->mkTerm(AND, x, y);
   d_solver->setOption("incremental", "true");
-
-  Sort realSort = d_solver->getRealSort();
-  Sort intSort = d_solver->getIntegerSort();
-
-  // Constants
-  Term x = d_solver->mkConst(intSort, "x");
-  Term y = d_solver->mkConst(realSort, "y");
-  // Values
-  Term three = d_solver->mkReal(3);
-  Term neg2 = d_solver->mkReal(-2);
-  Term two_thirds = d_solver->mkReal(2, 3);
-  // Terms
-  Term three_y = d_solver->mkTerm(MULT, three, y);
-  Term diff = d_solver->mkTerm(MINUS, y, x);
-  // Formulas
-  Term x_geq_3y = d_solver->mkTerm(GEQ, x, three_y);
-  Term x_leq_y = d_solver->mkTerm(LEQ, x, y);
-  Term neg2_lt_x = d_solver->mkTerm(LT, neg2, x);
-  // Assertions
-  Term assertions = d_solver->mkTerm(AND, x_geq_3y, x_leq_y, neg2_lt_x);
-
-  TS_ASSERT_THROWS_NOTHING(d_solver->checkValid());
-  d_solver->assertFormula(assertions);
-  TS_ASSERT_THROWS_NOTHING(d_solver->checkValid());
-}
-
-void SolverBlack::testCheckValidAssuming1()
-{
-  d_solver->setOption("incremental", "false");
-  TS_ASSERT_THROWS_NOTHING(d_solver->checkValidAssuming(d_solver->mkTrue()));
-  TS_ASSERT_THROWS(d_solver->checkValidAssuming(d_solver->mkTrue()),
-                   CVC4ApiException&);
+  TS_ASSERT_THROWS_NOTHING(d_solver->checkEntailed(d_solver->mkTrue()));
+  TS_ASSERT_THROWS(d_solver->checkEntailed(Term()), CVC4ApiException&);
+  TS_ASSERT_THROWS_NOTHING(d_solver->checkEntailed(d_solver->mkTrue()));
+  TS_ASSERT_THROWS_NOTHING(d_solver->checkEntailed(z));
 }
 
-void SolverBlack::testCheckValidAssuming2()
+void SolverBlack::testCheckEntailed2()
 {
   d_solver->setOption("incremental", "true");
 
@@ -1185,15 +1161,15 @@ void SolverBlack::testCheckValidAssuming2()
                            p_f_y                             // p(f(y))
                        });
 
-  TS_ASSERT_THROWS_NOTHING(d_solver->checkValidAssuming(d_solver->mkTrue()));
+  TS_ASSERT_THROWS_NOTHING(d_solver->checkEntailed(d_solver->mkTrue()));
   d_solver->assertFormula(assertions);
   TS_ASSERT_THROWS_NOTHING(
-      d_solver->checkValidAssuming(d_solver->mkTerm(DISTINCT, x, y)));
-  TS_ASSERT_THROWS_NOTHING(d_solver->checkValidAssuming(
+      d_solver->checkEntailed(d_solver->mkTerm(DISTINCT, x, y)));
+  TS_ASSERT_THROWS_NOTHING(d_solver->checkEntailed(
       {d_solver->mkFalse(), d_solver->mkTerm(DISTINCT, x, y)}));
-  TS_ASSERT_THROWS(d_solver->checkValidAssuming(n), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->checkEntailed(n), CVC4ApiException&);
   TS_ASSERT_THROWS(
-      d_solver->checkValidAssuming({n, d_solver->mkTerm(DISTINCT, x, y)}),
+      d_solver->checkEntailed({n, d_solver->mkTerm(DISTINCT, x, y)}),
       CVC4ApiException&);
 }