From: Gereon Kremer Date: Tue, 30 Nov 2021 22:37:30 +0000 (-0800) Subject: Extend docs example extension (#7717) X-Git-Tag: cvc5-1.0.0~752 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=bcabf70ae1fefd2eb77c48baf9db1e2c88259622;p=cvc5.git Extend docs example extension (#7717) This PR extends the custom sphinx extension for examples. It now allows for simple patterns in the file names and matches the file types using arbitrary regular expressions instead of just looking at the file extensions. This is necessary to integrate examples from the z3pycompat API: the examples live at a nontrivial place (in the build folder), which we inject via the file name patterns; we will have two separate examples which both end in .py but can be distinguished via the pattern used in the beginning. --- diff --git a/docs/api/cpp/quickstart.rst b/docs/api/cpp/quickstart.rst index d171edda9..cb3e00fab 100644 --- a/docs/api/cpp/quickstart.rst +++ b/docs/api/cpp/quickstart.rst @@ -181,7 +181,7 @@ Example | The source code for this example can be found at `examples/api/cpp/quickstart.cpp `_. .. api-examples:: - ../../../examples/api/cpp/quickstart.cpp - ../../../examples/api/java/QuickStart.java - ../../../examples/api/python/quickstart.py - ../../../examples/api/smtlib/quickstart.smt2 + /api/cpp/quickstart.cpp + /api/java/QuickStart.java + /api/python/quickstart.py + /api/smtlib/quickstart.smt2 diff --git a/docs/api/python/regular/quickstart.rst b/docs/api/python/regular/quickstart.rst index bf8773ce8..783bcfd1f 100644 --- a/docs/api/python/regular/quickstart.rst +++ b/docs/api/python/regular/quickstart.rst @@ -169,7 +169,7 @@ Example | The source code for this example can be found at `examples/api/python/quickstart.py `_. .. api-examples:: - ../../../../examples/api/cpp/quickstart.cpp - ../../../../examples/api/java/QuickStart.java - ../../../../examples/api/python/quickstart.py - ../../../../examples/api/smtlib/quickstart.smt2 + /api/cpp/quickstart.cpp + /api/java/QuickStart.java + /api/python/quickstart.py + /api/smtlib/quickstart.smt2 diff --git a/docs/binary/quickstart.rst b/docs/binary/quickstart.rst index f3c9c4ad8..ddfc7d9f0 100644 --- a/docs/binary/quickstart.rst +++ b/docs/binary/quickstart.rst @@ -119,7 +119,7 @@ Example | The source code for this example can be found at `examples/api/smtlib/quickstart.smt2 `_. .. api-examples:: - ../../examples/api/smtlib/quickstart.smt2 - ../../examples/api/cpp/quickstart.cpp - ../../examples/api/java/QuickStart.java - ../../examples/api/python/quickstart.py + /api/smtlib/quickstart.smt2 + /api/cpp/quickstart.cpp + /api/java/QuickStart.java + /api/python/quickstart.py diff --git a/docs/conf.py.in b/docs/conf.py.in index 47bccd1fd..453a56aad 100644 --- a/docs/conf.py.in +++ b/docs/conf.py.in @@ -11,6 +11,7 @@ # documentation root, use os.path.abspath to make it absolute, like shown here. # +import os import sys # add path to enable extensions @@ -78,6 +79,12 @@ html_show_sourcelink = False html_extra_path = [] + +ex_patterns = { + '': '/../examples', + '': '/' + os.path.relpath('${CMAKE_BINARY_DIR}/deps/src/z3pycompat-EP', '${CMAKE_CURRENT_SOURCE_DIR}'), +} + # -- C++ / Breathe configuration --------------------------------------------- breathe_default_project = "cvc5" breathe_domain_by_extension = {"h" : "cpp"} diff --git a/docs/examples/bitvectors.rst b/docs/examples/bitvectors.rst index 2d6469611..d703d9211 100644 --- a/docs/examples/bitvectors.rst +++ b/docs/examples/bitvectors.rst @@ -3,7 +3,7 @@ Theory of Bit-Vectors .. api-examples:: - ../../examples/api/cpp/bitvectors.cpp - ../../examples/api/java/BitVectors.java - ../../examples/api/python/bitvectors.py - ../../examples/api/smtlib/bitvectors.smt2 + /api/cpp/bitvectors.cpp + /api/java/BitVectors.java + /api/python/bitvectors.py + /api/smtlib/bitvectors.smt2 diff --git a/docs/examples/bitvectors_and_arrays.rst b/docs/examples/bitvectors_and_arrays.rst index 9a9d47bd5..695ba5493 100644 --- a/docs/examples/bitvectors_and_arrays.rst +++ b/docs/examples/bitvectors_and_arrays.rst @@ -3,7 +3,7 @@ Theory of Bit-Vectors and Arrays .. api-examples:: - ../../examples/api/cpp/bitvectors_and_arrays.cpp - ../../examples/api/java/BitVectorsAndArrays.java - ../../examples/api/python/bitvectors_and_arrays.py - ../../examples/api/smtlib/bitvectors_and_arrays.smt2 + /api/cpp/bitvectors_and_arrays.cpp + /api/java/BitVectorsAndArrays.java + /api/python/bitvectors_and_arrays.py + /api/smtlib/bitvectors_and_arrays.smt2 diff --git a/docs/examples/combination.rst b/docs/examples/combination.rst index e5f38e21e..80e0e5d1b 100644 --- a/docs/examples/combination.rst +++ b/docs/examples/combination.rst @@ -1,9 +1,8 @@ Theory Combination ================== - .. api-examples:: - ../../examples/api/cpp/combination.cpp - ../../examples/api/java/Combination.java - ../../examples/api/python/combination.py - ../../examples/api/smtlib/combination.smt2 + /api/cpp/combination.cpp + /api/java/Combination.java + /api/python/combination.py + /api/smtlib/combination.smt2 diff --git a/docs/examples/datatypes.rst b/docs/examples/datatypes.rst index 4f2cbf176..ce26bc3de 100644 --- a/docs/examples/datatypes.rst +++ b/docs/examples/datatypes.rst @@ -3,7 +3,7 @@ Theory of Datatypes .. api-examples:: - ../../examples/api/cpp/datatypes.cpp - ../../examples/api/java/Datatypes.java - ../../examples/api/python/datatypes.py - ../../examples/api/smtlib/datatypes.smt2 + /api/cpp/datatypes.cpp + /api/java/Datatypes.java + /api/python/datatypes.py + /api/smtlib/datatypes.smt2 diff --git a/docs/examples/exceptions.rst b/docs/examples/exceptions.rst index 6598e8fb0..3f5074389 100644 --- a/docs/examples/exceptions.rst +++ b/docs/examples/exceptions.rst @@ -3,5 +3,5 @@ Exception Handling .. api-examples:: - ../../examples/api/java/Exceptions.java - ../../examples/api/python/exceptions.py + /api/java/Exceptions.java + /api/python/exceptions.py diff --git a/docs/examples/extract.rst b/docs/examples/extract.rst index 1f6d9b9bf..01b3716df 100644 --- a/docs/examples/extract.rst +++ b/docs/examples/extract.rst @@ -3,7 +3,7 @@ Theory of Bit-Vectors: :code:`extract` .. api-examples:: - ../../examples/api/cpp/extract.cpp - ../../examples/api/java/Extract.java - ../../examples/api/python/extract.py - ../../examples/api/smtlib/extract.smt2 + /api/cpp/extract.cpp + /api/java/Extract.java + /api/python/extract.py + /api/smtlib/extract.smt2 diff --git a/docs/examples/floatingpoint.rst b/docs/examples/floatingpoint.rst index 1b09102b2..f69c99cf8 100644 --- a/docs/examples/floatingpoint.rst +++ b/docs/examples/floatingpoint.rst @@ -3,5 +3,5 @@ Theory of Floating-Points .. api-examples:: - ../../examples/api/java/FloatingPointArith.java - ../../examples/api/python/floating_point.py + /api/java/FloatingPointArith.java + /api/python/floating_point.py diff --git a/docs/examples/helloworld.rst b/docs/examples/helloworld.rst index cdc424dfa..046ab07a0 100644 --- a/docs/examples/helloworld.rst +++ b/docs/examples/helloworld.rst @@ -5,7 +5,7 @@ This example shows the very basic usage of the API. We create a solver, declare a Boolean variable and check whether it is entailed (by ``true``, as nothing has been asserted to the solver). .. api-examples:: - ../../examples/api/cpp/helloworld.cpp - ../../examples/api/java/HelloWorld.java - ../../examples/api/python/helloworld.py - ../../examples/api/smtlib/helloworld.smt2 + /api/cpp/helloworld.cpp + /api/java/HelloWorld.java + /api/python/helloworld.py + /api/smtlib/helloworld.smt2 diff --git a/docs/examples/lineararith.rst b/docs/examples/lineararith.rst index 29d84cae5..f6914c88e 100644 --- a/docs/examples/lineararith.rst +++ b/docs/examples/lineararith.rst @@ -7,7 +7,7 @@ Secondly, it checks that this bound is tight by asserting :code:`y - x = 2/3` an The two checks are separated by using :code:`push` and :code:`pop`. .. api-examples:: - ../../examples/api/cpp/linear_arith.cpp - ../../examples/api/java/LinearArith.java - ../../examples/api/python/linear_arith.py - ../../examples/api/smtlib/linear_arith.smt2 + /api/cpp/linear_arith.cpp + /api/java/LinearArith.java + /api/python/linear_arith.py + /api/smtlib/linear_arith.smt2 diff --git a/docs/examples/quickstart.rst b/docs/examples/quickstart.rst index 330cc7065..8a58c89b2 100644 --- a/docs/examples/quickstart.rst +++ b/docs/examples/quickstart.rst @@ -3,7 +3,7 @@ Quickstart Example .. api-examples:: - ../../examples/api/cpp/quickstart.cpp - ../../examples/api/java/QuickStart.java - ../../examples/api/python/quickstart.py - ../../examples/api/smtlib/quickstart.smt2 + /api/cpp/quickstart.cpp + /api/java/QuickStart.java + /api/python/quickstart.py + /api/smtlib/quickstart.smt2 diff --git a/docs/examples/relations.rst b/docs/examples/relations.rst index d81eb8fee..a1a0541f7 100644 --- a/docs/examples/relations.rst +++ b/docs/examples/relations.rst @@ -3,6 +3,6 @@ Theory of Relations .. api-examples:: - ../../examples/api/java/Relations.java - ../../examples/api/smtlib/relations.smt2 + /api/java/Relations.java + /api/smtlib/relations.smt2 diff --git a/docs/examples/sequences.rst b/docs/examples/sequences.rst index b0a9ab1f1..cfaeab7fb 100644 --- a/docs/examples/sequences.rst +++ b/docs/examples/sequences.rst @@ -3,7 +3,7 @@ Theory of Sequences .. api-examples:: - ../../examples/api/cpp/sequences.cpp - ../../examples/api/java/Sequences.java - ../../examples/api/python/sequences.py - ../../examples/api/smtlib/sequences.smt2 + /api/cpp/sequences.cpp + /api/java/Sequences.java + /api/python/sequences.py + /api/smtlib/sequences.smt2 diff --git a/docs/examples/sets.rst b/docs/examples/sets.rst index 09cad0cce..384205c63 100644 --- a/docs/examples/sets.rst +++ b/docs/examples/sets.rst @@ -3,7 +3,7 @@ Theory of Sets .. api-examples:: - ../../examples/api/cpp/sets.cpp - ../../examples/api/java/Sets.java - ../../examples/api/python/sets.py - ../../examples/api/smtlib/sets.smt2 + /api/cpp/sets.cpp + /api/java/Sets.java + /api/python/sets.py + /api/smtlib/sets.smt2 diff --git a/docs/examples/strings.rst b/docs/examples/strings.rst index cc6211061..afc6a5a7c 100644 --- a/docs/examples/strings.rst +++ b/docs/examples/strings.rst @@ -3,7 +3,7 @@ Theory of Strings .. api-examples:: - ../../examples/api/cpp/strings.cpp - ../../examples/api/java/Strings.java - ../../examples/api/python/strings.py - ../../examples/api/smtlib/strings.smt2 + /api/cpp/strings.cpp + /api/java/Strings.java + /api/python/strings.py + /api/smtlib/strings.smt2 diff --git a/docs/examples/sygus-fun.rst b/docs/examples/sygus-fun.rst index 02ec56577..164a8f65b 100644 --- a/docs/examples/sygus-fun.rst +++ b/docs/examples/sygus-fun.rst @@ -3,7 +3,7 @@ SyGuS: Functions .. api-examples:: - ../../examples/api/cpp/sygus-fun.cpp - ../../examples/api/java/SygusFun.java - ../../examples/api/python/sygus-fun.py - ../../examples/api/smtlib/sygus-fun.sy + /api/cpp/sygus-fun.cpp + /api/java/SygusFun.java + /api/python/sygus-fun.py + /api/smtlib/sygus-fun.sy diff --git a/docs/examples/sygus-grammar.rst b/docs/examples/sygus-grammar.rst index ad22bdc85..4d416b5f8 100644 --- a/docs/examples/sygus-grammar.rst +++ b/docs/examples/sygus-grammar.rst @@ -3,7 +3,7 @@ SyGuS: Grammars .. api-examples:: - ../../examples/api/cpp/sygus-grammar.cpp - ../../examples/api/java/SygusGrammar.java - ../../examples/api/python/sygus-grammar.py - ../../examples/api/smtlib/sygus-grammar.sy + /api/cpp/sygus-grammar.cpp + /api/java/SygusGrammar.java + /api/python/sygus-grammar.py + /api/smtlib/sygus-grammar.sy diff --git a/docs/examples/sygus-inv.rst b/docs/examples/sygus-inv.rst index 54afe7727..b2addf8c1 100644 --- a/docs/examples/sygus-inv.rst +++ b/docs/examples/sygus-inv.rst @@ -3,7 +3,7 @@ SyGuS: Invariants .. api-examples:: - ../../examples/api/cpp/sygus-inv.cpp - ../../examples/api/java/SygusInv.java - ../../examples/api/python/sygus-inv.py - ../../examples/api/smtlib/sygus-inv.sy + /api/cpp/sygus-inv.cpp + /api/java/SygusInv.java + /api/python/sygus-inv.py + /api/smtlib/sygus-inv.sy diff --git a/docs/ext/examples.py b/docs/ext/examples.py index 42bcab3f8..204271f64 100644 --- a/docs/ext/examples.py +++ b/docs/ext/examples.py @@ -1,4 +1,5 @@ import os +import re from docutils import nodes from docutils.statemachine import StringList @@ -19,12 +20,37 @@ class APIExamples(SphinxDirective): """ # Set tab title and language for syntax highlighting - exts = { - '.cpp': {'title': 'C++', 'lang': 'c++'}, - '.java': {'title': 'Java', 'lang': 'java'}, - '.py': {'title': 'Python', 'lang': 'python'}, - '.smt2': {'title': 'SMT-LIBv2', 'lang': 'smtlib'}, - '.sy': {'title': 'SyGuS', 'lang': 'smtlib'}, + types = { + '\.cpp$': { + 'title': 'C++', + 'lang': 'c++', + 'group': 'c++' + }, + '\.java$': { + 'title': 'Java', + 'lang': 'java', + 'group': 'java' + }, + '.*\.py$': { + 'title': 'Python', + 'lang': 'python', + 'group': 'py-regular' + }, + '.*\.py$': { + 'title': 'Python z3py', + 'lang': 'python', + 'group': 'py-z3pycompat' + }, + '\.smt2$': { + 'title': 'SMT-LIBv2', + 'lang': 'smtlib', + 'group': 'smt2' + }, + '\.sy$': { + 'title': 'SyGuS', + 'lang': 'smtlib', + 'group': 'smt2' + }, } # The "arguments" are actually the content of the directive @@ -37,20 +63,27 @@ class APIExamples(SphinxDirective): # collect everything in a list of strings content = ['.. tabs::', ''] - remaining = set([self.exts[e]['lang'] for e in self.exts]) + remaining = set([t['group'] for t in self.types.values()]) location = '{}:{}'.format(*self.get_source_info()) for file in self.content: # detect file extension - _, ext = os.path.splitext(file) - if ext in self.exts: - title = self.exts[ext]['title'] - lang = self.exts[ext]['lang'] - remaining.remove(lang) - else: - self.logger.warning(f'{location} is using unknown file extension "{ext}"') - title = ext - lang = ext + lang = None + title = None + for type in self.types: + if re.search(type, file) != None: + lang = self.types[type]['lang'] + title = self.types[type]['title'] + remaining.discard(self.types[type]['group']) + break + if lang == None: + self.logger.warning( + f'file type of {location} could not be detected') + title = os.path.splitext(file)[1] + lang = title + + for k, v in self.env.config.ex_patterns.items(): + file = file.replace(k, v) # generate tabs content.append(f' .. tab:: {title}') @@ -70,6 +103,7 @@ class APIExamples(SphinxDirective): def setup(app): app.setup_extension('sphinx_tabs.tabs') + app.add_config_value('ex_patterns', {}, 'env') app.add_directive("api-examples", APIExamples) return { 'version': '0.1', diff --git a/docs/theories/sets-and-relations.rst b/docs/theories/sets-and-relations.rst index 8bce6b72c..2da6715e3 100644 --- a/docs/theories/sets-and-relations.rst +++ b/docs/theories/sets-and-relations.rst @@ -8,9 +8,9 @@ cvc5 supports the theory of finite sets. The simplest way to get a sense of the syntax is to look at an example: .. api-examples:: - ../../examples/api/cpp/sets.cpp - ../../examples/api/python/sets.py - ../../examples/api/smtlib/sets.smt2 + /api/cpp/sets.cpp + /api/python/sets.py + /api/smtlib/sets.smt2 The source code of these examples is available at: @@ -148,7 +148,7 @@ Finite Relations Example: .. api-examples:: - ../../examples/api/smtlib/relations.smt2 + /api/smtlib/relations.smt2 For reference, below is a short summary of the sorts, constants, functions and predicates. diff --git a/docs/theories/transcendentals.rst b/docs/theories/transcendentals.rst index cf52b0889..6d35e6cce 100644 --- a/docs/theories/transcendentals.rst +++ b/docs/theories/transcendentals.rst @@ -50,6 +50,6 @@ Examples -------- .. api-examples:: - ../../examples/api/cpp/transcendentals.cpp - ../../examples/api/python/transcendentals.py - ../../examples/api/smtlib/transcendentals.smt2 \ No newline at end of file + /api/cpp/transcendentals.cpp + /api/python/transcendentals.py + /api/smtlib/transcendentals.smt2 \ No newline at end of file