From 01e84d511e40604b01328b1e96ecdbe2b818b3c3 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Thu, 8 Aug 2019 17:19:05 -0700 Subject: [PATCH] New C++ API: Add checks and tests for Solver::simplify. (#3170) --- src/api/cvc4cpp.cpp | 14 +++++-- test/unit/api/solver_black.h | 77 ++++++++++++++++++++++++++++++++++++ 2 files changed, 87 insertions(+), 4 deletions(-) diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index ad49efce6..b29d6a26f 100644 --- 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 37eccb94c..3a90f7ed2 100644 --- 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")); -- 2.30.2