public class Services extends java.lang.Object implements TermServices
Modifier and Type | Class and Description |
---|---|
static interface |
Services.ITermProgramVariableCollectorFactory |
Constructor and Description |
---|
Services(Profile profile)
creates a new Services object with a new TypeConverter and a new
JavaInfo object with no information stored at none of these.
|
Modifier and Type | Method and Description |
---|---|
void |
addNameProposal(Name proposal) |
Services |
copy(boolean shareCaches)
creates a new services object containing a copy of the java info of
this object and a new TypeConverter (shallow copy)
The copy does not belong to a
Proof object and can hence be used for a new proof. |
Services |
copy(Profile profile,
boolean shareCaches)
|
Services |
copyPreservesLDTInformation()
creates a new service object with the same ldt information
as the actual one
|
Services |
copyProofSpecific(Proof p_proof,
boolean shareCaches) |
Lookup |
createLookup() |
ServiceCaches |
getCaches()
Returns the used
ServiceCaches . |
ConstantExpressionEvaluator |
getConstantExpressionEvaluator()
Returns the ConstantExpressionEvaluator associated with this Services object.
|
Counter |
getCounter(java.lang.String name) |
Services.ITermProgramVariableCollectorFactory |
getFactory() |
JavaInfo |
getJavaInfo()
Returns the JavaInfo associated with this Services object.
|
JavaModel |
getJavaModel()
returns the
JavaModel with all path information |
NameRecorder |
getNameRecorder() |
NamespaceSet |
getNamespaces()
returns the namespaces for functions, predicates etc.
|
Services |
getOverlay(NamespaceSet namespaces) |
Profile |
getProfile()
Returns the sued
Profile . |
Proof |
getProof()
Returns the proof to which this object belongs, or null if it does not
belong to any proof.
|
SpecificationRepository |
getSpecificationRepository() |
TermBuilder |
getTermBuilder()
Returns the
TermBuilder used to create Term s. |
TermBuilder |
getTermBuilder(boolean withCache)
Returns either the cache backed or raw
TermBuilder used to create Term s. |
TermFactory |
getTermFactory()
Returns the
TermFactory used to create Term s. |
TypeConverter |
getTypeConverter()
Returns the TypeConverter associated with this Services object.
|
VariableNamer |
getVariableNamer()
Returns the VariableNamer associated with this Services object.
|
void |
saveNameRecorder(Node n) |
void |
setFactory(Services.ITermProgramVariableCollectorFactory factory) |
void |
setJavaModel(JavaModel javaModel) |
void |
setNamespaces(NamespaceSet namespaces)
sets the namespaces of known predicates, functions, variables
|
void |
setProof(Proof p_proof)
Marks this services as proof specific
Please make sure that the
Services does not not yet belong to an existing proof
or that it is owned by a proof environment. |
Services |
shallowCopy()
Generate a copy of this object.
|
public Services(Profile profile)
public Services getOverlay(NamespaceSet namespaces)
public TypeConverter getTypeConverter()
public ConstantExpressionEvaluator getConstantExpressionEvaluator()
public JavaInfo getJavaInfo()
public NameRecorder getNameRecorder()
public void saveNameRecorder(Node n)
public void addNameProposal(Name proposal)
public SpecificationRepository getSpecificationRepository()
public VariableNamer getVariableNamer()
public Services copy(boolean shareCaches)
Proof
object and can hence be used for a new proof.shareCaches
- true
The created Services
will use the same ServiceCaches
like this instance; false
the created Services
will use a new empty ServiceCaches
instance.public Services copy(Profile profile, boolean shareCaches)
Services
in which the Profile
is replaced.
The copy does not belong to a Proof
object and can hence be used for a new proof.profile
- The new Profile
to use in the copy of this Services
.shareCaches
- true
The created Services
will use the same ServiceCaches
like this instance; false
the created Services
will use a new empty ServiceCaches
instance.public Services shallowCopy()
public Services copyPreservesLDTInformation()
public void setProof(Proof p_proof)
Services
does not not yet belong to an existing proof
or that it is owned by a proof environment. In both cases copy the InitConfig
via
InitConfig.deepCopy()
or one of the other copy methods first.p_proof
- the Proof to which this Services
instance belongspublic Counter getCounter(java.lang.String name)
public NamespaceSet getNamespaces()
getNamespaces
in interface TermServices
public void setNamespaces(NamespaceSet namespaces)
namespaces
- the NamespaceSet with the proof specific namespacespublic Proof getProof()
public ServiceCaches getCaches()
ServiceCaches
.ServiceCaches
.public TermBuilder getTermBuilder(boolean withCache)
TermBuilder
used to create Term
s.
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
versiongetTermBuilder
in interface TermServices
TermBuilder
used to create Term
s.public TermBuilder getTermBuilder()
TermBuilder
used to create Term
s.
Same as {@link #getTermBuilder(true).getTermBuilder
in interface TermServices
TermBuilder
used to create Term
s.public TermFactory getTermFactory()
TermFactory
used to create Term
s.getTermFactory
in interface TermServices
TermFactory
used to create Term
s.public Services.ITermProgramVariableCollectorFactory getFactory()
public void setFactory(Services.ITermProgramVariableCollectorFactory factory)
public JavaModel getJavaModel()
JavaModel
with all path informationJavaModel
on which this services is based onpublic void setJavaModel(JavaModel javaModel)
public Lookup createLookup()
Copyright © 2003-2019 The KeY-Project.