###############################################################################
# Top contributors (to current version):
#   Gereon Kremer, Aina Niemetz, Mathias Preiner
#
# This file is part of the cvc5 project.
#
# Copyright (c) 2009-2025 by the authors listed in the file AUTHORS
# in the top-level source directory and their institutional affiliations.
# All rights reserved.  See the file COPYING in the top-level source
# directory for licensing information.
# #############################################################################
#
# 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
import datetime

# add path to enable extensions
sys.path.insert(0, '${CMAKE_CURRENT_SOURCE_DIR}/ext/')

# path to python api
sys.path.insert(0, '${CMAKE_BINARY_DIR}/src/api/python')

if("${BUILD_BINDINGS_PYTHON}" == "ON"):
        tags.add('bindings_python')
if("${BUILD_BINDINGS_JAVA}" == "ON"):
        tags.add('bindings_java')


# -- Project information -----------------------------------------------------

project = 'cvc5'
copyright = f'{datetime.date.today().year}, the authors of cvc5'
author = 'The authors of cvc5'


# -- 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 = [
        # sphinx core extensions
        'sphinx.ext.autodoc',
        'sphinx.ext.autosectionlabel',
        'sphinx.ext.extlinks',
        'sphinx.ext.mathjax',
        # other sphinx extensions
        'breathe',
        'sphinxcontrib.bibtex',
        'sphinxcontrib.programoutput',
        'sphinx_tabs.tabs',
        # custom cvc5 extensions
        'autoenum',
        'examples',
        'include_build_file',
        'run_command',
]

# Google analytics
if ${GOOGLE_ANALYTICS_ENABLE}:
  extensions += ['sphinxcontrib.googleanalytics']

# 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'
html_theme_options = {
    'navigation_depth': 5
}
html_static_path = ['${CMAKE_CURRENT_SOURCE_DIR}/_static/']
html_css_files = ['custom.css']
html_show_sourcelink = False

html_extra_path = []


# -- SMT-LIB syntax highlighting ---------------------------------------------

from smtliblexer import SmtLibLexer
from sphinx.highlighting import lexers
lexers['smtlib'] = SmtLibLexer()


# -- Java configuration ------------------------------------------------------
if tags.has('bindings_java'):
        html_extra_path.append('${CMAKE_BINARY_DIR}/docs/api/java/build/')


# -- core extension:: sphinx.ext.autosectionlabel ----------------------------

# Make sure the target is unique
autosectionlabel_prefix_document = True

# -- core extension:: sphinx.ext.extlinks ------------------------------------

extlinks = {
        'cvc5src': ('https://github.com/cvc5/cvc5/blob/main/src/%s', '%s'),
        'cvc5repo': ('https://github.com/cvc5/cvc5/blob/main/%s', '%s'),
}


# -- core extension:: sphinx.ext.mathjax -------------------------------------

# enforce using mathjax3
mathjax_path = "https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js"

# load additional packages and predefine some macros
mathjax3_config = {
  'loader': {
    'load': ['[tex]/ams', '[tex]/bussproofs'],
  },
  'tex': {
    'packages': {
      '[+]': ['ams', 'bussproofs'],
    },
    'macros': {
      'xor': r'\mathbin{xor}',
      'ite': [r'#1 \mathbin{?} #2 \mathbin{:} #3', 3],
      'inferrule': [r'\begin{prooftree}\AxiomC{$#1$}\UnaryInfC{$#2$}\end{prooftree}', 2],
      'inferruleSC': [r'\begin{prooftree}\AxiomC{$#1$}\RightLabel{ #3}\UnaryInfC{$#2$}\end{prooftree}', 3],
    }
  }
}

# -- extension:: breathe -----------------------------------------------------
breathe_default_project = "cvc5"
breathe_domain_by_extension = {"h" : "cpp"}
cpp_index_common_prefix = ["cvc5::"]


# -- extension:: sphinxcontrib.bibtex ----------------------------------------

bibtex_bibfiles = ['references.bib']

# -- extension:: sphinxcontrib.googleanalytics -------------------------------

googleanalytics_id = 'G-ML12X2V35B'
googleanalytics_enabled = ${GOOGLE_ANALYTICS_ENABLE}

# -- custom extension:: examples ---------------------------------------------

# Configuration for tabs: title, language and group for detecting missing files
examples_types = {
        r'\.cpp$': {
                'title': 'C++',
                'lang': 'c++',
                'group': 'c++'
        },
        r'\.c$': {
                'title': 'C',
                'lang': 'c',
                'group': 'c'
        },
        r'\.h$': {
                'title': 'C++ (header)',
                'lang': 'c++',
                'group': 'c++'
        },
        r'\.java$': {
                'title': 'Java',
                'lang': 'java',
                'group': 'java'
        },
        r'^<examples>.*pythonic.*\.py$': {
                'title': 'Python (pythonic)',
                'lang': 'python',
                'group': 'py-pythonicapi'
        },
        r'^<examples>.*\.py$': {
                'title': 'Python (base)',
                'lang': 'python',
                'group': 'py-regular'
        },
        r'^<pythonicapi>.*\.py$': {
                'title': 'Python (pythonic)',
                'lang': 'python',
                'group': 'py-pythonicapi'
        },
        r'\.smt2$': {
                'title': 'SMT-LIBv2',
                'lang': 'smtlib',
                'group': 'smt2'
        },
        r'\.sy$': {
                'title': 'SyGuS',
                'lang': 'smtlib',
                'group': 'smt2'
        },
}
# Special file patterns
examples_file_patterns = {
        r'^<examples>(.*)': {
                'local': '/../examples{}',
                'url': 'https://github.com/cvc5/cvc5/tree/main/examples{}',
                'urlname': 'examples{}',
        },
        r'<pythonicapi>(.*)': {
                'local': '/' + os.path.relpath('${CMAKE_BINARY_DIR}/deps/src/CVC5PythonicAPI', '${CMAKE_CURRENT_SOURCE_DIR}') + '{}',
                'url': 'https://github.com/cvc5/cvc5_pythonic_api/tree/main{}',
                'urlname': 'cvc5_pythonic_api:{}',
        }
}


# -- custom extension:: include_build_file -----------------------------------

# where to look for include-build-file
ibf_folders = ['${CMAKE_CURRENT_BINARY_DIR}']


# -- custom extension:: run_command ------------------------------------------

runcmd_build = '/' + os.path.relpath('${CMAKE_BINARY_DIR}', '${CMAKE_CURRENT_SOURCE_DIR}')