de.uka.ilkd.key.strategy.feature

Class AbstractBetaFeature

java.lang.Object

de.uka.ilkd.key.strategy.feature.AbstractBetaFeature

All Implemented Interfaces:

Feature

Direct Known Subclasses:

ContainsQuantifierFeature, CountMaxDPathFeature, CountPosDPathFeature, LeftmostNegAtomFeature, PurePosDPathFeature, SimplifyBetaCandidateFeature

public abstract class AbstractBetaFeature
extends java.lang.Object
implements Feature

This abstract class contains some auxiliary methods for the selection of beta rules that are supposed to be applied. Used terminology is defined in Diss. by Martin Giese.

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
private static class	AbstractBetaFeature.MaxDPathHelper
private static class	AbstractBetaFeature.MaxPathHelper
private static class	AbstractBetaFeature.MaxPosPathHelper
static class	AbstractBetaFeature.TermInfo Informations about a term as cached within "betaCandidates"

Field Summary

Fields

Modifier and Type	Field and Description
private static AbstractBetaFeature.MaxDPathHelper	maxDPathHelper helper for computing maxDPath_* in TermInfo
private static AbstractBetaFeature.MaxPosPathHelper	maxPosPathHelper helper for computing maxPosPath_* in TermInfo

Constructor Summary

Constructors

Constructor and Description
AbstractBetaFeature()

Method Summary

Modifier and Type	Method and Description
static boolean	alwaysReplace(Term p_t)
private static AbstractBetaFeature.TermInfo.Candidate	candidateHelp(Term p_t, AbstractBetaFeature.TermInfo p_ti)
RuleAppCost	computeCost(RuleApp app, PosInOccurrence pos, Goal goal) Compute the cost of a RuleApp.
protected static boolean	containsNegAtom(Term p_t, boolean p_positive, ServiceCaches caches)
private static boolean	containsNegAtomHelp(Term p_t, boolean p_positive, ServiceCaches caches)
protected static boolean	containsQuantifier(Term p_t, ServiceCaches caches)
private static boolean	containsQuantifierHelp(Term p_t, ServiceCaches caches)
protected abstract RuleAppCost	doComputation(PosInOccurrence pos, Term findTerm, ServiceCaches caches)
protected static boolean	hasPurePosPath(Term p_t, boolean p_positive, ServiceCaches caches) p_t contains a d-path consisting only of positive literals (as a formula of the antecedent)
private static boolean	hasPurePosPathHelp(Term p_t, boolean p_positive, ServiceCaches caches) TODO: It would be nice to integrate this with the framework for computing maxPosPath/maxDPath, however different return types pose a problem.
protected static boolean	isBetaCandidate(Term p_t, boolean p_inAntec, ServiceCaches caches)
private static boolean	isBetaCandidateHelp(AbstractBetaFeature.TermInfo p_ti, boolean p_positive)
protected static int	maxDPath(Term p_t, boolean p_positive, ServiceCaches caches) The length (number of literals) of the maximum d-path of the given formula as a formula of the antecedent
private static int	maxDPathHelp(Term p_t, boolean p_positive)
protected static int	maxPosPath(Term p_t, boolean p_positive, ServiceCaches caches) The maximal number of positive literals occurring within a d-path of "p_t" as a formula of the antecedent
private static int	maxPosPathHelp(Term p_t, boolean p_positive)
private static AbstractBetaFeature.TermInfo	termInfo(Term p_t, ServiceCaches caches) Get the informations about a term

Methods inherited from class java.lang.Object

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

Field Detail

maxPosPathHelper

private static AbstractBetaFeature.MaxPosPathHelper maxPosPathHelper

helper for computing maxPosPath_* in TermInfo

maxDPathHelper

private static AbstractBetaFeature.MaxDPathHelper maxDPathHelper

helper for computing maxDPath_* in TermInfo

Constructor Detail

AbstractBetaFeature

public AbstractBetaFeature()

Method Detail

termInfo

private static AbstractBetaFeature.TermInfo termInfo(Term p_t,
                                                     ServiceCaches caches)

Get the informations about a term

Parameters:

caches - TODO

maxPosPathHelp

private static int maxPosPathHelp(Term p_t,
                                  boolean p_positive)

maxDPathHelp

private static int maxDPathHelp(Term p_t,
                                boolean p_positive)

hasPurePosPathHelp

private static boolean hasPurePosPathHelp(Term p_t,
                                          boolean p_positive,
                                          ServiceCaches caches)

TODO: It would be nice to integrate this with the framework for computing maxPosPath/maxDPath, however different return types pose a problem. Perhaps this could be solved using generics?

Parameters:

caches - TODO

containsNegAtomHelp

private static boolean containsNegAtomHelp(Term p_t,
                                           boolean p_positive,
                                           ServiceCaches caches)

containsQuantifierHelp

private static boolean containsQuantifierHelp(Term p_t,
                                              ServiceCaches caches)

candidateHelp

private static AbstractBetaFeature.TermInfo.Candidate candidateHelp(Term p_t,
                                                                    AbstractBetaFeature.TermInfo p_ti)

isBetaCandidateHelp

private static boolean isBetaCandidateHelp(AbstractBetaFeature.TermInfo p_ti,
                                           boolean p_positive)

hasPurePosPath

protected static boolean hasPurePosPath(Term p_t,
                                        boolean p_positive,
                                        ServiceCaches caches)

p_t contains a d-path consisting only of positive literals (as a formula of the antecedent)

Parameters:

caches - TODO

maxPosPath

protected static int maxPosPath(Term p_t,
                                boolean p_positive,
                                ServiceCaches caches)

The maximal number of positive literals occurring within a d-path of "p_t" as a formula of the antecedent

Parameters:

caches - TODO

maxDPath

protected static int maxDPath(Term p_t,
                              boolean p_positive,
                              ServiceCaches caches)

The length (number of literals) of the maximum d-path of the given formula as a formula of the antecedent

Parameters:

caches - TODO

containsQuantifier

protected static boolean containsQuantifier(Term p_t,
                                            ServiceCaches caches)

Parameters:

caches - TODO

Returns:

true iff "p_t" contains a quantifier or a modality

containsNegAtom

protected static boolean containsNegAtom(Term p_t,
                                         boolean p_positive,
                                         ServiceCaches caches)

Parameters:

caches - TODO

Returns:

true iff the given formula contains a negated atom as a formula of the antecedent

alwaysReplace

public static boolean alwaysReplace(Term p_t)

Returns:

true iff the sign of "p_t" is not relevant (quantifiers etc. could be positive or negative)

isBetaCandidate

protected static boolean isBetaCandidate(Term p_t,
                                         boolean p_inAntec,
                                         ServiceCaches caches)

Parameters:

caches - TODO

Returns:

true iff the formula p_t could be splitted using the beta rule

computeCost

public RuleAppCost computeCost(RuleApp app,
                               PosInOccurrence pos,
                               Goal goal)

Compute the cost of a RuleApp.

Specified by:

computeCost in interface Feature

Parameters:

app - the RuleApp

pos - position where app is to be applied

goal - the goal on which app is to be applied

Returns:

the cost of app

doComputation

protected abstract RuleAppCost doComputation(PosInOccurrence pos,
                                             Term findTerm,
                                             ServiceCaches caches)