Modifier and Type | Field and Description |
---|---|
static IsInRangeProvable |
INSTANCE |
Modifier and Type | Method and Description |
---|---|
RuleAppCost |
computeCost(RuleApp app,
PosInOccurrence pos,
Goal goal)
Evaluate the cost of a
RuleApp . |
protected Term |
createConsequence(PosInOccurrence pos,
Services services)
creates the term to be proven to follow from a (possibly empty) set of axioms
|
protected boolean |
isProvable(Sequent seq,
Services services)
checks if the sequent is provable
|
protected StrategyProperties |
setupStrategy()
creates the strategy configuration to be used for the side proof
|
protected Sequent |
toSequent(ImmutableSet<Term> axioms,
Term toProve)
creates the sequent
axioms ==> toProve |
public static final IsInRangeProvable INSTANCE
protected boolean isProvable(Sequent seq, Services services)
protected StrategyProperties setupStrategy()
public RuleAppCost computeCost(RuleApp app, PosInOccurrence pos, Goal goal)
Feature
RuleApp
.computeCost
in interface Feature
app
- the RuleApppos
- position where app
is to be appliedgoal
- the goal on which app
is to be appliedRuleAppCost
object. TopRuleAppCost.INSTANCE
indicates that the rule shall not be applied at all (it is discarded by
the strategy).protected Term createConsequence(PosInOccurrence pos, Services services)
pos
- the PosInOccurrence
of the focus termservices
- the Services
protected Sequent toSequent(ImmutableSet<Term> axioms, Term toProve)
axioms ==> toProve
axioms
- set of terms (conjunctive)toProve
- the Term to be provenCopyright © 2003-2019 The KeY-Project.