public class Model
extends java.lang.Object
Constructor and Description |
---|
Model()
creates an empty SMT model
|
Modifier and Type | Method and Description |
---|---|
void |
addAliases()
For all values it adds the names of the constants which have the same
values.
|
void |
addConstant(java.lang.String key,
java.lang.String value)
Adds a constant to the model.
|
void |
addHeap(Heap e)
Adds a heap to the model.
|
void |
addLocationSet(LocationSet e)
Adds a location set to the model.
|
void |
addSequence(Sequence s)
Adds a sequence set to the model.
|
ObjectVal |
findObject(java.lang.String ref)
finds the object the ref parameter is referring to
|
java.util.Map<java.lang.String,java.lang.String> |
getConstants()
returns map from constant names to constant values
|
java.util.List<Heap> |
getHeaps() |
java.util.List<LocationSet> |
getLocsets() |
java.util.Set<ObjectVal> |
getNecessaryPrestateObjects(java.lang.String location)
returns set of necessary prestate objects
|
ObjectVal |
getObject(java.lang.String name,
Heap heap)
returns the object of the given name found in the heap
|
java.util.Set<ObjectVal> |
getReachableObjects(java.lang.String name,
Heap heap)
returns all objects reachable from the specified one in the fiven heap
|
java.util.List<Sequence> |
getSequences() |
ProblemTypeInformation |
getTypes() |
boolean |
isEmpty()
returns true if the model is empty
|
java.util.Set<ObjectVal> |
pointsTo(java.lang.String name,
Heap heap)
set of objects the specified object points to
|
java.lang.String |
processAnyValue(java.lang.String val)
Transforms a binary value of an any to a human readable form: #sn, where
s is the first letter of the actual sort name and n is the decimal value
of corresponding to the any value after the removal of the three type
bits and the fill up bits.
|
void |
processArrayValues()
Transforms the values of array fields of objects from binary/hexidecimal
to human readable form.
|
void |
processConstantsAndFieldValues()
Transforms the values of constants and object fields from
binary/hexadecimal to a human readable from.
|
java.lang.String |
processConstantValue(java.lang.String val,
SMTSort s)
Transforms a constant value from binary/hexadecimal form to a human
redable form.
|
void |
processObjectNames()
Rewrite the object names from binary/hexadecimal to a human readable
form.
|
void |
processSequenceNames()
Rewrite the sequence names from binary/hexadecimal to a human readable
form.
|
void |
processSeqValues()
Transforms values of sequences from binary/hexadecimal to human readable
form
|
static java.lang.String |
removePipes(java.lang.String s)
removes the pipe character at the start and end from the given string
|
void |
removeUnnecessaryObjects()
cleans up maps from unused/unnecessary objects
|
void |
setEmpty(boolean empty)
marks the model as empty or full
|
void |
setTypes(ProblemTypeInformation types) |
java.lang.String |
toString()
returns a string representation of this SMT model
|
public boolean isEmpty()
public void setEmpty(boolean empty)
empty
- indicates model statuspublic java.util.Map<java.lang.String,java.lang.String> getConstants()
public void processObjectNames()
public void processSequenceNames()
public java.util.List<Heap> getHeaps()
public java.util.List<Sequence> getSequences()
public java.util.List<LocationSet> getLocsets()
public ProblemTypeInformation getTypes()
public void setTypes(ProblemTypeInformation types)
types
- the types to setpublic void addConstant(java.lang.String key, java.lang.String value)
key
- the constant namevalue
- the constant valuepublic void addHeap(Heap e)
e
- The heap to be addedpublic void addLocationSet(LocationSet e)
e
- The location set to be added.public void addSequence(Sequence s)
s
- The sequence to be added.public java.lang.String processConstantValue(java.lang.String val, SMTSort s)
val
- binary/hexadecimal value of constants
- sort of constantpublic java.lang.String processAnyValue(java.lang.String val)
val
- the original any value in binary/hexadecimalpublic void processArrayValues()
public void processSeqValues()
public void addAliases()
public java.util.Set<ObjectVal> getNecessaryPrestateObjects(java.lang.String location)
location
- public ObjectVal findObject(java.lang.String ref)
ref
- the reference to the objectpublic void removeUnnecessaryObjects()
public java.util.Set<ObjectVal> getReachableObjects(java.lang.String name, Heap heap)
name
- the name of the object from where to lookheap
- the heappublic java.util.Set<ObjectVal> pointsTo(java.lang.String name, Heap heap)
name
- the source objectheap
- the heappublic ObjectVal getObject(java.lang.String name, Heap heap)
name
- the object to look upheap
- the heappublic static java.lang.String removePipes(java.lang.String s)
s
- the String to processpublic void processConstantsAndFieldValues()
public java.lang.String toString()
toString
in class java.lang.Object
Copyright © 2003-2019 The KeY-Project.