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 |