Package io.github.cvc5

Class SymbolManager

java.lang.Object
io.github.cvc5.SymbolManager
All Implemented Interfaces:
AutoCloseable
public class SymbolManager extends Object implements AutoCloseable
Symbol manager. Internally, this class manages a symbol table and other meta-information pertaining to SMT2 file inputs (e.g. named assertions, declared functions, etc.). A symbol manager can be modified by invoking commands, see Command.invoke(Solver, SymbolManager). A symbol manager can be provided when constructing an InputParser, in which case that InputParser has symbols of this symbol manager preloaded. The symbol manager's interface is otherwise not publicly available.

  • Field Summary

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

  • Constructor Summary

    Constructors
    Constructor
    Description
    SymbolManager(Solver solver)
    Deprecated.
    This function is deprecated and replaced by Solver(TermManager).
    SymbolManager(TermManager tm)
    Create symbol manager instance.

  • Method Summary

    Modifier and Type
    Method
    Description
    void
    close()
    Free the native symbol manager, see deletePointer().
    void
    deletePointer()
    Free the native resource associated with this pointer.
    boolean
    equals(Object s)
     
    Sort[]
    getDeclaredSorts()
    Get the list of sorts that have been declared via `declare-sort` commands.
    Term[]
    getDeclaredTerms()
    Get the list of terms that have been declared via `declare-fun` and `declare-const`.
    String
    getLogic()
    Get the logic used by this symbol manager.
    Map<Term,String>
    getNamedTerms()
    Get a mapping from terms to names that have been given to them via the :named attribute.
    long
    getPointer()
    Return the raw native pointer.
    int
    hashCode()
    Return a hash code value for this symbol manager.
    boolean
    isLogicSet()
    Determine if the logic of this symbol manager has been set.
    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

    • SymbolManager

      public SymbolManager(TermManager tm)
      Create symbol manager instance.
      Parameters:
      tm - The associated term manager.

    • SymbolManager

      @Deprecated public SymbolManager(Solver solver)
      Deprecated.
      This function is deprecated and replaced by Solver(TermManager). It will be removed in a future release.
      Create symbol manager instance.
      Parameters:
      solver - The associated solver.

  • Method Details

    • 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 the pointer

    • close

      public void close()
      Free the native symbol manager, see deletePointer().
      Specified by:
      close in interface AutoCloseable

    • equals

      public boolean equals(Object s)
      Overrides:
      equals in class Object

    • hashCode

      public int hashCode()
      Return a hash code value for this symbol manager. The hash code is derived from the underlying native pointer, which is what equals(Object) compares, so that instances that are equal have the same hash code.
      Overrides:
      hashCode in class Object
      Returns:
      a hash code value for this symbol manager

    • isLogicSet

      public boolean isLogicSet()
      Determine if the logic of this symbol manager has been set.
      Returns:
      True if the logic of this symbol manager has been set.

    • getLogic

      public String getLogic()
      Get the logic used by this symbol manager.
      Returns:
      The logic used by this symbol manager.
      Note:
      Asserts isLogicSet().

    • getDeclaredSorts

      public Sort[] getDeclaredSorts()
      Get the list of sorts that have been declared via `declare-sort` commands. These are the sorts that are printed as part of a response to a `get-model` command.
      Returns:
      The declared sorts.

    • getDeclaredTerms

      public Term[] getDeclaredTerms()
      Get the list of terms that have been declared via `declare-fun` and `declare-const`. These are the terms that are printed in response to a `get-model` command.
      Returns:
      The declared terms.

    • getNamedTerms

      public Map<Term,String> getNamedTerms()
      Get a mapping from terms to names that have been given to them via the :named attribute.
      Returns:
      A map of the named terms to their names.

    • 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