* datatype sort constructed for the datatype declaration it is associated
* with.
*
- * @apiNote Create unresolved sorts with Solver::mkUnresolvedSort().
+ * @api.note Create unresolved sorts with Solver::mkUnresolvedSort().
*
* @param dtypedecls the datatype declarations from which the sort is
* created
/**
* Create a sort parameter.
*
- * @apiNote This method is experimental and may change in future versions.
+ * @api.note This method is experimental and may change in future versions.
*
* @param symbol the name of the sort
* @return the sort parameter
/**
* Create a sort parameter.
*
- * @apiNote This method is experimental and may change in future versions.
+ * @api.note This method is experimental and may change in future versions.
*
* @return the sort parameter
*/
/**
* Create a record sort
*
- * @apiNote This method is experimental and may change in future versions.
+ * @api.note This method is experimental and may change in future versions.
*
* @param fields the list of fields of the record
* @return the record sort
* The Kind may not be the Kind for an indexed operator
* (e.g. BITVECTOR_EXTRACT).
*
- * @apiNote In this case, the Op simply wraps the Kind. The Kind can be used
+ * @api.note In this case, the Op simply wraps the Kind. The Kind can be used
* in mkTerm directly without creating an op first.
*
* @param kind the kind to wrap
/**
* Create a separation logic empty term.
*
- * @apiNote This method is experimental and may change in future versions.
+ * @api.note This method is experimental and may change in future versions.
*
* @return the separation logic empty term
*/
/**
* Create a separation logic nil term.
*
- * @apiNote This method is experimental and may change in future versions.
+ * @api.note This method is experimental and may change in future versions.
*
* @param sort the sort of the nil term
* @return the separation logic nil term
/**
* Create a bit-vector constant of given size and value.
*
- * @apiNote The given value must fit into a bit-vector of the given size.
+ * @api.note The given value must fit into a bit-vector of the given size.
*
* @param size the bit-width of the bit-vector sort
* @param val the value of the constant
* Create a bit-vector constant of a given bit-width from a given string of
* base 2, 10 or 16.
*
- * @apiNote The given value must fit into a bit-vector of the given size.
+ * @api.note The given value must fit into a bit-vector of the given size.
*
* @param size the bit-width of the constant
* @param s the string representation of the constant
/**
* Create a cardinality constraint for an uninterpreted sort.
*
- * @apiNote This method is experimental and may change in future versions.
+ * @api.note 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
* 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.
+ * @api.note This method is experimental and may change in future versions.
*
* @param t the formula to simplify
* @return the simplified formula
* ( declare-sort <symbol> <numeral> )
* }
*
- * @apiNote This corresponds to mkUninterpretedSort() const if arity = 0, and
+ * @api.note This corresponds to mkUninterpretedSort() const if arity = 0, and
* to mkUninterpretedSortConstructorSort() const if arity > 0.
*
* @param symbol the name of the sort
* ( get-learned-literals )
* }
*
- * @apiNote This method is experimental and may change in future versions.
+ * @api.note This method is experimental and may change in future versions.
*
* @return the list of learned literals
*/
* }
* Requires to enable option 'produce-unsat-cores'.
*
- * @apiNote In contrast to SMT-LIB, the API does not distinguish between
+ * @api.note In contrast to SMT-LIB, the API does not distinguish between
* named and unnamed assertions when producing an unsatisfiable
* core. Additionally, the API allows this option to be called after
* a check with assumptions. A subset of those assumptions may be
* 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.
+ * @api.note 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
* }
* Requires to enable option 'produce-proofs'.
*
- * @apiNote This method is experimental and may change in future versions.
+ * @api.note This method is experimental and may change in future versions.
*
* @return a string representing the proof, according to the value of
* proof-format-mode.
* current model. This method will only return false (for any v) if
* the model-cores option has been set.
*
- * @apiNote This method is experimental and may change in future versions.
+ * @api.note This method is experimental and may change in future versions.
*
* @param v The term in question
* @return true if v is a model core symbol
* }
* Requires to enable option 'produce-models'.
*
- * @apiNote This method is experimental and may change in future versions.
+ * @api.note This method is experimental and may change in future versions.
*
* @param sorts The list of uninterpreted sorts that should be printed in the
* model.
* 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.
+ * @api.note 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 )
* 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.
+ * @api.note 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 )
* datatype sort to the given ones. This method should be invoked exactly
* once, before any separation logic constraints are provided.
*
- * @apiNote This method is experimental and may change in future versions.
+ * @api.note This method is experimental and may change in future versions.
*
* @param locSort The location sort of the heap
* @param dataSort The data sort of the heap
/**
* When using separation logic, obtain the term for the heap.
*
- * @apiNote This method is experimental and may change in future versions.
+ * @api.note This method is experimental and may change in future versions.
*
* @return The term for the heap
*/
/**
* When using separation logic, obtain the term for nil.
*
- * @apiNote This method is experimental and may change in future versions.
+ * @api.note This method is experimental and may change in future versions.
*
* @return The term for nil
*/
* ( declare-pool <symbol> <sort> ( <term>* ) )
* }
*
- * @apiNote This method is experimental and may change in future versions.
+ * @api.note 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.
* }
* Requires 'produce-interpolants' to be set to a mode different from 'none'.
*
- * @apiNote This method is experimental and may change in future versions.
+ * @api.note This method is experimental and may change in future versions.
*
* @param conj the conjecture term
* @return a Term I such that {@code A->I} and {@code I->B} are valid, where
* }
* Requires 'produce-interpolants' to be set to a mode different from 'none'.
*
- * @apiNote This method is experimental and may change in future versions.
+ * @api.note This method is experimental and may change in future versions.
*
* @param conj the conjecture term
* @param grammar the grammar for the interpolant I
* set to a mode different from 'none'.
* \endverbatim
*
- * @apiNote This method is experimental and may change in future versions.
+ * @api.note This method is experimental and may change in future versions.
*
* @return a Term I such that {@code A->I} and {@code I->B} are valid,
* where A is the current set of assertions and B is given in the input
* }
* Requires enabling option 'produce-abducts'
*
- * @apiNote This method is experimental and may change in future versions.
+ * @api.note This method is experimental and may change in future versions.
*
* @param conj the conjecture term
* @return a term C such that A^C is satisfiable, and A^~B^C is
* }
* Requires enabling option 'produce-abducts'
*
- * @apiNote This method is experimental and may change in future versions.
+ * @api.note This method is experimental and may change in future versions.
*
* @param conj the conjecture term
* @param grammar the grammar for the abduct C
* }
* Requires enabling incremental mode and option 'produce-abducts'
*
- * @apiNote This method is experimental and may change in future versions.
+ * @api.note This method is experimental and may change in future versions.
*
* @return a term C such that A^C is satisfiable, and A^~B^C is
* unsatisfiable, where A is the current set of assertions and B is
* Requires enabling 'produce-models' option and setting 'block-models' option
* to a mode other than "none".
*
- * @apiNote This method is experimental and may change in future versions.
+ * @api.note This method is experimental and may change in future versions.
*/
public void blockModel()
{
* }
* Requires enabling 'produce-models' option.
*
- * @apiNote This method is experimental and may change in future versions.
+ * @api.note This method is experimental and may change in future versions.
*/
public void blockModelValues(Term[] terms)
{
* Return a string that contains information about all instantiations made by
* the quantifiers module.
*
- * @apiNote This method is experimental and may change in future versions.
+ * @api.note This method is experimental and may change in future versions.
*/
public String getInstantiations()
{
projects / cvc5.git / commitdiff