de.uka.ilkd.key.strategy

Class IfInstantiator

java.lang.Object

de.uka.ilkd.key.strategy.IfInstantiator

public class IfInstantiator
extends java.lang.Object

This class implements custom instantiation of if-formulas.

Field Summary

Fields

Modifier and Type	Field and Description
private ImmutableList<IfFormulaInstantiation>	allAntecFormulas
private ImmutableList<IfFormulaInstantiation>	allSuccFormulas
private Goal	goal
private IfInstantiationCachePool.IfInstantiationCache	ifInstCache
private ImmutableList<NoPosTacletApp>	results
private TacletAppContainer	tacletAppContainer

Constructor Summary

Constructors

Constructor and Description
IfInstantiator(TacletAppContainer tacletAppContainer, Goal goal)

Method Summary

Modifier and Type	Method and Description
private void	addNewSequentFormulasToCache(ImmutableList<IfFormulaInstantiation> p_list, boolean p_antec)
private void	addResult(NoPosTacletApp app)
void	findIfFormulaInstantiations() Find all possible instantiations of the if sequent formulas within the sequent "p_seq".
private void	findIfFormulaInstantiationsHelp(ImmutableList<SequentFormula> p_ifSeqTail, ImmutableList<SequentFormula> p_ifSeqTail2nd, ImmutableList<IfFormulaInstantiation> p_alreadyMatched, MatchConditions p_matchCond, boolean p_alreadyMatchedNewFor) Recursive function for matching the remaining tail of an if sequent
private ImmutableList<IfFormulaInstantiation>	getAllSequentFormulas(boolean p_antec)
private ImmutableList<IfFormulaInstantiation>	getNewSequentFormulasFromCache(boolean p_antec)
ImmutableList<NoPosTacletApp>	getResults()
private ImmutableList<IfFormulaInstantiation>	getSequentFormulas(boolean p_antec, boolean p_all)
private Services	getServices()
private Taclet	getTaclet()
private boolean	isNewFormula(IfFormulaInstSeq p_ifInstantiation)
private boolean	isNewFormulaDirect(IfFormulaInstSeq p_ifInstantiation)
private ImmutableList<IfFormulaInstantiation>	selectNewFormulas(boolean p_antec)
private NoPosTacletApp	setAllInstantiations(MatchConditions p_matchCond, ImmutableList<IfFormulaInstantiation> p_alreadyMatched)

Methods inherited from class java.lang.Object

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

Field Detail

goal

private final Goal goal

ifInstCache

private final IfInstantiationCachePool.IfInstantiationCache ifInstCache

allAntecFormulas

private ImmutableList<IfFormulaInstantiation> allAntecFormulas

allSuccFormulas

private ImmutableList<IfFormulaInstantiation> allSuccFormulas

results

private ImmutableList<NoPosTacletApp> results

tacletAppContainer

private final TacletAppContainer tacletAppContainer

Constructor Detail

IfInstantiator

IfInstantiator(TacletAppContainer tacletAppContainer,
               Goal goal)

Method Detail

addResult

private void addResult(NoPosTacletApp app)

findIfFormulaInstantiations

public void findIfFormulaInstantiations()

Find all possible instantiations of the if sequent formulas within the sequent "p_seq".

getTaclet

private Taclet getTaclet()

getSequentFormulas

private ImmutableList<IfFormulaInstantiation> getSequentFormulas(boolean p_antec,
                                                                 boolean p_all)

Parameters:

p_all - if true then return all formulas of the particular semisequent, otherwise only the formulas returned by selectNewFormulas

Returns:

a list of potential if-formula instantiations (analogously to IfFormulaInstSeq.createList)

selectNewFormulas

private ImmutableList<IfFormulaInstantiation> selectNewFormulas(boolean p_antec)

Returns:

a list of potential if-formula instantiations (analogously to IfFormulaInstSeq.createList), but consisting only of those formulas of the current goal for which the method isNewFormula returns true

isNewFormula

private boolean isNewFormula(IfFormulaInstSeq p_ifInstantiation)

Returns:

true iff the formula described by the argument has been modified (or introduced) since the latest point of time when the if-formulas of the enclosing taclet app (container) have been matched

isNewFormulaDirect

private boolean isNewFormulaDirect(IfFormulaInstSeq p_ifInstantiation)

Returns:

true iff the formula described by the argument has been modified (or introduced) since the latest point of time when the if-formulas of the enclosing taclet app (container) have been matched (this method does not use the cache)

getNewSequentFormulasFromCache

private ImmutableList<IfFormulaInstantiation> getNewSequentFormulasFromCache(boolean p_antec)

addNewSequentFormulasToCache

private void addNewSequentFormulasToCache(ImmutableList<IfFormulaInstantiation> p_list,
                                          boolean p_antec)

getAllSequentFormulas

private ImmutableList<IfFormulaInstantiation> getAllSequentFormulas(boolean p_antec)

findIfFormulaInstantiationsHelp

private void findIfFormulaInstantiationsHelp(ImmutableList<SequentFormula> p_ifSeqTail,
                                             ImmutableList<SequentFormula> p_ifSeqTail2nd,
                                             ImmutableList<IfFormulaInstantiation> p_alreadyMatched,
                                             MatchConditions p_matchCond,
                                             boolean p_alreadyMatchedNewFor)

Recursive function for matching the remaining tail of an if sequent

Parameters:

p_ifSeqTail - tail of the current semisequent as list

p_ifSeqTail2nd - the following semisequent (i.e. antecedent) or null

p_matchCond - match conditions until now, i.e. after matching the first formulas of the if sequent

p_alreadyMatchedNewFor - at least one new formula has already been matched, i.e. a formula that has been modified recently

getServices

private Services getServices()

setAllInstantiations

private NoPosTacletApp setAllInstantiations(MatchConditions p_matchCond,
                                            ImmutableList<IfFormulaInstantiation> p_alreadyMatched)

getResults

public ImmutableList<NoPosTacletApp> getResults()

Returns:

Returns the results.