Package io.github.cvc5

Class SymbolManager

java.lang.Object
io.github.cvc5.SymbolManager
public class SymbolManager extends Object
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
    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 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

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