de.uka.ilkd.key.symbolic_execution.strategy

Class CutHeapObjectsFeature

java.lang.Object

de.uka.ilkd.key.strategy.feature.BinaryFeature

de.uka.ilkd.key.symbolic_execution.strategy.CutHeapObjectsFeature

All Implemented Interfaces:

Feature

public class CutHeapObjectsFeature
extends BinaryFeature

This BinaryFeature checks if a cut with an equality for an alias check should be done or not.

This means the cut is only applied if the cut formula is not an equality or if it is not a negated formula or if the (negated) equality is not contained as top term (SequentFormula) in the Sequent ignoring the order of the equality children.

Author:

Martin Hentschel

Field Summary

Fields inherited from class de.uka.ilkd.key.strategy.feature.BinaryFeature

TOP_COST, ZERO_COST

Constructor Summary

Constructors

Constructor and Description
CutHeapObjectsFeature()

Method Summary

Modifier and Type	Method and Description
protected boolean	filter(RuleApp app, PosInOccurrence pos, Goal goal) Compute whether the result of the feature is zero (true) or infinity (false)

Methods inherited from class de.uka.ilkd.key.strategy.feature.BinaryFeature

computeCost

Methods inherited from class java.lang.Object

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

Constructor Detail

CutHeapObjectsFeature

public CutHeapObjectsFeature()

Method Detail

filter

protected boolean filter(RuleApp app,
                         PosInOccurrence pos,
                         Goal goal)

Compute whether the result of the feature is zero (true) or infinity (false)

Specified by:

filter in class BinaryFeature

Parameters:

app - the RuleApp

pos - position where app is to be applied

goal - the goal on which app is to be applied

Returns:

true iff the the result of the feature is supposed to be zero.