diff options
Diffstat (limited to 'src/api')
-rw-r--r-- | src/api/cvc4cpp.cpp | 18 | ||||
-rw-r--r-- | src/api/cvc4cpp.h | 12 | ||||
-rw-r--r-- | src/api/python/cvc4.pxd | 3 | ||||
-rw-r--r-- | src/api/python/cvc4.pxi | 13 |
4 files changed, 37 insertions, 9 deletions
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<CVC4::RoundingMode>(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 @@ -2153,6 +2153,12 @@ class CVC4_PUBLIC Solver 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[(<int?> index)] elif isinstance(index, str): - dc.cdc = self.cd[(<const string &> name.encode())] + dc.cdc = self.cd[(<const string &> 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 = { <int> ROUND_NEAREST_TIES_TO_EVEN: "RoundNearestTiesToEven", <int> ROUND_TOWARD_POSITIVE: "RoundTowardPositive", + <int> ROUND_TOWARD_NEGATIVE: "RoundTowardNegative", <int> ROUND_TOWARD_ZERO: "RoundTowardZero", <int> ROUND_NEAREST_TIES_TO_AWAY: "RoundNearestTiesToAway" } |