de.uka.ilkd.key.rule

Class UninstantiatedNoPosTacletApp

java.lang.Object

de.uka.ilkd.key.rule.TacletApp

de.uka.ilkd.key.rule.NoPosTacletApp

de.uka.ilkd.key.rule.UninstantiatedNoPosTacletApp

All Implemented Interfaces:

RuleApp

class UninstantiatedNoPosTacletApp
extends NoPosTacletApp

A subclass of NoPosTacletApp for the special case of a taclet app without any instantiations. The method setupMatchConditions is overwritten to avoid object creations.

Field Summary

Fields inherited from class de.uka.ilkd.key.rule.TacletApp

ifInstantiations, instantiations, updateContextFixed

Constructor Summary

Constructors

Constructor and Description
UninstantiatedNoPosTacletApp(Taclet taclet)

Method Summary

Modifier and Type	Method and Description
protected MatchConditions	setupMatchConditions(PosInOccurrence pos, TermServices services)

Methods inherited from class de.uka.ilkd.key.rule.NoPosTacletApp

addInstantiation, addInstantiation, addInstantiation, addInstantiation, checkVarCondNotFreeIn, complete, contextVars, createFixedNoPosTacletApp, createNoPosTacletApp, createNoPosTacletApp, createNoPosTacletApp, createNoPosTacletApp, matchFind, matchFind, posInOccurrence, setAllInstantiations, setInstantiation, setMatchConditions

Methods inherited from class de.uka.ilkd.key.rule.TacletApp

addCheckedInstantiation, addCheckedInstantiation, addInstantiation, admissible, boundAtOccurrenceSet, boundAtOccurrenceSet, calculateNonInstantiatedSV, checkVarCondNotFreeIn, collectBoundVarsAbove, createSkolemConstant, createSkolemConstant, equals, execute, extendedFunctionNameSpace, extendVarNamespaceForSV, findIfFormulaInstantiations, getProgramElement, getRealSort, hashCode, ifFormulaInstantiations, ifInstsComplete, ifInstsCorrectSize, instantiations, isExecutable, isInstantiationRequired, matchConditions, prepareUserInstantiation, registerSkolemConstants, replaceInstantiation, resolveCollisionVarSV, rule, setIfFormulaInstantiations, setPosInOccurrence, taclet, toString, tryToInstantiate, tryToInstantiateAsMuchAsPossible, uninstantiatedVars, varSVNameConflict

Methods inherited from class java.lang.Object

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

Constructor Detail

UninstantiatedNoPosTacletApp

UninstantiatedNoPosTacletApp(Taclet taclet)

Parameters:

taclet -

Method Detail

setupMatchConditions

protected MatchConditions setupMatchConditions(PosInOccurrence pos,
                                               TermServices services)

Overrides:

setupMatchConditions in class NoPosTacletApp