de.uka.ilkd.key.rule.tacletbuilder

Class RewriteTacletGoalTemplate

java.lang.Object

de.uka.ilkd.key.rule.tacletbuilder.TacletGoalTemplate

de.uka.ilkd.key.rule.tacletbuilder.RewriteTacletGoalTemplate

public class RewriteTacletGoalTemplate
extends TacletGoalTemplate

this class inherits from TacletGoalTemplate. It is used if there is a replacewith in the ruleGoals that replaces a term by another term. For a sequent AntecSuccTacletGoalTemplate

Field Summary

Fields

Modifier and Type	Field and Description
private Term	replacewith term that replaces another one

Constructor Summary

Constructors

Constructor and Description
RewriteTacletGoalTemplate(Sequent addedSeq, ImmutableList<Taclet> addedRules, Term replacewith)
RewriteTacletGoalTemplate(Sequent addedSeq, ImmutableList<Taclet> addedRules, Term replacewith, ImmutableSet<SchemaVariable> pvs) creates new Goaldescription
RewriteTacletGoalTemplate(Term replacewith)

Method Summary

Modifier and Type	Method and Description
boolean	equals(java.lang.Object o)
ImmutableSet<QuantifiableVariable>	getBoundVariables() rertieves and returns all variables that are bound in the goal template
int	hashCode()
Term	replaceWith() a Taclet may replace a Term by another.
java.lang.Object	replaceWithExpressionAsObject() a Taclet may replace parts of sequent.
java.lang.String	toString() toString

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

addedProgVars, name, rules, sequent, setName

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Field Detail

replacewith

private Term replacewith

term that replaces another one

Constructor Detail

RewriteTacletGoalTemplate

public RewriteTacletGoalTemplate(Sequent addedSeq,
                                 ImmutableList<Taclet> addedRules,
                                 Term replacewith,
                                 ImmutableSet<SchemaVariable> pvs)

creates new Goaldescription

Parameters:

addedSeq - new Sequent to be added

addedRules - IList contains the new allowed rules at this branch

replacewith - the Term that replaces another one

pvs - the set of schema variables

RewriteTacletGoalTemplate

public RewriteTacletGoalTemplate(Sequent addedSeq,
                                 ImmutableList<Taclet> addedRules,
                                 Term replacewith)

RewriteTacletGoalTemplate

public RewriteTacletGoalTemplate(Term replacewith)

Method Detail

replaceWith

public Term replaceWith()

a Taclet may replace a Term by another. The new Term is returned.

Returns:

Term being paramter in the rule goal replacewith(Seq)

getBoundVariables

public ImmutableSet<QuantifiableVariable> getBoundVariables()

rertieves and returns all variables that are bound in the goal template

Overrides:

getBoundVariables in class TacletGoalTemplate

Returns:

all variables that occur bound in this goal template

replaceWithExpressionAsObject

public java.lang.Object replaceWithExpressionAsObject()

Description copied from class: TacletGoalTemplate

a Taclet may replace parts of sequent.

Overrides:

replaceWithExpressionAsObject in class TacletGoalTemplate

Returns:

Term being paramter in the rule goal replacewith(term)

equals

public boolean equals(java.lang.Object o)

Overrides:

equals in class TacletGoalTemplate

hashCode

public int hashCode()

Overrides:

hashCode in class TacletGoalTemplate

toString

public java.lang.String toString()

toString

Overrides:

toString in class TacletGoalTemplate