public class TriggeredInstantiations extends Object implements TermGenerator
Modifier and Type | Field and Description |
---|---|
private boolean |
checkConditions |
private Sequent |
last |
private ImmutableSet<Term> |
lastAxioms |
private Set<Term> |
lastCandidates |
Constructor and Description |
---|
TriggeredInstantiations(boolean checkConditions) |
Modifier and Type | Method and Description |
---|---|
private void |
collectAxiomsAndCandidateTerms(Set<Term> terms,
Set<Term> axioms,
IntegerLDT integerLDT,
Semisequent antecedent,
boolean inAntecedent,
TermServices services) |
private void |
collectTerms(Term instanceCandidate,
Set<Term> terms,
IntegerLDT intLDT) |
private void |
computeAxiomAndCandidateSets(Sequent seq,
Set<Term> terms,
Set<Term> axioms,
Services services) |
private HashSet<Term> |
computeInstances(Services services,
Term comprehension,
Metavariable mv,
Term trigger,
Set<Term> terms,
ImmutableSet<Term> axioms,
TacletApp app) |
static TermGenerator |
create(boolean skipConditions) |
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) |
private Sequent last
private ImmutableSet<Term> lastAxioms
private boolean checkConditions
public TriggeredInstantiations(boolean checkConditions)
checkConditions
- boolean indicating if conditions should be checkedpublic static TermGenerator create(boolean skipConditions)
public Iterator<Term> generate(RuleApp app, PosInOccurrence pos, Goal goal)
generate
in interface TermGenerator
private Term instantiateTerm(Term term, Services services, SVInstantiations svInst)
private void computeAxiomAndCandidateSets(Sequent seq, Set<Term> terms, Set<Term> axioms, Services services)
private void collectAxiomsAndCandidateTerms(Set<Term> terms, Set<Term> axioms, IntegerLDT integerLDT, Semisequent antecedent, boolean inAntecedent, TermServices services)
private boolean isAvoidConditionProvable(Term cond, ImmutableSet<Term> axioms, Services services)
private HashSet<Term> computeInstances(Services services, Term comprehension, Metavariable mv, Term trigger, Set<Term> terms, ImmutableSet<Term> axioms, TacletApp app)
private ImmutableList<Term> instantiateConditions(Services services, TacletApp app, Term middle)
private void collectTerms(Term instanceCandidate, Set<Term> terms, IntegerLDT intLDT)