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
Trigger s
for a quantified formula in Prenex CNF(PCNF). |
TriggerUtils | |
TwoSidedMatching |
Matching triggers within another quantifier expression.
|
UniTrigger |