From 5a3a6090c6e71de72f90b4e3e89af0eb9589b5d0 Mon Sep 17 00:00:00 2001
From: Alex Ozdemir <aozdemir@hmc.edu>
Date: Fri, 7 Jan 2022 12:42:28 -0800
Subject: [PATCH] Python Idomatic API: Document solver, results, utilities, and
 fns (#7882)

I put fns into "Core & Booleans".
---
 docs/api/python/z3compat/boolean.rst   |  6 +++
 docs/api/python/z3compat/commands.rst  |  2 -
 docs/api/python/z3compat/internals.rst |  8 ++++
 docs/api/python/z3compat/solver.rst    | 54 +++++++++++++++++++++++++-
 docs/api/python/z3compat/z3compat.rst  |  1 -
 5 files changed, 66 insertions(+), 5 deletions(-)
 delete mode 100644 docs/api/python/z3compat/commands.rst

diff --git a/docs/api/python/z3compat/boolean.rst b/docs/api/python/z3compat/boolean.rst
index 085ed157f..57ef4e695 100644
--- 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
index 27956e958..000000000
--- 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 81a630965..f555d3eb5 100644
--- 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 871b78f45..c268ec3ab 100644
--- 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 33f2f98f1..bc2c9162e 100644
--- 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
-- 
2.30.2