Scaffold the idiomatic API's documentation (#7715)

Scaffolding the documentation, and fleshing it out for the Boolean functions and terms.

14 files changed, 119 insertions, 1 deletions

diff --git a/docs/api/python/z3compat/arith.rst b/docs/api/python/z3compat/arith.rst
new file mode 100644
index 000000000..783518e32
--- /dev/null
+++ b/docs/api/python/z3compat/arith.rst
@@ -0,0 +1,2 @@
+Arithmetic
+============
diff --git a/docs/api/python/z3compat/array.rst b/docs/api/python/z3compat/array.rst
new file mode 100644
index 000000000..27a6608b6
--- /dev/null
+++ b/docs/api/python/z3compat/array.rst
@@ -0,0 +1,2 @@
+Arrays
+============
diff --git a/docs/api/python/z3compat/bitvec.rst b/docs/api/python/z3compat/bitvec.rst
new file mode 100644
index 000000000..df4eb16ec
--- /dev/null
+++ b/docs/api/python/z3compat/bitvec.rst
@@ -0,0 +1,2 @@
+Bit-Vectors
+============
diff --git a/docs/api/python/z3compat/boolean.rst b/docs/api/python/z3compat/boolean.rst
new file mode 100644
index 000000000..e48e7f9e9
--- /dev/null
+++ b/docs/api/python/z3compat/boolean.rst
@@ -0,0 +1,70 @@
+Core & Booleans
+================
+
+Basic Boolean Term Builders
+-------------------
+.. autofunction:: cvc5_z3py_compat.Bool
+.. autofunction:: cvc5_z3py_compat.Bools
+.. autofunction:: cvc5_z3py_compat.BoolVal
+.. autofunction:: cvc5_z3py_compat.BoolSort
+.. autofunction:: cvc5_z3py_compat.FreshBool
+.. autofunction:: cvc5_z3py_compat.BoolVector
+
+Basic Generic Term Builders
+-------------------
+.. autofunction:: cvc5_z3py_compat.Const
+.. autofunction:: cvc5_z3py_compat.Consts
+.. autofunction:: cvc5_z3py_compat.FreshConst
+
+Boolean Operators
+-------------------
+.. autofunction:: cvc5_z3py_compat.And
+.. autofunction:: cvc5_z3py_compat.Or
+.. autofunction:: cvc5_z3py_compat.Not
+.. autofunction:: cvc5_z3py_compat.mk_not
+.. autofunction:: cvc5_z3py_compat.Implies
+.. autofunction:: cvc5_z3py_compat.Xor
+
+Generic Operators
+-------------------
+.. autofunction:: cvc5_z3py_compat.If
+.. autofunction:: cvc5_z3py_compat.Distinct
+
+Equality
+~~~~~~~~
+
+See
+:py:meth:`cvc5_z3py_compat.ExprRef.__eq__`
+and
+:py:meth:`cvc5_z3py_compat.ExprRef.__ne__`
+for building equality and disequality terms.
+
+
+Testers
+-------------------
+.. autofunction:: cvc5_z3py_compat.is_bool
+.. autofunction:: cvc5_z3py_compat.is_true
+.. autofunction:: cvc5_z3py_compat.is_false
+.. autofunction:: cvc5_z3py_compat.is_and
+.. autofunction:: cvc5_z3py_compat.is_or
+.. autofunction:: cvc5_z3py_compat.is_implies
+.. autofunction:: cvc5_z3py_compat.is_not
+.. autofunction:: cvc5_z3py_compat.is_eq
+.. autofunction:: cvc5_z3py_compat.is_distinct
+.. autofunction:: cvc5_z3py_compat.is_const
+
+
+Classes
+--------
+.. autoclass:: cvc5_z3py_compat.ExprRef
+   :members:
+   :special-members:
+.. autoclass:: cvc5_z3py_compat.SortRef
+   :members:
+   :special-members:
+.. autoclass:: cvc5_z3py_compat.BoolRef
+   :members:
+   :special-members:
+.. autoclass:: cvc5_z3py_compat.BoolSortRef
+   :members:
+   :special-members:
diff --git a/docs/api/python/z3compat/commands.rst b/docs/api/python/z3compat/commands.rst
new file mode 100644
index 000000000..27956e958
--- /dev/null
+++ b/docs/api/python/z3compat/commands.rst
@@ -0,0 +1,2 @@
+Commands
+============
diff --git a/docs/api/python/z3compat/dt.rst b/docs/api/python/z3compat/dt.rst
new file mode 100644
index 000000000..82fb2c7fe
--- /dev/null
+++ b/docs/api/python/z3compat/dt.rst
@@ -0,0 +1,2 @@
+Datatypes
+============
diff --git a/docs/api/python/z3compat/fp.rst b/docs/api/python/z3compat/fp.rst
new file mode 100644
index 000000000..2306028c1
--- /dev/null
+++ b/docs/api/python/z3compat/fp.rst
@@ -0,0 +1,2 @@
+Floating Point
+============
diff --git a/docs/api/python/z3compat/internals.rst b/docs/api/python/z3compat/internals.rst
new file mode 100644
index 000000000..81a630965
--- /dev/null
+++ b/docs/api/python/z3compat/internals.rst
@@ -0,0 +1,9 @@
+Internals
+============
+
+
+Testers
+-------------------
+.. autofunction:: cvc5_z3py_compat.is_expr
+.. autofunction:: cvc5_z3py_compat.is_app
+.. autofunction:: cvc5_z3py_compat.is_app_of
diff --git a/docs/api/python/z3compat/quant.rst b/docs/api/python/z3compat/quant.rst
new file mode 100644
index 000000000..8f4a756c7
--- /dev/null
+++ b/docs/api/python/z3compat/quant.rst
@@ -0,0 +1,4 @@
+Quantifiers
+============
+
+.. autofunction:: cvc5_z3py_compat.is_var
diff --git a/docs/api/python/z3compat/quickstart.rst b/docs/api/python/z3compat/quickstart.rst
new file mode 100644
index 000000000..764b1573f
--- /dev/null
+++ b/docs/api/python/z3compat/quickstart.rst
@@ -0,0 +1,2 @@
+Quickstart
+==========
diff --git a/docs/api/python/z3compat/set.rst b/docs/api/python/z3compat/set.rst
new file mode 100644
index 000000000..52a853ce8
--- /dev/null
+++ b/docs/api/python/z3compat/set.rst
@@ -0,0 +1,2 @@
+Sets
+============
diff --git a/docs/api/python/z3compat/solver.rst b/docs/api/python/z3compat/solver.rst
new file mode 100644
index 000000000..871b78f45
--- /dev/null
+++ b/docs/api/python/z3compat/solver.rst
@@ -0,0 +1,2 @@
+Solvers
+============
diff --git a/docs/api/python/z3compat/z3compat.rst b/docs/api/python/z3compat/z3compat.rst
index a9db13d49..ad7c8524b 100644
--- a/docs/api/python/z3compat/z3compat.rst
+++ b/docs/api/python/z3compat/z3compat.rst
@@ -7,6 +7,21 @@ z3py compatibility API
 
         This documentation was built while python bindings were disabled. This part of the documentation is likely either empty or outdated. Please enable :code:`BUILD_BINDINGS_PYTHON` in :code:`cmake` and build the documentation again.
 
+.. toctree::
+    :maxdepth: 2
+
+    quickstart
+    boolean
+    bitvec
+    arith
+    array
+    set
+    solver
+    commands
+    fp
+    dt
+    quant
+    internals
 
 .. automodule:: cvc5_z3py_compat
    :members:
diff --git a/docs/conf.py.in b/docs/conf.py.in
index b8aacf129..47bccd1fd 100644
--- a/docs/conf.py.in
+++ b/docs/conf.py.in
@@ -69,7 +69,9 @@ exclude_patterns = ['_build', 'Thumbs.db', '.DS_Store']
 # a list of builtin themes.
 #
 html_theme = 'sphinx_rtd_theme'
-html_theme_options = {}
+html_theme_options = {
+    'navigation_depth': 5
+}
 html_static_path = ['${CMAKE_CURRENT_SOURCE_DIR}/_static/']
 html_css_files = ['custom.css']
 html_show_sourcelink = False