summaryrefslogtreecommitdiff
path: root/src/api
diff options
context:
space:
mode:
Diffstat (limited to 'src/api')
-rw-r--r--src/api/cvc4cpp.cpp18
-rw-r--r--src/api/cvc4cpp.h12
-rw-r--r--src/api/python/cvc4.pxd3
-rw-r--r--src/api/python/cvc4.pxi13
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"
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback