Package io.github.cvc5

Class Command

java.lang.Object
io.github.cvc5.Command
public class Command extends Object
Encapsulation of a command. Commands are constructed by the input parser and can be invoked on the solver and symbol manager.

  • Field Details

    • pointer

      protected long pointer
      The raw native pointer value.

  • Method Details

    • invoke

      public String invoke(Solver solver, SymbolManager symbolManager)
      Invoke the command on the solver and symbol manager sm and return any resulting output as a string.
      Parameters:
      solver - The solver to invoke the command on.
      symbolManager - The symbol manager to invoke the command on.
      Returns:
      The output of invoking the command.

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

    • getCommandName

      public String getCommandName()
      Get the name for this command, e.g. "assert".
      Returns:
      The name of this command.

    • isNull

      public boolean isNull()
      Determine if this command is null.
      Returns:
      True if this command is null.

    • 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