de.uka.ilkd.key.strategy

Class IsInRangeProvable

java.lang.Object

de.uka.ilkd.key.strategy.IsInRangeProvable

All Implemented Interfaces:

Feature

public class IsInRangeProvable
extends java.lang.Object
implements Feature

Feature used to check if the value of a given term with moduloXXX (with XXX being Long, Int, etc.) is in the range of Long, Integer etc.

Field Summary

Fields

Modifier and Type	Field and Description
static IsInRangeProvable	INSTANCE
private int	maxRuleApps
private int	timeoutInMillis

Constructor Summary

Constructors

Modifier	Constructor and Description
private	IsInRangeProvable(int timeoutInMillis, int maxRuleApps)

Method Summary

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

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

INSTANCE

public static final IsInRangeProvable INSTANCE

timeoutInMillis

private final int timeoutInMillis

maxRuleApps

private final int maxRuleApps

Constructor Detail

IsInRangeProvable

private IsInRangeProvable(int timeoutInMillis,
                          int maxRuleApps)

Method Detail

collectAxioms

private ImmutableSet<Term> collectAxioms(Sequent seq,
                                         PosInOccurrence ignore,
                                         Services services)

Helper method used to extract the axioms from a given sequent

Parameters:

seq - the Sequent from which the axioms are extracted

ignore - the SequentFormula not to be used as axiom

services - the Services

Returns:

the set of axioms

extractAssumptionsFrom

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)

Parameters:

semisequent - the Semisequent, i.e., antecedent or succedent from which axioms are extracted

negated - a boolean true if not the formulas of the sequent itself, but their negation should be used as axiom

assumptions - the already identified axioms

ops - the Set of operators of interest used to identify axiom candidates

formulaToIgnore - the SequentFormula that should not be used as axiom under any circumstances (the consequence is derived from this formula)

services - the Services

Returns:

the set of axioms (including the already found axioms assumptions

filterSequent

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

Parameters:

ops - the Set of Operators

integerLDT - the IntegerLDT

formula - the formula to check

Returns:

true if the formula should be used axiom

isProvable

protected boolean isProvable(Sequent seq,
                             Services services)

checks if the sequent is provable

Parameters:

seq - the Sequent to be proven

services - the Services

Returns:

true if the sequent could be proven valid

setupStrategy

protected StrategyProperties setupStrategy()

creates the strategy configuration to be used for the side proof

Returns:

the StrategyProperties

computeCost

public RuleAppCost computeCost(RuleApp app,
                               PosInOccurrence pos,
                               Goal goal)

Description copied from interface: Feature

Evaluate the cost of a RuleApp.

Specified by:

computeCost in interface Feature

Parameters:

app - the RuleApp

pos - position where app is to be applied

goal - the goal on which app is to be applied

Returns:

the cost of the rule application expressed as a RuleAppCost object. TopRuleAppCost.INSTANCE indicates that the rule shall not be applied at all (it is discarded by the strategy).

createConsequence

protected Term createConsequence(PosInOccurrence pos,
                                 Services services)

creates the term to be proven to follow from a (possibly empty) set of axioms

Parameters:

pos - the PosInOccurrence of the focus term

services - the Services

Returns:

the term to prove

toSequent

protected Sequent toSequent(ImmutableSet<Term> axioms,
                            Term toProve)

creates the sequent axioms ==> toProve

Parameters:

axioms - set of terms (conjunctive)

toProve - the Term to be proven

Returns:

the sequent to be proven valid