Modifier and Type | Field and Description |
---|---|
static IsInRangeProvable |
INSTANCE |
private int |
maxRuleApps |
private int |
timeoutInMillis |
Modifier | Constructor and Description |
---|---|
private |
IsInRangeProvable(int timeoutInMillis,
int maxRuleApps) |
Modifier and Type | Method and Description |
---|---|
private ImmutableSet<Term> |
collectAxioms(Sequent seq,
PosInOccurrence ignore,
Services services)
Helper method used to extract the axioms from a given sequent
|
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
|
private ImmutableSet<Term> |
extractAssumptionsFrom(Semisequent semisequent,
boolean negated,
ImmutableSet<Term> assumptions,
java.util.HashSet<Operator> ops,
SequentFormula formulaToIgnore,
Services services)
helper method to determine teh formulas in a semisequent to be used as axioms (or their negations)
|
private boolean |
filterSequent(java.util.HashSet<Operator> ops,
IntegerLDT integerLDT,
Term formula)
helper methods to filter out the sequent formulas of interest,
here those formulas with an equality between ints or any of the operators in
ops as top level operator
|
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
private final int timeoutInMillis
private final int maxRuleApps
private IsInRangeProvable(int timeoutInMillis, int maxRuleApps)
private ImmutableSet<Term> collectAxioms(Sequent seq, PosInOccurrence ignore, Services services)
seq
- the Sequent
from which the axioms are extractedignore
- the SequentFormula
not to be used as axiomservices
- the Services
private ImmutableSet<Term> extractAssumptionsFrom(Semisequent semisequent, boolean negated, ImmutableSet<Term> assumptions, java.util.HashSet<Operator> ops, SequentFormula formulaToIgnore, Services services)
semisequent
- the Semisequent
, i.e., antecedent or succedent from which axioms are extractednegated
- a boolean true if not the formulas of the sequent itself, but their negation should be used as axiomassumptions
- the already identified axiomsops
- the Set
of operators of interest used to identify axiom candidatesformulaToIgnore
- the SequentFormula
that should not be used as axiom under any circumstances (the consequence is derived from this formula)services
- the Services
assumptions
private boolean filterSequent(java.util.HashSet<Operator> ops, IntegerLDT integerLDT, Term formula)
ops
- the Set
of Operator
sintegerLDT
- the IntegerLDT
formula
- the formula to checkprotected 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 proven