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