private native long getBooleanSort(long pointer);
/**
- * @return Sort Integer (in cvc5, Integer is a subtype of Real).
+ * @return Sort Integer.
*/
public Sort getIntegerSort()
{
/**
* Create an operator for a builtin Kind
* The Kind may not be the Kind for an indexed operator
- * (e.g. BITVECTOR_EXTRACT).
+ * (e.g. {@link Kind#BITVECTOR_EXTRACT}).
*
* @api.note In this case, the Op simply wraps the Kind. The Kind can be used
* in mkTerm directly without creating an op first.
private native long mkOp(long pointer, int kindValue);
/**
* Create operator of kind:
- * - RECORD_UPDATE
- * - DIVISIBLE (to support arbitrary precision integers)
+ * <ul>
+ * <li>
+ * {@link Kind#DIVISIBLE} (to support arbitrary precision integers)
+ * </li>
+ * </ul>
* See enum {@link Kind} for a description of the parameters.
* @param kind The kind of the operator.
* @param arg The string argument to this operator.
/**
* Create operator of kind:
- * - DIVISIBLE
- * - BITVECTOR_REPEAT
- * - BITVECTOR_ZERO_EXTEND
- * - BITVECTOR_SIGN_EXTEND
- * - BITVECTOR_ROTATE_LEFT
- * - BITVECTOR_ROTATE_RIGHT
- * - INT_TO_BITVECTOR
- * - FLOATINGPOINT_TO_UBV
- * - FLOATINGPOINT_TO_UBV_TOTAL
- * - FLOATINGPOINT_TO_SBV
- * - FLOATINGPOINT_TO_SBV_TOTAL
- * - TUPLE_UPDATE
+ * <ul>
+ * <li>DIVISIBLE</li>
+ * <li>BITVECTOR_REPEAT</li>
+ * <li>BITVECTOR_ZERO_EXTEND</li>
+ * <li>BITVECTOR_SIGN_EXTEND</li>
+ * <li>BITVECTOR_ROTATE_LEFT</li>
+ * <li>BITVECTOR_ROTATE_RIGHT</li>
+ * <li>INT_TO_BITVECTOR</li>
+ * <li>FLOATINGPOINT_TO_UBV</li>
+ * <li>FLOATINGPOINT_TO_UBV_TOTAL</li>
+ * <li>FLOATINGPOINT_TO_SBV</li>
+ * <li>FLOATINGPOINT_TO_SBV_TOTAL</li>
+ * <li>TUPLE_UPDATE</li>
+ * </ul>
* See enum {@link Kind} for a description of the parameters.
* @param kind The kind of the operator.
* @param arg The unsigned int argument to this operator.
/**
* Create operator of Kind:
- * - BITVECTOR_EXTRACT
- * - FLOATINGPOINT_TO_FP_FROM_IEEE_BV
- * - FLOATINGPOINT_TO_FP_FROM_FP
- * - FLOATINGPOINT_TO_FP_FROM_REAL
- * - FLOATINGPOINT_TO_FP_FROM_SBV
- * - FLOATINGPOINT_TO_FP_FROM_UBV
+ * <ul>
+ * <li>BITVECTOR_EXTRACT</li>
+ * <li>FLOATINGPOINT_TO_FP_FROM_IEEE_BV</li>
+ * <li>FLOATINGPOINT_TO_FP_FROM_FP</li>
+ * <li>FLOATINGPOINT_TO_FP_FROM_REAL</li>
+ * <li>FLOATINGPOINT_TO_FP_FROM_SBV</li>
+ * <li>FLOATINGPOINT_TO_FP_FROM_UBV</li>
+ * </ul>
* See enum {@link Kind} for a description of the parameters.
* @param kind The kind of the operator.
* @param arg1 The first unsigned int argument to this operator.
/**
* Create operator of Kind:
- * - TUPLE_PROJECT
+ * <ul>
+ * <li>TUPLE_PROJECT</li>
+ * </ul>
* See enum {@link Kind} for a description of the parameters.
* @param kind The kind of the operator.
* @param args The arguments (indices) of the operator.
/* .................................................................... */
/**
- * Create a Boolean true constant.
+ * Create a Boolean {@code true} constant.
* @return The true constant.
*/
public Term mkTrue()
private native long mkTrue(long pointer);
/**
- * Create a Boolean false constant.
+ * Create a Boolean {@code false} constant.
* @return The false constant.
*/
public Term mkFalse()
* Create an integer constant from a string.
* @param s The string representation of the constant, may represent an.
* integer (e.g., "123").
- * @return A constant of sort Integer assuming 's' represents an integer)
+ * @return A constant of sort Integer assuming {@code s} represents an
+ * integer).
* @throws CVC5ApiException
*/
public Term mkInteger(String s) throws CVC5ApiException
private native long mkInteger(long pointer, String s) throws CVC5ApiException;
/**
- * Create an integer constant from a c++ int.
+ * Create an integer constant from a C++ {@code int}.
* @param val The value of the constant.
* @return A constant of sort Integer.
*/
private native long mkReal(long pointer, long num, long den);
/**
- * Create a regular expression none (re.none) term.
+ * Create a regular expression none ({@code re.none}) term.
* @return The none term.
*/
public Term mkRegexpNone()
private native long mkRegexpNone(long pointer);
/**
- * Create a regular expression all (re.all) term.
+ * Create a regular expression all ({@code re.all}) term.
* @return The all term.
*/
public Term mkRegexpAll()
private native long mkRegexpAll(long pointer);
/**
- * Create a regular expression allchar (re.allchar) term.
+ * Create a regular expression allchar ({@code re.allchar}) term.
* @return The allchar term.
*/
public Term mkRegexpAllchar()
/**
* Create a String constant.
* @param s The string this constant represents.
- * @param useEscSequences Determines whether escape sequences in `s`
- * should be converted to the corresponding unicode character
+ * @param useEscSequences Determines whether escape sequences in {@code s}
+ * should be converted to the corresponding unicode
+ * character.
* @return The String constant.
*/
public Term mkString(String s, boolean useEscSequences)
/**
* Create a String constant.
- * @param s A list of unsigned (unicode) values this constant represents.
- * as
- * string
+ * @param s A list of unsigned (unicode) values this constant represents
+ * as string.
* @return The String constant.
* @throws CVC5ApiException
*/
* Create a constant array with the provided constant value stored at
* every index
* @param sort The sort of the constant array (must be an array sort)
- * @param val The constant value to store (must match the sort's element.
- * sort)
+ * @param val The constant value to store (must match the sort's element
+ * sort).
* @return The constant array term.
*/
public Term mkConstArray(Sort sort, Term val)
private native long mkConstArray(long pointer, long sortPointer, long valPointer);
/**
- * Create a positive infinity floating-point constant.
+ * Create a positive infinity floating-point constant (SMT-LIB: {@code +oo}).
* @param exp Number of bits in the exponent.
* @param sig Number of bits in the significand.
* @return The floating-point constant.
private native long mkFloatingPointPosInf(long pointer, int exp, int sig);
/**
- * Create a negative infinity floating-point constant.
+ * Create a negative infinity floating-point constant (SMT-LIB: {@code -oo}).
* @param exp Number of bits in the exponent.
* @param sig Number of bits in the significand.
* @return The floating-point constant.
private native long mkFloatingPointNegInf(long pointer, int exp, int sig);
/**
- * Create a not-a-number (NaN) floating-point constant.
+ * Create a not-a-number floating-point constant (SMT-LIB: {@code NaN}).
* @param exp Number of bits in the exponent.
* @param sig Number of bits in the significand.
* @return The floating-point constant.
private native long mkFloatingPointNaN(long pointer, int exp, int sig);
/**
- * Create a positive zero (+0.0) floating-point constant.
+ * Create a positive zero floating-point constant (SMT-LIB: {@code +zero}).
* @param exp Number of bits in the exponent.
* @param sig Number of bits in the significand.
* @return The floating-point constant.
private native long mkFloatingPointPosZero(long pointer, int exp, int sig);
/**
- * Create a negative zero (-0.0) floating-point constant.
+ * Create a negative zero floating-point constant (SMT-LIB: {@code -zero}).
* @param exp Number of bits in the exponent.
* @param sig Number of bits in the significand.
* @return The floating-point constant.
private native long mkFloatingPointNegZero(long pointer, int exp, int sig);
/**
- * Create a roundingmode constant.
+ * Create a rounding mode constant.
* @param rm The floating point rounding mode this constant represents.
*/
public Term mkRoundingMode(RoundingMode rm)
/* .................................................................... */
/**
- * Create (first-order) constant (0-arity function symbol).
+ * Create a free constant.
+ *
* SMT-LIB:
* {@code
* ( declare-const <symbol> <sort> )
private native long mkConst(long pointer, long sortPointer, String symbol);
/**
- * Create (first-order) constant (0-arity function symbol), with a default
- * symbol name.
+ * Create a free constant with a default symbol name.
*
* @param sort The sort of the constant.
* @return The first-order constant.
private native long mkConst(long pointer, long sortPointer);
/**
- * Create a bound variable to be used in a binder (i.e. a quantifier, a
+ * Create a bound variable to be used in a binder (i.e., a quantifier, a
* lambda, or a witness binder).
* @param sort The sort of the variable.
* @return The variable.
}
/**
- * Create a bound variable to be used in a binder (i.e. a quantifier, a
+ * Create a bound variable to be used in a binder (i.e., a quantifier, a
* lambda, or a witness binder).
* @param sort The sort of the variable.
* @param symbol The name of the variable.
/**
* Create a datatype declaration.
- * Create sorts parameter with Solver::mkParamSort().
+ *
+ * Create sorts parameter with {@link Solver#mkParamSort(String)}.
*
* @api.note This method is experimental and may change in future versions.
*
/**
* Create a datatype declaration.
- * Create sorts parameter with Solver::mkParamSort().
+ *
+ * Create sorts parameter with {@link Solver#mkParamSort(String)}.
+ *
* @param name The name of the datatype.
* @param params A list of sort parameters.
* @param isCoDatatype True if a codatatype is to be constructed.
/* .................................................................... */
/**
- * Simplify a formula without doing "much" work. Does not involve
- * 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.
+ * Simplify a formula without doing "much" work.
+ *
+ * Does not involve 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.
*
* @api.note This method is experimental and may change in future versions.
*
/**
* Check satisfiability.
+ *
* SMT-LIB:
* {@code
* ( check-sat )
* }
+ *
* @return The result of the satisfiability check.
*/
public Result checkSat()
private native long checkSat(long pointer);
/**
* Check satisfiability assuming the given formula.
+ *
* SMT-LIB:
* {@code
* ( check-sat-assuming ( <prop_literal> ) )
* }
+ *
* @param assumption The formula to assume.
* @return The result of the satisfiability check.
*/
/**
* Check satisfiability assuming the given formulas.
+ *
* SMT-LIB:
* {@code
* ( check-sat-assuming ( <prop_literal>+ ) )
* }
+ *
* @param assumptions The formulas to assume.
* @return The result of the satisfiability check.
*/
/**
* Create datatype sort.
+ *
* SMT-LIB:
* {@code
* ( declare-datatype <symbol> <datatype_decl> )
* }
+ *
* @param symbol The name of the datatype sort.
* @param ctors The constructor declarations of the datatype sort.
* @return The datatype sort.
/**
* Declare n-ary function symbol.
+ *
* SMT-LIB:
* {@code
* ( declare-fun <symbol> ( <sort>* ) <sort> )
* }
+ *
* @param symbol The name of the function.
* @param sorts The sorts of the parameters to this function.
* @param sort The sort of the return value of this function.
/**
* Declare uninterpreted sort.
+ *
* SMT-LIB:
* {@code
* ( declare-sort <symbol> <numeral> )
* }
*
* @api.note This corresponds to mkUninterpretedSort() const if arity = 0, and
- * to mkUninterpretedSortConstructorSort() const if arity > 0.
+ * to mkUninterpretedSortConstructorSort() const if arity > 0.
*
* @param symbol The name of the sort.
* @param arity The arity of the sort.
/**
* Define n-ary function in the current context.
+ *
* SMT-LIB:
* {@code
* ( define-fun <function_def> )
* }
+ *
* @param symbol The name of the function.
* @param boundVars The parameters to this function.
* @param sort The sort of the return value of this function.
/**
* Define n-ary function.
+ *
* SMT-LIB:
* {@code
* ( define-fun <function_def> )
* }
+ *
* @param symbol The name of the function.
* @param boundVars The parameters to this function.
* @param sort The sort of the return value of this function.
/**
* Define recursive function in the current context.
+ *
* SMT-LIB:
* {@code
* ( define-fun-rec <function_def> )
* }
+ *
* @param symbol The name of the function.
* @param boundVars The parameters to this function.
* @param sort The sort of the return value of this function.
/**
* Define recursive function.
+ *
* SMT-LIB:
* {@code
* ( define-fun-rec <function_def> )
* }
+ *
* @param symbol The name of the function.
* @param boundVars The parameters to this function.
* @param sort The sort of the return value of this function.
/**
* Define recursive function in the current context.
+ *
* SMT-LIB:
* {@code
* ( define-fun-rec <function_def> )
* }
- * Create parameter 'fun' with mkConst().
+ *
+ * Create parameter {@code fun} with {@link Solver#mkConst(Sort)}.
+ *
* @param fun The sorted function.
* @param boundVars The parameters to this function.
* @param term The function body.
/**
* Define recursive function.
+ *
* SMT-LIB:
* {@code
* ( define-fun-rec <function_def> )
* }
- * Create parameter 'fun' with mkConst().
+ *
+ * Create parameter {@code fun} with {@link Solver#mkConst(Sort)}.
+ *
* @param fun The sorted function.
* @param boundVars The parameters to this function.
* @param term The function body.
/**
* Define recursive functions in the current context.
+ *
* SMT-LIB:
* {@code
* ( define-funs-rec ( <function_decl>^{n+1} ) ( <term>^{n+1} ) )
* }
- * Create elements of parameter 'funs' with mkConst().
+ *
+ * Create elements of parameter {@code funs} with
+ * {@link Solver#mkConst(Sort)}.
+ *
* @param funs The sorted functions.
* @param boundVars The list of parameters to the functions.
* @param terms The list of function bodies of the functions.
}
/**
* Define recursive functions.
+ *
* SMT-LIB:
* {@code
* ( define-funs-rec ( <function_decl>^{n+1} ) ( <term>^{n+1} ) )
* }
- * Create elements of parameter 'funs' with mkConst().
+ *
+ * Create elements of parameter {@code funs} with
+ * {@link Solver#mkConst(Sort)}.
+ *
* @param funs The sorted functions.
* @param boundVars The list of parameters to the functions.
* @param terms The list of function bodies of the functions.
boolean global);
/**
- * Get a list of literals that are entailed by the current set of assertions
+ * Get a list of literals that are entailed by the current set of assertions.
+ *
* SMT-LIB:
* {@code
* ( get-learned-literals )
/**
* Get the list of asserted formulas.
+ *
* SMT-LIB:
* {@code
* ( get-assertions )
* }
+ *
* @return The list of asserted formulas.
*/
public Term[] getAssertions()
private native String getOption(long pointer, String option);
/**
- * Get all option names that can be used with `setOption`, `getOption` and
- * `getOptionInfo`.
+ * Get all option names that can be used with
+ * {@link Solver#setOption(String, String)},
+ * {@link Solver#getOption(String)} and
+ * {@link Solver#getOptionInfo(String)}.
* @return All option names.
*/
public String[] getOptionNames()
private native String[] getOptionNames(long pointer);
/**
- * Get some information about the given option. Check the `OptionInfo` class
- * for more details on which information is available.
+ * Get some information about the given option.
+ *
+ * Check the {@link OptionInfo} class for more details on which information
+ * is available.
+ *
* @return Information about the given option.
*/
public OptionInfo getOptionInfo(String option)
/**
* Get the set of unsat ("failed") assumptions.
+ *
* SMT-LIB:
* {@code
* ( get-unsat-assumptions )
* }
- * Requires to enable option 'produce-unsat-assumptions'.
+ *
+ * Requires to enable option {@code produce-unsat-assumptions}.
+ *
* @return The set of unsat assumptions.
*/
public Term[] getUnsatAssumptions()
* {@code
* (get-unsat-core)
* }
- * Requires to enable option 'produce-unsat-cores'.
+ * Requires to enable option {@code produce-unsat-cores}.
*
- * @api.note In contrast to SMT-LIB, the API does not distinguish between
+ * @api.note In contrast to SMT-LIB, cvc5's 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 the refutation proof
+ *
* SMT-LIB:
* {@code
* ( get-proof )
* }
- * Requires to enable option 'produce-proofs'.
+ *
+ * Requires to enable option {@code produce-proofs}.
*
* @api.note This method is experimental and may change in future versions.
*
/**
* Get the value of the given term in the current model.
+ *
* SMT-LIB:
* {@code
* ( get-value ( <term> ) )
* }
+ *
* @param term The term for which the value is queried.
* @return The value of the given term.
*/
/**
* Get the values of the given terms in the current model.
+ *
* SMT-LIB:
* {@code
* ( get-value ( <term>+ ) )
* }
+ *
* @param terms The terms for which the value is queried.
* @return The values of the given terms.
*/
private native long[] getValue(long pointer, long[] termPointers);
/**
- * Get the domain elements of uninterpreted sort s in the current model. The
- * current model interprets s as the finite sort whose domain elements are
- * given in the return value of this method.
+ * Get the domain elements of uninterpreted sort s in the current model.
+ *
+ * The current model interprets {@code s} as the finite sort whose domain
+ * elements are given in the return value of this method.
*
* @param s The uninterpreted sort in question.
- * @return The domain elements of s in the current model.
+ * @return The domain elements of {@code s} in the current model.
*/
public Term[] getModelDomainElements(Sort s)
{
private native long[] getModelDomainElements(long pointer, long sortPointer);
/**
- * This returns false if the model value of free constant v was not essential
- * for showing the satisfiability of the last call to checkSat using the
- * current model. This method will only return false (for any v) if
- * the model-cores option has been set.
+ * This returns false if the model value of free constant {@code v} was not
+ * essential for showing the satisfiability of the last call to
+ * {@link Solver#checkSat()} using the current model. This method will only
+ * return false (for any {@code v}) if the option {@code model-cores} has
+ * been set.
*
* @api.note This method is experimental and may change in future versions.
*
/**
* Get the model
+ *
* SMT-LIB:
* {@code
* ( get-model )
* }
- * Requires to enable option 'produce-models'.
+ *
+ * Requires to enable option {@code produce-models}.
*
* @api.note This method is experimental and may change in future versions.
*
/**
* Declare a symbolic pool of terms with the given initial value.
+ *
* SMT-LIB:
* {@code
* ( declare-pool <symbol> <sort> ( <term>* ) )
/**
* Pop a level from the assertion stack.
+ *
* SMT-LIB:
* {@code
* ( pop <numeral> )
* }
+ *
* @throws CVC5ApiException
*/
public void pop() throws CVC5ApiException
/**
* Pop (a) level(s) from the assertion stack.
+ *
* SMT-LIB:
* {@code
* ( pop <numeral> )
* }
+ *
* @param nscopes The number of levels to pop.
* @throws CVC5ApiException
*/
/**
* Get an interpolant
+ *
* SMT-LIB:
* {@code
* ( get-interpolant <conj> )
* }
- * Requires 'produce-interpolants' to be set to a mode different from 'none'.
+ *
+ * Requires option {@code produce-interpolants} to be set to a mode different
+ * from {@code none}.
*
* @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.
- * A is the current set of assertions and B is given in the input by
- * conj, or the null term if such a term cannot be found.
+ * @return A Term I such that {@code A->I} and {@code I->B} are valid, where
+ * {@code A} is the current set of assertions and {@code B} is given
+ * in the input by {@code conj}, or the null term if such a term
+ * cannot be found.
*/
public Term getInterpolant(Term conj)
{
/**
* Get an interpolant
+ *
* SMT-LIB:
* {@code
* ( get-interpolant <conj> <g> )
* }
- * Requires 'produce-interpolants' to be set to a mode different from 'none'.
+ *
+ * Requires option {@code produce-interpolants} to be set to a mode different
+ * from {@code none}.
*
* @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.
- * @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 by
- * conj, or the null term if such a term cannot be found.
+ * @return A Term I such that {@code A->I} and {@code I->B} are valid, where
+ * {@code A} is the current set of assertions and {@code B} is given
+ * in the input by {@code conj}, or the null term if such a term
+ * cannot be found.
*/
public Term getInterpolant(Term conj, Grammar grammar)
{
private native long getInterpolant(long pointer, long conjPointer, long grammarPointer);
/**
- * Get the next interpolant. Can only be called immediately after a successful
- * call to get-interpolant or get-interpolant-next. Is guaranteed to produce a
- * syntactically different interpolant wrt the last returned interpolant if
- * successful.
- *
- * SMT-LIB:
+ * Get the next interpolant.
*
- * \verbatim embed:rst:leading-asterisk
- * .. code:: smtlib
+ * Can only be called immediately after a successful call to
+ * {@code get-interpolant} or {@code get-interpolant-next}. Is guaranteed to
+ * produce a syntactically different interpolant wrt the last returned
+ * interpolant if successful.
*
+ * SMT-LIB:
+ * {@code
* (get-interpolant-next)
+ * }
*
- * Requires to enable incremental mode, and option 'produce-interpolants' to be
- * set to a mode different from 'none'.
- * \endverbatim
+ * Requires to enable incremental mode, and option
+ * {@code produce-interpolants} to be set to a mode different from
+ * {@code none}.
*
* @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
- * by conj on the last call to getInterpolant, or the null term if such
- * a term cannot be found.
+ * where {@code A} is the current set of assertions and {@code B}
+ * is given in the input by conj on the last call to getInterpolant,
+ * or the null term if such a term cannot be found.
*/
public Term getInterpolantNext()
{
/**
* Get an abduct.
+ *
* SMT-LIB:
* {@code
* ( get-abduct <conj> )
* }
- * Requires enabling option 'produce-abducts'
+ * Requires enabling option {@code produce-abducts}.
*
* @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.
- * unsatisfiable, where A is the current set of assertions and B is
- * given in the input by conj, or the null term if such a term cannot
- * be found.
+ * @return A term {@code C} such that {@code A && C} is satisfiable, and
+ * {@code A && ~B && C} is unsatisfiable, where {@code A} is the
+ * current set of assertions and {@code B} is given in the input by
+ * {@code conj}, or the null term if such a term cannot be found.
*/
public Term getAbduct(Term conj)
{
private native long getAbduct(long pointer, long conjPointer);
/**
* Get an abduct.
+ *
* SMT-LIB:
* {@code
* ( get-abduct <conj> <g> )
* }
- * Requires enabling option 'produce-abducts'
+ *
+ * Requires enabling option {@code produce-abducts}.
*
* @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.
- * @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
- * given in the input by conj, or the null term if such a term cannot
- * be found.
+ * @param grammar The grammar for the abduct {@code C}.
+ * @return A term {@code C} such that {@code A && C} is satisfiable, and
+ * {@code A && ~B && C} is unsatisfiable, where {@code A} is the
+ * current set of assertions and {@code B} is given in the input by
+ * {@code conj}, or the null term if such a term cannot be found.
*/
public Term getAbduct(Term conj, Grammar grammar)
{
* {@code
* ( get-abduct-next )
* }
- * Requires enabling incremental mode and option 'produce-abducts'
+ * Requires enabling incremental mode and option {@code produce-abducts}.
*
* @api.note This method is experimental and may change in future versions.
*
private native long getAbductNext(long pointer);
/**
- * Block the current model. Can be called only if immediately preceded by a
- * SAT or INVALID query.
+ * Block the current model.
+ *
+ * Can be called only if immediately preceded by a SAT or INVALID query.
+ *
* SMT-LIB:
* {@code
* ( block-model )
* }
- * Requires enabling 'produce-models' option and setting 'block-models' option
- * to a mode other than "none".
+ *
+ * Requires enabling option {@code produce-models}.
*
* @api.note This method is experimental and may change in future versions.
*
private native void blockModel(long pointer, int modeValue);
/**
- * Block the current model values of (at least) the values in terms. Can be
- * called only if immediately preceded by a SAT or NOT_ENTAILED query.
+ * Block the current model values of (at least) the values in terms.
+ *
+ * Can be called only if immediately preceded by a SAT or NOT_ENTAILED query.
+ *
* SMT-LIB:
* {@code
* ( block-model-values ( <terms>+ ) )
* }
- * Requires enabling 'produce-models' option.
+ *
+ * Requires enabling option {@code produce-models}.
*
* @api.note This method is experimental and may change in future versions.
*/
/**
* Push a level to the assertion stack.
+ *
* SMT-LIB:
* {@code
* ( push <numeral> )
* }
+ *
* @throws CVC5ApiException
*/
public void push() throws CVC5ApiException
/**
* Push (a) level(s) to the assertion stack.
+ *
* SMT-LIB:
* {@code
* ( push <numeral> )
* }
+ *
* @param nscopes The number of levels to push.
* @throws CVC5ApiException
*/
/**
* Remove all assertions.
+ *
* SMT-LIB:
* {@code
* ( reset-assertions )
/**
* Set info.
+ *
* SMT-LIB:
* {@code
* ( set-info <attribute> )
* }
+ *
* @param keyword The info flag.
* @param value The value of the info flag.
* @throws CVC5ApiException
/**
* Set logic.
+ *
* SMT-LIB:
* {@code
* ( set-logic <symbol> )
* }
+ *
* @param logic The logic to set.
* @throws CVC5ApiException
*/
/**
* Set option.
+ *
* SMT-LIB:
* {@code
* ( set-option <option> )
* }
+ *
* @param option The option name.
* @param value The option value.
*/
private native void setOption(long pointer, String option, String value);
/**
- * Append \p symbol to the current list of universal variables.
+ * Append {@code symbol} to the current list of universal variables.
+ *
* SyGuS v2:
* {@code
* ( declare-var <symbol> <sort> )
* }
+ *
* @param sort The sort of the universal variable.
* @param symbol The name of the universal variable.
* @return The universal variable.
/**
* Synthesize n-ary function.
+ *
* SyGuS v2:
* {@code
* ( synth-fun <symbol> ( <boundVars>* ) <sort> )
* }
+ *
* @param symbol The name of the function.
* @param boundVars The parameters to this function.
* @param sort The sort of the return value of this function.
/**
* Synthesize n-ary function following specified syntactic constraints.
+ *
* SyGuS v2:
* {@code
* ( synth-fun <symbol> ( <boundVars>* ) <sort> <g> )
* }
+ *
* @param symbol The name of the function.
* @param boundVars The parameters to this function.
* @param sort The sort of the return value of this function.
/**
* Synthesize invariant.
+ *
* SyGuS v2:
* {@code
* ( synth-inv <symbol> ( <boundVars>* ) )
* }
+ *
* @param symbol The name of the invariant.
* @param boundVars The parameters to this invariant.
* @return The invariant.
/**
* Synthesize invariant following specified syntactic constraints.
+ *
* SyGuS v2:
* {@code
* ( synth-inv <symbol> ( <boundVars>* ) <g> )
* }
+ *
* @param symbol The name of the invariant.
* @param boundVars The parameters to this invariant.
* @param grammar The syntactic constraints.
/**
* Add a forumla to the set of Sygus constraints.
+ *
* SyGuS v2:
* {@code
* ( constraint <term> )
* }
+ *
* @param term The formula to add as a constraint.
*/
public void addSygusConstraint(Term term)
/**
* Add a forumla to the set of Sygus assumptions.
+ *
* SyGuS v2:
* {@code
* ( assume <term> )
* }
+ *
* @param term The formula to add as an assumption.
*/
public void addSygusAssume(Term term)
/**
* Add a set of Sygus constraints to the current state that correspond to an
* invariant synthesis problem.
+ *
* SyGuS v2:
* {@code
* ( inv-constraint <inv> <pre> <trans> <post> )
* }
+ *
* @param inv The function-to-synthesize.
* @param pre The pre-condition.
* @param trans The transition relation.
* Try to find a solution for the synthesis conjecture corresponding to the
* current list of functions-to-synthesize, universal variables and
* constraints.
+ *
* SyGuS v2:
* {@code
* ( check-synth )
* }
+ *
* @return The result of the check, which is "solution" if the check found a.
* solution in which case solutions are available via
* getSynthSolutions, "no solution" if it was determined there is no
* Try to find a next solution for the synthesis conjecture corresponding to
* the current list of functions-to-synthesize, universal variables and
* constraints. Must be called immediately after a successful call to
- * check-synth or check-synth-next. Requires incremental mode.
+ * {@code check-synth} or {@code check-synth-next}.
+ *
+ * @api.note Requires incremental mode.
+ *
* SyGuS v2:
* {@code
* ( check-synth-next )
* }
+ *
* @return The result of the check, which is "solution" if the check found a
* solution in which case solutions are available via
* getSynthSolutions, "no solution" if it was determined there is no
private native long checkSynthNext(long pointer);
/**
- * Get the synthesis solution of the given term. This method should be called
- * immediately after the solver answers unsat for sygus input.
+ * Get the synthesis solution of the given term.
+ *
+ * This method should be called immediately after the solver answers unsat
+ * for sygus input.
+ *
* @param term The term for which the synthesis solution is queried.
* @return The synthesis solution of the given term.
*/
private native long getSynthSolution(long pointer, long termPointer);
/**
- * Get the synthesis solutions of the given terms. This method should be
- * called immediately after the solver answers unsat for sygus input.
+ * Get the synthesis solutions of the given terms.
+ *
+ * This method should be called immediately after the solver answers unsat
+ * for sygus input.
+ *
* @param terms The terms for which the synthesis solutions is queried.
* @return The synthesis solutions of the given terms.
*/
* Return true if both terms are syntactically identical.
* Both terms must belong to the same solver object.
*
- * @param t the term to compare to for equality
- * @return true if the terms are equal
+ * @param t The term to compare to for equality.
+ * @return True if the terms are equal.
*/
@Override
public boolean equals(Object t)
/**
* Comparison for ordering on terms.
*
- * @param t the term to compare to
- * @return a negative integer, zero, or a positive integer as this term
+ * @param t The term to compare to.
+ * @return A negative integer, zero, or a positive integer as this term.
* is less than, equal to, or greater than the specified term.
*/
@Override
private native int compareTo(long pointer1, long pointer2);
/**
- * @return the number of children of this term
+ * @return The number of children of this term.
*/
public int getNumChildren()
{
/**
* Get the child term at a given index.
*
- * @param index the index of the child term to return
- * @return the child term with the given index
+ * @param index The index of the child term to return.
+ * @return The child term with the given index.
*/
public Term getChild(int index) throws CVC5ApiException
{
private native long getChild(long pointer, int index);
/**
- * @return the id of this term
+ * @return The id of this term.
*/
public long getId()
{
private native long getId(long pointer);
/**
- * @return the kind of this term
+ * @return The kind of this term.
*/
public Kind getKind() throws CVC5ApiException
{
private native int getKind(long pointer);
/**
- * @return the sort of this term
+ * @return The sort of this term.
*/
public Sort getSort()
{
private native long getSort(long pointer);
/**
- * @return the result of replacing 'term' by 'replacement' in this term
+ * Replace {@code term} with {@code replacement} in this term.
*
- * Note that this replacement is applied during a pre-order traversal and
- * only once to the term. It is not run until fix point.
+ * @return The result of replacing {@code term} with {@code replacement} in
+ * this term.
+ *
+ * @api.note This replacement is applied during a pre-order traversal and
+ * only once (it is not run until fixed point).
*/
public Term substitute(Term term, Term replacement)
{
private native long substitute(long pointer, long termPointer, long replacementPointer);
/**
- * @return the result of simultaneously replacing 'terms' by 'replacements'
- * in this term
+ * Simultaneously replace {@code terms} with {@code replacements} in this
+ * term.
+ *
+ * In the case that terms contains duplicates, the replacement earliest in
+ * the vector takes priority. For example, calling substitute on
+ * {@code f(x,y)} with {@code terms = { x, z }},
+ * {@code replacements = { g(z), w }} results in the term
+ * {@code f(g(z),y)}.
+ *
+ * @api.note This replacement is applied during a pre-order traversal and
+ * only once (it is not run until fixed point).
+ *
+ * @return The result of simultaneously replacing {@code terms} with
+ * {@code replacements} in this term.
*/
public Term substitute(Term[] terms, Term[] replacements)
{
private native long substitute(long pointer, long[] termPointers, long[] replacementPointers);
/**
- * @return true iff this term has an operator
+ * @return True iff this term has an operator.
*/
public boolean hasOp()
{
private native boolean hasOp(long pointer);
/**
- * @return the Op used to create this term
- * @api.note This is safe to call when hasOp() returns true.
+ * @return The Op used to create this term.
+ * @api.note This is safe to call when {@link Term#hasOp()} returns true.
*/
public Op getOp()
{
private native long getOp(long pointer);
/**
- * @return true if the term has a symbol.
+ * @return True if the term has a symbol.
*/
public boolean hasSymbol()
{
/**
* Asserts hasSymbol().
- * @return the raw symbol of the term.
+ * @return The raw symbol of the term.
*/
public String getSymbol()
{
private native String getSymbol(long pointer);
/**
- * @return true if this Term is a null term
+ * @return True if this Term is a null term.
*/
public boolean isNull()
{
/**
* Boolean negation.
*
- * @return the Boolean negation of this term
+ * @return The Boolean negation of this term.
*/
public Term notTerm()
{
/**
* Boolean and.
*
- * @param t a Boolean term
- * @return the conjunction of this term and the given term
+ * @param t A Boolean term.
+ * @return The conjunction of this term and the given term.
*/
public Term andTerm(Term t)
{
/**
* Boolean or.
*
- * @param t a Boolean term
- * @return the disjunction of this term and the given term
+ * @param t A Boolean term.
+ * @return The disjunction of this term and the given term.
*/
public Term orTerm(Term t)
{
/**
* Boolean exclusive or.
*
- * @param t a Boolean term
- * @return the exclusive disjunction of this term and the given term
+ * @param t A Boolean term.
+ * @return The exclusive disjunction of this term and the given term.
*/
public Term xorTerm(Term t)
{
/**
* Equality.
*
- * @param t a Boolean term
- * @return the Boolean equivalence of this term and the given term
+ * @param t A Boolean term.
+ * @return The Boolean equivalence of this term and the given term.
*/
public Term eqTerm(Term t)
{
/**
* Boolean implication.
*
- * @param t a Boolean term
- * @return the implication of this term and the given term
+ * @param t A Boolean term.
+ * @return The implication of this term and the given term.
*/
public Term impTerm(Term t)
{
/**
* If-then-else with this term as the Boolean condition.
*
- * @param thenTerm the 'then' term
- * @param elseTerm the 'else' term
- * @return the if-then-else term with this term as the Boolean condition
+ * @param thenTerm The 'then' term.
+ * @param elseTerm The 'else' term.
+ * @return The if-then-else term with this term as the Boolean condition.
*/
public Term iteTerm(Term thenTerm, Term elseTerm)
{
private native long iteTerm(long pointer, long thenPointer, long elsePointer);
/**
- * @return a string representation of this term.
+ * @return A string representation of this term.
*/
protected native String toString(long pointer);
* Get integer or real value sign. Must be called on integer or real values,
* or otherwise an exception is thrown.
* @return 0 if this term is zero, -1 if this term is a negative real or
- * integer value, 1 if this term is a positive real or integer value.
+ * integer value, 1 if this term is a positive real or integer value.
*/
public int getRealOrIntegerValueSign()
{
private native int getRealOrIntegerValueSign(long pointer);
/**
- * @return true if the term is an integer value.
+ * @return True if the term is an integer value.
*/
public boolean isIntegerValue()
{
/**
* Asserts isIntegerValue().
- * @return the integer represented by this term.
+ * @return The integer represented by this term.
*/
public BigInteger getIntegerValue()
{
private native String getIntegerValue(long pointer);
/**
- * @return true if the term is a string constant.
+ * @return True if the term is a string constant.
*/
public boolean isStringValue()
{
private native boolean isStringValue(long pointer);
/**
- * @return the stored string constant.
+ * @return The stored string constant.
*
* Asserts isString().
*
- * @api.note This method is not to be confused with toString() which returns
- * the term in some string representation, whatever data it may hold.
+ * @api.note This method is not to be confused with {@link Term#toString()})
+ * which returns the term in some string representation, whatever
+ * data it may hold.
*/
public String getStringValue()
{
private native String getStringValue(long pointer);
/**
- * @return true if the term is a rational value.
+ * @return True if the term is a rational value.
*/
public boolean isRealValue()
{
/**
* Asserts isRealValue().
- * @return the representation of a rational value as a pair of its numerator
- * and denominator.
+ * @return The representation of a rational value as a pair of its numerator.
+ * and denominator.
*/
public Pair<BigInteger, BigInteger> getRealValue()
{
private native String getRealValue(long pointer);
/**
- * @return true if the term is a constant array.
+ * @return True if the term is a constant array.
*/
public boolean isConstArray()
{
/**
* Asserts isConstArray().
- * @return the base (element stored at all indices) of a constant array
+ * @return The base (element stored at all indices) of a constant array.
*/
public Term getConstArrayBase()
{
private native long getConstArrayBase(long pointer);
/**
- * @return true if the term is a Boolean value.
+ * @return True if the term is a Boolean value.
*/
public boolean isBooleanValue()
{
private native boolean isBooleanValue(long pointer);
/**
* Asserts isBooleanValue().
- * @return the representation of a Boolean value as a native Boolean value.
+ * @return The representation of a Boolean value as a native Boolean value.
*/
public boolean getBooleanValue()
{
private native boolean getBooleanValue(long pointer);
/**
- * @return true if the term is a bit-vector value.
+ * @return True if the term is a bit-vector value.
*/
public boolean isBitVectorValue()
{
/**
* Asserts isBitVectorValue().
- * @return the representation of a bit-vector value in bit string representation.
+ * @return The representation of a bit-vector value in bit string
+ * representation.
*/
public String getBitVectorValue() throws CVC5ApiException
{
}
/**
- * Asserts isBitVectorValue().
- * @return the representation of a bit-vector value in string representation.
- * Supported bases are 2 (bit string), 10 (decimal string) or 16 (hexadecimal
- * string).
+ * Get the string representation of a bit-vector value.
+ *
+ * Supported values for {@code base} are {@code 2} (bit string), {@code 10}
+ * (decimal string) or {@code 16} (hexadecimal string).
+ *
+ * @api.note Asserts {@code Term#isBitVectorValue()}.
+ *
+ * @return The string representation of a bit-vector value.
*/
public String getBitVectorValue(int base) throws CVC5ApiException
{
private native String getBitVectorValue(long pointer, int base);
/**
- * @return true if the term is an uninterpreted sort value.
+ * @return True if the term is an uninterpreted sort value.
*/
public boolean isUninterpretedSortValue()
{
/**
* Asserts isUninterpretedSortValue().
- * @return the representation of an uninterpreted sort value as a string.
+ * @return The representation of an uninterpreted sort value as a string.
*/
public String getUninterpretedSortValue()
{
private native String getUninterpretedSortValue(long pointer);
/**
- * @return true if the term is a floating-point rounding mode value.
+ * @return True if the term is a floating-point rounding mode value.
*/
public boolean isRoundingModeValue()
{
/**
* Asserts isRoundingModeValue().
- * @return the floating-point rounding mode value held by the term.
+ * @return The floating-point rounding mode value held by the term.
*/
public RoundingMode getRoundingModeValue() throws CVC5ApiException
{
private native int getRoundingModeValue(long pointer);
/**
- * @return true if the term is a tuple value.
+ * @return True if the term is a tuple value.
*/
public boolean isTupleValue()
{
/**
* Asserts isTupleValue().
- * @return the representation of a tuple value as a vector of terms.
+ * @return The representation of a tuple value as a vector of terms.
*/
public Term[] getTupleValue()
{
private native long[] getTupleValue(long pointer);
/**
- * @return true if the term is the floating-point value for positive zero.
+ * @return True if the term is the floating-point value for positive zero.
*/
public boolean isFloatingPointPosZero()
{
private native boolean isFloatingPointPosZero(long pointer);
/**
- * @return true if the term is the floating-point value for negative zero.
+ * @return True if the term is the floating-point value for negative zero.
*/
public boolean isFloatingPointNegZero()
{
private native boolean isFloatingPointNegZero(long pointer);
/**
- * @return true if the term is the floating-point value for positive
+ * @return True if the term is the floating-point value for positive.
* infinity.
*/
public boolean isFloatingPointPosInf()
private native boolean isFloatingPointPosInf(long pointer);
/**
- * @return true if the term is the floating-point value for negative
+ * @return True if the term is the floating-point value for negative.
* infinity.
*/
public boolean isFloatingPointNegInf()
private native boolean isFloatingPointNegInf(long pointer);
/**
- * @return true if the term is the floating-point value for not a number.
+ * @return True if the term is the floating-point value for not a number.
*/
public boolean isFloatingPointNaN()
{
private native boolean isFloatingPointNaN(long pointer);
/**
- * @return true if the term is a floating-point value.
+ * @return True if the term is a floating-point value.
*/
public boolean isFloatingPointValue()
{
private native boolean isFloatingPointValue(long pointer);
/**
* Asserts isFloatingPointValue().
- * @return the representation of a floating-point value as a tuple of the
+ * @return The representation of a floating-point value as a tuple of the.
* exponent width, the significand width and a bit-vector value.
*/
public Triplet<Long, Long, Term> getFloatingPointValue()
private native Triplet<Long, Long, Long> getFloatingPointValue(long pointer);
/**
- * @return true if the term is a set value.
+ * @return True if the term is a set value.
*/
public boolean isSetValue()
{
private native boolean isSetValue(long pointer);
/**
* Asserts isSetValue().
- * @return the representation of a set value as a set of terms.
+ * @return The representation of a set value as a set of terms.
*/
public Set<Term> getSetValue()
{
private native long[] getSetValue(long pointer);
/**
- * @return true if the term is a sequence value.
+ * @return True if the term is a sequence value.
*/
public boolean isSequenceValue()
{
/**
* Asserts isSequenceValue().
* @api.note It is usually necessary for sequences to call
- * `Solver::simplify()` to turn a sequence that is constructed by,
- * e.g., concatenation of unit sequences, into a sequence value.
- * @return the representation of a sequence value as a vector of terms.
+ * {@link Solver#simplify(Term)} to turn a sequence that is
+ * constructed by, e.g., concatenation of unit sequences, into a
+ * sequence value.
+ * @return The representation of a sequence value as a vector of terms.
*/
public Term[] getSequenceValue()
{
private native long[] getSequenceValue(long pointer);
/**
- * @return true if the term is a cardinality constraint
+ * @return True if the term is a cardinality constraint.
*/
public boolean isCardinalityConstraint()
{
/**
* Asserts isCardinalityConstraint().
- * @return the sort the cardinality constraint is for and its upper bound.
+ * @return The sort the cardinality constraint is for and its upper bound.
*/
public Pair<Sort, BigInteger> getCardinalityConstraint()
{
projects / cvc5.git / commitdiff