Package io.github.cvc5

Class Proof

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

  • Field Details

    • pointer

      protected long pointer
      The raw native pointer value.

  • Constructor Details

    • Proof

      public Proof()
      Null proof

  • Method Details

    • 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`.

    • getAnnotationId

      public AnnotationId getAnnotationId() throws CVC5ApiException
      Get the annotation identifier used by the root step of the proof.
      Returns:
      The annotation identifier used by the root step of the proof.
      Throws:
      CVC5ApiException - if `getRule()` does not return `ANNOTATE`.
      Note:
      This method is experimental and may change in future versions.

    • 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.

    • getArgumentToString

      public String getArgumentToString(int i) throws CVC5ApiException
      Get a string representation of an argument of the root step of the proof. The string is computed by the internal proof printer, which takes into account how the argument is used by the proof rule. For example, an argument that encodes an identifier (e.g., of a theory or a rewrite rule) is converted to the name of that identifier. All other arguments are converted to the string representation of the corresponding term returned by getArguments().
      Parameters:
      i - The index of the argument.
      Returns:
      The string representation of the argument.
      Throws:
      CVC5ApiException - on error
      Note:
      This method is experimental and may change in future versions.

    • 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.

      Every native call obtains the pointers of the objects it uses through this method, so that using an object after its native resource has been released raises an exception instead of crashing the JVM.

      Returns:
      the pointer value
      Throws:
      IllegalStateException - if the native resource of this object has been released, e.g., via deletePointer()

    • deletePointer

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

      Native resources are freed automatically once the Java object is no longer reachable. This method frees the native resource immediately instead; afterwards, using the object raises an IllegalStateException. It must be called from the thread that is using the associated term manager. Calling it more than once has no further effect.

    • toString

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