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.

Note

The returned proofs are released together with the solver that created proof , or, if that solver has already been deleted, together with proof . To use them afterwards, keep a reference to them via cvc5_proof_copy() .

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

A proof is released together with the solver that created it (or, for a proof obtained via cvc5_proof_get_children() after that solver has been deleted, together with its parent proof). To use it afterwards, keep a reference to it via cvc5_proof_copy() .

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.