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

• cvc5::Solver::proofToString()

• std::hash<cvc5::Term>

class 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.

Public Functions

Proof()

Nullary constructor. Needed for the Cython API.

~Proof()

bool isNull() const

Determine if this is the null proof (Proof::Proof()).

Returns:

True if this grammar is the null proof.

ProofRule getRule() const

Get the proof rule used by the root step of the proof.

Returns:

The proof rule.

ProofRewriteRule getRewriteRule() const

Get the proof rewrite rule used by the root step of the proof.

Requires that getRule() does not return #DSL_REWRITE or #THEORY_REWRITE.

Returns:

The proof rewrite rule.

Term getResult() const

Returns:

The conclusion of the root step of the proof.

const std::vector<Proof> getChildren() const

Returns:

The premises of the root step of the proof.

const std::vector<Term> getArguments() const

Returns:

The arguments of the root step of the proof as a vector of terms. Some of those terms might be strings.

bool operator==(const Proof &p) const

Operator overloading for referential equality of two proofs.

Parameters:

p – The proof to compare to for equality.

Returns:

True if both proofs point to the same internal proof object.

bool operator!=(const Proof &p) const

Referential disequality operator.

Parameters:

p – The proof to compare to for disequality.

Returns:

True if both proofs point to different internal proof objects.

Friends

friend struct std::hash< Proof >

template<>
struct hash<cvc5::Proof>

Hash function for proofs.

Public Functions

size_t operator()(const cvc5::Proof &p) const