/**
* Is this a record sort?
+ * @warning This method is experimental and may change in future versions.
* @return true if the sort is a record sort
*/
bool isRecord() const;
size_t getNumConstructors() const;
/**
+ * @warning This method is experimental and may change in future versions.
+ *
* @return the parameters of this datatype, if it is parametric. An exception
* is thrown if this datatype is not parametric.
*/
std::vector<Sort> getParameters() const;
- /** @return true if this datatype is parametric */
+ /**
+ * @warning This method is experimental and may change in future versions.
+ * @return true if this datatype is parametric
+ */
bool isParametric() const;
/** @return true if this datatype corresponds to a co-datatype */
/** @return true if this datatype corresponds to a tuple */
bool isTuple() const;
- /** @return true if this datatype corresponds to a record */
+ /**
+ * @warning This method is experimental and may change in future versions.
+ * @return true if this datatype corresponds to a record
+ */
bool isRecord() const;
/** @return true if this datatype is finite */
/**
* Create a sort parameter.
+ *
+ * @warning This method is experimental and may change in future versions.
+ *
* @param symbol the name of the sort
* @return the sort parameter
*/
/**
* Create a record sort
+ *
+ * @warning This method is experimental and may change in future versions.
+ *
* @param fields the list of fields of the record
* @return the record sort
*/
/**
* Create a cardinality constraint for an uninterpreted sort.
+ *
+ * @warning This method is experimental and may change in future versions.
+ *
* @param sort the sort the cardinality constraint is for
* @param upperBound the upper bound on the cardinality of the sort
* @return the cardinality constraint
/* Create datatype constructor declarations */
/* .................................................................... */
+ /**
+ * Create a datatype constructor declaration.
+ * @param name the name of the datatype constructor
+ * @return the DatatypeConstructorDecl
+ */
DatatypeConstructorDecl mkDatatypeConstructorDecl(const std::string& name);
/* .................................................................... */
* the SAT Engine in the simplification, but uses the current
* definitions, assertions, and the current partial model, if one
* has been constructed. It also involves theory normalization.
+ *
+ * @warning This method is experimental and may change in future versions.
+ *
* @param t the formula to simplify
* @return the simplified formula
*/
* Get a difficulty estimate for an asserted formula. This method is
* intended to be called immediately after any response to a checkSat.
*
+ * @warning This method is experimental and may change in future versions.
+ *
* @return a map from (a subset of) the input assertions to a real value that
* is an estimate of how difficult each assertion was to solve.
* Unmentioned assertions can be assumed to have zero difficulty.
* (get-qe <q>)
* \endverbatim
*
- * Requires a logic that supports quantifier elimination. Currently, the only
- * logics supported by quantifier elimination is LRA and LIA.
+ * @note Quantifier Elimination is is only complete for logics such as LRA,
+ * LIA and BV.
*
- * @note Quantifier Elimination is is only complete for LRA and LIA.
+ * @warning This method is experimental and may change in future versions.
*
* @param q a quantified formula of the form
* @f$Q\bar{x}_1... Q\bar{x}_n. P( x_1...x_i, y_1...y_j)@f$
* (get-qe-disjunct <q>)
* \endverbatim
*
- * Requires a logic that supports quantifier elimination. Currently, the only
- * logics supported by quantifier elimination is LRA and LIA.
+ * @note Quantifier Elimination is is only complete for logics such as LRA,
+ * LIA and BV.
+ *
+ * @warning This method is experimental and may change in future versions.
+ *
* @param q a quantified formula of the form
* @f$Q\bar{x}_1... Q\bar{x}_n. P( x_1...x_i, y_1...y_j)@f$
* where
* (declare-pool <symbol> <sort> ( <term>* ))
* \endverbatim
*
+ * @warning This method is experimental and may change in future versions.
+ *
* @param symbol The name of the pool
* @param sort The sort of the elements of the pool.
* @param initValue The initial value of the pool
*
* @note The sort of the term must be convertible into the target sort.
* Currently only Int to Real conversions are supported.
+ *
+ * @warning This method is experimental and may change in future versions.
+ *
* @param t the term
* @param s the target sort
* @return the term wrapped into a sort conversion if needed
private native int getNumConstructors(long pointer);
/**
+ * @apiNote This method is experimental and may change in future versions.
+ *
* @return the parameters of this datatype, if it is parametric. An exception
* is thrown if this datatype is not parametric.
*/
private native long[] getParameters(long pointer);
- /** @return true if this datatype is parametric */
+ /**
+ * @apiNote This method is experimental and may change in future versions.
+ *
+ * @return true if this datatype is parametric
+ */
public boolean isParametric()
{
return isParametric(pointer);
private native boolean isTuple(long pointer);
- /** @return true if this datatype corresponds to a record */
+ /**
+ * @apiNote This method is experimental and may change in future versions.
+ *
+ * @return true if this datatype corresponds to a record
+ */
public boolean isRecord()
{
return isRecord(pointer);
/**
* Create a sort parameter.
+ *
+ * @apiNote This method is experimental and may change in future versions.
+ *
* @param symbol the name of the sort
* @return the sort parameter
*/
/**
* Create a record sort
+ *
+ * @apiNote This method is experimental and may change in future versions.
+ *
* @param fields the list of fields of the record
* @return the record sort
*/
/**
* Create a cardinality constraint for an uninterpreted sort.
+ *
+ * @apiNote This method is experimental and may change in future versions.
+ *
* @param sort the sort the cardinality constraint is for
* @param upperBound the upper bound on the cardinality of the sort
* @return the cardinality constraint
/* Create datatype constructor declarations */
/* .................................................................... */
+ /**
+ * Create a datatype constructor declaration.
+ * @param name the name of the datatype constructor
+ * @return the DatatypeConstructorDecl
+ */
public DatatypeConstructorDecl mkDatatypeConstructorDecl(String name)
{
long declPointer = mkDatatypeConstructorDecl(pointer, name);
* the SAT Engine in the simplification, but uses the current
* definitions, assertions, and the current partial model, if one
* has been constructed. It also involves theory normalization.
+ *
+ * @apiNote This method is experimental and may change in future versions.
+ *
* @param t the formula to simplify
* @return the simplified formula
*/
long[] termPointers,
boolean global);
- /**
- * Echo a given string to the given output stream.
- * SMT-LIB:
- * {@code
- * ( echo <std::string> )
- * }
- * @param out the output stream
- * @param str the string to echo
- */
- // TODO: void echo(std::ostream& out, String str)
-
/**
* Get a list of literals that are entailed by the current set of assertions
* SMT-LIB:
* Get a difficulty estimate for an asserted formula. This method is
* intended to be called immediately after any response to a checkSat.
*
+ * @apiNote This method is experimental and may change in future versions.
+ *
* @return a map from (a subset of) the input assertions to a real value that
* is an estimate of how difficult each assertion was to solve. Unmentioned
* assertions can be assumed to have zero difficulty.
* {@code
* ( get-qe <q> )
* }
- * Requires a logic that supports quantifier elimination. Currently, the only
- * logics supported by quantifier elimination is LRA and LIA.
+ * Quantifier Elimination is is only complete for logics such as LRA,
+ * LIA and BV.
+ *
+ * @apiNote This method is experimental and may change in future versions.
+ *
* @param q a quantified formula of the form:
* Q x1...xn. P( x1...xn, y1...yn )
* where P( x1...xn, y1...yn ) is a quantifier-free formula
* {@code
* ( get-qe-disjunct <q> )
* }
- * Requires a logic that supports quantifier elimination. Currently, the only
- * logics supported by quantifier elimination is LRA and LIA.
+ * Quantifier Elimination is is only complete for logics such as LRA,
+ * LIA and BV.
+ *
+ * @apiNote This method is experimental and may change in future versions.
+ *
* @param q a quantified formula of the form:
* Q x1...xn. P( x1...xn, y1...yn )
* where P( x1...xn, y1...yn ) is a quantifier-free formula
* {@code
* ( declare-pool <symbol> <sort> ( <term>* ) )
* }
+ *
+ * @apiNote This method is experimental and may change in future versions.
+ *
* @param symbol The name of the pool
* @param sort The sort of the elements of the pool.
* @param initValue The initial value of the pool
*
* @apiNote The sort of the term must be convertible into the target sort.
* Currently only Int to Real conversions are supported.
+ *
+ * @apiNote This method is experimental and may change in future versions.
+ *
* @param t the term
* @param s the target sort
* @return the term wrapped into a sort conversion if needed
/**
* Is this a record sort?
+ *
+ * @apiNote This method is experimental and may change in future versions.
+ *
* @return true if the sort is a record sort
*/
public boolean isRecord()
return param_sorts
def isParametric(self):
- """:return: True if this datatype is parametric."""
+ """
+ .. warning:: This method is experimental and may change in future
+ versions.
+ :return: True if this datatype is parametric.
+ """
return self.cd.isParametric()
def isCodatatype(self):
return self.cd.isTuple()
def isRecord(self):
- """:return: True if this datatype corresponds to a record."""
+ """
+ .. warning:: This method is experimental and may change in future
+ versions.
+ :return: True if this datatype corresponds to a record.
+ """
return self.cd.isRecord()
def isFinite(self):
def mkParamSort(self, symbolname):
""" Create a sort parameter.
+ .. warning:: This method is experimental and may change in future
+ versions.
+
:param symbol: the name of the sort
:return: the sort parameter
"""
def mkRecordSort(self, *fields):
"""Create a record sort
+ .. warning:: This method is experimental and may change in future
+ versions.
+
:param fields: the list of fields of the record, as a list or as distinct arguments
:return: the record sort
"""
def mkCardinalityConstraint(self, Sort sort, int index):
"""Create cardinality constraint.
+ .. warning:: This method is experimental and may change in future
+ versions.
+
:param sort: Sort of the constraint
:param index: The upper bound for the cardinality of the sort
"""
def mkDatatypeConstructorDecl(self, str name):
"""
- :return: a datatype constructor declaration
:param name: the constructor's name
+ :return: the DatatypeConstructorDecl
"""
cdef DatatypeConstructorDecl ddc = DatatypeConstructorDecl(self)
ddc.cddc = self.csolver.mkDatatypeConstructorDecl(name.encode())
assertions, and the current partial model, if one has been constructed.
It also involves theory normalization.
+ .. warning:: This method is experimental and may change in future
+ versions.
+
:param t: the formula to simplify
:return: the simplified formula
"""
def getValueSepHeap(self):
"""When using separation logic, obtain the term for the heap.
+ .. warning:: This method is experimental and may change in future
+ versions.
+
:return: The term for the heap
"""
cdef Term term = Term(self)
def getValueSepNil(self):
"""When using separation logic, obtain the term for nil.
+ .. warning:: This method is experimental and may change in future
+ versions.
+
:return: The term for nil
"""
cdef Term term = Term(self)
"""
Is this a record sort?
+ .. warning:: This method is experimental and may change in future
+ versions.
+
:return: True if the sort is a record sort.
"""
return self.csort.isRecord()
projects / cvc5.git / commitdiff