public class NoPosTacletApp extends TacletApp
TacletIndex
manages no position taclet
application objects instead of the taclets itself.
ifInstantiations, instantiations, updateContextFixed
Modifier | Constructor and Description |
---|---|
protected |
NoPosTacletApp(Taclet taclet)
creates a NoPosTacletApp for the given taclet and no instantiation
information
|
private |
NoPosTacletApp(Taclet taclet,
SVInstantiations instantiations,
ImmutableList<IfFormulaInstantiation> ifInstantiations)
creates a NoPosTacletApp for the given taclet with some known instantiations
|
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 hold the old ones
|
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.
|
boolean |
complete()
returns true iff all necessary informations are collected, so
that the Taclet can be applied.
|
protected ImmutableSet<QuantifiableVariable> |
contextVars(SchemaVariable sv) |
static NoPosTacletApp |
createFixedNoPosTacletApp(Taclet taclet,
SVInstantiations instantiations,
Services services)
Create TacletApp with immutable "instantiations", i.e. this
instantiations must not be modified later (e.g. by
"addInstantiation").
|
static NoPosTacletApp |
createNoPosTacletApp(Taclet taclet)
creates a NoPosTacletApp for the given taclet and no instantiation
information and CHECKS variable conditions as well as it resolves
collisions
|
static NoPosTacletApp |
createNoPosTacletApp(Taclet taclet,
MatchConditions matchCond,
Services services) |
static NoPosTacletApp |
createNoPosTacletApp(Taclet taclet,
SVInstantiations instantiations,
ImmutableList<IfFormulaInstantiation> ifInstantiations,
Services services) |
static NoPosTacletApp |
createNoPosTacletApp(Taclet taclet,
SVInstantiations instantiations,
Services services)
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.
|
private NoPosTacletApp |
evalCheckRes(MatchConditions res,
Services services) |
NoPosTacletApp |
matchFind(PosInOccurrence pos,
Services services)
PRECONDITION: ifFormulaInstantiations () == null &&
( pos == null || termConstraint.isSatisfiable () )
|
NoPosTacletApp |
matchFind(PosInOccurrence pos,
Services services,
Term t) |
PosInOccurrence |
posInOccurrence()
returns the PositionInOccurrence (representing a SequentFormula and
a position in the corresponding formula)
|
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 ones in this TacletApp
|
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
|
protected MatchConditions |
setupMatchConditions(PosInOccurrence pos,
TermServices services) |
private boolean |
updateContextCompatible(MatchConditions p_mc) |
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
protected NoPosTacletApp(Taclet taclet)
taclet
- the Tacletprivate NoPosTacletApp(Taclet taclet, SVInstantiations instantiations, ImmutableList<IfFormulaInstantiation> ifInstantiations)
taclet
- the Tacletinstantiations
- the SVInstantiationspublic static NoPosTacletApp createNoPosTacletApp(Taclet taclet)
taclet
- the Tacletpublic static NoPosTacletApp createNoPosTacletApp(Taclet taclet, SVInstantiations instantiations, Services services)
taclet
- the Tacletinstantiations
- the SVInstantiationspublic static NoPosTacletApp createNoPosTacletApp(Taclet taclet, SVInstantiations instantiations, ImmutableList<IfFormulaInstantiation> ifInstantiations, Services services)
public static NoPosTacletApp createNoPosTacletApp(Taclet taclet, MatchConditions matchCond, Services services)
public static NoPosTacletApp createFixedNoPosTacletApp(Taclet taclet, SVInstantiations instantiations, Services services)
protected static boolean checkVarCondNotFreeIn(Taclet taclet, SVInstantiations instantiations)
taclet
- the Taclet that is tried to be instantiated. A match for the
find (or/and if) has been found.instantiations
- the SVInstantiations so that the find(if) matchespublic 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, java.lang.Object[] list, boolean interesting, Services services)
addInstantiation
in class TacletApp
public 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(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()
protected ImmutableSet<QuantifiableVariable> contextVars(SchemaVariable sv)
contextVars
in class TacletApp
public PosInOccurrence posInOccurrence()
public NoPosTacletApp matchFind(PosInOccurrence pos, Services services)
public NoPosTacletApp matchFind(PosInOccurrence pos, Services services, Term t)
private NoPosTacletApp evalCheckRes(MatchConditions res, Services services)
protected MatchConditions setupMatchConditions(PosInOccurrence pos, TermServices services)
private boolean updateContextCompatible(MatchConditions p_mc)