api: Fix formatting of docs for Term::getSetValue(). (#7914)
authorAina Niemetz <aina.niemetz@gmail.com>
Tue, 11 Jan 2022 16:25:00 +0000 (08:25 -0800)
committerGitHub <noreply@github.com>
Tue, 11 Jan 2022 16:25:00 +0000 (16:25 +0000)
docs/ext/smtliblexer.py
src/api/cpp/cvc5.h

index f6f1679c078c694256d4fad433f45dc91526ec55..04c70133ee9c99528c6abf20fc8cd9c395a5285e 100644 (file)
@@ -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 ")")
index b3dc03250c2206bd1a49eec633cb800a3613c05a..6c29e36f28e648eca0c0e54320638c078ee0d64a 100644 (file)
@@ -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;