io.github.cvc5

Class SymbolManager

java.lang.Object

io.github.cvc5.SymbolManager

public class SymbolManager
extends Object

Field Summary

Fields

Modifier and Type	Field and Description
protected long	pointer

Constructor Summary

Constructors

Constructor and Description
SymbolManager(Solver solver) Deprecated. This function is deprecated and replaced by Solver(TermManager). It will be removed in a future release.
SymbolManager(TermManager tm) Create symbol manager instance.

Method Summary

Modifier and Type	Method and Description
void	deletePointer()
protected void	deletePointer(long 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()
long	getPointer()
boolean	isLogicSet()
String	toString()
protected String	toString(long pointer)

Methods inherited from class java.lang.Object

clone, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Field Detail

pointer

protected 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 by Solver(TermManager). It will be removed in a future release.

Create symbol manager instance.

Parameters:

solver - The associated solver.

Method Detail

toString

protected String toString(long pointer)

deletePointer

protected void deletePointer(long pointer)

equals

public boolean equals(Object s)

Overrides:

equals in class Object

isLogicSet

public boolean isLogicSet()

Returns:

True if the logic of this symbol manager has been set.

getLogic

public String getLogic()

Returns:

The logic used by this symbol manager.

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.

getPointer

public long getPointer()

deletePointer

public void deletePointer()

toString

public String toString()

Overrides:

toString in class Object