public abstract class SubtermGenerator extends java.lang.Object implements TermGenerator
RecSubTermFeature
, a term feature can be given
that determines when traversal should be stopped, i.e., when one should not
descend further into a term.Modifier and Type | Method and Description |
---|---|
protected Term |
getTermInst(RuleApp app,
PosInOccurrence pos,
Goal goal) |
static TermGenerator |
leftTraverse(ProjectionToTerm cTerm,
TermFeature cond)
Left-traverse the subterms of a term in depth-first order.
|
static TermGenerator |
rightTraverse(ProjectionToTerm cTerm,
TermFeature cond)
Right-traverse the subterms of a term in depth-first order.
|
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
generate
public static TermGenerator leftTraverse(ProjectionToTerm cTerm, TermFeature cond)
public static TermGenerator rightTraverse(ProjectionToTerm cTerm, TermFeature cond)
protected Term getTermInst(RuleApp app, PosInOccurrence pos, Goal goal)
Copyright © 2003-2019 The KeY-Project.