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 d171edda957baadf6c8e4b8ff64f8137ded74943..cb3e00fabbcaa20b703f3aafd086d8b5252b1824 100644 (file)
--- 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 <https://github.com/cvc5/cvc5/blob/master/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
+    <examples>/api/cpp/quickstart.cpp
+    <examples>/api/java/QuickStart.java
+    <examples>/api/python/quickstart.py
+    <examples>/api/smtlib/quickstart.smt2

diff --git a/docs/api/python/regular/quickstart.rst b/docs/api/python/regular/quickstart.rst
index bf8773ce871e1d89816cde0e1f39b875271857db..783bcfd1f5e3663129aa50281aba1d404db921a5 100644 (file)
--- 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 <https://github.com/cvc5/cvc5/blob/master/examples/api/python/quickstart.cpp>`_.
 
 .. api-examples::
-    ../../../../examples/api/cpp/quickstart.cpp
-    ../../../../examples/api/java/QuickStart.java
-    ../../../../examples/api/python/quickstart.py
-    ../../../../examples/api/smtlib/quickstart.smt2
+    <examples>/api/cpp/quickstart.cpp
+    <examples>/api/java/QuickStart.java
+    <examples>/api/python/quickstart.py
+    <examples>/api/smtlib/quickstart.smt2

diff --git a/docs/binary/quickstart.rst b/docs/binary/quickstart.rst
index f3c9c4ad870843f42c7084d7303a69f0b1a242d6..ddfc7d9f07cbae862a3de912f6e4919c05c61195 100644 (file)
--- 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 <https://github.com/cvc5/cvc5/blob/master/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
+    <examples>/api/smtlib/quickstart.smt2
+    <examples>/api/cpp/quickstart.cpp
+    <examples>/api/java/QuickStart.java
+    <examples>/api/python/quickstart.py

diff --git a/docs/conf.py.in b/docs/conf.py.in
index 47bccd1fd1ad0b9adfe0252932489a34992809a3..453a56aad905778ec5245200b366579571306277 100644 (file)
--- 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>': '/../examples',
+        '<z3pycompat>': '/' + 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 2d6469611feea9ae1064a873b23887cc907b7a64..d703d921160b4e6125a1d626971f80710a69a13d 100644 (file)
--- 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
+    <examples>/api/cpp/bitvectors.cpp
+    <examples>/api/java/BitVectors.java
+    <examples>/api/python/bitvectors.py
+    <examples>/api/smtlib/bitvectors.smt2

diff --git a/docs/examples/bitvectors_and_arrays.rst b/docs/examples/bitvectors_and_arrays.rst
index 9a9d47bd5f5424ed428d34ef922ca2c0337c4ae6..695ba549332802d0b1ee7fb2b2896c71cab5084f 100644 (file)
--- 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
+    <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

diff --git a/docs/examples/combination.rst b/docs/examples/combination.rst
index e5f38e21e9426f07aeb2fdd512ff8ccb0d6bb52d..80e0e5d1b129047ee5f319984ac32462ca0b78d5 100644 (file)
--- 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
+    <examples>/api/cpp/combination.cpp
+    <examples>/api/java/Combination.java
+    <examples>/api/python/combination.py
+    <examples>/api/smtlib/combination.smt2

diff --git a/docs/examples/datatypes.rst b/docs/examples/datatypes.rst
index 4f2cbf1768cc0565ada3f352c073ebc4f75aadd2..ce26bc3de261153301824ff01b8d9c27adb95ec5 100644 (file)
--- 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
+    <examples>/api/cpp/datatypes.cpp
+    <examples>/api/java/Datatypes.java
+    <examples>/api/python/datatypes.py
+    <examples>/api/smtlib/datatypes.smt2

diff --git a/docs/examples/exceptions.rst b/docs/examples/exceptions.rst
index 6598e8fb02a137bae4a50d887bec4b425f6fa653..3f50743895532e6801d639e2468cc7bd5d8d20e8 100644 (file)
--- 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
+    <examples>/api/java/Exceptions.java
+    <examples>/api/python/exceptions.py

diff --git a/docs/examples/extract.rst b/docs/examples/extract.rst
index 1f6d9b9bfed8821a956f6e98b61ddf59a89d2fb1..01b3716df767cfd7a8ad605a5fa8bee557527e38 100644 (file)
--- 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
+    <examples>/api/cpp/extract.cpp
+    <examples>/api/java/Extract.java
+    <examples>/api/python/extract.py
+    <examples>/api/smtlib/extract.smt2

diff --git a/docs/examples/floatingpoint.rst b/docs/examples/floatingpoint.rst
index 1b09102b26fec7b441dd238aa0e8612e3b90b1c3..f69c99cf8fdd01cdd3b5fd81147fdb7074b2c31c 100644 (file)
--- 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
+    <examples>/api/java/FloatingPointArith.java
+    <examples>/api/python/floating_point.py

diff --git a/docs/examples/helloworld.rst b/docs/examples/helloworld.rst
index cdc424dfadb16580759a3295149c9790f884933d..046ab07a04bd2ae8c0d2355c3e90125bea7e354a 100644 (file)
--- 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
+    <examples>/api/cpp/helloworld.cpp
+    <examples>/api/java/HelloWorld.java
+    <examples>/api/python/helloworld.py
+    <examples>/api/smtlib/helloworld.smt2

