2024-07-16 16:07:30 -07:00
|
|
|
ProofRule and ProofRewriteRule
|
|
|
|
|
==============================
|
|
|
|
|
|
|
|
|
|
Enum :py:obj:`ProofRule <cvc5.ProofRule>` captures the reasoning steps
|
|
|
|
|
performed by the SAT solver, the theory solvers and the preprocessor. It
|
|
|
|
|
represents the inference rules used to derive conclusions within a proof.
|
|
|
|
|
|
|
|
|
|
Enum :py:obj:`ProofRewriteRule <cvc5.ProofRewriteRule>` pertains to
|
|
|
|
|
rewrites performed on terms. These identifiers are arguments of the proof rules
|
|
|
|
|
:py:obj:`THEORY_REWRITE <cvc5.ProofRule.THEORY_REWRITE>` and
|
|
|
|
|
:py:obj:`DSL_REWRITE <cvc5.ProofRule.DSL_REWRITE>`.
|
|
|
|
|
|
|
|
|
|
----
|
2023-09-26 19:58:03 -05:00
|
|
|
|
|
|
|
|
.. autoclass:: cvc5.ProofRule
|
|
|
|
|
:members:
|
|
|
|
|
:undoc-members:
|
2024-07-16 16:07:30 -07:00
|
|
|
|
2024-08-05 11:47:34 -07:00
|
|
|
----
|
|
|
|
|
|
2024-07-16 16:07:30 -07:00
|
|
|
.. autoclass:: cvc5.ProofRewriteRule
|
|
|
|
|
:members:
|
|
|
|
|
:undoc-members:
|
