public final class OneStepSimplifier extends Object implements BuiltInRule
Modifier and Type | Class and Description |
---|---|
private static class |
OneStepSimplifier.Instantiation |
static class |
OneStepSimplifier.Protocol |
private static class |
OneStepSimplifier.TermReplacementKey
|
Modifier and Type | Field and Description |
---|---|
private boolean |
active |
private static int |
APPLICABILITY_CACHE_SIZE |
private Map<SequentFormula,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 Map<Term,Term>[] |
notSimplifiableCaches |
private static ImmutableList<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) |
String |
displayName()
returns the display name of the rule
|
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) |
private SequentFormula |
replaceKnown(Services services,
SequentFormula cf,
boolean inAntecedent,
Map<OneStepSimplifier.TermReplacementKey,PosInOccurrence> context,
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(Map<OneStepSimplifier.TermReplacementKey,PosInOccurrence> map,
Term in,
boolean inAntecedent,
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,
Map<OneStepSimplifier.TermReplacementKey,PosInOccurrence> context,
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,
String ruleSetName,
ImmutableList<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).
|
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<String> ruleSets
private static final boolean[] bottomUp
private final Map<SequentFormula,Boolean> applicabilityCache
private Proof lastProof
private ImmutableList<NoPosTacletApp> appsTakenOver
private TacletIndex[] indices
private boolean active
private ImmutableList<Taclet> tacletsForRuleSet(Proof proof, String ruleSetName, ImmutableList<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(Map<OneStepSimplifier.TermReplacementKey,PosInOccurrence> map, Term in, boolean inAntecedent, List<PosInOccurrence> ifInsts, OneStepSimplifier.Protocol protocol, Services services, Goal goal, RuleApp ruleApp)
protocol
- services
- TODOprivate SequentFormula replaceKnown(Services services, SequentFormula cf, boolean inAntecedent, Map<OneStepSimplifier.TermReplacementKey,PosInOccurrence> context, 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, Map<OneStepSimplifier.TermReplacementKey,PosInOccurrence> context, 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)
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 String displayName()
Rule
displayName
in interface Rule
public Set<NoPosTacletApp> getCapturedTaclets()
public OneStepSimplifierRuleApp createApp(PosInOccurrence pos, TermServices services)
createApp
in interface BuiltInRule
public boolean isApplicableOnSubTerms()
isApplicableOnSubTerms
in interface BuiltInRule