Package io.github.cvc5

Class Result

java.lang.Object
io.github.cvc5.Result
public class Result extends Object
Encapsulation of a three-valued solver result, with explanations.

  • Field Summary

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

  • Constructor Summary

    Constructors
    Constructor
    Description
    Result()
    Null result

  • 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 r)
    Operator overloading for equality of two results.
    long
    getPointer()
    Return the raw native pointer.
    UnknownExplanation
    getUnknownExplanation()
    Get an explanation for an unknown query result.
    int
    hashCode()
    Get the hash value of a result.
    boolean
    isNull()
    Determine if Result is empty, i.e., a nullary Result, and not an actual result returned from a checkSat() (and friends) query.
    boolean
    isSat()
    Determine if query was a satisfiable checkSat() or checkSatAssuming() query.
    boolean
    isUnknown()
    Determine if query was a checkSat() or checkSatAssuming() query and cvc5 was not able to determine (un)satisfiability.
    boolean
    isUnsat()
    Determine if if query was an unsatisfiable checkSat() or checkSatAssuming() query.
    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

    • Result

      public Result()
      Null result

  • 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

    • isNull

      public boolean isNull()
      Determine if Result is empty, i.e., a nullary Result, and not an actual result returned from a checkSat() (and friends) query.
      Returns:
      True if Result is empty, i.e., a nullary Result, and not an actual result returned from a checkSat() (and friends) query.

    • isSat

      public boolean isSat()
      Determine if query was a satisfiable checkSat() or checkSatAssuming() query.
      Returns:
      True if query was a satisfiable checkSat() or checkSatAssuming() query.

    • isUnsat

      public boolean isUnsat()
      Determine if if query was an unsatisfiable checkSat() or checkSatAssuming() query.
      Returns:
      True if query was an unsatisfiable checkSat() or checkSatAssuming() query.

    • isUnknown

      public boolean isUnknown()
      Determine if query was a checkSat() or checkSatAssuming() query and cvc5 was not able to determine (un)satisfiability.
      Returns:
      True if query was a checkSat() or checkSatAssuming() query and cvc5 was not able to determine (un)satisfiability.

    • equals

      public boolean equals(Object r)
      Operator overloading for equality of two results.
      Overrides:
      equals in class Object
      Parameters:
      r - The result to compare to for equality.
      Returns:
      True if the results are equal.

    • getUnknownExplanation

      public UnknownExplanation getUnknownExplanation()
      Get an explanation for an unknown query result.
      Returns:
      The explanation.

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

    • hashCode

      public int hashCode()
      Get the hash value of a result.
      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