de.uka.ilkd.key.strategy.termgenerator

Class SuperTermGenerator.SuperTermWithIndexGenerator

java.lang.Object

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

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

All Implemented Interfaces:

TermGenerator

Enclosing class:

SuperTermGenerator

abstract static class SuperTermGenerator.SuperTermWithIndexGenerator
extends SuperTermGenerator

Nested Class Summary

Nested classes/interfaces inherited from class de.uka.ilkd.key.strategy.termgenerator.SuperTermGenerator

SuperTermGenerator.SuperTermWithIndexGenerator, SuperTermGenerator.UpwardsIterator

Field Summary

Fields

Modifier and Type	Field and Description
private Operator	binFunc
private Services	services

Constructor Summary

Constructors

Modifier	Constructor and Description
protected	SuperTermWithIndexGenerator(TermFeature cond)

Method Summary

Modifier and Type	Method and Description
java.util.Iterator<Term>	generate(RuleApp app, PosInOccurrence pos, Goal goal)
protected Term	generateOneTerm(Term superterm, int child)

Methods inherited from class de.uka.ilkd.key.strategy.termgenerator.SuperTermGenerator

createIterator, upwards, upwardsWithIndex

Methods inherited from class java.lang.Object

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

Field Detail

services

private Services services

binFunc

private Operator binFunc

Constructor Detail

SuperTermWithIndexGenerator

protected SuperTermWithIndexGenerator(TermFeature cond)

Method Detail

generate

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

Specified by:

generate in interface TermGenerator

Overrides:

generate in class SuperTermGenerator

generateOneTerm

protected Term generateOneTerm(Term superterm,
                               int child)

Overrides:

generateOneTerm in class SuperTermGenerator