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.