class UninstantiatedNoPosTacletApp extends NoPosTacletApp
NoPosTacletApp
for the special case of a
taclet app without any instantiations. The method
setupMatchConditions
is overwritten to avoid object
creations.ifInstantiations, instantiations, updateContextFixed
Constructor and Description |
---|
UninstantiatedNoPosTacletApp(Taclet taclet) |
Modifier and Type | Method and Description |
---|---|
protected MatchConditions |
setupMatchConditions(PosInOccurrence pos,
TermServices services) |
addInstantiation, addInstantiation, addInstantiation, addInstantiation, checkVarCondNotFreeIn, complete, contextVars, createFixedNoPosTacletApp, createNoPosTacletApp, createNoPosTacletApp, createNoPosTacletApp, createNoPosTacletApp, matchFind, matchFind, posInOccurrence, setAllInstantiations, setInstantiation, setMatchConditions
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
UninstantiatedNoPosTacletApp(Taclet taclet)
taclet
- protected MatchConditions setupMatchConditions(PosInOccurrence pos, TermServices services)
setupMatchConditions
in class NoPosTacletApp