public class Services extends java.lang.Object implements TermServices
Modifier and Type | Class and Description |
---|---|
static interface |
Services.ITermProgramVariableCollectorFactory |
Modifier and Type | Field and Description |
---|---|
private ServiceCaches |
caches |
private ConstantExpressionEvaluator |
cee
used to determine whether an expression is a compile-time
constant and if so the type and result of the expression
|
private java.util.HashMap<java.lang.String,Counter> |
counters
map of names to counters
|
private Services.ITermProgramVariableCollectorFactory |
factory |
private VariableNamer |
innerVarNamer
variable namer for inner renaming
|
private JavaInfo |
javainfo
the information object on the Java model
|
private JavaModel |
javaModel |
private NameRecorder |
nameRecorder |
private NamespaceSet |
namespaces
proof specific namespaces (functions, predicates, sorts, variables)
|
private Profile |
profile |
private Proof |
proof
the proof
|
private SpecificationRepository |
specRepos
specification repository
|
private TermBuilder |
termBuilder |
private TermBuilder |
termBuilderWithoutCache |
private TypeConverter |
typeconverter
used to convert types, expressions and so on to logic elements
(in special into to terms or formulas)
|
Modifier | 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.
|
private |
Services(Profile profile,
KeYCrossReferenceServiceConfiguration crsc,
KeYRecoderMapping rec2key,
java.util.HashMap<java.lang.String,Counter> counters,
ServiceCaches caches) |
private |
Services(Services s) |
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)
|
private java.util.HashMap<java.lang.String,Counter> |
copyCounters()
|
Services |
copyPreservesLDTInformation()
creates a new service object with the same ldt information
as the actual one
|
Services |
copyProofSpecific(Proof p_proof,
boolean shareCaches) |
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. |
private void |
setTypeConverter(TypeConverter tc) |
Services |
shallowCopy()
Generate a copy of this object.
|
private Proof proof
private NamespaceSet namespaces
private ConstantExpressionEvaluator cee
private TypeConverter typeconverter
private final JavaInfo javainfo
private final VariableNamer innerVarNamer
private java.util.HashMap<java.lang.String,Counter> counters
private SpecificationRepository specRepos
private JavaModel javaModel
private NameRecorder nameRecorder
private Services.ITermProgramVariableCollectorFactory factory
private final Profile profile
private final ServiceCaches caches
private final TermBuilder termBuilder
private final TermBuilder termBuilderWithoutCache
public Services(Profile profile)
private Services(Profile profile, KeYCrossReferenceServiceConfiguration crsc, KeYRecoderMapping rec2key, java.util.HashMap<java.lang.String,Counter> counters, ServiceCaches caches)
private Services(Services s)
public Services getOverlay(NamespaceSet namespaces)
public TypeConverter getTypeConverter()
private void setTypeConverter(TypeConverter tc)
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()
private java.util.HashMap<java.lang.String,Counter> copyCounters()
counters
which means that a new
list is created with a copy of each contained Counter
.Counter
instances.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)