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.

2 files changed, 44 insertions, 72 deletions

diff --git a/test/unit/api/result_black.h b/test/unit/api/result_black.h
index ab5d65e72..cbfc9cf23 100644
--- a/test/unit/api/result_black.h
+++ b/test/unit/api/result_black.h
@@ -29,9 +29,8 @@ class ResultBlack : public CxxTest::TestSuite
   void testIsSat();
   void testIsUnsat();
   void testIsSatUnknown();
-  void testIsValid();
-  void testIsInvalid();
-  void testIsValidUnknown();
+  void testIsEntailed();
+  void testIsEntailmentUnknown();
 
  private:
   std::unique_ptr<Solver> d_solver;
@@ -44,9 +43,9 @@ void ResultBlack::testIsNull()
   TS_ASSERT(!res_null.isSat());
   TS_ASSERT(!res_null.isUnsat());
   TS_ASSERT(!res_null.isSatUnknown());
-  TS_ASSERT(!res_null.isValid());
-  TS_ASSERT(!res_null.isInvalid());
-  TS_ASSERT(!res_null.isValidUnknown());
+  TS_ASSERT(!res_null.isEntailed());
+  TS_ASSERT(!res_null.isNotEntailed());
+  TS_ASSERT(!res_null.isEntailmentUnknown());
   Sort u_sort = d_solver->mkUninterpretedSort("u");
   Term x = d_solver->mkVar(u_sort, "x");
   d_solver->assertFormula(x.eqTerm(x));
@@ -100,27 +99,24 @@ void ResultBlack::testIsSatUnknown()
   TS_ASSERT(res.isSatUnknown());
 }
 
-void ResultBlack::testIsValid()
+void ResultBlack::testIsEntailed()
 {
+  d_solver->setOption("incremental", "true");
   Sort u_sort = d_solver->mkUninterpretedSort("u");
-  Term x = d_solver->mkVar(u_sort, "x");
-  d_solver->assertFormula(x.eqTerm(x).notTerm());
-  Result res = d_solver->checkValid();
-  TS_ASSERT(res.isValid());
-  TS_ASSERT(!res.isValidUnknown());
-}
-
-void ResultBlack::testIsInvalid()
-{
-  Sort u_sort = d_solver->mkUninterpretedSort("u");
-  Term x = d_solver->mkVar(u_sort, "x");
-  d_solver->assertFormula(x.eqTerm(x));
-  Result res = d_solver->checkValid();
-  TS_ASSERT(res.isInvalid());
-  TS_ASSERT(!res.isValidUnknown());
+  Term x = d_solver->mkConst(u_sort, "x");
+  Term y = d_solver->mkConst(u_sort, "y");
+  Term a = x.eqTerm(y).notTerm();
+  Term b = x.eqTerm(y);
+  d_solver->assertFormula(a);
+  Result entailed = d_solver->checkEntailed(a);
+  TS_ASSERT(entailed.isEntailed());
+  TS_ASSERT(!entailed.isEntailmentUnknown());
+  Result not_entailed = d_solver->checkEntailed(b);
+  TS_ASSERT(not_entailed.isNotEntailed());
+  TS_ASSERT(!not_entailed.isEntailmentUnknown());
 }
 
-void ResultBlack::testIsValidUnknown()
+void ResultBlack::testIsEntailmentUnknown()
 {
   d_solver->setLogic("QF_NIA");
   d_solver->setOption("incremental", "false");
@@ -128,9 +124,9 @@ void ResultBlack::testIsValidUnknown()
   Sort int_sort = d_solver->getIntegerSort();
   Term x = d_solver->mkVar(int_sort, "x");
   d_solver->assertFormula(x.eqTerm(x).notTerm());
-  Result res = d_solver->checkValid();
-  TS_ASSERT(!res.isValid());
-  TS_ASSERT(res.isValidUnknown());
+  Result res = d_solver->checkEntailed(x.eqTerm(x));
+  TS_ASSERT(!res.isEntailed());
+  TS_ASSERT(res.isEntailmentUnknown());
   TS_ASSERT_EQUALS(res.getUnknownExplanation(), "UNKNOWN_REASON");
 }
 
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&);
 }