de.uka.ilkd.key.rule.merge.procedures

Class MergeWithPredicateAbstraction

java.lang.Object

de.uka.ilkd.key.rule.merge.MergeProcedure

de.uka.ilkd.key.rule.merge.procedures.MergeWithLatticeAbstraction

de.uka.ilkd.key.rule.merge.procedures.MergeWithPredicateAbstraction

All Implemented Interfaces:

ParametricMergeProcedure

Direct Known Subclasses:

MergeWithPredicateAbstractionFactory

public class MergeWithPredicateAbstraction
extends MergeWithLatticeAbstraction

Rule that merges two sequents based on a lattice of user-defined predicates. This procedure is no singleton since the set of predicates has to be defined for each merge application.

Author:

Dominic Scheurer

Nested Class Summary

Nested classes/interfaces inherited from class de.uka.ilkd.key.rule.merge.MergeProcedure

MergeProcedure.ValuesMergeResult

Field Summary

Fields

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.

Constructor Summary

Constructors

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.

Method Summary

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()

Methods inherited from class de.uka.ilkd.key.rule.merge.procedures.MergeWithLatticeAbstraction

mergeValuesInStates, requiresDistinguishablePathConditions

Methods inherited from class de.uka.ilkd.key.rule.merge.MergeProcedure

getMergeProcedures, getProcedureByName

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Field Detail

DISPLAY_NAME

private static final java.lang.String DISPLAY_NAME

See Also:

Constant Field Values

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).

latticeType

private java.lang.Class<? extends AbstractPredicateAbstractionLattice> latticeType

The concrete lattice type which determines how abstract elements are generated from abstraction predicates.

userChoices

private java.util.LinkedHashMap<ProgramVariable,AbstractDomainElement> userChoices

Manually chosen lattice elements for program variables.

Constructor Detail

MergeWithPredicateAbstraction

protected MergeWithPredicateAbstraction()

Default constructor for subclasses.

MergeWithPredicateAbstraction

public MergeWithPredicateAbstraction(java.lang.Iterable<AbstractionPredicate> predicates,
                                     java.lang.Class<? extends AbstractPredicateAbstractionLattice> latticeType,
                                     java.util.Map<ProgramVariable,AbstractDomainElement> userChoices)

Creates a new instance of MergeWithPredicateAbstraction. This MergeProcedure cannot be a Singleton since it depends on the given list of predicates!

Parameters:

predicates - The predicates for the created lattices.

latticeType - The concrete lattice type which determines how abstract elements are generated from abstraction predicates.

Method Detail

complete

public boolean complete()

Description copied from class: MergeProcedure

Similar to AbstractBuiltInRuleApp.complete(). Method was introduced for predicate abstraction (which is not complete if the abstraction predicates are not set).

Overrides:

complete in class MergeWithLatticeAbstraction

Returns:

true iff the merge procedure is complete (all neede parameters are set).

getAbstractDomainForSort

public AbstractDomainLattice getAbstractDomainForSort(Sort s,
                                                      Services services)

Description copied from class: MergeWithLatticeAbstraction

Returns the abstract domain lattice for the given sort or null if there has no lattice been specified for that sort.

Specified by:

getAbstractDomainForSort in class MergeWithLatticeAbstraction

Parameters:

s - The sort to return the matching lattice for.

services - The services object.

Returns:

The abstract domain lattice suitable for the given sort. Return null if there is no abstract domain for that sort; in this case, an if-then-else merge will be performed.

instantiateAbstractDomain

public 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.

Parameters:

s - Sort of for elements in the lattice.

predicates - AbstractionPredicates for all sorts.

latticeType - Type of AbstractPredicateAbstractionLattice.

services - The Services object.

Returns:

The corresponding AbstractDomainLattice.

getPredicates

public java.util.HashMap<Sort,java.util.ArrayList<AbstractionPredicate>> getPredicates()

Returns:

The predicates for the abstraction.

setPredicates

public void setPredicates(java.util.HashMap<Sort,java.util.ArrayList<AbstractionPredicate>> predicates)

Parameters:

predicates - The abstraction predicates (map from program variables to formula terms).

addPredicate

public void addPredicate(AbstractionPredicate predicate)

Adds a new predicate to the set of abstraction predicates.

Parameters:

predicate - The predicate.

addPredicates

public void addPredicates(java.lang.Iterable<AbstractionPredicate> predicates)

Adds a new predicate to the set of abstraction predicates.

Parameters:

predicates - The predicates to set.

getLatticeType

public java.lang.Class<? extends AbstractPredicateAbstractionLattice> getLatticeType()

Returns:

The type of lattice, that is a subclass of AbstractPredicateAbstractionLattice which determines how abstract elements are constructed from abstraction predicates.

getUserChoices

public java.util.LinkedHashMap<ProgramVariable,AbstractDomainElement> getUserChoices()

Specified by:

getUserChoices in class MergeWithLatticeAbstraction

Returns:

Manually chosen lattice elements for program variables.

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object