| java.lang.Object
 de.uka.ilkd.key.rule.TacletApp
de.uka.ilkd.key.rule.NoPosTacletApp
All known Subclasses: de.uka.ilkd.key.rule.UninstantiatedNoPosTacletApp,
| NoPosTacletApp | | public class NoPosTacletApp extends TacletApp implements Contractable(Code) | | A no position taclet application has no position information yet. This can
have different reasons:
- the taclet application belongs to a no find taclet, this means it is
attached to a sequent and not to a formula or term.
- the taclet application has not been matched against a term or formula,
but may already contain instantiation information for some of its
schemavariables. This is the case, if the taclet of this application object
has been inserted by an addrule part of another taclet. For this reason
the
de.uka.ilkd.key.proof.TacletIndex manages no position taclet
application objects instead of the taclets itself.
|
| Method Summary | |
| public TacletApp | addInstantiation(SchemaVariable sv, Term term, boolean interesting)
| | public TacletApp | addInstantiation(SchemaVariable sv, Object[] list, boolean interesting)
| | public TacletApp | addInstantiation(SchemaVariable sv, ProgramElement pe, boolean interesting)
| | public TacletApp | addInstantiation(SVInstantiations svi)
| | protected static boolean | checkVarCondNotFreeIn(Taclet taclet, SVInstantiations instantiations)
checks if the variable conditions of type 'x not free in y' are
hold by the found instantiations. | | public boolean | complete()
returns true iff all necessary informations are collected, so
that the Taclet can be applied. | | protected SetOfQuantifiableVariable | contextVars(SchemaVariable sv)
| | public static NoPosTacletApp | createFixedNoPosTacletApp(Taclet taclet, SVInstantiations instantiations, Constraint constraint)
Create TacletApp with immutable "instantiations", i.e. | | public static NoPosTacletApp | createNoPosTacletApp(Taclet taclet)
| | public static NoPosTacletApp | createNoPosTacletApp(Taclet taclet, SVInstantiations instantiations)
creates a NoPosTacletApp for the given taclet with some known
instantiations and CHECKS variable conditions as well as it
resolves collisions
The ifInstantiations parameter is not
matched against the if sequence, but only stored. | | public static NoPosTacletApp | createNoPosTacletApp(Taclet taclet, SVInstantiations instantiations, Constraint matchConstraint, SetOfMetavariable matchNewMetavariables)
| | public static NoPosTacletApp | createNoPosTacletApp(Taclet taclet, SVInstantiations instantiations, Constraint matchConstraint, SetOfMetavariable matchNewMetavariables, ListOfIfFormulaInstantiation ifInstantiations)
| | public static NoPosTacletApp | createNoPosTacletApp(Taclet taclet, MatchConditions matchCond)
| | public boolean | equalContractable(Contractable c)
| | public boolean | equals(Object o)
| | public int | hashCode()
| | public NoPosTacletApp | matchFind(PosInOccurrence pos, Constraint termConstraint, Services services, Constraint userConstraint)
| | public NoPosTacletApp | matchFind(PosInOccurrence pos, Constraint termConstraint, Services services, Constraint userConstraint, Term t)
| | public PosInOccurrence | posInOccurrence()
| | protected TacletApp | setAllInstantiations(MatchConditions mc, ListOfIfFormulaInstantiation ifInstantiations)
| | protected TacletApp | setInstantiation(SVInstantiations svi)
| | protected TacletApp | setMatchConditions(MatchConditions mc)
| | protected MatchConditions | setupMatchConditions(PosInOccurrence pos, Services services, Constraint userConstraint)
| | public boolean | sufficientlyComplete()
|
| NoPosTacletApp | | protected NoPosTacletApp(Taclet taclet)(Code) | | creates a NoPosTacletApp for the given taclet and no instantiation
information
Parameters:
taclet - the Taclet |
| addInstantiation | | public TacletApp addInstantiation(SchemaVariable sv, Term term, boolean interesting)(Code) | | adds a new instantiation to this TacletApp
Parameters:
sv - the SchemaVariable to be instantiated
Parameters:
term - the Term the SchemaVariable is instantiated with the new TacletApp |
| addInstantiation | | public TacletApp addInstantiation(SchemaVariable sv, ProgramElement pe, boolean interesting)(Code) | | adds a new instantiation to this TacletApp
Parameters:
sv - the SchemaVariable to be instantiated
Parameters:
pe - the ProgramElement the SV is instantiated with the new TacletApp |
| addInstantiation | | public TacletApp addInstantiation(SVInstantiations svi)(Code) | | creates a new Taclet application containing all the
instantiations given
by the SVInstantiations and hold the old ones
Parameters:
svi - the SVInstantiations whose entries are the neededinstantiations the new Taclet application |
| checkVarCondNotFreeIn | | protected static boolean checkVarCondNotFreeIn(Taclet taclet, SVInstantiations instantiations)(Code) | | checks if the variable conditions of type 'x not free in y' are
hold by the found instantiations. The variable conditions is used
implicit in the prefix. (Used to calculate the prefix)
Parameters:
taclet - the Taclet that is tried to be instantiated. A match for thefind (or/and if) has been found.
Parameters:
instantiations - the SVInstantiations so that the find(if) matches true iff all variable conditions x not free in y are hold |
| complete | | public boolean complete()(Code) | | returns true iff all necessary informations are collected, so
that the Taclet can be applied.
true iff all necessary informations are collected, sothat the Taclet can be applied. |
| createFixedNoPosTacletApp | | public static NoPosTacletApp createFixedNoPosTacletApp(Taclet taclet, SVInstantiations instantiations, Constraint constraint)(Code) | | Create TacletApp with immutable "instantiations", i.e. this
instantiations must not be modified later (e.g. by
"addInstantiation"). However, this information is currently
only used to decide about introduction of
metavariables. Immutable instantiations are important for the
"addrules" part of taclets.
|
| createNoPosTacletApp | | public static NoPosTacletApp createNoPosTacletApp(Taclet taclet)(Code) | | creates a NoPosTacletApp for the given taclet and no instantiation
information and CHECKS variable conditions as well as it resolves
collisions
Parameters:
taclet - the Taclet |
| createNoPosTacletApp | | public static NoPosTacletApp createNoPosTacletApp(Taclet taclet, SVInstantiations instantiations)(Code) | | creates a NoPosTacletApp for the given taclet with some known
instantiations and CHECKS variable conditions as well as it
resolves collisions
The ifInstantiations parameter is not
matched against the if sequence, but only stored. For matching
use the method "setIfFormulaInstantiations".
Parameters:
taclet - the Taclet
Parameters:
instantiations - the SVInstantiations |
| hashCode | | public int hashCode()(Code) | | |
| posInOccurrence | | public PosInOccurrence posInOccurrence()(Code) | | returns the PositionInOccurrence (representing a ConstrainedFormula and
a position in the corresponding formula)
the PosInOccurrence |
| setAllInstantiations | | protected TacletApp setAllInstantiations(MatchConditions mc, ListOfIfFormulaInstantiation ifInstantiations)(Code) | | creates a new Taclet application containing all the
instantiations, constraints, new metavariables and if formula
instantiations given and forget the old ones
|
| setInstantiation | | protected TacletApp setInstantiation(SVInstantiations svi)(Code) | | creates a new Taclet application containing all the
instantiations given
by the SVInstantiations and forget the ones in this TacletApp
Parameters:
svi - the SVInstantiations whose entries are the neededinstantiations the new Taclet application |
| setMatchConditions | | protected TacletApp setMatchConditions(MatchConditions mc)(Code) | | creates a new Taclet application containing all the
instantiations, constraints and new metavariables given
by the mc object and forget the old ones
|
| sufficientlyComplete | | public boolean sufficientlyComplete()(Code) | | true iff the taclet instantiation can be made completeusing metavariables |
| Methods inherited from de.uka.ilkd.key.rule.TacletApp | public TacletApp addCheckedInstantiation(SchemaVariable sv, Term term, Services services, boolean interesting)(Code)(Java Doc)
public TacletApp addCheckedInstantiation(SchemaVariable sv, ProgramElement pe, Services services, boolean interesting)(Code)(Java Doc)
abstract public TacletApp addInstantiation(SchemaVariable sv, Term term, boolean interesting)(Code)(Java Doc)
abstract public TacletApp addInstantiation(SchemaVariable sv, Object[] list, boolean interesting)(Code)(Java Doc)
abstract public TacletApp addInstantiation(SchemaVariable sv, ProgramElement pe, boolean interesting)(Code)(Java Doc)
public TacletApp addInstantiation(SchemaVariable sv, Name name)(Code)(Java Doc)
abstract public TacletApp addInstantiation(SVInstantiations svi)(Code)(Java Doc)
public boolean admissible(boolean interactive, ListOfRuleSet ruleSets)(Code)(Java Doc)
protected static SetOfQuantifiableVariable boundAtOccurrenceSet(TacletPrefix prefix, SVInstantiations instantiations)(Code)(Java Doc)
protected static SetOfQuantifiableVariable boundAtOccurrenceSet(TacletPrefix prefix, SVInstantiations instantiations, PosInOccurrence pos)(Code)(Java Doc)
protected SetOfSchemaVariable calculateNeededNonInstantiatedSV()(Code)(Java Doc)
protected SetOfSchemaVariable calculateNonInstantiatedSV()(Code)(Java Doc)
protected boolean canUseMVAPosteriori(SchemaVariable p_var, Term p_term)(Code)(Java Doc)
public boolean canUseMVAPriori(SchemaVariable p_var)(Code)(Java Doc)
public static boolean checkVarCondNotFreeIn(Taclet taclet, SVInstantiations instantiations, PosInOccurrence pos)(Code)(Java Doc)
protected static SetOfQuantifiableVariable collectBoundVarsAbove(PosInOccurrence pos)(Code)(Java Doc)
abstract public boolean complete()(Code)(Java Doc)
public Constraint constraint()(Code)(Java Doc)
abstract protected SetOfQuantifiableVariable contextVars(SchemaVariable sv)(Code)(Java Doc)
public TacletApp createSkolemConstant(String instantiation, SchemaVariable sv, boolean interesting, Services services)(Code)(Java Doc)
public TacletApp createSkolemConstant(String instantiation, SchemaVariable sv, Sort sort, boolean interesting)(Code)(Java Doc)
public TacletApp createSkolemFunctions(Namespace p_func_ns, Services services)(Code)(Java Doc)
public boolean equals(Object o)(Code)(Java Doc)
public ListOfGoal execute(Goal goal, Services services)(Code)(Java Doc)
public Namespace extendVarNamespaceForSV(Namespace var_ns, SchemaVariable sv)(Code)(Java Doc)
public ListOfTacletApp findIfFormulaInstantiations(Sequent p_seq, Services p_services, Constraint p_userConstraint)(Code)(Java Doc)
public Sort getRealSort(SchemaVariable p_sv, Services services)(Code)(Java Doc)
public int hashCode()(Code)(Java Doc)
public ListOfIfFormulaInstantiation ifFormulaInstantiations()(Code)(Java Doc)
public boolean ifInstsComplete()(Code)(Java Doc)
protected static boolean ifInstsCorrectSize(Taclet p_taclet, ListOfIfFormulaInstantiation p_list)(Code)(Java Doc)
public TacletApp instantiateWithMV(Goal p_goal)(Code)(Java Doc)
public SVInstantiations instantiations()(Code)(Java Doc)
public boolean instsSufficientlyComplete()(Code)(Java Doc)
public boolean isDependingOnModifiesSV(SchemaVariable sv)(Code)(Java Doc)
public MatchConditions matchConditions()(Code)(Java Doc)
public SetOfSchemaVariable neededUninstantiatedVars()(Code)(Java Doc)
public SetOfMetavariable newMetavariables()(Code)(Java Doc)
abstract public PosInOccurrence posInOccurrence()(Code)(Java Doc)
public TacletApp prepareUserInstantiation()(Code)(Java Doc)
protected static SVInstantiations replaceInstantiation(Taclet taclet, SVInstantiations insts, SchemaVariable varSV)(Code)(Java Doc)
protected static SVInstantiations resolveCollisionVarSV(Taclet taclet, SVInstantiations insts)(Code)(Java Doc)
public Rule rule()(Code)(Java Doc)
abstract protected TacletApp setAllInstantiations(MatchConditions mc, ListOfIfFormulaInstantiation ifInstantiations)(Code)(Java Doc)
public TacletApp setIfFormulaInstantiations(ListOfIfFormulaInstantiation p_list, Services p_services, Constraint p_userConstraint)(Code)(Java Doc)
abstract protected TacletApp setInstantiation(SVInstantiations svi)(Code)(Java Doc)
abstract protected TacletApp setMatchConditions(MatchConditions mc)(Code)(Java Doc)
public PosTacletApp setPosInOccurrence(PosInOccurrence pos)(Code)(Java Doc)
abstract public boolean sufficientlyComplete()(Code)(Java Doc)
public Taclet taclet()(Code)(Java Doc)
public String toString()(Code)(Java Doc)
public TacletApp tryToInstantiate(Goal goal, Services services)(Code)(Java Doc)
public SetOfSchemaVariable uninstantiatedVars()(Code)(Java Doc)
public SchemaVariable varSVNameConflict()(Code)(Java Doc)
|
|
|