| Interface | Description |
|---|---|
| Feature |
| Class | Description |
|---|---|
| AbstractBetaFeature |
This abstract class contains some auxiliary methods for the selection of
beta rules that are supposed to be applied.
|
| AbstractBetaFeature.MaxDPathHelper | |
| AbstractBetaFeature.MaxPathHelper | |
| AbstractBetaFeature.MaxPosPathHelper | |
| AbstractBetaFeature.TermInfo |
Informations about a term as cached within "betaCandidates"
|
| AbstractMonomialSmallerThanFeature | |
| AbstractNonDuplicateAppFeature | |
| AbstractPolarityFeature |
Auxiliary class that contains methods to compute the polarity of a
position/subformula within a formula
|
| AgeFeature |
Feature that computes the age of the goal (i.e. total number of rules
applications that have been performed at the goal) to which a rule is
supposed to be applied
|
| AllowedCutPositionFeature |
Feature that returns zero iff the application focus of a rule is a potential
cut position (taclet cut_direct).
|
| ApplyTFFeature |
Feature for invoking a term feature on the instantiation of a schema variable
|
| AtomsSmallerThanFeature |
Feature that returns zero iff each variable/atom of one monomial is smaller
than all variables of a second monomial
|
| AutomatedRuleFeature |
This feature checks if a rule may be applied automatically.
|
| BinaryFeature |
Abstract superclass for features that have either zero cost or top cost.
|
| BinaryTacletAppFeature |
Abstract superclass for features of TacletApps that have either zero or top
cost.
|
| CheckApplyEqFeature |
This feature checks that an equation is not applied to itself.
|
| CompareCostsFeature | |
| ComprehendedSumFeature |
A feature that computes the sum of the values of a feature term when a given
variable ranges over a sequence of terms
|
| ConditionalFeature |
A feature that evaluates one of two given features, depending on the result
of a
RuleFilter |
| ConstFeature |
A feature that returns a constant value
|
| ContainsQuantifierFeature |
Binary feature that returns zero iff the focus of a rule contains a
quantifier
NB: this can nowadays be done more nicely using term features
|
| ContainsTermFeature |
Feature for checking if the term of the first projection contains the
term of the second projection.
|
| CountBranchFeature |
Feature that returns the number of branches for a given taclet application
Size of "assumes" sequents is currently not considered
|
| CountMaxDPathFeature |
Feature that returns the maximum number of literals occurring within a d-path
of the find-formula as a formula of the antecedent.
|
| CountPosDPathFeature |
Feature that returns the maximum number of positive literals occurring within
a d-path of the find-formula as a formula of the antecedent.
|
| DeleteMergePointRuleFeature |
Costs for the
DeleteMergePointRule; incredibly cheap if the previous
rule application was a MergeRule app, infinitely expensive otherwise. |
| DependencyContractFeature | |
| DiffFindAndIfFeature |
Binary feature that returns zero iff the \assumes- and find-formula
of a Taclet are matched to different members of the sequent.
|
| DiffFindAndReplacewithFeature |
Binary feature that returns zero iff the replacewith- and find-parts
of a Taclet are matched to different terms.
|
| DirectlyBelowFeature |
This feature returns zero if and only if the focus of the given rule
application exists, is not top-level and the symbol immediately above the
focus is
badSymbol. |
| DirectlyBelowSymbolFeature |
This feature returns zero if and only if the focus of the given rule
application exists, is not top-level and the symbol immediately above the
focus is
badSymbol. |
| EqNonDuplicateAppFeature |
Binary feature that returns zero iff a certain Taclet app has not already
been performed.
|
| FindDepthFeature |
A feature that computes the depth of the find-position of a taclet (top-level
positions have depth zero or if not a find taclet)
TODO: eliminate this class and use term features instead
|
| FindRightishFeature |
Walking from the root of a formula down to the focus of a rule application,
count how often we choose the left branch (subterm) and how the right
branches.
|
| FocusInAntecFeature | |
| FocusIsSubFormulaOfInfFlowContractAppFeature |
Checks whether the focus of the ruleApp is contained in one of the formulas
added by information flow contract applications.
|
| FormulaAddedByRuleFeature |
Binary feature that returns zero iff the find-formula of the concerned rule
app was introduced by a certain kind rule of rule (described via a
RuleFilter) |
| IfThenElseMalusFeature |
Feature that counts the IfThenElse operators above the focus of a rule
application.
|
| ImplicitCastNecessary | |
| InEquationMultFeature |
Feature that decides whether the multiplication of two inequations (using
rules of set inEqSimp_nonLin_multiply) is allowed.
|
| InfFlowContractAppFeature | |
| InstantiatedSVFeature |
Feature that returns zero iff a certain schema variable is instantiated.
|
| LeftmostNegAtomFeature |
Feature that returns zero if there is no atom with negative polarity on a
common d-path and on the left of the find-position within the find-formula as
a formula of the antecedent.
|
| LetFeature |
Feature for locally binding a
TermBuffer to a certain value,
namely to a term that is generated by a ProjectionToTerm. |
| MatchedIfFeature |
Binary features that returns zero iff the if-formulas of a Taclet are
instantiated or the Taclet does not have any if-formulas.
|
| MergeRuleFeature |
Costs for the
MergeRule; cheap if the first statement in the chosen
top-level formula is a MergePointStatement, otherwise, infinitely
expensive. |
| MonomialsSmallerThanFeature |
Feature that returns zero iff each monomial of one polynomial is smaller than
all monomials of a second polynomial
|
| NonDuplicateAppFeature |
Binary feature that returns zero iff a certain Taclet app has not already
been performed
|
| NonDuplicateAppModPositionFeature |
Binary feature that returns zero iff a certain Taclet app has not already
been performed
|
| NoSelfApplicationFeature |
This feature checks that the position of application is not contained in the
if-formulas.
|
| NotBelowBinderFeature |
Returns zero iff the position of a rule application is not below any
operators that bind variables
|
| NotBelowQuantifierFeature |
Binary feature that returns zero iff the position of the given rule app is
not within the scope of a quantifier
|
| NotInScopeOfModalityFeature |
Returns zero iff the position of a rule application is not in the scope of a
modal operator (a program block or an update).
|
| OnlyInScopeOfQuantifiersFeature |
BinaryFeature that return zero if all the operator is quantifier from root
to position it point to.
|
| PolynomialValuesCmpFeature |
Return zero only if the value of one (left) polynomial always will be (less
or equal) or (less) than the value of a second (right) polynomial.
|
| PrintFeature |
For debugging purposes.
|
| PurePosDPathFeature |
Binary feature that returns zero iff the find-formula of a rule contains a
d-path consisting only of positive literals (as a formula of the antecedent).
|
| QueryExpandCost |
A Feature that computes the cost for using the query expand rule.
|
| ReducibleMonomialsFeature |
Return zero iff the monomial
dividendSV can be made smaller
(in the polynomial reduction ordering) by adding or subtracting
divisorSV |
| RuleSetDispatchFeature |
Feature for relating rule sets with feature terms.
|
| ScaleFeature |
A feature that applies an affine transformation to the result of
a given feature.
|
| ScaleFeature.MultFeature | |
| SeqContainsExecutableCodeFeature | |
| SetsSmallerThanFeature | |
| ShannonFeature |
A conditional feature, in which the condition itself is a (binary) feature.
|
| SimplifyBetaCandidateFeature |
Binary feature that returns zero iff the hyper-tableaux simplification method
approves the given application (which is supposed to be the application of a
beta rule).
|
| SimplifyReplaceKnownCandidateFeature |
Binary feature that returns true iff the hyper-tableaux simplification method
approves the given application (which is supposed to be the application of a
replace-known rule).
|
| SmallerThanFeature |
Abstract superclass for features comparing terms (in particular polynomials
or monomials) using the term ordering
|
| SmallerThanFeature.Collector | |
| SortComparisonFeature | |
| SumFeature |
A feature that computes the sum of a given list (vector) of features
|
| SVNeedsInstantiation | |
| TacletRequiringInstantiationFeature |
Feature that returns zero iff the given rule app is a taclet app that needs
explicit instantiation of schema variables (which has not been done yet)
|
| TermSmallerThanFeature |
Feature that returns zero iff one term is smaller than another term in the
current term ordering
|
| ThrownExceptionFeature | |
| TopLevelFindFeature |
Feature for investigating whether the focus of a rule application is a
top-level formula, a top-level formula of the antecedent or a top-level
formula of the succedent
|
| TopLevelFindFeature.TopLevelWithoutUpdate | |
| TopLevelFindFeature.TopLevelWithUpdate | |
| TriggerVarInstantiatedFeature | |
| TrivialMonomialLCRFeature |
Return zero of the least common reducible of two monomials is so trivial that
it is not necessary to do the critical pair completion
"A critical-pair/completion algorithm for finitely generated ideals in rings"
|
| Enum | Description |
|---|---|
| AbstractBetaFeature.TermInfo.Candidate |