| Interface | Description |
|---|---|
| TermGenerator |
Interface for objects that generate lists/sequences of terms or formulas.
|
| Class | Description |
|---|---|
| AllowedCutPositionsGenerator |
Enumerate potential subformulas of a formula that could be used for a cut
(taclet cut_direct).
|
| AllowedCutPositionsGenerator.ACPIterator | |
| HeapGenerator |
The heap generator returns an iterator over all terms of sort heap
that
can be found in the sequent
are top level in the sense that they are not part of a larger term expression
depending on the mode: heaps just occurring in updates are included or ignored
|
| MultiplesModEquationsGenerator |
Try to rewrite a monomial (term)
source so that it becomes a
multiple of another monomial target, using the integer
equations of the antecedent. |
| MultiplesModEquationsGenerator.CofactorItem | |
| MultiplesModEquationsGenerator.CofactorMonomial | |
| MultiplesModEquationsGenerator.CofactorPolynomial | |
| RootsGenerator |
Term generator for inferring the range of values that a variable can have from
a given non-linear (in)equation.
|
| SequentFormulasGenerator |
Term generator that enumerates the formulas of the current
sequent/antecedent/succedent.
|
| SequentFormulasGenerator.SFIterator | |
| SubtermGenerator |
Term generator that enumerates the subterms or subformulas of a given term.
|
| SuperTermGenerator | |
| SuperTermGenerator.SuperTermWithIndexGenerator | |
| TriggeredInstantiations |