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

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 java.lang.String toString(long pointer)

deletePointer

protected void deletePointer(long pointer)

equals

public boolean equals(java.lang.Object s)

Overrides:

equals in class java.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 class java.lang.Object