public class PosTacletApp extends TacletApp
NoPosTacletApp
) is used to keep track of the (partial)
instantiation information.Modifier and Type | Field and Description |
---|---|
private PosInOccurrence |
pos
stores the information where the Taclet is to be applied.
|
ifInstantiations, instantiations, updateContextFixed
Modifier | Constructor and Description |
---|---|
private |
PosTacletApp(FindTaclet taclet,
PosInOccurrence pos)
creates a PosTacletApp for the given taclet
and a position information
|
private |
PosTacletApp(FindTaclet taclet,
SVInstantiations instantiations,
ImmutableList<IfFormulaInstantiation> ifInstantiations,
PosInOccurrence pos)
creates a PosTacletApp for the given taclet with some known instantiations
and a position information
|
Modifier and Type | Method and Description |
---|---|
TacletApp |
addInstantiation(SchemaVariable sv,
java.lang.Object[] list,
boolean interesting,
Services services) |
TacletApp |
addInstantiation(SchemaVariable sv,
ProgramElement pe,
boolean interesting,
Services services)
adds a new instantiation to this TacletApp
|
TacletApp |
addInstantiation(SchemaVariable sv,
Term term,
boolean interesting,
Services services)
adds a new instantiation to this TacletApp
|
TacletApp |
addInstantiation(SVInstantiations svi,
Services services)
creates a new Taclet application containing all the
instantiations given
by the SVInstantiations and the ones of this TacletApp
|
private static java.util.Iterator<SchemaVariable> |
allVariableSV(Taclet taclet) |
boolean |
complete()
returns true iff all necessary informations are collected, so
that the Taclet can be applied.
|
protected ImmutableSet<QuantifiableVariable> |
contextVars(SchemaVariable sv) |
static PosTacletApp |
createPosTacletApp(FindTaclet taclet,
MatchConditions matchCond,
PosInOccurrence pos,
Services services) |
static PosTacletApp |
createPosTacletApp(FindTaclet taclet,
SVInstantiations instantiations,
ImmutableList<IfFormulaInstantiation> ifInstantiations,
PosInOccurrence pos,
Services services) |
static PosTacletApp |
createPosTacletApp(FindTaclet taclet,
SVInstantiations instantiations,
PosInOccurrence pos,
Services services)
creates a PosTacletApp for the given taclet with some known instantiations
and a position information
and CHECKS variable conditions as well as it resolves
collisions
The ifInstantiations parameter is not
matched against the if sequence, but only stored.
|
boolean |
equals(java.lang.Object o)
compares the given Object with this one and returns true iff both are
from type TacletApp with equal taclets, instantiations and positions.
|
int |
hashCode() |
PosInOccurrence |
posInOccurrence()
returns the PositionInOccurrence (representing a SequentFormula and
a position in the corresponding formula)
|
private static SVInstantiations |
resolveCollisionWithContext(Taclet taclet,
SVInstantiations insts,
PosInOccurrence pos,
Services services)
resolves collisions with the context
in an SVInstantiation
|
protected TacletApp |
setAllInstantiations(MatchConditions mc,
ImmutableList<IfFormulaInstantiation> ifInstantiations,
Services services)
creates a new Taclet application containing all the
instantiations, constraints, new metavariables and if formula
instantiations given and forget the old ones
|
protected TacletApp |
setInstantiation(SVInstantiations svi,
Services services)
creates a new Taclet application containing all the
instantiations given
by the SVInstantiations and forget the old ones.
|
TacletApp |
setMatchConditions(MatchConditions mc,
Services services)
creates a new Taclet application containing all the
instantiations, constraints and new metavariables given
by the mc object and forget the old ones
|
java.lang.String |
toString() |
private static ImmutableSet<QuantifiableVariable> |
varsBoundAboveFindPos(Taclet taclet,
PosInOccurrence pos)
returns the LogicVariables that are bound above the
PositionInOccurrence of the PosTacletApp.
|
addCheckedInstantiation, addCheckedInstantiation, addInstantiation, admissible, boundAtOccurrenceSet, boundAtOccurrenceSet, calculateNonInstantiatedSV, checkVarCondNotFreeIn, collectBoundVarsAbove, createSkolemConstant, createSkolemConstant, execute, extendedFunctionNameSpace, extendVarNamespaceForSV, findIfFormulaInstantiations, getProgramElement, getRealSort, ifFormulaInstantiations, ifInstsComplete, ifInstsCorrectSize, instantiations, isExecutable, isInstantiationRequired, matchConditions, prepareUserInstantiation, registerSkolemConstants, replaceInstantiation, resolveCollisionVarSV, rule, setIfFormulaInstantiations, setPosInOccurrence, taclet, tryToInstantiate, tryToInstantiateAsMuchAsPossible, uninstantiatedVars, varSVNameConflict
private final PosInOccurrence pos
private PosTacletApp(FindTaclet taclet, PosInOccurrence pos)
taclet
- the FindTacletpos
- the PosInOccurrence storing the position where to apply the
Tacletprivate PosTacletApp(FindTaclet taclet, SVInstantiations instantiations, ImmutableList<IfFormulaInstantiation> ifInstantiations, PosInOccurrence pos)
taclet
- the FindTacletinstantiations
- the SVInstantiationspos
- the PosInOccurrence storing the position where to apply the
Tacletpublic static PosTacletApp createPosTacletApp(FindTaclet taclet, SVInstantiations instantiations, PosInOccurrence pos, Services services)
taclet
- the FindTacletinstantiations
- the SVInstantiationspos
- the PosInOccurrence storing the position where to apply the
Tacletpublic static PosTacletApp createPosTacletApp(FindTaclet taclet, SVInstantiations instantiations, ImmutableList<IfFormulaInstantiation> ifInstantiations, PosInOccurrence pos, Services services)
public static PosTacletApp createPosTacletApp(FindTaclet taclet, MatchConditions matchCond, PosInOccurrence pos, Services services)
private static ImmutableSet<QuantifiableVariable> varsBoundAboveFindPos(Taclet taclet, PosInOccurrence pos)
private static java.util.Iterator<SchemaVariable> allVariableSV(Taclet taclet)
protected ImmutableSet<QuantifiableVariable> contextVars(SchemaVariable sv)
contextVars
in class TacletApp
private static SVInstantiations resolveCollisionWithContext(Taclet taclet, SVInstantiations insts, PosInOccurrence pos, Services services)
insts
- the original SVInstantiationspublic TacletApp addInstantiation(SchemaVariable sv, Term term, boolean interesting, Services services)
addInstantiation
in class TacletApp
sv
- the SchemaVariable to be instantiatedterm
- the Term the SchemaVariable is instantiated withpublic TacletApp addInstantiation(SchemaVariable sv, ProgramElement pe, boolean interesting, Services services)
addInstantiation
in class TacletApp
sv
- the SchemaVariable to be instantiatedpe
- the ProgramElement the SV is instantiated withinteresting
- a boolean marking if the instantiation of this sv needs to be
saved for later proof loading (interesting==true
)
or if it can be derived deterministically (e.g. by matching) (
interesting==false
)public TacletApp addInstantiation(SchemaVariable sv, java.lang.Object[] list, boolean interesting, Services services)
addInstantiation
in class TacletApp
public TacletApp addInstantiation(SVInstantiations svi, Services services)
addInstantiation
in class TacletApp
svi
- the SVInstantiations whose entries are the needed
instantiationsprotected TacletApp setInstantiation(SVInstantiations svi, Services services)
setInstantiation
in class TacletApp
svi
- the SVInstantiations whose entries are the needed
instantiationspublic TacletApp setMatchConditions(MatchConditions mc, Services services)
setMatchConditions
in class TacletApp
protected TacletApp setAllInstantiations(MatchConditions mc, ImmutableList<IfFormulaInstantiation> ifInstantiations, Services services)
setAllInstantiations
in class TacletApp
public boolean complete()
public PosInOccurrence posInOccurrence()
public boolean equals(java.lang.Object o)
TacletApp