de.uka.ilkd.key.strategy.termgenerator

Class TriggeredInstantiations

java.lang.Object

de.uka.ilkd.key.strategy.termgenerator.TriggeredInstantiations

All Implemented Interfaces:

TermGenerator

public class TriggeredInstantiations
extends java.lang.Object
implements TermGenerator

Field Summary

Fields

Modifier and Type	Field and Description
private boolean	checkConditions
private Sequent	last
private ImmutableSet<Term>	lastAxioms
private java.util.Set<Term>	lastCandidates

Constructor Summary

Constructors

Constructor and Description
TriggeredInstantiations(boolean checkConditions)

Method Summary

Modifier and Type	Method and Description
private void	collectAxiomsAndCandidateTerms(java.util.Set<Term> terms, java.util.Set<Term> axioms, IntegerLDT integerLDT, Semisequent antecedent, boolean inAntecedent, TermServices services)
private void	collectTerms(Term instanceCandidate, java.util.Set<Term> terms, IntegerLDT intLDT)
private void	computeAxiomAndCandidateSets(Sequent seq, java.util.Set<Term> terms, java.util.Set<Term> axioms, Services services)
private java.util.HashSet<Term>	computeInstances(Services services, Term comprehension, Metavariable mv, Term trigger, java.util.Set<Term> terms, ImmutableSet<Term> axioms, TacletApp app)
static TermGenerator	create(boolean skipConditions)
java.util.Iterator<Term>	generate(RuleApp app, PosInOccurrence pos, Goal goal)
private ImmutableList<Term>	instantiateConditions(Services services, TacletApp app, Term middle)
private Term	instantiateTerm(Term term, Services services, SVInstantiations svInst)
private boolean	isAvoidConditionProvable(Term cond, ImmutableSet<Term> axioms, Services services)

Methods inherited from class java.lang.Object

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

Field Detail

last

private Sequent last

lastCandidates

private java.util.Set<Term> lastCandidates

lastAxioms

private ImmutableSet<Term> lastAxioms

checkConditions

private boolean checkConditions

Constructor Detail

TriggeredInstantiations

public TriggeredInstantiations(boolean checkConditions)

Parameters:

checkConditions - boolean indicating if conditions should be checked

Method Detail

create

public static TermGenerator create(boolean skipConditions)

generate

public java.util.Iterator<Term> generate(RuleApp app,
                                         PosInOccurrence pos,
                                         Goal goal)

Specified by:

generate in interface TermGenerator

instantiateTerm

private Term instantiateTerm(Term term,
                             Services services,
                             SVInstantiations svInst)

computeAxiomAndCandidateSets

private void computeAxiomAndCandidateSets(Sequent seq,
                                          java.util.Set<Term> terms,
                                          java.util.Set<Term> axioms,
                                          Services services)

collectAxiomsAndCandidateTerms

private void collectAxiomsAndCandidateTerms(java.util.Set<Term> terms,
                                            java.util.Set<Term> axioms,
                                            IntegerLDT integerLDT,
                                            Semisequent antecedent,
                                            boolean inAntecedent,
                                            TermServices services)

isAvoidConditionProvable

private boolean isAvoidConditionProvable(Term cond,
                                         ImmutableSet<Term> axioms,
                                         Services services)

computeInstances

private java.util.HashSet<Term> computeInstances(Services services,
                                                 Term comprehension,
                                                 Metavariable mv,
                                                 Term trigger,
                                                 java.util.Set<Term> terms,
                                                 ImmutableSet<Term> axioms,
                                                 TacletApp app)

instantiateConditions

private ImmutableList<Term> instantiateConditions(Services services,
                                                  TacletApp app,
                                                  Term middle)

collectTerms

private void collectTerms(Term instanceCandidate,
                          java.util.Set<Term> terms,
                          IntegerLDT intLDT)