1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
|
##
# Configuration file for the Sphinx documentation builder.
#
# This file only contains a selection of the most common options. For a full
# list see the documentation:
# https://www.sphinx-doc.org/en/master/usage/configuration.html
# -- Path setup --------------------------------------------------------------
# If extensions (or modules to document with autodoc) are in another directory,
# add these directories to sys.path here. If the directory is relative to the
# documentation root, use os.path.abspath to make it absolute, like shown here.
#
# import os
# import sys
# sys.path.insert(0, os.path.abspath('.'))
# Specify where to find bitwuzla
import sys
sys.path.insert(0, "@bitwuzla_python_dir@")
# Add path to enable custom extensions
sys.path.insert(0, '@current_source_dir@/extensions/')
# -- Project information -----------------------------------------------------
from datetime import datetime
project = 'Bitwuzla'
copyright = f'{datetime.now().year}, the authors of Bitwuzla'
author = 'The authors of Bitwuzla'
version = '@version@'
# -- General configuration ---------------------------------------------------
# Add any Sphinx extension module names here, as strings. They can be
# extensions coming with Sphinx (named 'sphinx.ext.*') or your custom
# ones.
extensions = [
'sphinxcontrib.bibtex',
'sphinx.ext.autodoc',
'sphinx.ext.autosectionlabel',
'sphinx_tabs.tabs',
'sphinx.ext.todo',
'breathe',
'examples',
'literalincludegen'
]
todo_include_todos = True
# Make sure the target is unique
autosectionlabel_prefix_document = True
bibtex_bibfiles = ['references.bib']
# Add any paths that contain templates here, relative to this directory.
templates_path = ['_templates']
# List of patterns, relative to source directory, that match files and
# directories to ignore when looking for source files.
# This pattern also affects html_static_path and html_extra_path.
exclude_patterns = ['_build', 'Thumbs.db', '.DS_Store']
# -- Options for HTML output -------------------------------------------------
# The theme to use for HTML and HTML Help pages. See the documentation for
# a list of builtin themes.
#
html_theme = 'sphinx_rtd_theme'
# Add any paths that contain custom static files (such as style sheets) here,
# relative to this directory. They are copied after the builtin static files,
# so a file named "default.css" will overwrite the builtin "default.css".
html_static_path = ['@current_source_dir@/_static']
html_css_files = ['custom.css']
html_show_sourcelink = False
# -- Breathe configuration ---------------------------------------------------
breathe_domain_by_extension = {"h" : "cpp"}
# -- Literal include extension for generated files ---------------------------
lig_source_dir = '@current_source_dir@'
lig_build_dir = '@current_build_dir@'
# -- SMT-LIB syntax highlighting ---------------------------------------------
from pygments.lexer import RegexLexer
from pygments import token
from sphinx.highlighting import lexers
class SmtLibLexer(RegexLexer):
name = 'smtlib'
tokens = {
'root': [
(r'QF_BV', token.Text),
(r'QF_ABV', token.Text),
(r'set-logic', token.Keyword),
(r'set-option', token.Keyword),
(r'declare-const', token.Keyword),
(r'declare-fun', token.Keyword),
(r'define-fun', token.Keyword),
(r'assert\b', token.Keyword),
(r'check-sat-assuming', token.Keyword),
(r'check-sat', token.Keyword),
(r'exit', token.Keyword),
(r'get-model', token.Keyword),
(r'get-unsat-assumptions', token.Keyword),
(r'get-unsat-core', token.Keyword),
(r'get-value', token.Keyword),
(r'reset-assertions', token.Keyword),
(r'reset', token.Keyword),
(r'push', token.Keyword),
(r'pop', token.Keyword),
(r':named', token.Name.Attribute),
(r':produce-models', token.Name.Attribute),
(r':produce-unsat-cores', token.Name.Attribute),
(r':produce-unsat-assumptions', token.Name.Attribute),
(r':verbosity', token.Name.Attribute),
(r':bv-solver', token.Name.Attribute),
(r'!', token.Name.Attribute),
(r'BitVec', token.Name.Attribute),
(r'RNE', token.Name.Attribute),
(r'true', token.String),
(r'false', token.String),
(r'distinct', token.Operator),
(r'=', token.Operator),
(r'and', token.Operator),
(r'bvadd', token.Operator),
(r'bvashr', token.Operator),
(r'bvmul', token.Operator),
(r'bvugt', token.Operator),
(r'bvult', token.Operator),
(r'bvule', token.Operator),
(r'bvsdiv', token.Operator),
(r'extract', token.Operator),
(r'fp.gt', token.Operator),
(r'ite', token.Operator),
(r'to_fp_unsigned', token.Operator),
(r'\+zero', token.Operator),
(r'#b[0-1]+', token.String),
(r'bv[0-9]+', token.String),
(r'[a-zA-Z][a-zA-Z0-9]*', token.Name),
(r'[0-9]+', token.Number),
(r'\s', token.Text),
(r'\(_', token.Text),
(r'\(', token.Text),
(r'\)', token.Text),
(r'@bzla.var_', token.Text),
(r';.*$', token.Comment),
(r'".*"', token.String)
]
}
lexers['smtlib'] = SmtLibLexer()
|
