Files

53 lines
985 B
ReStructuredText
Raw Permalink Normal View History

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