Proof
This class encapsulates a cvc5 proof object, which can be retrieved via
function
cvc5.Solver.getProof()
after a
cvc5.Solver.checkSat()
query returns an
unsat
result.
- class cvc5. Proof
-
A cvc5 proof. Proofs are trees and every proof object corresponds to the root step of a proof. The branches of the root step are the premises of the step.
Wrapper class for
cvc5::Proof.- getArguments ( )
-
- Returns :
-
The arguments of the root step of the proof as a vector of terms. Some of those terms might be strings.
- getChildren ( )
-
- Returns :
-
The premises of the root step of the proof.
- getResult ( )
-
- Returns :
-
The conclusion of the root step of the proof.
- getRewriteRule ( )
-
- Returns :
-
The proof rewrite rule used by the root step of the proof. Raises an exception if getRule() does not return DSL_REWRITE or THEORY_REWRITE .
- getRule ( )
-
- Returns :
-
The proof rule used by the root step of the proof.