public class UserDefinedSymbols
extends java.lang.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 java.lang.String |
ruleHeader |
(package private) java.util.Set<Function> |
usedExtraFunctions |
(package private) java.util.Set<Function> |
usedExtraPredicates |
(package private) java.util.Set<Sort> |
usedExtraSorts |
(package private) java.util.Set<QuantifiableVariable> |
usedExtraVariables |
(package private) java.util.Set<Named> |
usedSchemaVariables |
Constructor and Description |
---|
UserDefinedSymbols(NamespaceSet referenceNamespaces,
ImmutableSet<Taclet> axioms) |
UserDefinedSymbols(UserDefinedSymbols parent) |
Modifier and Type | Method and Description |
---|---|
void |
addFunction(Function symbol) |
void |
addPredicate(Function symbol) |
void |
addSchemaVariable(SchemaVariable symbol) |
void |
addSort(Named symbol) |
private <T extends Named> |
addSymbolsToNamespace(Namespace<T> namespace,
java.util.Collection<T> symbols) |
void |
addSymbolsToNamespaces(NamespaceSet namespaces) |
private <T extends Named> |
addUserDefiniedSymbol(T symbol,
java.util.Set<T> set,
Namespace<T> excludeNamespace) |
void |
addVariable(QuantifiableVariable symbol) |
private <T extends Named> |
contains(T symbol,
java.util.Set<T> set) |
java.lang.String |
createHeader(Services services) |
private java.lang.StringBuffer |
createHeaderFor(Taclet taclet,
Services services) |
private void |
createHeaderForFunctions(java.lang.StringBuffer result) |
private void |
createHeaderForPredicates(java.lang.StringBuffer result) |
private void |
createHeaderForSchemaVariables(java.lang.StringBuffer result) |
private void |
createHeaderForSorts(java.lang.StringBuffer result) |
private java.lang.String |
createRuleHeader(Services services) |
private java.lang.String |
createSignature(Function op) |
private java.util.LinkedList<Named> |
ensureRightOrderOfSorts(java.util.LinkedList<Named> list) |
private void |
getAllSorts(java.util.LinkedList<Named> resultingSorts) |
java.util.Map<Name,Sort> |
getExtraSorts() |
java.lang.String |
getRuleHeader(Services services) |
void |
replaceGenericByProxySorts() |
java.lang.String |
toString() |
final UserDefinedSymbols parent
final java.util.Set<Function> usedExtraFunctions
final java.util.Set<Function> usedExtraPredicates
final java.util.Set<Sort> usedExtraSorts
final java.util.Set<QuantifiableVariable> usedExtraVariables
final java.util.Set<Named> usedSchemaVariables
final ImmutableSet<Taclet> axioms
private final NamespaceSet referenceNamespaces
private java.lang.String ruleHeader
public UserDefinedSymbols(NamespaceSet referenceNamespaces, ImmutableSet<Taclet> axioms)
public UserDefinedSymbols(UserDefinedSymbols parent)
private <T extends Named> void addUserDefiniedSymbol(T symbol, java.util.Set<T> set, Namespace<T> excludeNamespace)
private <T extends Named> boolean contains(T symbol, java.util.Set<T> set)
public void addFunction(Function symbol)
public void addPredicate(Function symbol)
public void addSort(Named symbol)
public void addVariable(QuantifiableVariable symbol)
public void addSchemaVariable(SchemaVariable symbol)
public void addSymbolsToNamespaces(NamespaceSet namespaces)
private <T extends Named> void addSymbolsToNamespace(Namespace<T> namespace, java.util.Collection<T> symbols)
public java.lang.String getRuleHeader(Services services)
private java.lang.String createRuleHeader(Services services)
public void replaceGenericByProxySorts()
public java.lang.String createHeader(Services services)
private java.util.LinkedList<Named> ensureRightOrderOfSorts(java.util.LinkedList<Named> list)
private void getAllSorts(java.util.LinkedList<Named> resultingSorts)
private void createHeaderForSorts(java.lang.StringBuffer result)
private void createHeaderForFunctions(java.lang.StringBuffer result)
private void createHeaderForPredicates(java.lang.StringBuffer result)
private void createHeaderForSchemaVariables(java.lang.StringBuffer result)
private java.lang.String createSignature(Function op)
public java.lang.String toString()
toString
in class java.lang.Object