de.uka.ilkd.key.strategy.feature.findprefix

Class AntecSuccPrefixChecker

java.lang.Object

de.uka.ilkd.key.strategy.feature.findprefix.AntecSuccPrefixChecker

All Implemented Interfaces:

Checker

class AntecSuccPrefixChecker
extends java.lang.Object
implements Checker

Checks, whether the position in occurrence has antecedent/succedent polarity.

Author:

christoph

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
private static class	AntecSuccPrefixChecker.Polarity

Field Summary

Fields

Modifier and Type	Field and Description
static AntecSuccPrefixChecker	ANTE_POLARITY_CHECKER
private AntecSuccPrefixChecker.Polarity	polarity
static AntecSuccPrefixChecker	SUCC_POLARITY_CHECKER

Constructor Summary

Constructors

Modifier	Constructor and Description
private	AntecSuccPrefixChecker(AntecSuccPrefixChecker.Polarity polarity)

Method Summary

Modifier and Type	Method and Description
boolean	check(PosInOccurrence pio) Called to get the result of the prefix check.
private int	checkOperator(Operator op, int child, int pol)

Methods inherited from class java.lang.Object

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

Field Detail

ANTE_POLARITY_CHECKER

public static final AntecSuccPrefixChecker ANTE_POLARITY_CHECKER

SUCC_POLARITY_CHECKER

public static final AntecSuccPrefixChecker SUCC_POLARITY_CHECKER

polarity

private AntecSuccPrefixChecker.Polarity polarity

Constructor Detail

AntecSuccPrefixChecker

private AntecSuccPrefixChecker(AntecSuccPrefixChecker.Polarity polarity)

Method Detail

checkOperator

private int checkOperator(Operator op,
                          int child,
                          int pol)

check

public boolean check(PosInOccurrence pio)

Description copied from interface: Checker

Called to get the result of the prefix check.

Specified by:

check in interface Checker

Parameters:

pio - the initial position of occurrence