Package io.github.cvc5

Class Proof

  • public class Proof
extends java.lang.Object
    A cvc5 Proof.

    • 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()

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