Package io.github.cvc5

Class Op

java.lang.Object
io.github.cvc5.Op
public class Op extends Object
A cvc5 operator. An operator is a term that represents certain operators, instantiated with its required parameters, e.g., a Term of kind Kind.BITVECTOR_EXTRACT.

  • Field Summary

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

  • Constructor Summary

    Constructors
    Constructor
    Description
    Op()
    Null op

  • 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 t)
    Syntactic equality operator.
    Term
    get(int i)
    Get the index at position i.
    Kind
    getKind()
    Get the kind of this operator.
    int
    getNumIndices()
    Get the number of indices of this op.
    long
    getPointer()
    Return the raw native pointer.
    int
    hashCode()
    Get the hash value of an operator.
    boolean
    isIndexed()
    Determine if this operator is indexed.
    boolean
    isNull()
    Determine if this operator is a null term.
    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

    • Op

      public Op()
      Null op

  • 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

    • equals

      public boolean equals(Object t)
      Syntactic equality operator.
      Overrides:
      equals in class Object
      Parameters:
      t - The operator to compare to for equality.
      Returns:
      True if the operators are syntactically identical.

    • getKind

      public Kind getKind()
      Get the kind of this operator.
      Returns:
      The kind of this operator.

    • isNull

      public boolean isNull()
      Determine if this operator is a null term.
      Returns:
      True if this operator is a null term.

    • isIndexed

      public boolean isIndexed()
      Determine if this operator is indexed.
      Returns:
      True iff this operator is indexed.

    • getNumIndices

      public int getNumIndices()
      Get the number of indices of this op.
      Returns:
      The number of indices of this op.

    • get

      public Term get(int i) throws CVC5ApiException
      Get the index at position i.
      Parameters:
      i - The position of the index to return.
      Returns:
      The index at position i.
      Throws:
      CVC5ApiException - on error

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

    • hashCode

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