From eb3b04319a26e3573dd2ba520f12432ce2d797b3 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Wed, 15 Dec 2021 15:09:51 -0800 Subject: [PATCH] api: Fix smt-lib code blocks and math in C++ docs. (#7795) --- docs/api/java/java.rst | 4 +- docs/api/python/z3compat/boolean.rst | 12 +- docs/ext/smtliblexer.py | 16 +- src/api/cpp/cvc5.h | 602 ++++++++++++++++++++------- 4 files changed, 468 insertions(+), 166 deletions(-) diff --git a/docs/api/java/java.rst b/docs/api/java/java.rst index 725e2bf7c..71a70023b 100644 --- a/docs/api/java/java.rst +++ b/docs/api/java/java.rst @@ -1,5 +1,5 @@ Java API -====================== +======== The Java API for cvc5 mostly mirrors the :doc:`C++ API <../cpp/cpp>` and supports operator overloading, iterators, and exceptions. @@ -56,7 +56,7 @@ Building cvc5 Java API (< (+ a b) 1) `Package io.github.cvc5.api `_ -^^^^^^^^^^^^^^^ +^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ * class `Datatype `_ * class `DatatypeConstructor `_ diff --git a/docs/api/python/z3compat/boolean.rst b/docs/api/python/z3compat/boolean.rst index e48e7f9e9..8ccc649c5 100644 --- a/docs/api/python/z3compat/boolean.rst +++ b/docs/api/python/z3compat/boolean.rst @@ -2,7 +2,7 @@ Core & Booleans ================ Basic Boolean Term Builders -------------------- +--------------------------- .. autofunction:: cvc5_z3py_compat.Bool .. autofunction:: cvc5_z3py_compat.Bools .. autofunction:: cvc5_z3py_compat.BoolVal @@ -11,13 +11,13 @@ Basic Boolean Term Builders .. autofunction:: cvc5_z3py_compat.BoolVector Basic Generic Term Builders -------------------- +--------------------------- .. autofunction:: cvc5_z3py_compat.Const .. autofunction:: cvc5_z3py_compat.Consts .. autofunction:: cvc5_z3py_compat.FreshConst Boolean Operators -------------------- +----------------- .. autofunction:: cvc5_z3py_compat.And .. autofunction:: cvc5_z3py_compat.Or .. autofunction:: cvc5_z3py_compat.Not @@ -26,7 +26,7 @@ Boolean Operators .. autofunction:: cvc5_z3py_compat.Xor Generic Operators -------------------- +----------------- .. autofunction:: cvc5_z3py_compat.If .. autofunction:: cvc5_z3py_compat.Distinct @@ -41,7 +41,7 @@ for building equality and disequality terms. Testers -------------------- +------- .. autofunction:: cvc5_z3py_compat.is_bool .. autofunction:: cvc5_z3py_compat.is_true .. autofunction:: cvc5_z3py_compat.is_false @@ -55,7 +55,7 @@ Testers Classes --------- +------- .. autoclass:: cvc5_z3py_compat.ExprRef :members: :special-members: diff --git a/docs/ext/smtliblexer.py b/docs/ext/smtliblexer.py index 54441ca25..f6f1679c0 100644 --- a/docs/ext/smtliblexer.py +++ b/docs/ext/smtliblexer.py @@ -16,16 +16,18 @@ class SmtLibLexer(RegexLexer): name = 'smtlib' COMMANDS = [ - 'assert', 'check-sat', 'check-sat-assuming', 'declare-const', - 'declare-datatype', 'declare-datatypes', 'declare-codatatypes', - 'declare-fun', 'declare-sort', 'define-fun', 'define-fun-rec', - 'define-funs-rec', 'define-sort', 'echo', 'exit', 'get-assertions', - 'get-assignment', 'get-info', 'get-model', 'get-option', 'get-proof', + 'assert', 'block-model', 'block-model-values', 'check-sat', + 'check-sat-assuming', 'declare-const', 'declare-datatype', + 'declare-datatypes', 'declare-codatatypes', 'declare-fun', + 'declare-sort', 'define-fun', 'define-fun-rec', 'define-funs-rec', + 'define-sort', 'echo', 'exit', 'get-abduct', 'get-assertions', + 'get-assignment', 'get-info', 'get-interpol', 'get-model', + 'get-option', 'get-proof', 'get-qe', 'get-qe-disjunct', 'get-unsat-assumptions', 'get-unsat-core', 'get-value', 'pop', 'push', 'reset', 'reset-assertions', 'set-info', 'set-logic', 'set-option', # SyGuS v2 - 'declare-var', 'constraint', 'inv-constraint', 'synth-fun', - 'check-synth', 'synth-inv', 'declare-pool', + 'assume', 'check-synth', 'constraint', 'declare-var', 'inv-constraint', + 'synth-fun', 'synth-inv', 'declare-pool', ] SORTS = [ 'Array', 'BitVec', 'Bool', 'FloatingPoint', 'Float[0-9]+', 'Int', diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index e3f64349f..ec7b92088 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -1510,13 +1510,13 @@ class CVC5_EXPORT Term * * 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; @@ -1532,7 +1532,7 @@ class CVC5_EXPORT Term 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. @@ -1983,13 +1983,26 @@ class CVC5_EXPORT DatatypeConstructor * * 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 @@ -3691,10 +3704,14 @@ class CVC5_EXPORT Solver /** * Create (first-order) constant (0-arity function symbol). + * * SMT-LIB: - * \verbatim - * ( declare-const ) - * ( declare-fun ( ) ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (declare-const ) + * (declare-fun () ) * \endverbatim * * @param sort the sort of the constant @@ -3779,30 +3796,45 @@ class CVC5_EXPORT Solver /** * Assert a formula. + * * SMT-LIB: - * \verbatim - * ( assert ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (assert ) * \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 ( ) ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (check-sat-assuming ( )) * \endverbatim + * * @param assumption the formula to assume * @return the result of the satisfiability check. */ @@ -3810,10 +3842,15 @@ class CVC5_EXPORT Solver /** * Check satisfiability assuming the given formulas. + * * SMT-LIB: - * \verbatim - * ( check-sat-assuming ( + ) ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (check-sat-assuming ( + )) * \endverbatim + * * @param assumptions the formulas to assume * @return the result of the satisfiability check. */ @@ -3836,10 +3873,15 @@ class CVC5_EXPORT Solver /** * Create datatype sort. + * * SMT-LIB: - * \verbatim - * ( declare-datatype ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (declare-datatype ) * \endverbatim + * * @param symbol the name of the datatype sort * @param ctors the constructor declarations of the datatype sort * @return the datatype sort @@ -3849,10 +3891,15 @@ class CVC5_EXPORT Solver /** * Declare n-ary function symbol. + * * SMT-LIB: - * \verbatim - * ( declare-fun ( * ) ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (declare-fun ( * ) ) * \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 @@ -3864,10 +3911,15 @@ class CVC5_EXPORT Solver /** * Declare uninterpreted sort. + * * SMT-LIB: - * \verbatim - * ( declare-sort ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (declare-sort ) * \endverbatim + * * @param symbol the name of the sort * @param arity the arity of the sort * @return the sort @@ -3876,10 +3928,15 @@ class CVC5_EXPORT Solver /** * Define n-ary function. + * * SMT-LIB: - * \verbatim - * ( define-fun ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (define-fun ) * \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 @@ -3896,10 +3953,15 @@ class CVC5_EXPORT Solver /** * Define recursive function. + * * SMT-LIB: - * \verbatim - * ( define-fun-rec ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (define-fun-rec ) * \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 @@ -3916,10 +3978,15 @@ class CVC5_EXPORT Solver /** * Define recursive function. + * * SMT-LIB: - * \verbatim - * ( define-fun-rec ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (define-fun-rec ) * \endverbatim + * * Create parameter 'fun' with mkConst(). * @param fun the sorted function * @param bound_vars the parameters to this function @@ -3935,10 +4002,18 @@ class CVC5_EXPORT Solver /** * Define recursive functions. + * * SMT-LIB: - * \verbatim - * ( define-funs-rec ( ^{n+1} ) ( ^{n+1} ) ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (define-funs-rec + * ( _1 ... _n ) + * ( _1 ... _n ) + * ) * \endverbatim + * * Create elements of parameter 'funs' with mkConst(). * @param funs the sorted functions * @param bound_vars the list of parameters to the functions @@ -3954,10 +4029,15 @@ class CVC5_EXPORT Solver /** * Echo a given string to the given output stream. + * * SMT-LIB: - * \verbatim - * ( echo ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (echo ) * \endverbatim + * * @param out the output stream * @param str the string to echo */ @@ -3965,27 +4045,45 @@ class CVC5_EXPORT Solver /** * 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 getAssertions() const; /** * Get info from the solver. - * SMT-LIB: \verbatim( get-info )\endverbatim + * + * SMT-LIB: + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (get-info ) + * \endverbatim + * * @return the info */ std::string getInfo(const std::string& flag) const; /** * Get the value of a given option. + * * SMT-LIB: - * \verbatim - * ( get-option ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (get-option ) * \endverbatim + * * @param option the option for which the value is queried * @return a string representation of the option value */ @@ -4014,22 +4112,36 @@ class CVC5_EXPORT Solver /** * 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 `. * \endverbatim - * Requires to enable option 'produce-unsat-assumptions'. + * * @return the set of unsat assumptions. */ std::vector 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 `. * \endverbatim - * Requires to enable option 'produce-unsat-cores'. + * * @return a set of terms representing the unsatisfiable core */ std::vector getUnsatCore() const; @@ -4039,18 +4151,25 @@ class CVC5_EXPORT Solver * 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 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 `. * \endverbatim - * Requires to enable option 'produce-proofs'. + * * @return a string representing the proof, according to the value of * proof-format-mode. */ @@ -4058,10 +4177,15 @@ class CVC5_EXPORT Solver /** * Get the value of the given term in the current model. + * * SMT-LIB: - * \verbatim - * ( get-value ( ) ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (get-value ( )) * \endverbatim + * * @param term the term for which the value is queried * @return the value of the given term */ @@ -4069,10 +4193,15 @@ class CVC5_EXPORT Solver /** * Get the values of the given terms in the current model. + * * SMT-LIB: - * \verbatim - * ( get-value ( + ) ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (get-value ( * )) * \endverbatim + * * @param terms the terms for which the value is queried * @return the values of the given terms */ @@ -4092,7 +4221,11 @@ class CVC5_EXPORT Solver * 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 ` + * \endverbatim + * has been set. * * @param v The term in question * @return true if v is a model core symbol @@ -4101,11 +4234,20 @@ class CVC5_EXPORT Solver /** * Get the model + * * SMT-LIB: - * \verbatim - * ( get-model ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (get-model) + * + * Requires to enable option + * :ref:`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 @@ -4117,49 +4259,76 @@ class CVC5_EXPORT Solver /** * Do quantifier elimination. + * * SMT-LIB: - * \verbatim - * ( get-qe ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (get-qe ) * \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 ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (get-qe-disjunct ) * \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; @@ -4186,10 +4355,15 @@ class CVC5_EXPORT Solver /** * Declare a symbolic pool of terms with the given initial value. + * * SMT-LIB: - * \verbatim - * ( declare-pool ( * ) ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (declare-pool ( * )) * \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 @@ -4199,21 +4373,33 @@ class CVC5_EXPORT Solver const std::vector& initValue) const; /** * Pop (a) level(s) from the assertion stack. + * * SMT-LIB: - * \verbatim - * ( pop ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (pop ) * \endverbatim + * * @param nscopes the number of levels to pop */ void pop(uint32_t nscopes = 1) const; /** * Get an interpolant + * * SMT-LIB: - * \verbatim - * ( get-interpol ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (get-interpol ) + * + * Requires to enable option + * :ref:`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. @@ -4223,11 +4409,18 @@ class CVC5_EXPORT Solver /** * Get an interpolant + * * SMT-LIB: - * \verbatim - * ( get-interpol ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (get-interpol ) + * + * Requires to enable option + * :ref:`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 @@ -4238,56 +4431,88 @@ class CVC5_EXPORT Solver /** * Get an abduct. + * * SMT-LIB: - * \verbatim - * ( get-abduct ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (get-abduct ) + * + * Requires to enable option + * :ref:`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 ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (get-abduct ) + * + * Requires to enable option + * :ref:`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 `. + * 'produce-models' and setting option + * :ref:`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 ( + ) ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (block-model-values ( + )) + * + * Requires enabling option + * :ref:`produce-models `. + * 'produce-models' and setting option + * :ref:`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& terms) const; @@ -4299,29 +4524,44 @@ class CVC5_EXPORT Solver /** * Push (a) level(s) to the assertion stack. + * * SMT-LIB: - * \verbatim - * ( push ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (push ) * \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 ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (set-info ) * \endverbatim + * * @param keyword the info flag * @param value the value of the info flag */ @@ -4329,20 +4569,30 @@ class CVC5_EXPORT Solver /** * Set logic. + * * SMT-LIB: - * \verbatim - * ( set-logic ) + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (set-logic ) * \endverbatim + * * @param logic the logic to set */ void setLogic(const std::string& logic) const; /** * Set option. + * * SMT-LIB: - * \verbatim - * ( set-option