Python Idomatic API: Document solver, results, utilities, and fns (#7882)

I put fns into "Core & Booleans".

diff --git a/docs/api/python/z3compat/boolean.rst b/docs/api/python/z3compat/boolean.rst
index 085ed157ff87468f4a51fc8b8c25dd3b08a1b67b..57ef4e69502d7dc0ee2a63c5f9c18804aef991ba 100644 (file)
--- a/docs/api/python/z3compat/boolean.rst
+++ b/docs/api/python/z3compat/boolean.rst
@@ -15,6 +15,8 @@ Basic Generic Term Builders
 .. autofunction:: cvc5_z3py_compat.Const
 .. autofunction:: cvc5_z3py_compat.Consts
 .. autofunction:: cvc5_z3py_compat.FreshConst
+.. autofunction:: cvc5_z3py_compat.Function
+.. autofunction:: cvc5_z3py_compat.FreshFunction
 
 Boolean Operators
 -----------------
@@ -53,6 +55,7 @@ Testers
 .. autofunction:: cvc5_z3py_compat.is_eq
 .. autofunction:: cvc5_z3py_compat.is_distinct
 .. autofunction:: cvc5_z3py_compat.is_const
+.. autofunction:: cvc5_z3py_compat.is_func_decl
 
 
 Classes (with overloads)
@@ -69,3 +72,6 @@ Classes (with overloads)
 .. autoclass:: cvc5_z3py_compat.BoolSortRef
    :members:
    :special-members:
+.. autoclass:: cvc5_z3py_compat.FuncDeclRef
+   :members:
+   :special-members:

diff --git a/docs/api/python/z3compat/commands.rst b/docs/api/python/z3compat/commands.rst
deleted file mode 100644 (file)
index 27956e9..0000000
--- a/docs/api/python/z3compat/commands.rst
+++ /dev/null
@@ -1,2 +0,0 @@
-Commands
-============

diff --git a/docs/api/python/z3compat/internals.rst b/docs/api/python/z3compat/internals.rst
index 81a630965e87a57d09c1c07ead3464ae4ac75a29..f555d3eb5f29595a2b17a0e13b18740dbc44f9d4 100644 (file)
--- a/docs/api/python/z3compat/internals.rst
+++ b/docs/api/python/z3compat/internals.rst
@@ -5,5 +5,13 @@ Internals
 Testers
 -------------------
 .. autofunction:: cvc5_z3py_compat.is_expr
+.. autofunction:: cvc5_z3py_compat.is_sort
 .. autofunction:: cvc5_z3py_compat.is_app
 .. autofunction:: cvc5_z3py_compat.is_app_of
+
+Exceptions
+-------------------
+
+.. autoclass:: cvc5_z3py_compat.SMTException
+   :members:
+   :special-members:

diff --git a/docs/api/python/z3compat/solver.rst b/docs/api/python/z3compat/solver.rst
index 871b78f4513cee8345ebd1f5cd38bf2015a5acdd..c268ec3ab81cda81ca0291f4c9a6ecc22eb9be6b 100644 (file)
--- a/docs/api/python/z3compat/solver.rst
+++ b/docs/api/python/z3compat/solver.rst
@@ -1,2 +1,52 @@
-Solvers
-============
+Solvers & Results
+===========================
+
+Simple Solving
+----------------
+
+.. autofunction:: cvc5_z3py_compat.solve
+.. autofunction:: cvc5_z3py_compat.solve_using
+.. autofunction:: cvc5_z3py_compat.prove
+
+
+The Solver Class
+----------------
+
+.. autofunction:: cvc5_z3py_compat.SolverFor
+
+.. autofunction:: cvc5_z3py_compat.SimpleSolver
+
+.. autoclass:: cvc5_z3py_compat.Solver
+  :members:
+  :special-members:
+
+Results & Models
+----------------
+.. data:: cvc5_z3py_compat.unsat
+
+  An *UNSAT* result.
+
+.. data:: cvc5_z3py_compat.sat
+
+  A *SAT* result.
+
+.. data:: cvc5_z3py_compat.unknown
+
+  The satisfiability could not be determined.
+
+.. autoclass:: cvc5_z3py_compat.CheckSatResult
+  :members:
+  :special-members:
+
+.. autoclass:: cvc5_z3py_compat.ModelRef
+  :members:
+  :special-members:
+
+Utilities
+--------------
+
+.. autofunction:: cvc5_z3py_compat.evaluate
+.. autofunction:: cvc5_z3py_compat.simplify
+.. autofunction:: cvc5_z3py_compat.substitute
+.. autofunction:: cvc5_z3py_compat.Sum
+.. autofunction:: cvc5_z3py_compat.Product

diff --git a/docs/api/python/z3compat/z3compat.rst b/docs/api/python/z3compat/z3compat.rst
index 33f2f98f14a2055820bf2bfbd8c7ee055b6ebdfe..bc2c9162e172a22a9612e734f6e841598842150a 100644 (file)
--- a/docs/api/python/z3compat/z3compat.rst
+++ b/docs/api/python/z3compat/z3compat.rst
@@ -20,5 +20,4 @@ z3py compatibility Python API
     set
     quant
     solver
-    commands
     internals