New C++ API: Add checks and tests for Solver::simplify. (#3170)

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index ad49efce652b4090709145412c612364d3d3b4bb..b29d6a26fe5c90700b5b06ec3734f3775ca96cc0 100644 (file)
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -656,7 +656,10 @@ class CVC4ApiExceptionStream
                             << "', expected non-null object";
 
 #define CVC4_API_ARG_CHECK_NOT_NULL(arg) \
-  CVC4_API_CHECK(arg != nullptr)         \
+  CVC4_API_CHECK(!arg.isNull()) << "Invalid null argument for '" << #arg << "'";
+
+#define CVC4_API_ARG_CHECK_NOT_NULLPTR(arg) \
+  CVC4_API_CHECK(arg != nullptr)            \
       << "Invalid null argument for '" << #arg << "'";
 
 #define CVC4_API_KIND_CHECK(kind)     \
@@ -2352,7 +2355,7 @@ Term Solver::mkPi() const
 Term Solver::mkReal(const char* s) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
-  CVC4_API_ARG_CHECK_NOT_NULL(s);
+  CVC4_API_ARG_CHECK_NOT_NULLPTR(s);
 
   return mkRealFromStrHelper(std::string(s));
 
@@ -2521,7 +2524,7 @@ Term Solver::mkBitVector(uint32_t size, uint64_t val) const
 Term Solver::mkBitVector(const char* s, uint32_t base) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
-  CVC4_API_ARG_CHECK_NOT_NULL(s);
+  CVC4_API_ARG_CHECK_NOT_NULLPTR(s);
 
   return mkBVFromStrHelper(std::string(s), base);
 
@@ -2538,7 +2541,7 @@ Term Solver::mkBitVector(const std::string& s, uint32_t base) const
 Term Solver::mkBitVector(uint32_t size, const char* s, uint32_t base) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
-  CVC4_API_ARG_CHECK_NOT_NULL(s);
+  CVC4_API_ARG_CHECK_NOT_NULLPTR(s);
   return mkBVFromStrHelper(size, s, base);
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
@@ -3079,7 +3082,10 @@ OpTerm Solver::mkOpTerm(Kind kind, uint32_t arg1, uint32_t arg2) const
 
 Term Solver::simplify(const Term& t)
 {
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  CVC4_API_ARG_CHECK_NOT_NULL(t);
   return d_smtEngine->simplify(*t.d_expr);
+  CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 Result Solver::checkValid(void) const

diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h
index 37eccb94c681f28528063a8488ae5adf85309673..3a90f7ed278e0294d4db08cc39b513442ca20409 100644 (file)
--- a/test/unit/api/solver_black.h
+++ b/test/unit/api/solver_black.h
@@ -89,6 +89,7 @@ class SolverBlack : public CxxTest::TestSuite
   void testPop1();
   void testPop2();
   void testPop3();
+  void testSimplify();
 
   void testSetInfo();
   void testSetLogic();
@@ -950,6 +951,82 @@ void SolverBlack::testSetInfo()
   TS_ASSERT_THROWS(d_solver->setInfo("status", "asdf"), CVC4ApiException&);
 }
 
+void SolverBlack::testSimplify()
+{
+  TS_ASSERT_THROWS(d_solver->simplify(Term()), CVC4ApiException&);
+
+  Sort bvSort = d_solver->mkBitVectorSort(32);
+  Sort uSort = d_solver->mkUninterpretedSort("u");
+  Sort funSort1 = d_solver->mkFunctionSort({bvSort, bvSort}, bvSort);
+  Sort funSort2 = d_solver->mkFunctionSort(uSort, d_solver->getIntegerSort());
+
+  DatatypeDecl consListSpec("list");
+  DatatypeConstructorDecl cons("cons");
+  DatatypeSelectorDecl head("head", d_solver->getIntegerSort());
+  DatatypeSelectorDecl tail("tail", DatatypeDeclSelfSort());
+  cons.addSelector(head);
+  cons.addSelector(tail);
+  consListSpec.addConstructor(cons);
+  DatatypeConstructorDecl nil("nil");
+  consListSpec.addConstructor(nil);
+  Sort consListSort = d_solver->mkDatatypeSort(consListSpec);
+
+  Term x = d_solver->mkConst(bvSort, "x");
+  TS_ASSERT_THROWS_NOTHING(d_solver->simplify(x));
+  Term a = d_solver->mkConst(bvSort, "a");
+  TS_ASSERT_THROWS_NOTHING(d_solver->simplify(a));
+  Term b = d_solver->mkConst(bvSort, "b");
+  TS_ASSERT_THROWS_NOTHING(d_solver->simplify(b));
+  Term x_eq_x = d_solver->mkTerm(EQUAL, x, x);
+  TS_ASSERT_THROWS_NOTHING(d_solver->simplify(x_eq_x));
+  TS_ASSERT(d_solver->mkTrue() != x_eq_x);
+  TS_ASSERT(d_solver->mkTrue() == d_solver->simplify(x_eq_x));
+  Term x_eq_b = d_solver->mkTerm(EQUAL, x, b);
+  TS_ASSERT_THROWS_NOTHING(d_solver->simplify(x_eq_b));
+  TS_ASSERT(d_solver->mkTrue() != x_eq_b);
+  TS_ASSERT(d_solver->mkTrue() != d_solver->simplify(x_eq_b));
+
+  Term i1 = d_solver->mkConst(d_solver->getIntegerSort(), "i1");
+  TS_ASSERT_THROWS_NOTHING(d_solver->simplify(i1));
+  Term i2 = d_solver->mkTerm(MULT, i1, d_solver->mkReal("23"));
+  TS_ASSERT_THROWS_NOTHING(d_solver->simplify(i2));
+  TS_ASSERT(i1 != i2);
+  TS_ASSERT(i1 != d_solver->simplify(i2));
+  Term i3 = d_solver->mkTerm(PLUS, i1, d_solver->mkReal(0));
+  TS_ASSERT_THROWS_NOTHING(d_solver->simplify(i3));
+  TS_ASSERT(i1 != i3);
+  TS_ASSERT(i1 == d_solver->simplify(i3));
+
+  Datatype consList = consListSort.getDatatype();
+  Term dt1 = d_solver->mkTerm(
+      APPLY_CONSTRUCTOR,
+      consList.getConstructorTerm("cons"),
+      d_solver->mkReal(0),
+      d_solver->mkTerm(APPLY_CONSTRUCTOR, consList.getConstructorTerm("nil")));
+  TS_ASSERT_THROWS_NOTHING(d_solver->simplify(dt1));
+  Term dt2 = d_solver->mkTerm(
+      APPLY_SELECTOR, consList["cons"].getSelectorTerm("head"), dt1);
+  TS_ASSERT_THROWS_NOTHING(d_solver->simplify(dt2));
+
+  Term b1 = d_solver->mkVar(bvSort, "b1");
+  TS_ASSERT_THROWS_NOTHING(d_solver->simplify(b1));
+  Term b2 = d_solver->mkVar(bvSort, "b1");
+  TS_ASSERT_THROWS_NOTHING(d_solver->simplify(b2));
+  Term b3 = d_solver->mkVar(uSort, "b3");
+  TS_ASSERT_THROWS_NOTHING(d_solver->simplify(b3));
+  Term v1 = d_solver->mkConst(bvSort, "v1");
+  TS_ASSERT_THROWS_NOTHING(d_solver->simplify(v1));
+  Term v2 = d_solver->mkConst(d_solver->getIntegerSort(), "v2");
+  TS_ASSERT_THROWS_NOTHING(d_solver->simplify(v2));
+  Term f1 = d_solver->mkConst(funSort1, "f1");
+  TS_ASSERT_THROWS_NOTHING(d_solver->simplify(f1));
+  Term f2 = d_solver->mkConst(funSort2, "f2");
+  TS_ASSERT_THROWS_NOTHING(d_solver->simplify(f2));
+  d_solver->defineFunsRec({f1, f2}, {{b1, b2}, {b3}}, {v1, v2});
+  TS_ASSERT_THROWS_NOTHING(d_solver->simplify(f1));
+  TS_ASSERT_THROWS_NOTHING(d_solver->simplify(f2));
+}
+
 void SolverBlack::testSetLogic()
 {
   TS_ASSERT_THROWS_NOTHING(d_solver->setLogic("AUFLIRA"));