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 