de.uka.ilkd.key.strategy.feature

Class AbstractBetaFeature.TermInfo

java.lang.Object

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

Enclosing class:

AbstractBetaFeature

public static class AbstractBetaFeature.TermInfo
extends java.lang.Object

Informations about a term as cached within "betaCandidates"

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
(package private) static class	AbstractBetaFeature.TermInfo.Candidate

Field Summary

Fields

Modifier and Type	Field and Description
AbstractBetaFeature.TermInfo.Candidate	candidate one of CAND_*
boolean	containsNegAtom_negative formula contains a negative atom
boolean	containsNegAtom_positive formula contains a negative atom
boolean	containsQuantifier formula contains a quantifier or modality
int	maxDPath_negative
int	maxDPath_positive
int	maxPosPath_negative formula is negated
int	maxPosPath_positive formula is positive (not negated)
boolean	purePosPath_negative
boolean	purePosPath_positive

Constructor Summary

Constructors

Constructor and Description
TermInfo()

Method Summary

Methods inherited from class java.lang.Object

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

Field Detail

maxPosPath_positive

public int maxPosPath_positive

formula is positive (not negated)

purePosPath_positive

public boolean purePosPath_positive

maxDPath_positive

public int maxDPath_positive

containsNegAtom_positive

public boolean containsNegAtom_positive

formula contains a negative atom

maxPosPath_negative

public int maxPosPath_negative

formula is negated

purePosPath_negative

public boolean purePosPath_negative

maxDPath_negative

public int maxDPath_negative

containsNegAtom_negative

public boolean containsNegAtom_negative

formula contains a negative atom

containsQuantifier

public boolean containsQuantifier

formula contains a quantifier or modality

candidate

public AbstractBetaFeature.TermInfo.Candidate candidate

one of CAND_*

Constructor Detail

TermInfo

public TermInfo()