diff --git a/docs/examples/lineararith.rst b/docs/examples/lineararith.rst
index 29d84cae5a6f01a3a9d54e49947afc8526f6ea1c..f6914c88e76df1423c384aaacb91266cd0e70925 100644 (file)
--- 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
+    <examples>/api/cpp/linear_arith.cpp
+    <examples>/api/java/LinearArith.java
+    <examples>/api/python/linear_arith.py
+    <examples>/api/smtlib/linear_arith.smt2

diff --git a/docs/examples/quickstart.rst b/docs/examples/quickstart.rst
index 330cc706546a97f48fcaacce4532e2d1776ce202..8a58c89b28ead04758d4c784e97d3e96849a9be0 100644 (file)
--- 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
+    <examples>/api/cpp/quickstart.cpp
+    <examples>/api/java/QuickStart.java
+    <examples>/api/python/quickstart.py
+    <examples>/api/smtlib/quickstart.smt2

diff --git a/docs/examples/relations.rst b/docs/examples/relations.rst
index d81eb8feed2242ba416f74288fcd53fe2bb9b63b..a1a0541f7d174528729be3e8a4676badcf7ab8ac 100644 (file)
--- 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
+    <examples>/api/java/Relations.java
+    <examples>/api/smtlib/relations.smt2
 

diff --git a/docs/examples/sequences.rst b/docs/examples/sequences.rst
index b0a9ab1f1aefcfb8f710f1e345ef87b9a766a7ef..cfaeab7fb7db7da63aceb3d52cdb3375099cce03 100644 (file)
--- 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
+    <examples>/api/cpp/sequences.cpp
+    <examples>/api/java/Sequences.java
+    <examples>/api/python/sequences.py
+    <examples>/api/smtlib/sequences.smt2

diff --git a/docs/examples/sets.rst b/docs/examples/sets.rst
index 09cad0ccee0ef83ab12e8eff12a07c64c4263f82..384205c63aacfbe8a0cac4c95daafb0c3f88bf59 100644 (file)
--- 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
+    <examples>/api/cpp/sets.cpp
+    <examples>/api/java/Sets.java
+    <examples>/api/python/sets.py
+    <examples>/api/smtlib/sets.smt2

diff --git a/docs/examples/strings.rst b/docs/examples/strings.rst
index cc6211061dcc0880c68ef7396bf156be351a0592..afc6a5a7cd5c5922ca99842b8e2ea5a0fc411155 100644 (file)
--- 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
+    <examples>/api/cpp/strings.cpp
+    <examples>/api/java/Strings.java
+    <examples>/api/python/strings.py
+    <examples>/api/smtlib/strings.smt2

diff --git a/docs/examples/sygus-fun.rst b/docs/examples/sygus-fun.rst
index 02ec5657766364ea4b4945e6a02cb475a5650c8f..164a8f65b6d06c0bca49eb6978bb6287119e3ba2 100644 (file)
--- 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
+    <examples>/api/cpp/sygus-fun.cpp
+    <examples>/api/java/SygusFun.java
+    <examples>/api/python/sygus-fun.py
+    <examples>/api/smtlib/sygus-fun.sy

diff --git a/docs/examples/sygus-grammar.rst b/docs/examples/sygus-grammar.rst
index ad22bdc85e0d41bab289f6011ed354dd842f590f..4d416b5f824dfa1a6adc9418cbcfac15ae826da1 100644 (file)
--- 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
+    <examples>/api/cpp/sygus-grammar.cpp
+    <examples>/api/java/SygusGrammar.java
+    <examples>/api/python/sygus-grammar.py
+    <examples>/api/smtlib/sygus-grammar.sy

diff --git a/docs/examples/sygus-inv.rst b/docs/examples/sygus-inv.rst
index 54afe7727ade4e743ebea38dbc0169547152ea2d..b2addf8c172f35e410cdd1968743901b7da40d1a 100644 (file)
--- 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
+    <examples>/api/cpp/sygus-inv.cpp
+    <examples>/api/java/SygusInv.java
+    <examples>/api/python/sygus-inv.py
+    <examples>/api/smtlib/sygus-inv.sy

diff --git a/docs/ext/examples.py b/docs/ext/examples.py
index 42bcab3f81acdfff2312a5ba4c2d6149b4a66935..204271f643f33280732795afd3d581ce319910c9 100644 (file)
--- 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'
+        },
+        '<examples>.*\.py$': {
+            'title': 'Python',
+            'lang': 'python',
+            'group': 'py-regular'
+        },
+        '<z3pycompat>.*\.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 8bce6b72c80783c9867215f098eac0ee26a9e7c8..2da6715e3cf12926f4f46e4b5679f6d5cb7de583 100644 (file)
--- 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
+    <examples>/api/cpp/sets.cpp
+    <examples>/api/python/sets.py
+    <examples>/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
+    <examples>/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 cf52b08898b0dd1e4776531e6000c609a83c74e8..6d35e6cce68def1549c361affa145a91789663d7 100644 (file)
--- 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
+    <examples>/api/cpp/transcendentals.cpp
+    <examples>/api/python/transcendentals.py
+    <examples>/api/smtlib/transcendentals.smt2
\ No newline at end of file