public class TriggeredInstantiations extends java.lang.Object implements TermGenerator
Modifier and Type | Field and Description |
---|---|
private boolean |
checkConditions |
private Sequent |
last |
private ImmutableSet<Term> |
lastAxioms |
private java.util.Set<Term> |
lastCandidates |
Constructor and Description |
---|
TriggeredInstantiations(boolean checkConditions) |
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) |
private Sequent last
private java.util.Set<Term> lastCandidates
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 java.util.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, java.util.Set<Term> terms, java.util.Set<Term> axioms, Services services)
private void collectAxiomsAndCandidateTerms(java.util.Set<Term> terms, java.util.Set<Term> axioms, IntegerLDT integerLDT, Semisequent antecedent, boolean inAntecedent, TermServices services)
private boolean isAvoidConditionProvable(Term cond, ImmutableSet<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)
private ImmutableList<Term> instantiateConditions(Services services, TacletApp app, Term middle)
private void collectTerms(Term instanceCandidate, java.util.Set<Term> terms, IntegerLDT intLDT)