All Methods Static Methods Instance Methods Concrete Methods
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) |