de.uka.ilkd.key.logic

Interface TermServices

All Known Implementing Classes:

Services

public interface TermServices

This interface defines the basic functionalities of services required to construct Terms.

Author:

Richard Bubel

Method Summary

Modifier and Type	Method and Description
NamespaceSet	getNamespaces() returns the namespaces for functions, predicates etc.
TermBuilder	getTermBuilder() Returns the TermBuilder used to create Terms.
TermBuilder	getTermBuilder(boolean withCache) Returns either the cache backed or raw TermBuilder used to create Terms.
TermFactory	getTermFactory() Returns the TermBuilder used to create Terms.

Method Detail

getNamespaces

NamespaceSet getNamespaces()

returns the namespaces for functions, predicates etc.

Returns:

the proof specific namespaces

getTermBuilder

TermBuilder getTermBuilder()

Returns the TermBuilder used to create Terms.

Returns:

The TermBuilder used to create Terms.

getTermBuilder

TermBuilder getTermBuilder(boolean withCache)

Returns either the cache backed or raw TermBuilder used to create Terms. Usually the cache backed version is the intended one. The non-cached version is for use cases where a lot of intermediate terms are created of which most exist only for a very short time. To avoid polluting the cache it is then recommended to use the non-cache version

Returns:

The TermBuilder used to create Terms.

getTermFactory

TermFactory getTermFactory()

Returns the TermBuilder used to create Terms.

Returns:

The TermBuilder used to create Terms.