io.github.cvc5

Class Proof

java.lang.Object

io.github.cvc5.Proof

public class Proof
extends java.lang.Object

A cvc5 Proof.

Field Summary

Fields

Modifier and Type	Field and Description
protected long	pointer

Constructor Summary

Constructors

Constructor and Description
Proof() Null proof

Method Summary

Modifier and Type	Method and Description
void	deletePointer()
protected void	deletePointer(long pointer)
boolean	equals(java.lang.Object p) Referential equality operator.
Term[]	getArguments()
Proof[]	getChildren()
long	getPointer()
Term	getResult()
ProofRewriteRule	getRewriteRule()
ProofRule	getRule()
int	hashCode() Get the hash value of a proof.

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, toString, wait, wait, wait

Field Detail

pointer

protected long pointer

Constructor Detail

Proof

public Proof()

Null proof

Method Detail

deletePointer

public void deletePointer()

deletePointer

protected void deletePointer(long pointer)

getPointer

public long getPointer()

getRule

public ProofRule getRule()
                  throws CVC5ApiException

Returns:

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

Throws:

CVC5ApiException - on error

getRewriteRule

public ProofRewriteRule getRewriteRule()
                                throws CVC5ApiException

Returns:

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

Throws:

CVC5ApiException - if `getRule()` does not return `DSL_REWRITE` or `THEORY_REWRITE`.

getResult

public Term getResult()

Returns:

The conclusion of the root step of the proof.

getChildren

public Proof[] getChildren()

Returns:

The premises of the root step of the proof.

getArguments

public Term[] getArguments()

Returns:

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

equals

public boolean equals(java.lang.Object p)

Referential equality operator.

Overrides:

equals in class java.lang.Object

Parameters:

p - The proof to compare to for equality.

Returns:

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

hashCode

public int hashCode()

Get the hash value of a proof.

Overrides:

hashCode in class java.lang.Object

Returns:

The hash value.