public class MergeWithPredicateAbstraction extends MergeWithLatticeAbstraction
MergeProcedure.ValuesMergeResult
Modifier and Type | Field and Description |
---|---|
private static java.lang.String |
DISPLAY_NAME |
private java.lang.Class<? extends AbstractPredicateAbstractionLattice> |
latticeType
The concrete lattice type which determines how abstract elements are
generated from abstraction predicates.
|
private java.util.HashMap<Sort,java.util.ArrayList<AbstractionPredicate>> |
predicates
Mapping from sorts (e.g., int) to predicates (functions parametric in one
argument of the given sort).
|
private java.util.LinkedHashMap<ProgramVariable,AbstractDomainElement> |
userChoices
Manually chosen lattice elements for program variables.
|
Modifier | Constructor and Description |
---|---|
protected |
MergeWithPredicateAbstraction()
Default constructor for subclasses.
|
|
MergeWithPredicateAbstraction(java.lang.Iterable<AbstractionPredicate> predicates,
java.lang.Class<? extends AbstractPredicateAbstractionLattice> latticeType,
java.util.Map<ProgramVariable,AbstractDomainElement> userChoices)
Creates a new instance of
MergeWithPredicateAbstraction . |
Modifier and Type | Method and Description |
---|---|
void |
addPredicate(AbstractionPredicate predicate)
Adds a new predicate to the set of abstraction predicates.
|
void |
addPredicates(java.lang.Iterable<AbstractionPredicate> predicates)
Adds a new predicate to the set of abstraction predicates.
|
boolean |
complete()
Similar to
AbstractBuiltInRuleApp.complete() . |
AbstractDomainLattice |
getAbstractDomainForSort(Sort s,
Services services)
Returns the abstract domain lattice for the given sort or null if there
has no lattice been specified for that sort.
|
java.lang.Class<? extends AbstractPredicateAbstractionLattice> |
getLatticeType() |
java.util.HashMap<Sort,java.util.ArrayList<AbstractionPredicate>> |
getPredicates() |
java.util.LinkedHashMap<ProgramVariable,AbstractDomainElement> |
getUserChoices() |
static AbstractDomainLattice |
instantiateAbstractDomain(Sort s,
java.util.List<AbstractionPredicate> applicablePredicates,
java.lang.Class<? extends AbstractPredicateAbstractionLattice> latticeType,
Services services)
Instantiates the abstract domain lattice for the given sort or null if
there has no lattice been specified for that sort.
|
void |
setPredicates(java.util.HashMap<Sort,java.util.ArrayList<AbstractionPredicate>> predicates) |
java.lang.String |
toString() |
mergeValuesInStates, requiresDistinguishablePathConditions
getMergeProcedures, getProcedureByName
private static final java.lang.String DISPLAY_NAME
private java.util.HashMap<Sort,java.util.ArrayList<AbstractionPredicate>> predicates
private java.lang.Class<? extends AbstractPredicateAbstractionLattice> latticeType
private java.util.LinkedHashMap<ProgramVariable,AbstractDomainElement> userChoices
protected MergeWithPredicateAbstraction()
public MergeWithPredicateAbstraction(java.lang.Iterable<AbstractionPredicate> predicates, java.lang.Class<? extends AbstractPredicateAbstractionLattice> latticeType, java.util.Map<ProgramVariable,AbstractDomainElement> userChoices)
MergeWithPredicateAbstraction
. This
MergeProcedure
cannot be a Singleton since it depends on the given list of
predicates!predicates
- The predicates for the created lattices.latticeType
- The concrete lattice type which determines how abstract
elements are generated from abstraction predicates.public boolean complete()
MergeProcedure
AbstractBuiltInRuleApp.complete()
. Method was
introduced for predicate abstraction (which is not complete if the
abstraction predicates are not set).complete
in class MergeWithLatticeAbstraction
public AbstractDomainLattice getAbstractDomainForSort(Sort s, Services services)
MergeWithLatticeAbstraction
getAbstractDomainForSort
in class MergeWithLatticeAbstraction
s
- The sort to return the matching lattice for.services
- The services object.public static AbstractDomainLattice instantiateAbstractDomain(Sort s, java.util.List<AbstractionPredicate> applicablePredicates, java.lang.Class<? extends AbstractPredicateAbstractionLattice> latticeType, Services services)
s
- Sort
of for elements in the lattice.predicates
- AbstractionPredicate
s for all sorts.latticeType
- Type of AbstractPredicateAbstractionLattice
.services
- The Services
object.AbstractDomainLattice
.public java.util.HashMap<Sort,java.util.ArrayList<AbstractionPredicate>> getPredicates()
public void setPredicates(java.util.HashMap<Sort,java.util.ArrayList<AbstractionPredicate>> predicates)
predicates
- The abstraction predicates (map from program variables to
formula terms).public void addPredicate(AbstractionPredicate predicate)
predicate
- The predicate.public void addPredicates(java.lang.Iterable<AbstractionPredicate> predicates)
predicates
- The predicates to set.public java.lang.Class<? extends AbstractPredicateAbstractionLattice> getLatticeType()
AbstractPredicateAbstractionLattice
which determines how
abstract elements are constructed from abstraction predicates.public java.util.LinkedHashMap<ProgramVariable,AbstractDomainElement> getUserChoices()
getUserChoices
in class MergeWithLatticeAbstraction
public java.lang.String toString()
toString
in class java.lang.Object