##
# 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 -----------------------------------------------------

project = 'Bitwuzla'
copyright = '2023, 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()