public class RewriteTacletBuilder<T extends RewriteTaclet> extends FindTacletBuilder<T>
TacletBuilder.TacletBuilderException
Modifier and Type | Field and Description |
---|---|
protected int |
applicationRestriction
encodes restrictions on the state where a rewrite taclet is applicable
If the value is equal to
RewriteTaclet.NONE no state restrictions are posed
RewriteTaclet.SAME_UPDATE_LEVEL then \assumes
must match on a formula within the same state as \find
rsp. |
protected boolean |
surviveSmbExec |
find
attrs, choices, goal2Choices, goals, ifseq, name, NONAME, ruleSets, taclet, tacletAnnotations, variableConditions, varsNew, varsNewDependingOn, varsNotFreeIn
Constructor and Description |
---|
RewriteTacletBuilder() |
Modifier and Type | Method and Description |
---|---|
void |
addGoalTerm(Term goalTerm) |
void |
addTacletGoalTemplate(TacletGoalTemplate goal)
adds a new goal descriptions to the goal descriptions of the Taclet.
|
T |
getRewriteTaclet()
builds and returns the RewriteTaclet that is specified by
former set... / add... methods.
|
T |
getTaclet()
builds and returns the Taclet that is specified by
former set... / add... methods.
|
RewriteTacletBuilder<T> |
setApplicationRestriction(int p_applicationRestriction) |
RewriteTacletBuilder<T> |
setFind(Term findTerm)
sets the find of the Taclet that is to build to the given
term.
|
void |
setSurviveSmbExec(boolean b) |
checkBoundInIfAndFind, getFind
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
protected int applicationRestriction
RewriteTaclet.NONE
no state restrictions are posedRewriteTaclet.SAME_UPDATE_LEVEL
then \assumes
must match on a formula within the same state as \find
rsp. \add
. For efficiency no modalities are allowed above
the \find
position RewriteTaclet.IN_SEQUENT_STATE
the \find
part is
only allowed to match on formulas which are evaluated in the same state as
the sequentprotected boolean surviveSmbExec
public RewriteTacletBuilder<T> setApplicationRestriction(int p_applicationRestriction)
public void setSurviveSmbExec(boolean b)
public RewriteTacletBuilder<T> setFind(Term findTerm)
public T getRewriteTaclet()
public void addTacletGoalTemplate(TacletGoalTemplate goal)
addTacletGoalTemplate
in class TacletBuilder<T extends RewriteTaclet>
public void addGoalTerm(Term goalTerm)
public T getTaclet()
getTaclet
in class TacletBuilder<T extends RewriteTaclet>