de.uka.ilkd.key.strategy.termgenerator

Class SequentFormulasGenerator

java.lang.Object

de.uka.ilkd.key.strategy.termgenerator.SequentFormulasGenerator

All Implemented Interfaces:

TermGenerator

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

Term generator that enumerates the formulas of the current sequent/antecedent/succedent.

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
private static class	SequentFormulasGenerator.SFIterator

Constructor Summary

Constructors

Modifier	Constructor and Description
protected	SequentFormulasGenerator()

Method Summary

Modifier and Type	Method and Description
static SequentFormulasGenerator	antecedent()
java.util.Iterator<Term>	generate(RuleApp app, PosInOccurrence pos, Goal goal)
protected abstract java.util.Iterator<SequentFormula>	generateForIt(Goal goal)
static SequentFormulasGenerator	sequent()
static SequentFormulasGenerator	succedent()

Methods inherited from class java.lang.Object

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

Constructor Detail

SequentFormulasGenerator

protected SequentFormulasGenerator()

Method Detail

antecedent

public static SequentFormulasGenerator antecedent()

succedent

public static SequentFormulasGenerator succedent()

sequent

public static SequentFormulasGenerator sequent()

generateForIt

protected abstract java.util.Iterator<SequentFormula> generateForIt(Goal goal)

generate

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

Specified by:

generate in interface TermGenerator