Package | Description |
---|---|
de.uka.ilkd.key.core | |
de.uka.ilkd.key.informationflow.rule | |
de.uka.ilkd.key.logic |
provides a representation for the term and sequent
structure.
|
de.uka.ilkd.key.nparser.builder | |
de.uka.ilkd.key.pp |
This package contains pretty-printing functionality used by the GUI and for
saving proofs.
|
de.uka.ilkd.key.proof.init |
This package contains classes handling prover initialisation.
|
de.uka.ilkd.key.proof.rulefilter | |
de.uka.ilkd.key.rule |
This package contains classes for implementing rules.
|
de.uka.ilkd.key.rule.tacletbuilder | |
de.uka.ilkd.key.strategy |
This package contains classes implementing the proof search strategies of KeY.
|
de.uka.ilkd.key.strategy.feature |
Modifier and Type | Method and Description |
---|---|
Namespace<RuleSet> |
KeYMediator.heur_ns()
returns the heuristics namespace
|
Constructor and Description |
---|
InfFlowContractAppTaclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> ruleSets,
TacletAttributes attrs,
Term find,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
int p_applicationRestriction,
ImmutableSet<Choice> choices,
boolean surviveSymbExec,
ImmutableSet<TacletAnnotation> tacletAnnotations) |
InfFlowContractAppTaclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> ruleSets,
TacletAttributes attrs,
Term find,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
int p_applicationRestriction,
ImmutableSet<Choice> choices,
ImmutableSet<TacletAnnotation> tacletAnnotations) |
Modifier and Type | Method and Description |
---|---|
Namespace<RuleSet> |
NamespaceSet.ruleSets() |
Modifier and Type | Method and Description |
---|---|
void |
NamespaceSet.setRuleSets(Namespace<RuleSet> ruleSetNS) |
Constructor and Description |
---|
NamespaceSet(Namespace<QuantifiableVariable> varNS,
Namespace<Function> funcNS,
Namespace<Sort> sortNS,
Namespace<RuleSet> ruleSetNS,
Namespace<Choice> choiceNS,
Namespace<IProgramVariable> programVarNS) |
Modifier and Type | Method and Description |
---|---|
RuleSet |
DefaultBuilder.visitRuleset(KeYParser.RulesetContext ctx) |
Modifier and Type | Method and Description |
---|---|
protected Namespace<RuleSet> |
DefaultBuilder.ruleSets() |
java.util.List<RuleSet> |
DefaultBuilder.visitRulesets(KeYParser.RulesetsContext ctx) |
Modifier and Type | Method and Description |
---|---|
protected void |
LogicPrinter.printHeuristic(RuleSet sv) |
Modifier and Type | Method and Description |
---|---|
Namespace<RuleSet> |
InitConfig.ruleSetNS()
returns the heuristics namespace of this initial configuration
|
Constructor and Description |
---|
IHTacletFilter(boolean interactive,
ImmutableList<RuleSet> heuristics) |
Modifier and Type | Field and Description |
---|---|
protected ImmutableList<RuleSet> |
Taclet.ruleSets
list of rulesets (formerly known as heuristics) the taclet belongs to
|
Modifier and Type | Method and Description |
---|---|
ImmutableList<RuleSet> |
Taclet.getRuleSets() |
java.util.Iterator<RuleSet> |
Taclet.ruleSets()
returns an iterator over the rule sets.
|
Modifier and Type | Method and Description |
---|---|
boolean |
Taclet.admissible(boolean interactive,
ImmutableList<RuleSet> p_ruleSets) |
boolean |
TacletApp.admissible(boolean interactive,
ImmutableList<RuleSet> ruleSets) |
protected boolean |
Taclet.admissibleAutomatic(ImmutableList<RuleSet> admissibleRuleSets) |
protected boolean |
Taclet.admissibleInteractive(ImmutableList<RuleSet> notAdmissibleRuleSets) |
Constructor and Description |
---|
AntecTaclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> heuristics,
TacletAttributes attrs,
Term find,
boolean ignoreTopLevelUpdates,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
ImmutableSet<Choice> choices,
ImmutableSet<TacletAnnotation> tacletAnnotations)
creates a Schematic Theory Specific Rule (Taclet) with the given
parameters.
|
FindTaclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> ruleSets,
TacletAttributes attrs,
Term find,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
ImmutableSet<Choice> choices,
boolean surviveSymbExec,
ImmutableSet<TacletAnnotation> tacletAnnotations)
creates a FindTaclet
|
FindTaclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> ruleSets,
TacletAttributes attrs,
Term find,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
ImmutableSet<Choice> choices,
ImmutableSet<TacletAnnotation> tacletAnnotations)
creates a FindTaclet
|
NoFindTaclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> ruleSets,
TacletAttributes attrs,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
ImmutableSet<Choice> choices,
ImmutableSet<TacletAnnotation> tacletAnnotations)
creates a Schematic Theory Specific Rule (Taclet) with the given
parameters.
|
RewriteTaclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> ruleSets,
TacletAttributes attrs,
Term find,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
int p_applicationRestriction,
ImmutableSet<Choice> choices,
boolean surviveSymbExec,
ImmutableSet<TacletAnnotation> tacletAnnotations) |
RewriteTaclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> ruleSets,
TacletAttributes attrs,
Term find,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
int p_applicationRestriction,
ImmutableSet<Choice> choices,
ImmutableSet<TacletAnnotation> tacletAnnotations)
creates a Schematic Theory Specific Rule (Taclet) with the given
parameters that represents a rewrite rule.
|
SuccTaclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> heuristics,
TacletAttributes attrs,
Term find,
boolean ignoreTopLevelUpdates,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
ImmutableSet<Choice> choices,
ImmutableSet<TacletAnnotation> tacletAnnotations)
creates a Schematic Theory Specific Rule (Taclet) with the given
parameters that works on the succedent.
|
Taclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> ruleSets,
TacletAttributes attrs,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
ImmutableSet<Choice> choices,
boolean surviveSmbExec,
ImmutableSet<TacletAnnotation> tacletAnnotations)
creates a Taclet (originally known as Schematic Theory Specific Rules)
|
Taclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> ruleSets,
TacletAttributes attrs,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
ImmutableSet<Choice> choices,
ImmutableSet<TacletAnnotation> tacletAnnotations)
creates a Schematic Theory Specific Rule (Taclet) with the given
parameters.
|
Modifier and Type | Field and Description |
---|---|
protected ImmutableList<RuleSet> |
TacletBuilder.ruleSets |
Modifier and Type | Method and Description |
---|---|
void |
TacletBuilder.addRuleSet(RuleSet rs)
adds a new rule set to the rule sets of the Taclet.
|
Taclet |
TacletGenerator.generateAxiomTaclet(Name tacletName,
Term originalAxiom,
ImmutableList<ProgramVariable> programVars,
KeYJavaType kjt,
RuleSet ruleSet,
TermServices services)
Returns a no-find taclet to the passed axiom.
|
Taclet |
TacletGenerator.generateRewriteTaclet(Name tacletName,
Term originalFind,
Term originalAxiom,
ImmutableList<ProgramVariable> programVars,
RuleSet ruleSet,
TermServices services) |
Modifier and Type | Method and Description |
---|---|
void |
TacletBuilder.setRuleSets(ImmutableList<RuleSet> rs) |
Modifier and Type | Method and Description |
---|---|
protected RuleSet |
AbstractFeatureStrategy.getHeuristic(java.lang.String p_name) |
Modifier and Type | Method and Description |
---|---|
protected void |
AbstractFeatureStrategy.bindRuleSet(RuleSetDispatchFeature d,
RuleSet ruleSet,
Feature f) |
protected void |
AbstractFeatureStrategy.bindRuleSet(RuleSetDispatchFeature d,
RuleSet ruleSet,
long cost) |
protected void |
AbstractFeatureStrategy.clearRuleSetBindings(RuleSetDispatchFeature d,
RuleSet ruleSet) |
Modifier and Type | Method and Description |
---|---|
void |
RuleSetDispatchFeature.add(RuleSet ruleSet,
Feature f)
Bind feature
f to the rule set ruleSet . |
void |
RuleSetDispatchFeature.clear(RuleSet ruleSet)
Remove all features that have been related to
ruleSet . |
Feature |
RuleSetDispatchFeature.get(RuleSet ruleSet)
|
Copyright © 2003-2019 The KeY-Project.