From 0b287939efd35e0e98adbd704e61be864ffeb5aa Mon Sep 17 00:00:00 2001 From: Alex Ozdemir Date: Tue, 30 Nov 2021 13:06:30 -0800 Subject: [PATCH] Scaffold the idiomatic API's documentation (#7715) Scaffolding the documentation, and fleshing it out for the Boolean functions and terms. --- docs/api/python/z3compat/arith.rst | 2 + docs/api/python/z3compat/array.rst | 2 + docs/api/python/z3compat/bitvec.rst | 2 + docs/api/python/z3compat/boolean.rst | 70 +++++++++++++++++++++++++ docs/api/python/z3compat/commands.rst | 2 + docs/api/python/z3compat/dt.rst | 2 + docs/api/python/z3compat/fp.rst | 2 + docs/api/python/z3compat/internals.rst | 9 ++++ docs/api/python/z3compat/quant.rst | 4 ++ docs/api/python/z3compat/quickstart.rst | 2 + docs/api/python/z3compat/set.rst | 2 + docs/api/python/z3compat/solver.rst | 2 + docs/api/python/z3compat/z3compat.rst | 15 ++++++ docs/conf.py.in | 4 +- 14 files changed, 119 insertions(+), 1 deletion(-) create mode 100644 docs/api/python/z3compat/arith.rst create mode 100644 docs/api/python/z3compat/array.rst create mode 100644 docs/api/python/z3compat/bitvec.rst create mode 100644 docs/api/python/z3compat/boolean.rst create mode 100644 docs/api/python/z3compat/commands.rst create mode 100644 docs/api/python/z3compat/dt.rst create mode 100644 docs/api/python/z3compat/fp.rst create mode 100644 docs/api/python/z3compat/internals.rst create mode 100644 docs/api/python/z3compat/quant.rst create mode 100644 docs/api/python/z3compat/quickstart.rst create mode 100644 docs/api/python/z3compat/set.rst create mode 100644 docs/api/python/z3compat/solver.rst 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 -- 2.30.2