From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Tue, 11 Jan 2022 16:25:00 +0000 (-0800)
Subject: api: Fix formatting of docs for Term::getSetValue(). (#7914)
X-Git-Tag: cvc5-1.0.0~565
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ac0c6dea9bac470813685dfb8dd12576fa20686f;p=cvc5.git

api: Fix formatting of docs for Term::getSetValue(). (#7914)
---

diff --git a/docs/ext/smtliblexer.py b/docs/ext/smtliblexer.py
index f6f1679c0..04c70133e 100644
--- a/docs/ext/smtliblexer.py
+++ b/docs/ext/smtliblexer.py
@@ -100,6 +100,8 @@ class SmtLibLexer(RegexLexer):
             # parentheses
             (r'\(', token.Text),
             (r'\)', token.Text),
+            (r'\{', token.Text),
+            (r'\}', token.Text),
             # commands (terminated by whitespace or ")")
             ('(' + '|'.join(COMMANDS) + ')(?=(\s|\)))', token.Keyword),
             # sorts (terminated by whitespace or ")")
diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index b3dc03250..6c29e36f2 100644
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -1522,12 +1522,16 @@ 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:
    *
+   * \verbatim embed:rst:leading-asterisk
+   * .. code:: smtlib
+   *
    *     (union (singleton c1) ... (union (singleton c_{n-1}) (singleton c_n))))
+   * \endverbatim
    *
-   * where `c1 ... cn` are values ordered by id such that `c1 > ... > cn` (see
-   * also @ref Term::operator>(const Term&) const).
+   * where @f$c_1 ... c_n@f$ are values ordered by id such that
+   * @f$c_1 > ... > c_n@f$ (see @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;