| java.lang.Object
 de.uka.ilkd.key.rule.TacletBuilder
de.uka.ilkd.key.rule.FindTacletBuilder
de.uka.ilkd.key.rule.AntecTacletBuilder
| AntecTacletBuilder | | public class AntecTacletBuilder extends FindTacletBuilder (Code) | | class builds Schematic Theory Specific Rules (Taclets) with find part
int antecedent.
|
| addTacletGoalTemplate | | public void addTacletGoalTemplate(TacletGoalTemplate goal)(Code) | | adds a new goal descriptions to the goal descriptions of the Taclet.
the TacletGoalTemplate must not be a RewriteTacletGoalTemplate,
otherwise an illegal argument exception is thrown.
|
| getAntecTaclet | | public AntecTaclet getAntecTaclet()(Code) | | builds and returns the AntecTaclet that is specified by
former set... / add... methods. If no name is specified then
a taclet with an empty string name is build. No specifications
for variable conditions, goals or heuristics imply that the
corresponding parts of the Taclet are empty. No specification for
the if-sequence is represented as a sequent with two empty
semisequences. No specification for the interactive or
recursive flags imply that the flags are not set.
No specified find part causes an IllegalStateException.
Throws an
TacletBuilderException if a bound SchemaVariable occurs more than once in if
and find or an InvalidPrefixException if the building of the Taclet
Prefix fails.
|
| getTaclet | | public Taclet getTaclet()(Code) | | builds and returns the Taclet that is specified by
former set... / add... methods. If no name is specified then
an Taclet with an empty string name is build. No specifications
for variable conditions, goals or heuristics imply that the
corresponding parts of the Taclet are empty. No specification for
the if-sequent is represented as a sequent with two empty
semisequents. No specification for the interactive or
recursive flags imply that the flags are not set.
No specified find part causes an IllegalStateException.
|
| setFind | | public AntecTacletBuilder setFind(Term findTerm)(Code) | | sets the find of the Taclet that is to build to the given
term, if the sort of the given term is of Sort.FORMULA otherwise
nothing happens.
this AntecTacletBuilder |
| Methods inherited from de.uka.ilkd.key.rule.TacletBuilder | public void addGoal2ChoicesMapping(TacletGoalTemplate gt, SetOfChoice soc)(Code)(Java Doc)
public void addOldName(String s)(Code)(Java Doc)
public void addRuleSet(RuleSet rs)(Code)(Java Doc)
abstract public void addTacletGoalTemplate(TacletGoalTemplate goal)(Code)(Java Doc)
public void addVariableCondition(VariableCondition vc)(Code)(Java Doc)
public void addVarsNew(SchemaVariable v, SchemaVariable asSort, boolean elementsort)(Code)(Java Doc)
public void addVarsNew(SchemaVariable v, SchemaVariable asSort)(Code)(Java Doc)
public void addVarsNew(SchemaVariable v, Sort sort)(Code)(Java Doc)
public void addVarsNew(NewVarcond nv)(Code)(Java Doc)
public void addVarsNew(ListOfNewVarcond list)(Code)(Java Doc)
public void addVarsNewDependingOn(SchemaVariable v0, SchemaVariable v1)(Code)(Java Doc)
public void addVarsNotFreeIn(SchemaVariable v0, SchemaVariable v1)(Code)(Java Doc)
public void addVarsNotFreeIn(ListOfNotFreeIn list)(Code)(Java Doc)
static void checkContainsFreeVarSV(Sequent seq, Name tacletName, String str)(Code)(Java Doc)
static void checkContainsFreeVarSV(Term t, Name tacletName, String str)(Code)(Java Doc)
public SetOfChoice getChoices()(Code)(Java Doc)
public HashMap getGoal2Choices()(Code)(Java Doc)
public Name getName()(Code)(Java Doc)
abstract public Taclet getTaclet()(Code)(Java Doc)
public Taclet getTacletWithoutInactiveGoalTemplates(SetOfChoice active)(Code)(Java Doc)
public ListOfTacletGoalTemplate goalTemplates()(Code)(Java Doc)
public Sequent ifSequent()(Code)(Java Doc)
public void setChoices(SetOfChoice choices)(Code)(Java Doc)
public void setConstraint(Constraint constraint)(Code)(Java Doc)
public void setDisplayName(String s)(Code)(Java Doc)
public void setHelpText(String s)(Code)(Java Doc)
public void setIfSequent(Sequent seq)(Code)(Java Doc)
public void setName(Name name)(Code)(Java Doc)
public void setNoninteractive(boolean ni)(Code)(Java Doc)
public void setRuleSets(ListOfRuleSet rs)(Code)(Java Doc)
public void setTacletGoalTemplates(ListOfTacletGoalTemplate g)(Code)(Java Doc)
public IteratorOfNotFreeIn varsNotFreeIn()(Code)(Java Doc)
|
|
|