*
* A term is a set value if it is considered to be a (canonical) constant set
* value. A canonical set value is one whose AST is:
- * ```
- * (union (singleton c1) ... (union (singleton c_{n-1}) (singleton c_n))))
- * ```
+ *
+ * (union (singleton c1) ... (union (singleton c_{n-1}) (singleton c_n))))
+ *
* where `c1 ... cn` are values ordered by id such that `c1 > ... > cn` (see
* also @ref Term::operator>(const Term&) const).
*
- * @note A universe set term (kind SET_UNIVERSE) is not considered to be
+ * @note A universe set term `(kind SET_UNIVERSE)` is not considered to be
* a set value.
*/
bool isSetValue() const;
bool isSequenceValue() const;
/**
* Asserts isSequenceValue().
- * @note It is usually necessary for sequences to call `Solver::simplify()`
+ * @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.
*
* This method is required for constructors of parametric datatypes whose
* return type cannot be determined by type inference. For example, given:
- * (declare-datatype List (par (T) ((nil) (cons (head T) (tail (List T))))))
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (declare-datatype List
+ * (par (T) ((nil) (cons (head T) (tail (List T))))))
+ * \endverbatim
+ *
* The type of nil terms need to be provided by the user. In SMT version 2.6,
* this is done via the syntax for qualified identifiers:
- * (as nil (List Int))
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (as nil (List Int))
+ * \endverbatim
+ *
* This method is equivalent of applying the above, where this
* DatatypeConstructor is the one corresponding to nil, and retSort is
- * (List Int).
+ * ``(List Int)``.
*
* @note the returned constructor term ``t`` is an operator, while
* ``Solver::mkTerm(APPLY_CONSTRUCTOR, t)`` is used to construct the
/**
* Create (first-order) constant (0-arity function symbol).
+ *
* SMT-LIB:
- * \verbatim
- * ( declare-const <symbol> <sort> )
- * ( declare-fun <symbol> ( ) <sort> )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (declare-const <symbol> <sort>)
+ * (declare-fun <symbol> () <sort>)
* \endverbatim
*
* @param sort the sort of the constant
/**
* Assert a formula.
+ *
* SMT-LIB:
- * \verbatim
- * ( assert <term> )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (assert <term>)
* \endverbatim
+ *
* @param term the formula to assert
*/
void assertFormula(const Term& term) const;
/**
* Check satisfiability.
+ *
* SMT-LIB:
- * \verbatim
- * ( check-sat )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (check-sat)
* \endverbatim
+ *
* @return the result of the satisfiability check.
*/
Result checkSat() const;
/**
* Check satisfiability assuming the given formula.
+ *
* SMT-LIB:
- * \verbatim
- * ( check-sat-assuming ( <prop_literal> ) )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (check-sat-assuming ( <prop_literal> ))
* \endverbatim
+ *
* @param assumption the formula to assume
* @return the result of the satisfiability check.
*/
/**
* Check satisfiability assuming the given formulas.
+ *
* SMT-LIB:
- * \verbatim
- * ( check-sat-assuming ( <prop_literal>+ ) )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (check-sat-assuming ( <prop_literal>+ ))
* \endverbatim
+ *
* @param assumptions the formulas to assume
* @return the result of the satisfiability check.
*/
/**
* Create datatype sort.
+ *
* SMT-LIB:
- * \verbatim
- * ( declare-datatype <symbol> <datatype_decl> )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (declare-datatype <symbol> <datatype_decl>)
* \endverbatim
+ *
* @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:
- * \verbatim
- * ( declare-fun <symbol> ( <sort>* ) <sort> )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (declare-fun <symbol> ( <sort>* ) <sort>)
* \endverbatim
+ *
* @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:
- * \verbatim
- * ( declare-sort <symbol> <numeral> )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (declare-sort <symbol> <numeral>)
* \endverbatim
+ *
* @param symbol the name of the sort
* @param arity the arity of the sort
* @return the sort
/**
* Define n-ary function.
+ *
* SMT-LIB:
- * \verbatim
- * ( define-fun <function_def> )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (define-fun <function_def>)
* \endverbatim
+ *
* @param symbol the name of the function
* @param bound_vars the parameters to this function
* @param sort the sort of the return value of this function
/**
* Define recursive function.
+ *
* SMT-LIB:
- * \verbatim
- * ( define-fun-rec <function_def> )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (define-fun-rec <function_def>)
* \endverbatim
+ *
* @param symbol the name of the function
* @param bound_vars the parameters to this function
* @param sort the sort of the return value of this function
/**
* Define recursive function.
+ *
* SMT-LIB:
- * \verbatim
- * ( define-fun-rec <function_def> )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (define-fun-rec <function_def>)
* \endverbatim
+ *
* Create parameter 'fun' with mkConst().
* @param fun the sorted function
* @param bound_vars the parameters to this function
/**
* Define recursive functions.
+ *
* SMT-LIB:
- * \verbatim
- * ( define-funs-rec ( <function_decl>^{n+1} ) ( <term>^{n+1} ) )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (define-funs-rec
+ * ( <function_decl>_1 ... <function_decl>_n )
+ * ( <term>_1 ... <term>_n )
+ * )
* \endverbatim
+ *
* Create elements of parameter 'funs' with mkConst().
* @param funs the sorted functions
* @param bound_vars the list of parameters to the functions
/**
* Echo a given string to the given output stream.
+ *
* SMT-LIB:
- * \verbatim
- * ( echo <std::string> )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (echo <string>)
* \endverbatim
+ *
* @param out the output stream
* @param str the string to echo
*/
/**
* Get the list of asserted formulas.
+ *
* SMT-LIB:
- * \verbatim
- * ( get-assertions )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (get-assertions)
* \endverbatim
+ *
* @return the list of asserted formulas
*/
std::vector<Term> getAssertions() const;
/**
* Get info from the solver.
- * SMT-LIB: \verbatim( get-info <info_flag> )\endverbatim
+ *
+ * SMT-LIB:
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (get-info <info_flag>)
+ * \endverbatim
+ *
* @return the info
*/
std::string getInfo(const std::string& flag) const;
/**
* Get the value of a given option.
+ *
* SMT-LIB:
- * \verbatim
- * ( get-option <keyword> )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (get-option <keyword>)
* \endverbatim
+ *
* @param option the option for which the value is queried
* @return a string representation of the option value
*/
/**
* Get the set of unsat ("failed") assumptions.
+ *
* SMT-LIB:
- * \verbatim
- * ( get-unsat-assumptions )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (get-unsat-assumptions)
+ *
+ * Requires to enable option
+ * :ref:`produce-unsat-assumptions <lbl-option-produce-unsat-assumptions>`.
* \endverbatim
- * Requires to enable option 'produce-unsat-assumptions'.
+ *
* @return the set of unsat assumptions.
*/
std::vector<Term> getUnsatAssumptions() const;
/**
* Get the unsatisfiable core.
+ *
* SMT-LIB:
- * \verbatim
- * ( get-unsat-core )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (get-unsat-core)
+ *
+ * Requires to enable option
+ * :ref:`produce-unsat-cores <lbl-option-produce-unsat-cores>`.
* \endverbatim
- * Requires to enable option 'produce-unsat-cores'.
+ *
* @return a set of terms representing the unsatisfiable core
*/
std::vector<Term> getUnsatCore() const;
* intended to be called immediately after any response to a checkSat.
*
* @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.
+ * is an estimate of how difficult each assertion was to solve.
+ * Unmentioned assertions can be assumed to have zero difficulty.
*/
std::map<Term, Term> getDifficulty() const;
/**
* Get the refutation proof
+ *
* SMT-LIB:
- * \verbatim
- * ( get-proof )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (get-proof)
+ *
+ * Requires to enable option
+ * :ref:`produce-proofs <lbl-option-produce-proofs>`.
* \endverbatim
- * Requires to enable option 'produce-proofs'.
+ *
* @return a string representing the proof, according to the value of
* proof-format-mode.
*/
/**
* Get the value of the given term in the current model.
+ *
* SMT-LIB:
- * \verbatim
- * ( get-value ( <term> ) )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (get-value ( <term> ))
* \endverbatim
+ *
* @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:
- * \verbatim
- * ( get-value ( <term>+ ) )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (get-value ( <term>* ))
* \endverbatim
+ *
* @param terms the terms for which the value is queried
* @return the values of the given terms
*/
* 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.
+ * option
+ * \verbatim:rst:inline
+ * :ref:`model-cores <lbl-option-model-cores>`
+ * \endverbatim
+ * has been set.
*
* @param v The term in question
* @return true if v is a model core symbol
/**
* Get the model
+ *
* SMT-LIB:
- * \verbatim
- * ( get-model )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (get-model)
+ *
+ * Requires to enable option
+ * :ref:`produce-models <lbl-option-produce-models>`.
* \endverbatim
- * Requires to enable option 'produce-models'.
+ *
+ * \endverbatim
+ *
* @param sorts The list of uninterpreted sorts that should be printed in the
* model.
* @param vars The list of free constants that should be printed in the
/**
* Do quantifier elimination.
+ *
* SMT-LIB:
- * \verbatim
- * ( get-qe <q> )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (get-qe <q>)
* \endverbatim
+ *
* Requires a logic that supports quantifier elimination. Currently, the only
* logics supported by quantifier elimination is LRA and LIA.
- * @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
- * @return a formula ret such that, given the current set of formulas A
- * asserted to this solver:
- * - ( A ^ q ) and ( A ^ ret ) are equivalent
- * - ret is quantifier-free formula containing only free variables in
- * y1...yn.
+ *
+ * @note Quantifier Elimination is is only complete for LRA and LIA.
+ *
+ * @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
+ * @f$Q\bar{x}@f$ is a set of quantified variables of the form
+ * @f$Q x_1...x_k@f$ and
+ * @f$P( x_1...x_i, y_1...y_j )@f$ is a quantifier-free formula
+ * @return a formula @f$\phi@f$ such that, given the current set of formulas
+ * @f$A@f$ asserted to this solver:
+ * - @f$(A \wedge q)@f$ and @f$(A \wedge \phi)@f$ are equivalent
+ * - @f$\phi@f$ is quantifier-free formula containing only free
+ * variables in @f$y_1...y_n@f$.
*/
Term getQuantifierElimination(const Term& q) const;
/**
* Do partial quantifier elimination, which can be used for incrementally
* computing the result of a quantifier elimination.
+ *
* SMT-LIB:
- * \verbatim
- * ( get-qe-disjunct <q> )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (get-qe-disjunct <q>)
* \endverbatim
+ *
* Requires a logic that supports quantifier elimination. Currently, the only
* logics supported by quantifier elimination is LRA and LIA.
- * @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
- * @return a formula ret such that, given the current set of formulas A
- * asserted to this solver:
- * - (A ^ q) => (A ^ ret) if Q is forall or (A ^ ret) => (A ^ q) if Q is
- * exists,
- * - ret is quantifier-free formula containing only free variables in
- * y1...yn,
- * - If Q is exists, let A^Q_n be the formula
- * A ^ ~ret^Q_1 ^ ... ^ ~ret^Q_n
- * where for each i=1,...n, formula ret^Q_i is the result of calling
- * getQuantifierEliminationDisjunct for q with the set of assertions
- * A^Q_{i-1}. Similarly, if Q is forall, then let A^Q_n be
- * A ^ ret^Q_1 ^ ... ^ ret^Q_n
- * where ret^Q_i is the same as above. In either case, we have
- * that ret^Q_j will eventually be true or false, for some finite j.
+ * @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
+ * @f$Q\bar{x}@f$ is a set of quantified variables of the form
+ * @f$Q x_1...x_k@f$ and
+ * @f$P( x_1...x_i, y_1...y_j )@f$ is a quantifier-free formula
+ * @return a formula @f$\phi@f$ such that, given the current set of formulas
+ * @f$A@f$ asserted to this solver:
+ * - @f$(A \wedge q \implies A \wedge \phi)@f$ if @f$Q@f$ is
+ * @f$\forall@f$, and @f$(A \wedge \phi \implies A \wedge q)@f$ if
+ * @f$Q@f$ is @f$\exists@f$
+ * - @f$\phi@f$ is quantifier-free formula containing only free
+ * variables in @f$y_1...y_n@f$
+ * - If @f$Q@f$ is @f$\exists@f$, let @f$(A \wedge Q_n)@f$ be the
+ * formula
+ * @f$(A \wedge \neg (\phi \wedge Q_1) \wedge ... \wedge
+ * \neg (\phi \wedge Q_n))@f$
+ * where for each @f$i = 1...n@f$,
+ * formula @f$(\phi \wedge Q_i)@f$ is the result of calling
+ * Solver::getQuantifierEliminationDisjunct() for @f$q@f$ with the
+ * set of assertions @f$(A \wedge Q_{i-1})@f$.
+ * Similarly, if @f$Q@f$ is @f$\forall@f$, then let
+ * @f$(A \wedge Q_n)@f$ be
+ * @f$(A \wedge (\phi \wedge Q_1) \wedge ... \wedge (\phi \wedge
+ * Q_n))@f$
+ * where @f$(\phi \wedge Q_i)@f$ is the same as above.
+ * In either case, we have that @f$(\phi \wedge Q_j)@f$ will
+ * eventually be true or false, for some finite j.
*/
Term getQuantifierEliminationDisjunct(const Term& q) const;
/**
* Declare a symbolic pool of terms with the given initial value.
+ *
* SMT-LIB:
- * \verbatim
- * ( declare-pool <symbol> <sort> ( <term>* ) )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (declare-pool <symbol> <sort> ( <term>* ))
* \endverbatim
+ *
* @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
const std::vector<Term>& initValue) const;
/**
* Pop (a) level(s) from the assertion stack.
+ *
* SMT-LIB:
- * \verbatim
- * ( pop <numeral> )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (pop <numeral>)
* \endverbatim
+ *
* @param nscopes the number of levels to pop
*/
void pop(uint32_t nscopes = 1) const;
/**
* Get an interpolant
+ *
* SMT-LIB:
- * \verbatim
- * ( get-interpol <conj> )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (get-interpol <conj>)
+ *
+ * Requires to enable option
+ * :ref:`produce-interpols <lbl-option-produce-interpols>`.
* \endverbatim
- * Requires to enable option 'produce-interpols'.
+ *
* @param conj the conjecture term
* @param output a Term I such that A->I and I->B are valid, where A is the
* current set of assertions and B is given in the input by conj.
/**
* Get an interpolant
+ *
* SMT-LIB:
- * \verbatim
- * ( get-interpol <conj> <g> )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (get-interpol <conj> <grammar>)
+ *
+ * Requires to enable option
+ * :ref:`produce-interpols <lbl-option-produce-interpols>`.
* \endverbatim
- * Requires to enable option 'produce-interpols'.
+ *
* @param conj the conjecture term
* @param grammar the grammar for the interpolant I
* @param output a Term I such that A->I and I->B are valid, where A is the
/**
* Get an abduct.
+ *
* SMT-LIB:
- * \verbatim
- * ( get-abduct <conj> )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (get-abduct <conj>)
+ *
+ * Requires to enable option
+ * :ref:`produce-abducts <lbl-option-produce-abducts>`.
* \endverbatim
- * Requires enabling option 'produce-abducts'
+ *
* @param conj the conjecture term
- * @param output 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
- * @return true if it gets C successfully, false otherwise
+ * @param output a term @f$C@f$ such that @f$(A \wedge C)@f$ is satisfiable,
+ * and @f$(A \wedge \neg B \wedge C)@f$ is unsatisfiable, where
+ * @f$A@f$ is the current set of assertions and @f$B@f$ is
+ * given in the input by ``conj``.
+ * @return true if it gets abduct @f$C@f$ successfully, false otherwise
*/
bool getAbduct(const Term& conj, Term& output) const;
/**
* Get an abduct.
+ *
* SMT-LIB:
- * \verbatim
- * ( get-abduct <conj> <g> )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (get-abduct <conj> <grammar>)
+ *
+ * Requires to enable option
+ * :ref:`produce-abducts <lbl-option-produce-abducts>`.
* \endverbatim
- * Requires enabling option 'produce-abducts'
+ *
* @param conj the conjecture term
- * @param grammar the grammar for the abduct C
- * @param output 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
- * @return true if it gets C successfully, false otherwise
+ * @param grammar the grammar for the abduct @f$C@f$
+ * @param output a term C such that @f$(A \wedge C)@f$ is satisfiable, and
+ * @f$(A \wedge \neg B \wedge C)@f$ is unsatisfiable, where @f$A@f$ is
+ * the current set of assertions and @f$B@f$ is given in the input by
+ * ``conj``
+ * @return true if it gets abduct @f$C@f$ successfully, false otherwise
*/
bool getAbduct(const Term& conj, Grammar& grammar, Term& output) const;
/**
* Block the current model. Can be called only if immediately preceded by a
* SAT or INVALID query.
+ *
* SMT-LIB:
- * \verbatim
- * ( block-model )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (block-model)
+ *
+ * Requires enabling option
+ * :ref:`produce-models <lbl-option-produce-models>`.
+ * 'produce-models' and setting option
+ * :ref:`block-models <lbl-option-block-models>`.
+ * to a mode other than ``none``.
* \endverbatim
- * Requires enabling 'produce-models' option and setting 'block-models' option
- * to a mode other than "none".
*/
void blockModel() const;
/**
* 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:
- * \verbatim
- * ( block-model-values ( <terms>+ ) )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (block-model-values ( <terms>+ ))
+ *
+ * Requires enabling option
+ * :ref:`produce-models <lbl-option-produce-models>`.
+ * 'produce-models' and setting option
+ * :ref:`block-models <lbl-option-block-models>`.
+ * to a mode other than ``none``.
* \endverbatim
- * Requires enabling 'produce-models' option and setting 'block-models' option
- * to a mode other than "none".
*/
void blockModelValues(const std::vector<Term>& terms) const;
/**
* Push (a) level(s) to the assertion stack.
+ *
* SMT-LIB:
- * \verbatim
- * ( push <numeral> )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (push <numeral>)
* \endverbatim
+ *
* @param nscopes the number of levels to push
*/
void push(uint32_t nscopes = 1) const;
/**
* Remove all assertions.
+ *
* SMT-LIB:
- * \verbatim
- * ( reset-assertions )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (reset-assertions)
* \endverbatim
+ *
*/
void resetAssertions() const;
/**
* Set info.
+ *
* SMT-LIB:
- * \verbatim
- * ( set-info <attribute> )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (set-info <attribute>)
* \endverbatim
+ *
* @param keyword the info flag
* @param value the value of the info flag
*/
/**
* Set logic.
+ *
* SMT-LIB:
- * \verbatim
- * ( set-logic <symbol> )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (set-logic <symbol>)
* \endverbatim
+ *
* @param logic the logic to set
*/
void setLogic(const std::string& logic) const;
/**
* Set option.
+ *
* SMT-LIB:
- * \verbatim
- * ( set-option <option> )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (set-option :<option> <value>)
* \endverbatim
+ *
* @param option the option name
* @param value the option value
*/
/**
* Append \p symbol to the current list of universal variables.
+ *
* SyGuS v2:
- * \verbatim
- * ( declare-var <symbol> <sort> )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (declare-var <symbol> <sort>)
* \endverbatim
+ *
* @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:
- * \verbatim
- * ( synth-fun <symbol> ( <boundVars>* ) <sort> )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (synth-fun <symbol> ( <boundVars>* ) <sort>)
* \endverbatim
+ *
* @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:
- * \verbatim
- * ( synth-fun <symbol> ( <boundVars>* ) <sort> <g> )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (synth-fun <symbol> ( <boundVars>* ) <sort> <grammar>)
* \endverbatim
+ *
* @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:
- * \verbatim
- * ( synth-inv <symbol> ( <boundVars>* ) )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (synth-inv <symbol> ( <boundVars>* ))
* \endverbatim
+ *
* @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:
- * \verbatim
- * ( synth-inv <symbol> ( <boundVars>* ) <g> )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (synth-inv <symbol> ( <boundVars>* ) <grammar>)
* \endverbatim
+ *
* @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:
- * \verbatim
- * ( constraint <term> )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (constraint <term>)
* \endverbatim
+ *
* @param term the formula to add as a constraint
*/
void addSygusConstraint(const Term& term) const;
/**
* Add a forumla to the set of Sygus assumptions.
+ *
* SyGuS v2:
- * \verbatim
- * ( assume <term> )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (assume <term>)
* \endverbatim
+ *
* @param term the formula to add as an assumption
*/
void addSygusAssume(const Term& term) const;
/**
* Add a set of Sygus constraints to the current state that correspond to an
* invariant synthesis problem.
+ *
* SyGuS v2:
- * \verbatim
- * ( inv-constraint <inv> <pre> <trans> <post> )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (inv-constraint <inv> <pre> <trans> <post>)
* \endverbatim
+ *
* @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:
- * \verbatim
- * ( check-synth )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (check-synth)
* \endverbatim
+ *
* @return the result of the synthesis conjecture.
*/
Result checkSynth() const;
/**
* Synthesize n-ary function following specified syntactic constraints.
+ *
* SMT-LIB:
- * \verbatim
- * ( synth-fun <symbol> ( <boundVars>* ) <sort> <g>? )
+ *
+ * \verbatim embed:rst:leading-asterisk
+ * .. code:: smtlib
+ *
+ * (synth-fun <symbol> ( <boundVars>* ) <sort> <grammar>?)
* \endverbatim
+ *
* @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
projects / cvc5.git / commitdiff