mirror of
https://github.com/AdaCore/cvc5.git
synced 2026-02-12 12:32:16 -08:00
ea5e75d04a
We decided we want to ship the pythonic API together with our base python API. This PR adds a new target cvc5_python_api that first builds the base python API and then copies the pythonic API over. Furthermore we now use the cvc5.pythonic module to generate the corresponding documentation.
53 lines
985 B
ReStructuredText
53 lines
985 B
ReStructuredText
Solvers & Results
|
|
===========================
|
|
|
|
Simple Solving
|
|
----------------
|
|
|
|
.. autofunction:: cvc5.pythonic.solve
|
|
.. autofunction:: cvc5.pythonic.solve_using
|
|
.. autofunction:: cvc5.pythonic.prove
|
|
|
|
|
|
The Solver Class
|
|
----------------
|
|
|
|
.. autofunction:: cvc5.pythonic.SolverFor
|
|
|
|
.. autofunction:: cvc5.pythonic.SimpleSolver
|
|
|
|
.. autoclass:: cvc5.pythonic.Solver
|
|
:members:
|
|
:special-members:
|
|
|
|
Results & Models
|
|
----------------
|
|
.. data:: cvc5.pythonic.unsat
|
|
|
|
An *UNSAT* result.
|
|
|
|
.. data:: cvc5.pythonic.sat
|
|
|
|
A *SAT* result.
|
|
|
|
.. data:: cvc5.pythonic.unknown
|
|
|
|
The satisfiability could not be determined.
|
|
|
|
.. autoclass:: cvc5.pythonic.CheckSatResult
|
|
:members:
|
|
:special-members:
|
|
|
|
.. autoclass:: cvc5.pythonic.ModelRef
|
|
:members:
|
|
:special-members:
|
|
|
|
Utilities
|
|
--------------
|
|
|
|
.. autofunction:: cvc5.pythonic.evaluate
|
|
.. autofunction:: cvc5.pythonic.simplify
|
|
.. autofunction:: cvc5.pythonic.substitute
|
|
.. autofunction:: cvc5.pythonic.Sum
|
|
.. autofunction:: cvc5.pythonic.Product
|