de.uka.ilkd.key.rule.tacletbuilder

Class AntecTacletBuilder

java.lang.Object

de.uka.ilkd.key.rule.tacletbuilder.TacletBuilder<T>

de.uka.ilkd.key.rule.tacletbuilder.FindTacletBuilder<AntecTaclet>

de.uka.ilkd.key.rule.tacletbuilder.AntecTacletBuilder

public class AntecTacletBuilder
extends FindTacletBuilder<AntecTaclet>

class builds Schematic Theory Specific Rules (Taclets) with find part int antecedent.

Nested Class Summary

Nested classes/interfaces inherited from class de.uka.ilkd.key.rule.tacletbuilder.TacletBuilder

TacletBuilder.TacletBuilderException

Field Summary

Fields

Modifier and Type	Field and Description
private boolean	ignoreTopLevelUpdates

Fields inherited from class de.uka.ilkd.key.rule.tacletbuilder.FindTacletBuilder

find

Fields inherited from class de.uka.ilkd.key.rule.tacletbuilder.TacletBuilder

attrs, choices, goal2Choices, goals, ifseq, name, NONAME, ruleSets, taclet, tacletAnnotations, variableConditions, varsNew, varsNewDependingOn, varsNotFreeIn

Constructor Summary

Constructors

Constructor and Description
AntecTacletBuilder()

Method Summary

Modifier and Type	Method and Description
void	addTacletGoalTemplate(TacletGoalTemplate goal) adds a new goal descriptions to the goal descriptions of the Taclet.
AntecTaclet	getAntecTaclet() builds and returns the AntecTaclet that is specified by former set... / add... methods.
AntecTaclet	getTaclet() builds and returns the Taclet that is specified by former set... / add... methods.
AntecTacletBuilder	setFind(Term findTerm) 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.
void	setIgnoreTopLevelUpdates(boolean ignore)

Methods inherited from class de.uka.ilkd.key.rule.tacletbuilder.FindTacletBuilder

checkBoundInIfAndFind, getFind

Methods inherited from class de.uka.ilkd.key.rule.tacletbuilder.TacletBuilder

addGoal2ChoicesMapping, addRuleSet, addVariableCondition, addVarsNew, addVarsNew, addVarsNew, addVarsNew, addVarsNewDependingOn, addVarsNotFreeIn, addVarsNotFreeIn, addVarsNotFreeIn, addVarsNotFreeIn, checkContainsFreeVarSV, checkContainsFreeVarSV, getChoices, getGoal2Choices, getName, getTacletWithoutInactiveGoalTemplates, goalTemplates, ifSequent, setAnnotations, setChoices, setDisplayName, setHelpText, setIfSequent, setName, setRuleSets, setTacletGoalTemplates, setTrigger, varsNotFreeIn

Methods inherited from class java.lang.Object

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

Field Detail

ignoreTopLevelUpdates

private boolean ignoreTopLevelUpdates

Constructor Detail

AntecTacletBuilder

public AntecTacletBuilder()

Method Detail

setFind

public AntecTacletBuilder setFind(Term findTerm)

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.

Returns:

this AntecTacletBuilder

addTacletGoalTemplate

public void addTacletGoalTemplate(TacletGoalTemplate goal)

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.

Specified by:

addTacletGoalTemplate in class TacletBuilder<AntecTaclet>

getTaclet

public AntecTaclet getTaclet()

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.

Specified by:

getTaclet in class TacletBuilder<AntecTaclet>

getAntecTaclet

public AntecTaclet getAntecTaclet()

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.

setIgnoreTopLevelUpdates

public void setIgnoreTopLevelUpdates(boolean ignore)