All Methods Instance Methods Concrete Methods
Modifier and Type |
Method and Description |
private Feature |
allowInEqStrengthening(TermBuffer atom,
TermBuffer literal) |
private Feature |
allowPosNegCaseDistinction(TermBuffer atom) |
private Feature |
allowQuantifierSplitting() |
private Feature |
allowSplitting(ProjectionToTerm focus) |
protected boolean |
arithDefOps() |
private boolean |
arithNonLinInferences() |
private boolean |
autoInductionEnabled() |
private boolean |
autoInductionLemmaEnabled() |
private boolean |
classAxiomApplicationEnabled() |
private boolean |
classAxiomDelayedApplication() |
private Feature |
clausesSmallerThan(java.lang.String smaller,
java.lang.String bigger,
IntegerLDT numbers) |
RuleAppCost |
computeCost(RuleApp app,
PosInOccurrence pio,
Goal goal)
Evaluate the cost of a RuleApp .
|
protected RuleSetDispatchFeature |
getCostComputationDispatcher() |
protected RuleSetDispatchFeature |
getInstantiationDispatcher() |
protected Services |
getServices() |
protected RuleAppCost |
instantiateApp(RuleApp app,
PosInOccurrence pio,
Goal goal) |
private boolean |
instQuantifiersWithQueries() |
boolean |
isApprovedApp(RuleApp app,
PosInOccurrence pio,
Goal goal)
Re-Evaluate a RuleApp .
|
private Feature |
isBelow(TermFeature t) |
private Feature |
isRootInferenceProducer(TermBuffer intRel) |
boolean |
isStopAtFirstNonCloseableGoal()
Checks if the Strategy should stop at the first non closeable Goal .
|
Name |
name()
returns the name of this element
|
private boolean |
normalSplitting() |
private Feature |
oneStepSimplificationFeature(Feature cost) |
private boolean |
quantifierInstantiatedEnabled() |
private boolean |
quantifiersMightSplit() |
private void |
setClassAxiomInstantiation(RuleSetDispatchFeature d) |
private void |
setupApplyEq(RuleSetDispatchFeature d,
IntegerLDT numbers) |
private RuleSetDispatchFeature |
setupApprovalDispatcher() |
protected Feature |
setupApprovalF() |
private void |
setupArithPrimaryCategories(RuleSetDispatchFeature d) |
private void |
setupClassAxiomApproval(RuleSetDispatchFeature d) |
private RuleSetDispatchFeature |
setupCostComputationF() |
private void |
setupDefOpsExpandMod(RuleSetDispatchFeature d) |
private void |
setupDefOpsPrimaryCategories(RuleSetDispatchFeature d) |
private void |
setupDivModDivision(RuleSetDispatchFeature d) |
private void |
setupFormulaNormalisation(RuleSetDispatchFeature d,
IntegerLDT numbers,
LocSetLDT locSetLDT) |
protected Feature |
setupGlobalF(Feature dispatcher) |
private void |
setupInEqCaseDistinctions(RuleSetDispatchFeature d) |
private void |
setupInEqCaseDistinctionsApproval(RuleSetDispatchFeature d) |
private void |
setupInEqSimp(RuleSetDispatchFeature d,
IntegerLDT numbers) |
private void |
setupInEqSimpInstantiation(RuleSetDispatchFeature d) |
private void |
setupInEqSimpInstantiationWithoutRetry(RuleSetDispatchFeature d) |
private RuleSetDispatchFeature |
setupInstantiationF() |
private void |
setupInstantiationWithoutRetry(RuleSetDispatchFeature d)
For taclets that need instantiation, but where the instantiation is
deterministic and does not have to be repeated at a later point, we setup
the same feature terms both in the cost computation method and in the
instantiation method.
|
private void |
setupMultiplyInequations(RuleSetDispatchFeature d,
Feature notAllowedF) |
private void |
setupNewSymApproval(RuleSetDispatchFeature d,
IntegerLDT numbers) |
private void |
setupNonLinTermIsPosNeg(RuleSetDispatchFeature d,
java.lang.String ruleSet,
boolean pos) |
private void |
setupPolySimp(RuleSetDispatchFeature d,
IntegerLDT numbers) |
private void |
setupPolySimpInstantiationWithoutRetry(RuleSetDispatchFeature d) |
private void |
setupPullOutGcd(RuleSetDispatchFeature d,
java.lang.String ruleSet,
boolean roundingUp) |
private void |
setupQuantifierInstantiation(RuleSetDispatchFeature d) |
private void |
setupQuantifierInstantiationApproval(RuleSetDispatchFeature d) |
private void |
setupReplaceKnown(RuleSetDispatchFeature d) |
private void |
setupSelectSimplification(RuleSetDispatchFeature d) |
private void |
setupSplitting(RuleSetDispatchFeature d) |
private void |
setupSplittingApproval(RuleSetDispatchFeature d) |
private void |
setupSquaresAreNonNegative(RuleSetDispatchFeature d) |
private void |
setUpStringNormalisation(RuleSetDispatchFeature d) |
private void |
setupSystemInvariantSimp(RuleSetDispatchFeature d) |
private void |
setupUserTaclets(RuleSetDispatchFeature d) |
private Feature |
succIntEquationExists() |