de.uka.ilkd.key.strategy.termgenerator

Class SuperTermGenerator

java.lang.Object

de.uka.ilkd.key.strategy.termgenerator.SuperTermGenerator

All Implemented Interfaces:

TermGenerator

Direct Known Subclasses:

SuperTermGenerator.SuperTermWithIndexGenerator

public abstract class SuperTermGenerator
extends java.lang.Object
implements TermGenerator

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
(package private) static class	SuperTermGenerator.SuperTermWithIndexGenerator
(package private) class	SuperTermGenerator.UpwardsIterator

Field Summary

Fields

Modifier and Type	Field and Description
private TermFeature	cond

Constructor Summary

Constructors

Modifier	Constructor and Description
protected	SuperTermGenerator(TermFeature cond)

Method Summary

Modifier and Type	Method and Description
protected abstract java.util.Iterator<Term>	createIterator(PosInOccurrence focus)
java.util.Iterator<Term>	generate(RuleApp app, PosInOccurrence pos, Goal goal)
private boolean	generateFurther(Term t, Services services)
protected Term	generateOneTerm(Term superterm, int child)
static TermGenerator	upwards(TermFeature cond, Services services)
static TermGenerator	upwardsWithIndex(TermFeature cond, Services services)

Methods inherited from class java.lang.Object

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

Field Detail

cond

private final TermFeature cond

Constructor Detail

SuperTermGenerator

protected SuperTermGenerator(TermFeature cond)

Method Detail

upwards

public static TermGenerator upwards(TermFeature cond,
                                    Services services)

upwardsWithIndex

public static TermGenerator upwardsWithIndex(TermFeature cond,
                                             Services services)

generate

public java.util.Iterator<Term> generate(RuleApp app,
                                         PosInOccurrence pos,
                                         Goal goal)

Specified by:

generate in interface TermGenerator

createIterator

protected abstract java.util.Iterator<Term> createIterator(PosInOccurrence focus)

generateOneTerm

protected Term generateOneTerm(Term superterm,
                               int child)

generateFurther

private boolean generateFurther(Term t,
                                Services services)