1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
|
Solvers & Results
===========================
Simple Solving
----------------
.. autofunction:: cvc5.pythonic.solve
.. autofunction:: cvc5.pythonic.solve_using
.. autofunction:: cvc5.pythonic.prove
.. autofunction:: cvc5.pythonic.is_tautology
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
|
