From 3830d80ce312e8633b9de6311b809bd9418ddd4a Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Tue, 1 Sep 2020 23:37:14 -0700 Subject: [PATCH] [API] Fix Python Examples (#4943) When testing the API examples, Python examples were not included. This commit changes that and fixes multiple minor issues that came up once the tests were enabled: - It adds `Solver::supportsFloatingPoint()` as an API method that returns whether CVC4 is configured to support floating-point numbers or not (this is useful for failing gracefully when floating-point support is not available, e.g. in the case of our floating-point example). - It updates the `expections.py` example to use the new API. - It fixes the `sygus-fun.py` example. The example was passing a _set_ of non-terminals to `Solver::mkSygusGrammar()` but the order in which the non-terminals are passed in matters because the first non-terminal is considered to be the starting terminal. The commit also updates the documentation of that function. - It fixes the Python API for datatypes. The `__getitem__` function had a typo and the `datatypes.py` example was crashing as a result. --- CMakeLists.txt | 1 + cmake/CVC4Config.cmake.in | 5 +- examples/api/python/CMakeLists.txt | 15 ++++- examples/api/python/exceptions.py | 34 +++++----- examples/api/python/floating_point.py | 9 ++- examples/api/python/sygus-fun.py | 6 +- src/api/cvc4cpp.cpp | 18 ++++- src/api/cvc4cpp.h | 12 +++- src/api/python/cvc4.pxd | 3 +- src/api/python/cvc4.pxi | 13 ++-- src/parser/smt2/smt2.cpp | 2 +- src/theory/logic_info.cpp | 8 ++- .../quantifiers/issue3481-unsat1.smt2 | 2 +- .../regress1/quantifiers/issue3481.smt2 | 2 +- test/unit/api/python/test_sort.py | 30 ++++++--- test/unit/api/solver_black.h | 65 +++++++++++++++---- 16 files changed, 167 insertions(+), 58 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 5b1d1e292..02933762b 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -571,6 +571,7 @@ add_subdirectory(src) add_subdirectory(test) if(BUILD_BINDINGS_PYTHON) + set(BUILD_BINDINGS_PYTHON_VERSION ${PYTHON_VERSION_MAJOR}) add_subdirectory(src/api/python) endif() diff --git a/cmake/CVC4Config.cmake.in b/cmake/CVC4Config.cmake.in index 76535762d..7f6a80995 100644 --- a/cmake/CVC4Config.cmake.in +++ b/cmake/CVC4Config.cmake.in @@ -1,7 +1,8 @@ @PACKAGE_INIT@ -set(CVC4_BINDINGS_JAVA @BUILD_SWIG_BINDINGS_JAVA@) -set(CVC4_BINDINGS_PYTHON @BUILD_SWIG_BINDINGS_PYTHON@) +set(CVC4_BINDINGS_JAVA @BUILD_BINDINGS_JAVA@) +set(CVC4_BINDINGS_PYTHON @BUILD_BINDINGS_PYTHON@) +set(CVC4_BINDINGS_PYTHON_VERSION @BUILD_BINDINGS_PYTHON_VERSION@) if(NOT TARGET CVC4::cvc4) include(${CMAKE_CURRENT_LIST_DIR}/CVC4Targets.cmake) diff --git a/examples/api/python/CMakeLists.txt b/examples/api/python/CMakeLists.txt index e3966fa2d..0da960513 100644 --- a/examples/api/python/CMakeLists.txt +++ b/examples/api/python/CMakeLists.txt @@ -1,9 +1,22 @@ set(EXAMPLES_API_PYTHON + bitvectors_and_arrays + bitvectors + combination + datatypes exceptions + extract + floating_point + helloworld + linear_arith sequences + sets + strings + sygus-fun + sygus-grammar + sygus-inv ) -find_package(PythonInterp REQUIRED) +find_package(PythonInterp ${CVC4_BINDINGS_PYTHON_VERSION} REQUIRED) # Find Python bindings in the corresponding python-*/site-packages directory. # Lookup Python module directory and store path in PYTHON_MODULE_PATH. diff --git a/examples/api/python/exceptions.py b/examples/api/python/exceptions.py index 780f75bf7..27f068011 100644 --- a/examples/api/python/exceptions.py +++ b/examples/api/python/exceptions.py @@ -16,40 +16,40 @@ ## A simple demonstration of catching CVC4 execptions with the legacy Python ## API. -import CVC4 +import pycvc4 +from pycvc4 import kinds import sys def main(): - em = CVC4.ExprManager() - smt = CVC4.SmtEngine(em) + slv = pycvc4.Solver() - smt.setOption("produce-models", CVC4.SExpr("true")) + slv.setOption("produce-models", "true") # Setting an invalid option try: - smt.setOption("non-existing", CVC4.SExpr("true")) + slv.setOption("non-existing", "true") return 1 - except CVC4.Exception as e: - print(e.toString()) + except: + pass # Creating a term with an invalid type try: - integer = em.integerType() - x = em.mkVar("x", integer) - invalidExpr = em.mkExpr(CVC4.AND, x, x) - smt.checkSat(invalidExpr) + integer = slv.getIntegerSort() + x = slv.mkConst("x", integer) + invalidTerm = em.mkTerm(AND, x, x) + slv.checkSat(invalidTerm) return 1 - except CVC4.Exception as e: - print(e.toString()) + except: + pass # Asking for a model after unsat result try: - smt.checkSat(em.mkBoolConst(False)) - smt.getModel() + slv.checkSat(slv.mkBoolean(False)) + slv.getModel() return 1 - except CVC4.Exception as e: - print(e.toString()) + except: + pass return 0 diff --git a/examples/api/python/floating_point.py b/examples/api/python/floating_point.py index c92666c0b..6fb595e34 100755 --- a/examples/api/python/floating_point.py +++ b/examples/api/python/floating_point.py @@ -20,8 +20,15 @@ from pycvc4 import kinds if __name__ == "__main__": slv = pycvc4.Solver() + + if not slv.supportsFloatingPoint(): + # CVC4 must be built with SymFPU to support the theory of + # floating-point numbers + print("CVC4 was not built with floating-point support.") + exit() + slv.setOption("produce-models", "true") - slv.setLogic("FP") + slv.setLogic("QF_FP") # single 32-bit precision fp32 = slv.mkFloatingPointSort(8, 24) diff --git a/examples/api/python/sygus-fun.py b/examples/api/python/sygus-fun.py index 0f53bd343..25090bd8f 100644 --- a/examples/api/python/sygus-fun.py +++ b/examples/api/python/sygus-fun.py @@ -53,7 +53,7 @@ if __name__ == "__main__": leq = slv.mkTerm(kinds.Leq, start, start) # create the grammar object - g = slv.mkSygusGrammar({x, y}, {start, start_bool}) + g = slv.mkSygusGrammar([x, y], [start, start_bool]) # bind each non-terminal to its rules g.addRules(start, {zero, one, x, y, plus, minus, ite}) @@ -61,8 +61,8 @@ if __name__ == "__main__": # declare the functions-to-synthesize. Optionally, provide the grammar # constraints - max = slv.synthFun("max", {x, y}, integer, g) - min = slv.synthFun("min", {x, y}, integer) + max = slv.synthFun("max", [x, y], integer, g) + min = slv.synthFun("min", [x, y], integer) # declare universal variables. varX = slv.mkSygusVar(integer, "x") diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index c14bed6aa..6c39bfb91 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -3240,6 +3240,14 @@ void Solver::checkMkTerm(Kind kind, uint32_t nchildren) const << " children (the one under construction has " << nchildren << ")"; } +/* Solver Configuration */ +/* -------------------------------------------------------------------------- */ + +bool Solver::supportsFloatingPoint() const +{ + return Configuration::isBuiltWithSymFPU(); +} + /* Sorts Handling */ /* -------------------------------------------------------------------------- */ @@ -3285,9 +3293,11 @@ Sort Solver::getStringSort(void) const CVC4_API_SOLVER_TRY_CATCH_END; } -Sort Solver::getRoundingmodeSort(void) const +Sort Solver::getRoundingModeSort(void) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4_API_CHECK(Configuration::isBuiltWithSymFPU()) + << "Expected CVC4 to be compiled with SymFPU support"; return Sort(this, d_exprMgr->roundingModeType()); CVC4_API_SOLVER_TRY_CATCH_END; } @@ -3323,6 +3333,8 @@ Sort Solver::mkBitVectorSort(uint32_t size) const Sort Solver::mkFloatingPointSort(uint32_t exp, uint32_t sig) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4_API_CHECK(Configuration::isBuiltWithSymFPU()) + << "Expected CVC4 to be compiled with SymFPU support"; CVC4_API_ARG_CHECK_EXPECTED(exp > 0, exp) << "exponent size > 0"; CVC4_API_ARG_CHECK_EXPECTED(sig > 0, sig) << "significand size > 0"; @@ -3803,6 +3815,8 @@ Term Solver::mkNegZero(uint32_t exp, uint32_t sig) const Term Solver::mkRoundingMode(RoundingMode rm) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4_API_CHECK(Configuration::isBuiltWithSymFPU()) + << "Expected CVC4 to be compiled with SymFPU support"; return mkValHelper(s_rmodes.at(rm)); CVC4_API_SOLVER_TRY_CATCH_END; } @@ -5396,7 +5410,7 @@ Term Solver::synthFunHelper(const std::string& symbol, { CVC4_API_CHECK(g->d_ntSyms[0].d_node->getType().toType() == *sort.d_type) << "Invalid Start symbol for Grammar g, Expected Start's sort to be " - << *sort.d_type; + << *sort.d_type << " but found " << g->d_ntSyms[0].d_node->getType(); } Type funType = varTypes.empty() diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index 0c322d7da..d92660920 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -2152,6 +2152,12 @@ class CVC4_PUBLIC Solver Solver(const Solver&) = delete; Solver& operator=(const Solver&) = delete; + /* .................................................................... */ + /* Solver Configuration */ + /* .................................................................... */ + + bool supportsFloatingPoint() const; + /* .................................................................... */ /* Sorts Handling */ /* .................................................................... */ @@ -2184,7 +2190,7 @@ class CVC4_PUBLIC Solver /** * @return sort RoundingMode */ - Sort getRoundingmodeSort() const; + Sort getRoundingModeSort() const; /** * @return sort String @@ -3169,7 +3175,9 @@ class CVC4_PUBLIC Solver Term mkSygusVar(Sort sort, const std::string& symbol = std::string()) const; /** - * Create a Sygus grammar. + * Create a Sygus grammar. The first non-terminal is treated as the starting + * non-terminal, so the order of non-terminals matters. + * * @param boundVars the parameters to corresponding synth-fun/synth-inv * @param ntSymbols the pre-declaration of the non-terminal symbols * @return the grammar diff --git a/src/api/python/cvc4.pxd b/src/api/python/cvc4.pxd index 16d64b85e..841fbb44d 100644 --- a/src/api/python/cvc4.pxd +++ b/src/api/python/cvc4.pxd @@ -116,11 +116,12 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api": cdef cppclass Solver: Solver(Options*) except + + bint supportsFloatingPoint() except + Sort getBooleanSort() except + Sort getIntegerSort() except + Sort getRealSort() except + Sort getRegExpSort() except + - Sort getRoundingmodeSort() except + + Sort getRoundingModeSort() except + Sort getStringSort() except + Sort mkArraySort(Sort indexSort, Sort elemSort) except + Sort mkBitVectorSort(uint32_t size) except + diff --git a/src/api/python/cvc4.pxi b/src/api/python/cvc4.pxi index a51307d21..3caead057 100644 --- a/src/api/python/cvc4.pxi +++ b/src/api/python/cvc4.pxi @@ -21,7 +21,8 @@ from cvc4 cimport Grammar as c_Grammar from cvc4 cimport Sort as c_Sort from cvc4 cimport SortHashFunction as c_SortHashFunction from cvc4 cimport ROUND_NEAREST_TIES_TO_EVEN, ROUND_TOWARD_POSITIVE -from cvc4 cimport ROUND_TOWARD_ZERO, ROUND_NEAREST_TIES_TO_AWAY +from cvc4 cimport ROUND_TOWARD_NEGATIVE, ROUND_TOWARD_ZERO +from cvc4 cimport ROUND_NEAREST_TIES_TO_AWAY from cvc4 cimport Term as c_Term from cvc4 cimport TermHashFunction as c_TermHashFunction @@ -88,7 +89,7 @@ cdef class Datatype: if isinstance(index, int) and index >= 0: dc.cdc = self.cd[( index)] elif isinstance(index, str): - dc.cdc = self.cd[( name.encode())] + dc.cdc = self.cd[( index.encode())] else: raise ValueError("Expecting a non-negative integer or string") return dc @@ -395,6 +396,9 @@ cdef class Solver: def __dealloc__(self): del self.csolver + def supportsFloatingPoint(self): + return self.csolver.supportsFloatingPoint() + def getBooleanSort(self): cdef Sort sort = Sort(self) sort.csort = self.csolver.getBooleanSort() @@ -415,9 +419,9 @@ cdef class Solver: sort.csort = self.csolver.getRegExpSort() return sort - def getRoundingmodeSort(self): + def getRoundingModeSort(self): cdef Sort sort = Sort(self) - sort.csort = self.csolver.getRoundingmodeSort() + sort.csort = self.csolver.getRoundingModeSort() return sort def getStringSort(self): @@ -1457,6 +1461,7 @@ cdef class Term: cdef __rounding_modes = { ROUND_NEAREST_TIES_TO_EVEN: "RoundNearestTiesToEven", ROUND_TOWARD_POSITIVE: "RoundTowardPositive", + ROUND_TOWARD_NEGATIVE: "RoundTowardNegative", ROUND_TOWARD_ZERO: "RoundTowardZero", ROUND_NEAREST_TIES_TO_AWAY: "RoundNearestTiesToAway" } diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 1e5d2155a..c4899c8a8 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -718,7 +718,7 @@ Command* Smt2::setLogic(std::string name, bool fromCommand) } if (d_logic.isTheoryEnabled(theory::THEORY_FP)) { - defineType("RoundingMode", d_solver->getRoundingmodeSort()); + defineType("RoundingMode", d_solver->getRoundingModeSort()); defineType("Float16", d_solver->mkFloatingPointSort(5, 11)); defineType("Float32", d_solver->mkFloatingPointSort(8, 24)); defineType("Float64", d_solver->mkFloatingPointSort(11, 53)); diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp index 9805f602e..878815811 100644 --- a/src/theory/logic_info.cpp +++ b/src/theory/logic_info.cpp @@ -23,6 +23,7 @@ #include #include "base/check.h" +#include "base/configuration.h" #include "expr/kind.h" using namespace std; @@ -43,7 +44,12 @@ LogicInfo::LogicInfo() d_higherOrder(true), d_locked(false) { - for(TheoryId id = THEORY_FIRST; id < THEORY_LAST; ++id) { + for (TheoryId id = THEORY_FIRST; id < THEORY_LAST; ++id) + { + if (id == THEORY_FP && !Configuration::isBuiltWithSymFPU()) + { + continue; + } enableTheory(id); } } diff --git a/test/regress/regress1/quantifiers/issue3481-unsat1.smt2 b/test/regress/regress1/quantifiers/issue3481-unsat1.smt2 index fb7ff5485..9cf535dc7 100644 --- a/test/regress/regress1/quantifiers/issue3481-unsat1.smt2 +++ b/test/regress/regress1/quantifiers/issue3481-unsat1.smt2 @@ -2,7 +2,7 @@ ; EXPECT: unsat ;; produced by cvc4_16.drv ;; -(set-logic AUFBVFPDTNIRA) +(set-logic AUFBVDTNIRA) (set-info :smt-lib-version 2.6) ;;; generated by SMT-LIB2 driver ;;; SMT-LIB2 driver: bit-vectors, common part diff --git a/test/regress/regress1/quantifiers/issue3481.smt2 b/test/regress/regress1/quantifiers/issue3481.smt2 index fe8c84d62..3d9bfe981 100644 --- a/test/regress/regress1/quantifiers/issue3481.smt2 +++ b/test/regress/regress1/quantifiers/issue3481.smt2 @@ -3,7 +3,7 @@ ;; produced by cvc4_16.drv ;; (set-info :smt-lib-version 2.6) -(set-logic AUFBVFPDTNIRA) +(set-logic AUFBVDTNIRA) ;;; generated by SMT-LIB2 driver ;;; SMT-LIB2 driver: bit-vectors, common part ;;; SMT-LIB2: integer arithmetic diff --git a/test/unit/api/python/test_sort.py b/test/unit/api/python/test_sort.py index cd40fc807..5fdb49f48 100644 --- a/test/unit/api/python/test_sort.py +++ b/test/unit/api/python/test_sort.py @@ -223,21 +223,31 @@ def testGetBVSize(): def testGetFPExponentSize(): solver = pycvc4.Solver() - fpSort = solver.mkFloatingPointSort(4, 8) - fpSort.getFPExponentSize() - setSort = solver.mkSetSort(solver.getIntegerSort()) - with pytest.raises(Exception): - setSort.getFPExponentSize() + if solver.supportsFloatingPoint(): + fpSort = solver.mkFloatingPointSort(4, 8) + fpSort.getFPExponentSize() + setSort = solver.mkSetSort(solver.getIntegerSort()) + + with pytest.raises(Exception): + setSort.getFPExponentSize() + else: + with pytest.raises(Exception): + solver.mkFloatingPointSort(4, 8) def testGetFPSignificandSize(): solver = pycvc4.Solver() - fpSort = solver.mkFloatingPointSort(4, 8) - fpSort.getFPSignificandSize() - setSort = solver.mkSetSort(solver.getIntegerSort()) - with pytest.raises(Exception): - setSort.getFPSignificandSize() + if solver.supportsFloatingPoint(): + fpSort = solver.mkFloatingPointSort(4, 8) + fpSort.getFPSignificandSize() + setSort = solver.mkSetSort(solver.getIntegerSort()) + + with pytest.raises(Exception): + setSort.getFPSignificandSize() + else: + with pytest.raises(Exception): + solver.mkFloatingPointSort(4, 8) def testGetDatatypeParamSorts(): solver = pycvc4.Solver() diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h index 9837d6b00..11dbbb7ae 100644 --- a/test/unit/api/solver_black.h +++ b/test/unit/api/solver_black.h @@ -27,12 +27,14 @@ class SolverBlack : public CxxTest::TestSuite void setUp() override; void tearDown() override; + void testSupportsFloatingPoint(); + void testGetBooleanSort(); void testGetIntegerSort(); void testGetNullSort(); void testGetRealSort(); void testGetRegExpSort(); - void testGetRoundingmodeSort(); + void testGetRoundingModeSort(); void testGetStringSort(); void testMkArraySort(); @@ -169,6 +171,20 @@ void SolverBlack::setUp() { d_solver.reset(new Solver()); } void SolverBlack::tearDown() { d_solver.reset(nullptr); } +void SolverBlack::testSupportsFloatingPoint() +{ + if (d_solver->supportsFloatingPoint()) + { + TS_ASSERT_THROWS_NOTHING( + d_solver->mkRoundingMode(ROUND_NEAREST_TIES_TO_EVEN)); + } + else + { + TS_ASSERT_THROWS(d_solver->mkRoundingMode(ROUND_NEAREST_TIES_TO_EVEN), + CVC4ApiException&); + } +} + void SolverBlack::testGetBooleanSort() { TS_ASSERT_THROWS_NOTHING(d_solver->getBooleanSort()); @@ -199,9 +215,16 @@ void SolverBlack::testGetStringSort() TS_ASSERT_THROWS_NOTHING(d_solver->getStringSort()); } -void SolverBlack::testGetRoundingmodeSort() +void SolverBlack::testGetRoundingModeSort() { - TS_ASSERT_THROWS_NOTHING(d_solver->getRoundingmodeSort()); + if (d_solver->supportsFloatingPoint()) + { + TS_ASSERT_THROWS_NOTHING(d_solver->getRoundingModeSort()); + } + else + { + TS_ASSERT_THROWS(d_solver->getRoundingModeSort(), CVC4ApiException&); + } } void SolverBlack::testMkArraySort() @@ -210,15 +233,20 @@ void SolverBlack::testMkArraySort() Sort intSort = d_solver->getIntegerSort(); Sort realSort = d_solver->getRealSort(); Sort bvSort = d_solver->mkBitVectorSort(32); - Sort fpSort = d_solver->mkFloatingPointSort(3, 5); TS_ASSERT_THROWS_NOTHING(d_solver->mkArraySort(boolSort, boolSort)); TS_ASSERT_THROWS_NOTHING(d_solver->mkArraySort(intSort, intSort)); TS_ASSERT_THROWS_NOTHING(d_solver->mkArraySort(realSort, realSort)); TS_ASSERT_THROWS_NOTHING(d_solver->mkArraySort(bvSort, bvSort)); - TS_ASSERT_THROWS_NOTHING(d_solver->mkArraySort(fpSort, fpSort)); TS_ASSERT_THROWS_NOTHING(d_solver->mkArraySort(boolSort, intSort)); TS_ASSERT_THROWS_NOTHING(d_solver->mkArraySort(realSort, bvSort)); - TS_ASSERT_THROWS_NOTHING(d_solver->mkArraySort(bvSort, fpSort)); + + if (d_solver->supportsFloatingPoint()) + { + Sort fpSort = d_solver->mkFloatingPointSort(3, 5); + TS_ASSERT_THROWS_NOTHING(d_solver->mkArraySort(fpSort, fpSort)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkArraySort(bvSort, fpSort)); + } + Solver slv; TS_ASSERT_THROWS(slv.mkArraySort(boolSort, boolSort), CVC4ApiException&); } @@ -231,9 +259,16 @@ void SolverBlack::testMkBitVectorSort() void SolverBlack::testMkFloatingPointSort() { - TS_ASSERT_THROWS_NOTHING(d_solver->mkFloatingPointSort(4, 8)); - TS_ASSERT_THROWS(d_solver->mkFloatingPointSort(0, 8), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver->mkFloatingPointSort(4, 0), CVC4ApiException&); + if (d_solver->supportsFloatingPoint()) + { + TS_ASSERT_THROWS_NOTHING(d_solver->mkFloatingPointSort(4, 8)); + TS_ASSERT_THROWS(d_solver->mkFloatingPointSort(0, 8), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkFloatingPointSort(4, 0), CVC4ApiException&); + } + else + { + TS_ASSERT_THROWS(d_solver->mkFloatingPointSort(4, 8), CVC4ApiException&); + } } void SolverBlack::testMkDatatypeSort() @@ -480,8 +515,16 @@ void SolverBlack::testMkBoolean() void SolverBlack::testMkRoundingMode() { - TS_ASSERT_THROWS_NOTHING( - d_solver->mkRoundingMode(RoundingMode::ROUND_TOWARD_ZERO)); + if (CVC4::Configuration::isBuiltWithSymFPU()) + { + TS_ASSERT_THROWS_NOTHING( + d_solver->mkRoundingMode(RoundingMode::ROUND_TOWARD_ZERO)); + } + else + { + TS_ASSERT_THROWS(d_solver->mkRoundingMode(RoundingMode::ROUND_TOWARD_ZERO), + CVC4ApiException&); + } } void SolverBlack::testMkUninterpretedConst() -- 2.30.2