public final class OneStepSimplifier extends java.lang.Object implements BuiltInRule
Modifier and Type | Class and Description |
---|---|
static class |
OneStepSimplifier.Protocol |
Constructor and Description |
---|
OneStepSimplifier() |
Modifier and Type | Method and Description |
---|---|
ImmutableList<Goal> |
apply(Goal goal,
Services services,
RuleApp ruleApp)
the rule is applied on the given goal using the
information of rule application.
|
OneStepSimplifierRuleApp |
createApp(PosInOccurrence pos,
TermServices services) |
java.lang.String |
displayName()
returns the display name of the rule
|
java.util.Set<NoPosTacletApp> |
getCapturedTaclets()
Gets an immutable set containing all the taclets captured by the OSS.
|
boolean |
isApplicable(Goal goal,
PosInOccurrence pio)
returns true iff a rule is applicable at the given
position.
|
boolean |
isApplicableOnSubTerms() |
boolean |
isShutdown()
returns true if the indices are shutdown
|
Name |
name()
the name of the rule
|
static void |
refreshOSS(Proof proof)
Enables or disables the one step simplification, depending on the
strategy setting made.
|
void |
shutdownIndices()
Deactivate one-step simplification: clear caches, restore taclets to
the goals' taclet indices.
|
java.lang.String |
toString() |
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
getOrigin
public void shutdownIndices()
public boolean isShutdown()
public static void refreshOSS(Proof proof)
proof
- The Proof
for which to refresh the
OneStepSimplifier
instance.public boolean isApplicable(Goal goal, PosInOccurrence pio)
BuiltInRule
isApplicable
in interface BuiltInRule
public ImmutableList<Goal> apply(Goal goal, Services services, RuleApp ruleApp)
Rule
apply
in interface Rule
goal
- the Goal on which to apply ruleAppservices
- the Services with the necessary information
about the java programsruleApp
- the rule application to be executedpublic java.lang.String displayName()
Rule
displayName
in interface Rule
public java.lang.String toString()
toString
in class java.lang.Object
public java.util.Set<NoPosTacletApp> getCapturedTaclets()
public OneStepSimplifierRuleApp createApp(PosInOccurrence pos, TermServices services)
createApp
in interface BuiltInRule
public boolean isApplicableOnSubTerms()
isApplicableOnSubTerms
in interface BuiltInRule
Copyright © 2003-2019 The KeY-Project.