Cvc5Proof 

This struct encapsulates a cvc5 proof object, which can be retrieved via function cvc5_get_proof() after a cvc5_check_sat() query returns an unsat result.

typedef struct cvc5_proof_t * Cvc5Proof 

A cvc5 proof.

Cvc5ProofRule cvc5_proof_get_rule ( Cvc5Proof proof ) 

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

Returns :

The proof rule.

Cvc5ProofRewriteRule cvc5_proof_get_rewrite_rule ( Cvc5Proof proof ) 

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

Requires that cvc5_proof_get_rule() does not return CVC5_PROOF_RULE_DSL_REWRITE or CVC5_PROOF_RULE_THEORY_REWRITE .

Parameters :

proof – The proof.

Returns :

The proof rewrite rule.

Cvc5Term cvc5_proof_get_result ( Cvc5Proof proof ) 

Get the conclusion of the root step of a given proof.

Parameters :

proof – The proof.

Returns :

The conclusion term.

const Cvc5Proof * cvc5_proof_get_children ( Cvc5Proof proof , size_t * size ) 

Get the premises of the root step of a given proof.

Note

The returned Cvc5Proof array pointer is only valid until the next call to this function.

Parameters :

• proof – The proof.

• size – Output parameter to store the number of resulting premise proofs.

Returns :

The premise proofs.

const Cvc5Term * cvc5_proof_get_arguments ( Cvc5Proof proof , size_t * size ) 

Get the arguments of the root step of a given proof.

Parameters :

• proof – The proof.

• size – Output parameter to store the number of resulting argument terms.

Returns :

The argument terms.

bool cvc5_proof_is_equal ( Cvc5Proof a , Cvc5Proof b ) 

Compare two proofs for referential equality.

Parameters :

• a – The first proof.

• b – The second proof.

Returns :

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

bool cvc5_proof_is_disequal ( Cvc5Proof a , Cvc5Proof b ) 

Compare two proofs for referential disequality.

Parameters :

• a – The first proof.

• b – The second proof.

Returns :

True if both proof pointers point to different internal proof objects.

size_t cvc5_proof_hash ( Cvc5Proof proof ) 

Compute the hash value of a proof.

Parameters :

proof – The proof.

Returns :

The hash value of the proof.

Cvc5Proof cvc5_proof_copy ( Cvc5Proof proof ) 

Make copy of proof, increases reference counter of proof .

Note

This step is optional and allows users to manage resources in a more fine-grained manner.

Parameters :

proof – The proof to copy.

Returns :

The same proof with its reference count increased by one.

void cvc5_proof_release ( Cvc5Proof proof ) 

Release copy of proof, decrements reference counter of proof .

Note

This step is optional and allows users to release resources in a more fine-grained manner. Further, any API function that returns a copy that is owned by the callee of the function and thus, can be released.

Parameters :

proof – The proof to release.