public final class OneStepSimplifier extends java.lang.Object implements BuiltInRule
Modifier and Type | Class and Description |
---|---|
private static class |
OneStepSimplifier.Instantiation |
static class |
OneStepSimplifier.Protocol |
private static class |
OneStepSimplifier.TermReplacementKey
Instances of this class are used in the
Map of
OneStepSimplifier#replaceKnown(TermServices, SequentFormula, Map, List, Protocol)
to forece the same behavior as in Taclet rules where
names of logical variables and TermLabel s are ignored. |
Modifier and Type | Field and Description |
---|---|
private boolean |
active |
private static int |
APPLICABILITY_CACHE_SIZE |
private java.util.Map<SequentFormula,java.lang.Boolean> |
applicabilityCache |
private ImmutableList<NoPosTacletApp> |
appsTakenOver |
private static boolean[] |
bottomUp |
private static int |
DEFAULT_CACHE_SIZE |
private TacletIndex[] |
indices |
private Proof |
lastProof |
private static Name |
NAME |
private java.util.Map<Term,Term>[] |
notSimplifiableCaches |
private static ImmutableList<java.lang.String> |
ruleSets
Rule sets to capture.
|
Constructor and Description |
---|
OneStepSimplifier() |
Modifier and Type | Method and Description |
---|---|
private boolean |
applicableTo(Services services,
SequentFormula cf,
boolean inAntecedent,
Goal goal,
RuleApp ruleApp)
Tells whether the passed formula can be simplified
|
ImmutableList<Goal> |
apply(Goal goal,
Services services,
RuleApp ruleApp)
the rule is applied on the given goal using the
information of rule application.
|
private OneStepSimplifier.Instantiation |
computeInstantiation(Services services,
PosInOccurrence ossPIO,
Sequent seq,
OneStepSimplifier.Protocol protocol,
Goal goal,
RuleApp ruleApp)
Freshly computes the overall simplification result for the passed
constrained formula.
|
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.
|
private void |
initIndices(Proof proof)
If the rule is applied to a different proof than last time, then clear
all caches and initialise the taclet indices.
|
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
|
private RuleApp |
makeReplaceKnownTacletApp(Term formula,
boolean inAntecedent,
PosInOccurrence pio) |
Name |
name()
the name of the rule
|
private void |
refresh(Proof proof) |
static void |
refreshOSS(Proof proof)
Enables or disables the one step simplification, depending on the
strategy setting made.
|
private SequentFormula |
replaceKnown(Services services,
SequentFormula cf,
boolean inAntecedent,
java.util.Map<OneStepSimplifier.TermReplacementKey,PosInOccurrence> context,
java.util.List<PosInOccurrence> ifInsts,
OneStepSimplifier.Protocol protocol,
Goal goal,
RuleApp ruleApp)
Simplifies the given constrained formula as far as possible using
the replace-known rules (hardcoded here).
|
private Term |
replaceKnownHelper(java.util.Map<OneStepSimplifier.TermReplacementKey,PosInOccurrence> map,
Term in,
boolean inAntecedent,
java.util.List<PosInOccurrence> ifInsts,
OneStepSimplifier.Protocol protocol,
Services services,
Goal goal,
RuleApp ruleApp)
Helper for replaceKnown (handles recursion).
|
void |
shutdownIndices()
Deactivate one-step simplification: clear caches, restore taclets to
the goals' taclet indices.
|
private SequentFormula |
simplifyConstrainedFormula(Services services,
SequentFormula cf,
boolean inAntecedent,
java.util.Map<OneStepSimplifier.TermReplacementKey,PosInOccurrence> context,
java.util.List<PosInOccurrence> ifInsts,
OneStepSimplifier.Protocol protocol,
Goal goal,
RuleApp ruleApp)
Simplifies the passed constrained formula using a single taclet or
arbitrarily many replace-known steps.
|
private SequentFormula |
simplifyPos(Goal goal,
Services services,
PosInOccurrence pos,
int indexNr,
OneStepSimplifier.Protocol protocol)
Helper for simplifyPosOrSub.
|
private SequentFormula |
simplifyPosOrSub(Goal goal,
Services services,
PosInOccurrence pos,
int indexNr,
OneStepSimplifier.Protocol protocol)
Performs a single step of simplification at the given position or its
subterms using the given taclet index.
|
private SequentFormula |
simplifySub(Goal goal,
Services services,
PosInOccurrence pos,
int indexNr,
OneStepSimplifier.Protocol protocol)
Helper for simplifyPosOrSub.
|
private ImmutableList<Taclet> |
tacletsForRuleSet(Proof proof,
java.lang.String ruleSetName,
ImmutableList<java.lang.String> excludedRuleSetNames)
Selects the taclets suitable for one step simplification out of the
given rule set (where taclets that also belong to one of the "excluded"
rule sets are not considered).
|
java.lang.String |
toString() |
private static final int APPLICABILITY_CACHE_SIZE
private static final int DEFAULT_CACHE_SIZE
private static final Name NAME
private static final ImmutableList<java.lang.String> ruleSets
private static final boolean[] bottomUp
private final java.util.Map<SequentFormula,java.lang.Boolean> applicabilityCache
private Proof lastProof
private ImmutableList<NoPosTacletApp> appsTakenOver
private TacletIndex[] indices
private boolean active
private ImmutableList<Taclet> tacletsForRuleSet(Proof proof, java.lang.String ruleSetName, ImmutableList<java.lang.String> excludedRuleSetNames)
private void initIndices(Proof proof)
public void shutdownIndices()
public boolean isShutdown()
private SequentFormula simplifyPos(Goal goal, Services services, PosInOccurrence pos, int indexNr, OneStepSimplifier.Protocol protocol)
protocol
- private SequentFormula simplifySub(Goal goal, Services services, PosInOccurrence pos, int indexNr, OneStepSimplifier.Protocol protocol)
protocol
- private SequentFormula simplifyPosOrSub(Goal goal, Services services, PosInOccurrence pos, int indexNr, OneStepSimplifier.Protocol protocol)
protocol
- private Term replaceKnownHelper(java.util.Map<OneStepSimplifier.TermReplacementKey,PosInOccurrence> map, Term in, boolean inAntecedent, java.util.List<PosInOccurrence> ifInsts, OneStepSimplifier.Protocol protocol, Services services, Goal goal, RuleApp ruleApp)
protocol
- services
- TODOprivate SequentFormula replaceKnown(Services services, SequentFormula cf, boolean inAntecedent, java.util.Map<OneStepSimplifier.TermReplacementKey,PosInOccurrence> context, java.util.List<PosInOccurrence> ifInsts, OneStepSimplifier.Protocol protocol, Goal goal, RuleApp ruleApp)
proof
- protocol
- private RuleApp makeReplaceKnownTacletApp(Term formula, boolean inAntecedent, PosInOccurrence pio)
private SequentFormula simplifyConstrainedFormula(Services services, SequentFormula cf, boolean inAntecedent, java.util.Map<OneStepSimplifier.TermReplacementKey,PosInOccurrence> context, java.util.List<PosInOccurrence> ifInsts, OneStepSimplifier.Protocol protocol, Goal goal, RuleApp ruleApp)
protocol
- private OneStepSimplifier.Instantiation computeInstantiation(Services services, PosInOccurrence ossPIO, Sequent seq, OneStepSimplifier.Protocol protocol, Goal goal, RuleApp ruleApp)
protocol
- private boolean applicableTo(Services services, SequentFormula cf, boolean inAntecedent, Goal goal, RuleApp ruleApp)
private void refresh(Proof proof)
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