| Interface | Description |
|---|---|
| Constraint | Deprecated |
| Trigger |
| Class | Description |
|---|---|
| BasicMatching | |
| ClausesGraph |
This class describes the relation between different clauses in a CNF.
|
| ClausesSmallerThanFeature |
Ordering used to sort the clauses in a quantified formula.
|
| Constraint.Top | Deprecated |
| ConstraintAwareSyntacticalReplaceVisitor |
In KeY 1.x we supported a free variable calculus based on meta variables.
|
| EliminableQuantifierTF | |
| EqualityConstraint | Deprecated |
| EqualityConstraint.ECPair | |
| ExistentiallyConnectedFormulasFeature |
Binary feature that return zero if two given projection term is CS-Releated.
|
| HandleArith |
This class is used to prove some simple arithmetic problem which are
a==b, a>=b, a<=b; Besides it can be used to prove that a>=b or a<=b by
knowing that c>=d or c<=d;
|
| HeuristicInstantiation | |
| Instantiation | |
| InstantiationCost |
Feature that returns the number of branches after instantiated the quantifier
formula.
|
| InstantiationCostScalerFeature | |
| LiteralsSmallerThanFeature | |
| Matching |
Two kind of matching algorithm are coded in two nested classes BaseMatching
TwosideMatching
|
| Metavariable | Deprecated |
| MultiTrigger | |
| PredictCostProver |
TODO: rewrite, this seems pretty inefficient ...
|
| QuanEliminationAnalyser | |
| RecAndExistentiallyConnectedClausesFeature |
Binary Term Feature return zero if root is a CNF quantifier formula with several
clauses.
|
| ReplacerOfQuanVariablesWithMetavariables | Deprecated |
| SplittableQuantifiedFormulaFeature | |
| SplittableQuantifiedFormulaFeature.Analyser | |
| Substitution |
This class decribes a substitution,which store a map(varMap) from quantifiable
variable to a term(instance).
|
| TriggersSet |
This class is used to select and store
Triggers
for a quantified formula in Prenex CNF(PCNF). |
| TriggerUtils | |
| TwoSidedMatching |
Matching triggers within another quantifier expression.
|
| UniTrigger |