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
54
55
|
ProofRule and ProofRewriteRule
==============================
Enum class :cpp:enum:`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 class :cpp:enum:`ProofRewriteRule <cvc5::ProofRewriteRule>` pertains to
rewrites performed on terms. These identifiers are arguments of the proof rules
:cpp:enumerator:`THEORY_REWRITE <cvc5::ProofRule::THEORY_REWRITE>` and
:cpp:enumerator:`DSL_REWRITE <cvc5::ProofRule::DSL_REWRITE>`.
----
- enum class :cpp:enum:`cvc5::ProofRule`
- :cpp:func:`std::ostream& cvc5::operator<< (std::ostream& out, ProofRule pc)`
- :cpp:func:`std::string std::to_string(cvc5::ProofRule rule)`
- :cpp:struct:`std::hash\<cvc5::ProofRule>`
- enum class :cpp:enum:`cvc5::ProofRewriteRule`
- :cpp:func:`std::ostream& cvc5::operator<< (std::ostream& out, ProofRewriteRule pc)`
- :cpp:func:`std::string std::to_string(cvc5::ProofRewriteRule rule)`
- :cpp:struct:`std::hash\<cvc5::ProofRewriteRule>`
----
.. doxygenenum:: cvc5::ProofRule
:project: cvc5
.. doxygenfunction:: cvc5::operator<<(std::ostream& out, ProofRule pc)
:project: cvc5
.. doxygenfunction:: std::to_string(cvc5::ProofRule rule)
:project: cvc5
.. doxygenstruct:: std::hash< cvc5::ProofRule >
:project: std
:members:
:undoc-members:
----
.. doxygenenum:: cvc5::ProofRewriteRule
:project: cvc5
.. doxygenfunction:: cvc5::operator<<(std::ostream& out, ProofRewriteRule pc)
:project: cvc5
.. doxygenfunction:: std::to_string(cvc5::ProofRewriteRule rule)
:project: cvc5
.. doxygenstruct:: std::hash< cvc5::ProofRewriteRule >
:project: std
:members:
:undoc-members:
|
