Package | Description |
---|---|
de.uka.ilkd.key.proof |
This package contains the core data structures of proofs, nodes, goals, as well
as machinery to deal with these data structures.
|
de.uka.ilkd.key.proof.delayedcut | |
de.uka.ilkd.key.proof.init |
This package contains classes handling prover initialisation.
|
de.uka.ilkd.key.rule |
This package contains classes for implementing rules.
|
de.uka.ilkd.key.strategy |
This package contains classes implementing the proof search strategies of KeY.
|
Modifier and Type | Field and Description |
---|---|
protected java.util.HashMap<java.lang.Object,ImmutableList<NoPosTacletApp>> |
TacletIndex.antecList
contains antecedent Taclets
|
protected ImmutableList<NoPosTacletApp> |
TacletIndex.noFindList
contains NoFind-Taclets
|
protected java.util.HashSet<NoPosTacletApp> |
TacletIndex.partialInstantiatedRuleApps
keeps track of no pos taclet apps with partial
instantiations
|
protected java.util.HashMap<java.lang.Object,ImmutableList<NoPosTacletApp>> |
TacletIndex.rwList
contains rewrite Taclets
|
protected java.util.HashMap<java.lang.Object,ImmutableList<NoPosTacletApp>> |
TacletIndex.succList
contains succedent Taclets
|
Modifier and Type | Method and Description |
---|---|
NoPosTacletApp |
TacletIndex.lookup(Name name)
returns a NoPosTacletApp whose Taclet has a name that equals the given
name.
|
NoPosTacletApp |
TacletIndex.lookup(java.lang.String name)
returns a NoPosTacletApp whose Taclet has a name that equals the given
name.
|
Modifier and Type | Method and Description |
---|---|
java.util.Set<NoPosTacletApp> |
TacletIndex.allNoPosTacletApps() |
static ImmutableList<NoPosTacletApp> |
TermTacletAppIndex.filter(RuleFilter p_filter,
ImmutableList<NoPosTacletApp> taclets) |
ImmutableList<NoPosTacletApp> |
TacletIndex.getAntecedentTaclet(PosInOccurrence pos,
RuleFilter filter,
Services services)
get all Taclets for the antecedent.
|
ImmutableList<NoPosTacletApp> |
TacletAppIndex.getFindTaclet(PosInOccurrence pos,
TacletFilter filter,
TermServices services)
collects all FindTaclets with instantiations and position
|
ImmutableList<NoPosTacletApp> |
RuleAppIndex.getFindTaclet(TacletFilter filter,
PosInOccurrence pos,
TermServices services)
collects all FindTacletInstantiations for the given
heuristics and position
|
java.lang.Iterable<NoPosTacletApp> |
Node.getLocalIntroducedRules()
Returns the set of NoPosTacletApps at this node
|
ImmutableList<NoPosTacletApp> |
TacletIndex.getNoFindTaclet(RuleFilter filter,
Services services)
get all Taclets having no find expression.
|
ImmutableList<NoPosTacletApp> |
RuleAppIndex.getNoFindTaclet(TacletFilter filter,
Services services)
collects all NoFindTacletInstantiations for the given
heuristics
|
ImmutableList<NoPosTacletApp> |
TacletAppIndex.getNoFindTaclet(TacletFilter filter,
Services services)
collects all NoFindTacletInstantiations
|
ImmutableList<NoPosTacletApp> |
TacletIndex.getPartialInstantiatedApps()
returns a list with all partial instantiated no pos taclet apps
|
ImmutableList<NoPosTacletApp> |
TacletIndex.getRewriteTaclet(PosInOccurrence pos,
RuleFilter filter,
Services services)
get all Rewrite-Taclets.
|
ImmutableList<NoPosTacletApp> |
TacletAppIndex.getRewriteTaclet(PosInOccurrence pos,
TacletFilter filter,
TermServices services)
collects all RewriteTacletInstantiations in a subterm of the
constrainedFormula described by a PosInOccurrence.
|
ImmutableList<NoPosTacletApp> |
RuleAppIndex.getRewriteTaclet(TacletFilter filter,
PosInOccurrence pos,
TermServices services)
collects all RewriteTacletInstantiations for the given
heuristics in a subterm of the constraintformula described by a
PosInOccurrence
|
ImmutableList<NoPosTacletApp> |
TacletIndex.getSuccedentTaclet(PosInOccurrence pos,
RuleFilter filter,
Services services)
get all Taclets for the succedent.
|
ImmutableList<NoPosTacletApp> |
TermTacletAppIndex.getTacletAppAt(PosInOccurrence pos,
RuleFilter p_filter) |
ImmutableList<NoPosTacletApp> |
SemisequentTacletAppIndex.getTacletAppAt(PosInOccurrence pos,
RuleFilter filter) |
protected abstract ImmutableList<NoPosTacletApp> |
TacletIndex.matchTaclets(ImmutableList<NoPosTacletApp> tacletApps,
RuleFilter p_filter,
PosInOccurrence pos,
Services services)
Filter the given list of taclet apps, and match their find
parts at the given position of the sequent
|
static ImmutableSet<NoPosTacletApp> |
TacletIndex.toNoPosTacletApp(java.lang.Iterable<Taclet> rule) |
Modifier and Type | Method and Description |
---|---|
void |
TacletIndex.add(NoPosTacletApp tacletApp)
adds a new Taclet with instantiation information to this index.
|
void |
TacletAppIndex.addedNoPosTacletApp(NoPosTacletApp tacletApp)
updates the internal caches after a new Taclet with instantiation
information has been added to the TacletIndex.
|
void |
Goal.addNoPosTacletApp(NoPosTacletApp app)
puts the NoPosTacletApp to the set of TacletApps at the node
of the goal and to the current RuleAppIndex.
|
void |
RuleAppIndex.addNoPosTacletApp(NoPosTacletApp tacletApp)
adds a new Taclet with instantiation information to the Taclet Index
of this TacletAppIndex.
|
void |
Node.addNoPosTacletApp(NoPosTacletApp s)
adds a new NoPosTacletApp to the set of available NoPosTacletApps at this
node
|
void |
TacletIndex.remove(NoPosTacletApp tacletApp)
removes a Taclet with the given instantiation information from this index.
|
void |
TacletAppIndex.removedNoPosTacletApp(NoPosTacletApp tacletApp)
updates the internal caches after a Taclet with instantiation
information has been removed from the TacletIndex.
|
void |
RuleAppIndex.removeNoPosTacletApp(NoPosTacletApp tacletApp)
remove a Taclet with instantiation information from the Taclet
Index of this TacletAppIndex.
|
Modifier and Type | Method and Description |
---|---|
void |
TacletAppIndex.addedNoPosTacletApps(java.lang.Iterable<NoPosTacletApp> tacletApps)
updates the internal caches after a new Taclet with instantiation
information has been added to the TacletIndex.
|
void |
RuleAppIndex.addNoPosTacletApp(java.lang.Iterable<NoPosTacletApp> tacletApps)
adds a new Taclet with instantiation information to the Taclet Index
of this TacletAppIndex.
|
void |
TacletIndex.addTaclets(java.lang.Iterable<NoPosTacletApp> tacletAppList)
adds a set of NoPosTacletApp to this index
|
static ImmutableList<NoPosTacletApp> |
TermTacletAppIndex.filter(RuleFilter p_filter,
ImmutableList<NoPosTacletApp> taclets) |
protected abstract ImmutableList<NoPosTacletApp> |
TacletIndex.matchTaclets(ImmutableList<NoPosTacletApp> tacletApps,
RuleFilter p_filter,
PosInOccurrence pos,
Services services)
Filter the given list of taclet apps, and match their find
parts at the given position of the sequent
|
void |
TacletIndex.removeTaclets(java.lang.Iterable<NoPosTacletApp> tacletAppList)
removes the given NoPosTacletApps from this index
|
Constructor and Description |
---|
TacletIndex(java.util.HashMap<java.lang.Object,ImmutableList<NoPosTacletApp>> rwList,
java.util.HashMap<java.lang.Object,ImmutableList<NoPosTacletApp>> antecList,
java.util.HashMap<java.lang.Object,ImmutableList<NoPosTacletApp>> succList,
ImmutableList<NoPosTacletApp> noFindList,
java.util.HashSet<NoPosTacletApp> partialInstantiatedRuleApps) |
TacletIndex(java.util.HashMap<java.lang.Object,ImmutableList<NoPosTacletApp>> rwList,
java.util.HashMap<java.lang.Object,ImmutableList<NoPosTacletApp>> antecList,
java.util.HashMap<java.lang.Object,ImmutableList<NoPosTacletApp>> succList,
ImmutableList<NoPosTacletApp> noFindList,
java.util.HashSet<NoPosTacletApp> partialInstantiatedRuleApps) |
TacletIndex(java.util.HashMap<java.lang.Object,ImmutableList<NoPosTacletApp>> rwList,
java.util.HashMap<java.lang.Object,ImmutableList<NoPosTacletApp>> antecList,
java.util.HashMap<java.lang.Object,ImmutableList<NoPosTacletApp>> succList,
ImmutableList<NoPosTacletApp> noFindList,
java.util.HashSet<NoPosTacletApp> partialInstantiatedRuleApps) |
TacletIndex(java.util.HashMap<java.lang.Object,ImmutableList<NoPosTacletApp>> rwList,
java.util.HashMap<java.lang.Object,ImmutableList<NoPosTacletApp>> antecList,
java.util.HashMap<java.lang.Object,ImmutableList<NoPosTacletApp>> succList,
ImmutableList<NoPosTacletApp> noFindList,
java.util.HashSet<NoPosTacletApp> partialInstantiatedRuleApps) |
TacletIndex(java.util.HashMap<java.lang.Object,ImmutableList<NoPosTacletApp>> rwList,
java.util.HashMap<java.lang.Object,ImmutableList<NoPosTacletApp>> antecList,
java.util.HashMap<java.lang.Object,ImmutableList<NoPosTacletApp>> succList,
ImmutableList<NoPosTacletApp> noFindList,
java.util.HashSet<NoPosTacletApp> partialInstantiatedRuleApps) |
Modifier and Type | Method and Description |
---|---|
NoPosTacletApp |
DelayedCut.getHideApp() |
Modifier and Type | Field and Description |
---|---|
protected ImmutableSet<NoPosTacletApp> |
AbstractPO.taclets |
Modifier and Type | Method and Description |
---|---|
ImmutableSet<NoPosTacletApp> |
AbstractOperationPO.getInitialTaclets() |
Modifier and Type | Method and Description |
---|---|
static NoPosTacletApp |
NoPosTacletApp.createFixedNoPosTacletApp(Taclet taclet,
SVInstantiations instantiations,
Services services)
Create TacletApp with immutable "instantiations", i.e.
|
static NoPosTacletApp |
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 |
NoPosTacletApp.createNoPosTacletApp(Taclet taclet,
MatchConditions matchCond,
Services services) |
static NoPosTacletApp |
NoPosTacletApp.createNoPosTacletApp(Taclet taclet,
SVInstantiations instantiations,
ImmutableList<IfFormulaInstantiation> ifInstantiations,
Services services) |
static NoPosTacletApp |
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.
|
NoPosTacletApp |
NoPosTacletApp.matchFind(PosInOccurrence pos,
Services services)
PRECONDITION: ifFormulaInstantiations () == null &&
( pos == null || termConstraint.isSatisfiable () )
|
NoPosTacletApp |
NoPosTacletApp.matchFind(PosInOccurrence pos,
Services services,
Term t) |
Modifier and Type | Method and Description |
---|---|
java.util.Set<NoPosTacletApp> |
OneStepSimplifier.getCapturedTaclets()
Gets an immutable set containing all the taclets captured by the OSS.
|
Modifier and Type | Method and Description |
---|---|
protected NoPosTacletApp |
TacletAppContainer.getTacletApp() |
Modifier and Type | Method and Description |
---|---|
ImmutableList<NoPosTacletApp> |
IfInstantiator.getResults() |
Modifier and Type | Method and Description |
---|---|
protected static TacletAppContainer |
TacletAppContainer.createContainer(NoPosTacletApp p_app,
PosInOccurrence p_pio,
Goal p_goal,
boolean p_initial) |
Modifier and Type | Method and Description |
---|---|
protected static ImmutableList<RuleAppContainer> |
TacletAppContainer.createInitialAppContainers(ImmutableList<NoPosTacletApp> p_app,
PosInOccurrence p_pio,
Goal p_goal) |
Copyright © 2003-2019 The KeY-Project.