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.