Package io.github.cvc5

Class Proof

java.lang.Object
io.github.cvc5.Proof
public class Proof extends Object
A cvc5 Proof.

  • Field Summary

    Fields
    Modifier and Type
    Field
    Description
    protected long
    pointer
    The raw native pointer value.

  • Constructor Summary

    Constructors
    Constructor
    Description
    Proof()
    Null proof

  • Method Summary

    Modifier and Type
    Method
    Description
    void
    deletePointer()
    Free the native resource associated with this pointer.
    protected void
    deletePointer(long pointer)
    Delete the native resource associated with the specified pointer.
    boolean
    equals(Object p)
    Referential equality operator.
    Term[]
    getArguments()
    Get the arguments of the root step of the proof as a vector of terms.
    Proof[]
    getChildren()
    Get the premises of the root step of the proof.
    long
    getPointer()
    Return the raw native pointer.
    Term
    getResult()
    Get the conclusion of the root step of the proof.
    ProofRewriteRule
    getRewriteRule()
    Get the proof rewrite rule used by the root step of the proof.
    ProofRule
    getRule()
    Get the proof rule used by the root step of the proof.
    int
    hashCode()
    Get the hash value of a proof.
    String
    toString()
    Return a string representation of the pointer.
    protected String
    toString(long pointer)
    Return a string representation of the specified native pointer.

    Methods inherited from class java.lang.Object

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

  • Field Details

    • pointer

      protected long pointer
      The raw native pointer value.

  • Constructor Details

    • Proof

      public Proof()
      Null proof

  • Method Details

    • deletePointer

      protected void deletePointer(long pointer)
      Delete the native resource associated with the specified pointer.

      Subclasses must implement this method to provide resource-specific cleanup logic.

      Parameters:
      pointer - the native pointer to delete

    • toString

      protected String toString(long pointer)
      Return a string representation of the specified native pointer.

      Subclasses must implement this method to convert the native pointer into a meaningful string.

      Parameters:
      pointer - the native pointer
      Returns:
      a string representation of the pointer

    • getRule

      public ProofRule getRule() throws CVC5ApiException
      Get the proof rule used by the root step of the proof.
      Returns:
      The proof rule used by the root step of the proof.
      Throws:
      CVC5ApiException - on error

    • getRewriteRule

      public ProofRewriteRule getRewriteRule() throws CVC5ApiException
      Get the proof rewrite rule used by the root step of the proof.
      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()
      Get the conclusion of the root step of the proof.
      Returns:
      The conclusion of the root step of the proof.

    • getChildren

      public Proof[] getChildren()
      Get the premises of the root step of the proof.
      Returns:
      The premises of the root step of the proof.

    • getArguments

      public Term[] getArguments()
      Get the arguments of the root step of the proof as a vector of terms.
      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(Object p)
      Referential equality operator.
      Overrides:
      equals in class 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 Object
      Returns:
      The hash value.

    • getPointer

      public long getPointer()
      Return the raw native pointer.
      Returns:
      the pointer value

    • deletePointer

      public void deletePointer()
      Free the native resource associated with this pointer.

      This method should be called to explicitly clean up the underlying native resource. It removes this instance from the Context, then invokes the subclass-defined deletePointer(long) method to perform the actual cleanup.

    • toString

      public String toString()
      Return a string representation of the pointer.
      Overrides:
      toString in class Object
      Returns:
      a string representation of the pointer