public abstract class TacletApp extends java.lang.Object implements RuleApp
complete
or sufficientlyComplete
are
used to determine if the information is complete or at least sufficient (can
be completed using meta variables) complete, so that is can be applied.Modifier and Type | Field and Description |
---|---|
protected ImmutableList<IfFormulaInstantiation> |
ifInstantiations
chosen instantiations for the if sequent formulas
|
protected SVInstantiations |
instantiations
contains the instantiations of the schema variables of the Taclet
|
protected boolean |
updateContextFixed
the update context given by the current instantiations must not be
changed
|
Modifier and Type | Method and Description |
---|---|
TacletApp |
addCheckedInstantiation(SchemaVariable sv,
ProgramElement pe,
Services services,
boolean interesting)
checks if the instantiation of
sv with pe is
possible. |
TacletApp |
addCheckedInstantiation(SchemaVariable sv,
Term term,
Services services,
boolean interesting)
creates a new Tacletapp where the SchemaVariable sv is instantiated with
the the given Term term.
|
TacletApp |
addInstantiation(SchemaVariable sv,
Name name,
Services services) |
abstract TacletApp |
addInstantiation(SchemaVariable sv,
java.lang.Object[] list,
boolean interesting,
Services services) |
abstract TacletApp |
addInstantiation(SchemaVariable sv,
ProgramElement pe,
boolean interesting,
Services services)
adds a new instantiation to this TacletApp.
|
abstract TacletApp |
addInstantiation(SchemaVariable sv,
Term term,
boolean interesting,
Services services)
adds a new instantiation to this TacletApp
|
abstract TacletApp |
addInstantiation(SVInstantiations svi,
Services services)
creates a new Taclet application containing all the instantiations given
by the SVInstantiations
|
boolean |
admissible(boolean interactive,
ImmutableList<RuleSet> ruleSets) |
protected static ImmutableSet<QuantifiableVariable> |
boundAtOccurrenceSet(TacletPrefix prefix,
SVInstantiations instantiations)
collects all bound variables above the occurrence of the schemavariable
whose prefix is given
|
protected static ImmutableSet<QuantifiableVariable> |
boundAtOccurrenceSet(TacletPrefix prefix,
SVInstantiations instantiations,
PosInOccurrence pos)
collects all bound variables above the occurrence of the schemavariable
whose prefix is given
|
protected ImmutableSet<SchemaVariable> |
calculateNonInstantiatedSV()
calculate needed SchemaVariables that have not been instantiated yet.
|
static boolean |
checkVarCondNotFreeIn(Taclet taclet,
SVInstantiations instantiations,
PosInOccurrence pos)
checks if the variable conditions of type 'x not free in y' are hold by
the found instantiations.
|
protected static ImmutableSet<QuantifiableVariable> |
collectBoundVarsAbove(PosInOccurrence pos)
collects all bound vars that are bound above the subterm described by the
given term position information
|
protected abstract ImmutableSet<QuantifiableVariable> |
contextVars(SchemaVariable sv) |
TacletApp |
createSkolemConstant(java.lang.String instantiation,
SchemaVariable sv,
boolean interesting,
Services services)
Create a new constant named "instantiation" and instantiate "sv" with.
|
TacletApp |
createSkolemConstant(java.lang.String instantiation,
SchemaVariable sv,
Sort sort,
boolean interesting,
Services services) |
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.
|
ImmutableList<Goal> |
execute(Goal goal,
Services services)
applies the specified rule at the specified position if all schema
variables have been instantiated
|
Namespace<Function> |
extendedFunctionNameSpace(Namespace<Function> func_ns)
create a new function namespace by adding all newly instantiated skolem
symbols to a new namespace.
|
Namespace<QuantifiableVariable> |
extendVarNamespaceForSV(Namespace<QuantifiableVariable> var_ns,
SchemaVariable sv)
creates a new variable namespace by adding names of the instantiations of
the schema variables in the context of the given schema variable and (if
the TacletApp's prefix has the context flag set) by adding names of the
logic variables of the context.
|
ImmutableList<TacletApp> |
findIfFormulaInstantiations(Sequent p_seq,
Services p_services)
Find all possible instantiations of the if sequent formulas within the
sequent "p_seq".
|
ProgramElement |
getProgramElement(java.lang.String instantiation,
SchemaVariable sv,
Services services) |
Sort |
getRealSort(SchemaVariable p_sv,
TermServices services) |
int |
hashCode() |
ImmutableList<IfFormulaInstantiation> |
ifFormulaInstantiations() |
boolean |
ifInstsComplete() |
protected static boolean |
ifInstsCorrectSize(Taclet p_taclet,
ImmutableList<IfFormulaInstantiation> p_list) |
SVInstantiations |
instantiations()
returns the instantiations for the application of the Taclet at the
specified position.
|
boolean |
isExecutable(TermServices services) |
boolean |
isInstantiationRequired(SchemaVariable sv)
returns true if the given
SchemaVariable must be explicitly instantiated
it does not check whether sv is already instantiated or not |
MatchConditions |
matchConditions() |
TacletApp |
prepareUserInstantiation(Services services)
checks if there are name conflicts (i.e.
|
void |
registerSkolemConstants(NamespaceSet nss) |
protected static SVInstantiations |
replaceInstantiation(Taclet taclet,
SVInstantiations insts,
SchemaVariable varSV,
Services services)
returns a new SVInstantiations that modifies the given SVInstantiations
insts at the bound SchemaVariable varSV to a new LogicVariable.
|
protected static SVInstantiations |
resolveCollisionVarSV(Taclet taclet,
SVInstantiations insts,
Services services)
resolves collisions between bound SchemaVariables in an SVInstantiation
|
Rule |
rule()
returns the rule the application information is collected for
|
protected abstract 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
|
TacletApp |
setIfFormulaInstantiations(ImmutableList<IfFormulaInstantiation> p_list,
Services p_services)
Creates a new Taclet application by matching the given formulas against
the formulas of the if sequent, adding SV instantiations, constraints and
metavariables as needed.
|
protected abstract TacletApp |
setInstantiation(SVInstantiations svi,
Services services)
creates a new Taclet application containing all the instantiations given
by the SVInstantiations and forget the old ones
|
abstract 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
|
PosTacletApp |
setPosInOccurrence(PosInOccurrence pos,
Services services)
returns a new PosTacletApp that is equal to this TacletApp except that
the position is set to the given PosInOccurrence.
|
Taclet |
taclet()
returns the taclet the application information is collected for
|
java.lang.String |
toString() |
TacletApp |
tryToInstantiate(Services services) |
TacletApp |
tryToInstantiateAsMuchAsPossible(Services services) |
ImmutableSet<SchemaVariable> |
uninstantiatedVars()
returns the variables that have not yet been instantiated and need to be
instantiated to apply the Taclet.
|
SchemaVariable |
varSVNameConflict()
returns the bound SchemaVariable that causes a name conflict (i.e.
|
clone, finalize, getClass, notify, notifyAll, wait, wait, wait
complete, posInOccurrence
protected final SVInstantiations instantiations
protected final ImmutableList<IfFormulaInstantiation> ifInstantiations
protected boolean updateContextFixed
protected static ImmutableSet<QuantifiableVariable> boundAtOccurrenceSet(TacletPrefix prefix, SVInstantiations instantiations)
prefix
- the TacletPrefix of the schemavariableinstantiations
- the SVInstantiations so that the find(if)-expression matchesprotected static ImmutableSet<QuantifiableVariable> boundAtOccurrenceSet(TacletPrefix prefix, SVInstantiations instantiations, PosInOccurrence pos)
prefix
- the TacletPrefix of the schemavariableinstantiations
- the SVInstantiations so that the find(if)-expression matchespos
- the posInOccurrence describing the position of the
schemavariablepublic Taclet taclet()
public Rule rule()
public SVInstantiations instantiations()
public MatchConditions matchConditions()
public ImmutableList<IfFormulaInstantiation> ifFormulaInstantiations()
protected static SVInstantiations resolveCollisionVarSV(Taclet taclet, SVInstantiations insts, Services services)
insts
- the original SVInstantiationsprotected static SVInstantiations replaceInstantiation(Taclet taclet, SVInstantiations insts, SchemaVariable varSV, Services services)
public ImmutableList<Goal> execute(Goal goal, Services services)
public boolean isExecutable(TermServices services)
protected ImmutableSet<SchemaVariable> calculateNonInstantiatedSV()
public TacletApp addCheckedInstantiation(SchemaVariable sv, Term term, Services services, boolean interesting)
sv
- the SchemaVariable to be instantiatedterm
- the Term the SchemaVariable is instantiated withservices
- the services objectinteresting
- whether instantiations for this schema variable should
be kept in the list of "interesting" instantiationspublic ImmutableSet<SchemaVariable> uninstantiatedVars()
public boolean isInstantiationRequired(SchemaVariable sv)
SchemaVariable
must be explicitly instantiated
it does not check whether sv is already instantiated or notsv
- the SchemaVariablepublic final TacletApp tryToInstantiateAsMuchAsPossible(Services services)
public final TacletApp tryToInstantiate(Services services)
public Sort getRealSort(SchemaVariable p_sv, TermServices services)
services
- the Services class allowing access to the type modelGenericSortException
- iff p_s is a generic sort which is not yet instantiatedpublic TacletApp createSkolemConstant(java.lang.String instantiation, SchemaVariable sv, boolean interesting, Services services)
services
- the Services class allowing access to the type modelpublic TacletApp createSkolemConstant(java.lang.String instantiation, SchemaVariable sv, Sort sort, boolean interesting, Services services)
public void registerSkolemConstants(NamespaceSet nss)
public abstract TacletApp addInstantiation(SchemaVariable sv, Term term, boolean interesting, Services services)
sv
- the SchemaVariable to be instantiatedterm
- the Term the SchemaVariable is instantiated withpublic abstract TacletApp addInstantiation(SchemaVariable sv, java.lang.Object[] list, boolean interesting, Services services)
public abstract TacletApp addInstantiation(SchemaVariable sv, ProgramElement pe, boolean interesting, Services services)
(sv, pe)
will
result in a valid taclet instantiation, you have to use
addCheckedInstantiation(SchemaVariable, ProgramElement, Services, boolean)
insteadsv
- 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
)(sv, pe)
public TacletApp addCheckedInstantiation(SchemaVariable sv, ProgramElement pe, Services services, boolean interesting)
sv
with pe
is
possible. If the resulting instantiation is valid a new taclet
application with an extended instantiation mapping is created and
returned. Otherwise an exception is thrown.sv
- the SchemaVariable to be instantiatedpe
- the ProgramElement the SV is instantiated withservices
- the Servicesinteresting
- 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
)(sv, pe)
, if the
instantiation results in a valid taclet application otherwise an
exception is thrownIllegalInstantiationException
- exception thrown if sv
cannot be instantiated
with pe
no matter if in general or due to side
conditions posed by this particular applicationpublic TacletApp addInstantiation(SchemaVariable sv, Name name, Services services)
public abstract TacletApp addInstantiation(SVInstantiations svi, Services services)
svi
- the SVInstantiations whose entries are the needed
instantiationsprotected abstract TacletApp setInstantiation(SVInstantiations svi, Services services)
svi
- the SVInstantiations whose entries are the needed
instantiationspublic abstract TacletApp setMatchConditions(MatchConditions mc, Services services)
protected abstract TacletApp setAllInstantiations(MatchConditions mc, ImmutableList<IfFormulaInstantiation> ifInstantiations, Services services)
public TacletApp setIfFormulaInstantiations(ImmutableList<IfFormulaInstantiation> p_list, Services p_services)
public ImmutableList<TacletApp> findIfFormulaInstantiations(Sequent p_seq, Services p_services)
public PosTacletApp setPosInOccurrence(PosInOccurrence pos, Services services)
CAUTION: If you call this method, consider to call
NoPosTacletApp.matchFind(PosInOccurrence, Services)
first (if
applicable) as otherwise the TacletApp may become invalid.
(This happened sometimes during interactive proofs).
pos
- the PosInOccurrence of the newl created PosTacletApppublic boolean ifInstsComplete()
public boolean equals(java.lang.Object o)
equals
in class java.lang.Object
public int hashCode()
hashCode
in class java.lang.Object
public java.lang.String toString()
toString
in class java.lang.Object
public TacletApp prepareUserInstantiation(Services services)
protected abstract ImmutableSet<QuantifiableVariable> contextVars(SchemaVariable sv)
public Namespace<QuantifiableVariable> extendVarNamespaceForSV(Namespace<QuantifiableVariable> var_ns, SchemaVariable sv)
sv
- the schema variable to be consideredvar_ns
- the old variable namespacepublic Namespace<Function> extendedFunctionNameSpace(Namespace<Function> func_ns)
func_ns
- the original function namespace, not null
public SchemaVariable varSVNameConflict()
protected static boolean ifInstsCorrectSize(Taclet p_taclet, ImmutableList<IfFormulaInstantiation> p_list)
public boolean admissible(boolean interactive, ImmutableList<RuleSet> ruleSets)
public ProgramElement getProgramElement(java.lang.String instantiation, SchemaVariable sv, Services services)
public static boolean checkVarCondNotFreeIn(Taclet taclet, SVInstantiations instantiations, PosInOccurrence pos)
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) expression matchespos
- the PosInOccurrence where the Taclet is appliedprotected static ImmutableSet<QuantifiableVariable> collectBoundVarsAbove(PosInOccurrence pos)
pos
- the PosInOccurrence describing a subterm in TermCopyright © 2003-2019 The KeY-Project.