Package io.github.cvc5

Class SynthResult

java.lang.Object
io.github.cvc5.SynthResult
public class SynthResult extends Object
Encapsulation of a solver synth result. This is the return value of the API methods: - Solver.checkSynth() - Solver.checkSynthNext() which we call synthesis queries. This class indicates whether the synthesis query has a solution, has no solution, or is unknown.

  • Field Summary

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

  • Constructor Summary

    Constructors
    Constructor
    Description
    SynthResult()
    Null synthResult

  • Method Summary

    Modifier and Type
    Method
    Description
    void
    deletePointer()
    Free the native resource associated with this pointer.
    boolean
    equals(Object r)
    Operator overloading for equality of two synthesis results.
    long
    getPointer()
    Return the raw native pointer.
    int
    hashCode()
    Get the hash value of a synthesis result.
    boolean
    hasNoSolution()
    Determine if the synthesis query has no solution.
    boolean
    hasSolution()
    Determine if the synthesis query has a solution.
    boolean
    isNull()
    Determine if SynthResult is empty, i.e., a nullary SynthResult, and not an actual result returned from a synthesis query.
    boolean
    isUnknown()
    Determine if the result of the synthesis query could not be determined.
    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

    • SynthResult

      public SynthResult()
      Null synthResult

  • Method Details

    • equals

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

    • isNull

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

    • hasSolution

      public boolean hasSolution()
      Determine if the synthesis query has a solution.
      Returns:
      True if the synthesis query has a solution.

    • hasNoSolution

      public boolean hasNoSolution()
      Determine if the synthesis query has no solution.
      Returns:
      True if the synthesis query has no solution. In this case, it was determined there was no solution.

    • isUnknown

      public boolean isUnknown()
      Determine if the result of the synthesis query could not be determined.
      Returns:
      True if the result of the synthesis query could not be determined.

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