public class UserDefinedSymbols extends Object
Modifier and Type | Class and Description |
---|---|
(package private) static class |
UserDefinedSymbols.NamedComparator |
Modifier and Type | Field and Description |
---|---|
(package private) ImmutableSet<Taclet> |
axioms |
(package private) UserDefinedSymbols |
parent |
private NamespaceSet |
referenceNamespaces |
private String |
ruleHeader |
(package private) Set<Named> |
usedExtraFunctions |
(package private) Set<Named> |
usedExtraPredicates |
(package private) Set<Named> |
usedExtraSorts |
(package private) Set<Named> |
usedExtraVariables |
(package private) Set<Named> |
usedSchemaVariables |
Constructor and Description |
---|
UserDefinedSymbols(NamespaceSet referenceNamespaces,
ImmutableSet<Taclet> axioms) |
UserDefinedSymbols(UserDefinedSymbols parent) |
final UserDefinedSymbols parent
final ImmutableSet<Taclet> axioms
private final NamespaceSet referenceNamespaces
private String ruleHeader
public UserDefinedSymbols(NamespaceSet referenceNamespaces, ImmutableSet<Taclet> axioms)
public UserDefinedSymbols(UserDefinedSymbols parent)
private void addUserDefiniedSymbol(Named symbol, Set<Named> set, Namespace excludeNamespace)
public void addFunction(Named symbol)
public void addPredicate(Named symbol)
public void addSort(Named symbol)
public void addVariable(Named symbol)
public void addSchemaVariable(Named symbol)
public void addSymbolsToNamespaces(NamespaceSet namespaces)
private void addSymbolsToNamespace(Namespace namespace, Collection<Named> symbols)
private StringBuffer createHeaderFor(Taclet taclet, Services services)
public void replaceGenericByProxySorts()
private LinkedList<Named> ensureRightOrderOfSorts(LinkedList<Named> list)
private void getAllSorts(LinkedList<Named> resultingSorts)
private void createHeaderForSorts(StringBuffer result)
private void createHeaderForFunctions(StringBuffer result)
private void createHeaderForPredicates(StringBuffer result)
private void createHeaderForSchemaVariables(StringBuffer result)