Package io.github.cvc5
Class SymbolManager
- java.lang.Object
-
- io.github.cvc5.SymbolManager
-
public class SymbolManager extends java.lang.Object
-
-
Field Summary
Fields Modifier and Type Field Description protected long
pointer
-
Constructor Summary
Constructors Constructor Description SymbolManager(Solver solver)
Deprecated.This function is deprecated and replaced bySolver(TermManager)
.SymbolManager(TermManager tm)
Create symbol manager instance.
-
Method Summary
All Methods Instance Methods Concrete Methods Modifier and Type Method Description void
deletePointer()
protected void
deletePointer(long pointer)
boolean
equals(java.lang.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`.java.lang.String
getLogic()
java.util.Map<Term,java.lang.String>
getNamedTerms()
Get a mapping from terms to names that have been given to them via the :named attribute.long
getPointer()
boolean
isLogicSet()
java.lang.String
toString()
protected java.lang.String
toString(long pointer)
-
-
-
Constructor Detail
-
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 bySolver(TermManager)
. It will be removed in a future release.Create symbol manager instance.- Parameters:
solver
- The associated solver.
-
-
Method Detail
-
toString
protected java.lang.String toString(long pointer)
-
deletePointer
protected void deletePointer(long pointer)
-
equals
public boolean equals(java.lang.Object s)
- Overrides:
equals
in classjava.lang.Object
-
isLogicSet
public boolean isLogicSet()
- Returns:
- True if the logic of this symbol manager has been set.
-
getLogic
public java.lang.String getLogic()
- 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 java.util.Map<Term,java.lang.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()
-
deletePointer
public void deletePointer()
-
toString
public java.lang.String toString()
- Overrides:
toString
in classjava.lang.Object
-
-