public class IfInstantiator
extends java.lang.Object
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 and Description |
---|
IfInstantiator(TacletAppContainer tacletAppContainer,
Goal goal) |
private final Goal goal
private final IfInstantiationCachePool.IfInstantiationCache ifInstCache
private ImmutableList<IfFormulaInstantiation> allAntecFormulas
private ImmutableList<IfFormulaInstantiation> allSuccFormulas
private ImmutableList<NoPosTacletApp> results
private final TacletAppContainer tacletAppContainer
IfInstantiator(TacletAppContainer tacletAppContainer, Goal goal)
private void addResult(NoPosTacletApp app)
public void findIfFormulaInstantiations()
private Taclet getTaclet()
private ImmutableList<IfFormulaInstantiation> getSequentFormulas(boolean p_antec, boolean p_all)
p_all
- if true then return all formulas of the particular
semisequent, otherwise only the formulas returned by
selectNewFormulas
IfFormulaInstSeq.createList
)private ImmutableList<IfFormulaInstantiation> selectNewFormulas(boolean p_antec)
IfFormulaInstSeq.createList
), but consisting only of
those formulas of the current goal for which the method
isNewFormula
returns true
private boolean isNewFormula(IfFormulaInstSeq p_ifInstantiation)
private boolean isNewFormulaDirect(IfFormulaInstSeq p_ifInstantiation)
private ImmutableList<IfFormulaInstantiation> getNewSequentFormulasFromCache(boolean p_antec)
private void addNewSequentFormulasToCache(ImmutableList<IfFormulaInstantiation> p_list, boolean p_antec)
private ImmutableList<IfFormulaInstantiation> getAllSequentFormulas(boolean p_antec)
private void findIfFormulaInstantiationsHelp(ImmutableList<SequentFormula> p_ifSeqTail, ImmutableList<SequentFormula> p_ifSeqTail2nd, ImmutableList<IfFormulaInstantiation> p_alreadyMatched, MatchConditions p_matchCond, boolean p_alreadyMatchedNewFor)
p_ifSeqTail
- tail of the current semisequent as listp_ifSeqTail2nd
- the following semisequent (i.e. antecedent) or nullp_matchCond
- match conditions until now, i.e. after matching the first
formulas of the if sequentp_alreadyMatchedNewFor
- at least one new formula has already been matched, i.e. a
formula that has been modified recentlyprivate Services getServices()
private NoPosTacletApp setAllInstantiations(MatchConditions p_matchCond, ImmutableList<IfFormulaInstantiation> p_alreadyMatched)
public ImmutableList<NoPosTacletApp> getResults()