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.

24 files changed, 138 insertions, 98 deletions

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 <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 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 <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 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 <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 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>': '/../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 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
+    <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 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
+    <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 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
+    <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 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
+    <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 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
+    <examples>/api/java/Exceptions.java
+    <examples>/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
+    <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 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
+    <examples>/api/java/FloatingPointArith.java
+    <examples>/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
+    <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 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
+    <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 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
+    <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 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
+    <examples>/api/java/Relations.java
+    <examples>/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
+    <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 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
+    <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 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
+    <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 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
+    <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 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
+    <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 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
+    <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 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'
+        },
+        '<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 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
+    <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 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
+    <examples>/api/cpp/transcendentals.cpp
+    <examples>/api/python/transcendentals.py
+    <examples>/api/smtlib/transcendentals.smt2
\ No newline at end of file