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

    • 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