de.uka.ilkd.key.strategy.quantifierHeuristics
Interfaces
Constraint
Trigger
Classes
BasicMatching
ClausesGraph
ClausesSmallerThanFeature
Constraint.Top
ConstraintAwareSyntacticalReplaceVisitor
EliminableQuantifierTF
EqualityConstraint
EqualityConstraint.ECPair
ExistentiallyConnectedFormulasFeature
HandleArith
HeuristicInstantiation
Instantiation
InstantiationCost
InstantiationCostScalerFeature
LiteralsSmallerThanFeature
Matching
Metavariable
MultiTrigger
PredictCostProver
QuanEliminationAnalyser
RecAndExistentiallyConnectedClausesFeature
ReplacerOfQuanVariablesWithMetavariables
SplittableQuantifiedFormulaFeature
SplittableQuantifiedFormulaFeature.Analyser
Substitution
TriggersSet
TriggerUtils
TwoSidedMatching
UniTrigger