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.- getAnnotationId ( )
-
Warning
This function is experimental and may change in future versions.
- Returns :
-
The annotation identifier used by the root step of the proof. Raises an exception if getRule() does not return ANNOTATE .
- getArgumentToString ( )
-
Get a string representation of an argument of the root step of the proof.
The string is computed by the internal proof printer, which takes into account how the argument is used by the proof rule. For example, an argument that encodes an identifier (e.g., of a theory or a rewrite rule) is converted to the name of that identifier. All other arguments are converted to the string representation of the corresponding term returned by
getArguments().Warning
This function is experimental and may change in future versions.
- Parameters :
-
i – The index of the argument.
- Returns :
-
The string representation of the argument.
- 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.