api: Fix smt-lib code blocks and math in C++ docs. (#7795)

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 <io/github/cvc5/api/package-summary.html>`_
-^^^^^^^^^^^^^^^
+^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 
   * class `Datatype <io/github/cvc5/api/Datatype.html>`_
   * class `DatatypeConstructor <io/github/cvc5/api/DatatypeConstructor.html>`_
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 <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
@@ -3779,30 +3796,45 @@ class CVC5_EXPORT Solver
 
   /**
    * 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.
    */
@@ -3810,10 +3842,15 @@ class CVC5_EXPORT Solver
 
   /**
    * 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.
    */
@@ -3836,10 +3873,15 @@ class CVC5_EXPORT Solver
 
   /**
    * 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
@@ -3849,10 +3891,15 @@ class CVC5_EXPORT Solver
 
   /**
    * 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
@@ -3864,10 +3911,15 @@ class CVC5_EXPORT Solver
 
   /**
    * 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
@@ -3876,10 +3928,15 @@ class CVC5_EXPORT Solver
 
   /**
    * 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
@@ -3896,10 +3953,15 @@ class CVC5_EXPORT Solver
 
   /**
    * 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
@@ -3916,10 +3978,15 @@ class CVC5_EXPORT Solver
 
   /**
    * 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
@@ -3935,10 +4002,18 @@ class CVC5_EXPORT Solver
 
   /**
    * 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
@@ -3954,10 +4029,15 @@ class CVC5_EXPORT Solver
 
   /**
    * 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
    */
@@ -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<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
    */
@@ -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 <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;
@@ -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<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.
    */
@@ -4058,10 +4177,15 @@ class CVC5_EXPORT Solver
 
   /**
    * 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
    */
@@ -4069,10 +4193,15 @@ class CVC5_EXPORT Solver
 
   /**
    * 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
    */
@@ -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 <lbl-option-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 <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
@@ -4117,49 +4259,76 @@ class CVC5_EXPORT Solver
 
   /**
    * 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;
 
@@ -4186,10 +4355,15 @@ class CVC5_EXPORT Solver
 
   /**
    * 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
@@ -4199,21 +4373,33 @@ class CVC5_EXPORT Solver
                    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.
@@ -4223,11 +4409,18 @@ class CVC5_EXPORT Solver
 
   /**
    * 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
@@ -4238,56 +4431,88 @@ class CVC5_EXPORT Solver
 
   /**
    * 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;
 
@@ -4299,29 +4524,44 @@ class CVC5_EXPORT Solver
 
   /**
    * 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
    */
@@ -4329,20 +4569,30 @@ class CVC5_EXPORT Solver
 
   /**
    * 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
    */
@@ -4361,10 +4611,15 @@ class CVC5_EXPORT Solver
 
   /**
    * 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
@@ -4385,10 +4640,15 @@ class CVC5_EXPORT Solver
 
   /**
    * 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
@@ -4400,10 +4660,15 @@ class CVC5_EXPORT Solver
 
   /**
    * 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
@@ -4417,10 +4682,15 @@ class CVC5_EXPORT Solver
 
   /**
    * 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
@@ -4430,10 +4700,15 @@ class CVC5_EXPORT Solver
 
   /**
    * 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
@@ -4445,20 +4720,30 @@ class CVC5_EXPORT Solver
 
   /**
    * 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;
@@ -4466,10 +4751,15 @@ class CVC5_EXPORT Solver
   /**
    * 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
@@ -4481,10 +4771,15 @@ class CVC5_EXPORT Solver
    * 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;
@@ -4605,10 +4900,15 @@ class CVC5_EXPORT Solver
 
   /**
    * 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