Package | Description |
---|---|
de.uka.ilkd.key.gui.smt |
This package contains the graphical user interface of the SMT backend.
|
de.uka.ilkd.key.logic |
provides a representation for the term and sequent
structure.
|
de.uka.ilkd.key.proof |
This package contains the core data structures of proofs, nodes, goals, as well
as machinery to deal with these data structures.
|
de.uka.ilkd.key.rule |
This package contains classes for implementing rules.
|
de.uka.ilkd.key.strategy.quantifierHeuristics | |
de.uka.ilkd.key.symbolic_execution.util | |
de.uka.ilkd.key.taclettranslation |
Modifier and Type | Class and Description |
---|---|
protected static class |
SolverListener.ContainsModalityOrQueryVisitor
Utility class used to check whether a term contains constructs that are not handled by the SMT translation.
|
Modifier and Type | Class and Description |
---|---|
class |
BoundVarsVisitor
Visitor traversing a term and collecting all variables that occur bound.
|
static class |
ClashFreeSubst.VariableCollectVisitor
A Visitor class to collect all (not just the free) variables
occurring in a term.
|
class |
DefaultVisitor
This abstract Vistor class declares the interface for a common term visitor.
|
class |
OpCollector
Collects all operators occurring in the traversed term.
|
class |
SortCollector |
Modifier and Type | Method and Description |
---|---|
void |
TermImpl.execPostOrder(Visitor visitor) |
void |
Term.execPostOrder(Visitor visitor)
The visitor is handed through till the bottom of the tree and
then it walks upwards, while at each upstep the method visit of
the visitor is called.
|
void |
TermImpl.execPreOrder(Visitor visitor) |
void |
Term.execPreOrder(Visitor visitor)
The visitor walks downwards the tree, while at each downstep the method
visit of the visitor is called.
|
Modifier and Type | Class and Description |
---|---|
class |
TermProgramVariableCollector |
class |
TermProgramVariableCollectorKeepUpdatesForBreakpointconditions |
Modifier and Type | Class and Description |
---|---|
class |
LightweightSyntacticalReplaceVisitor
A lightweight version of
SyntacticalReplaceVisitor which does not
replace labels. |
class |
SVNameCorrespondenceCollector
This visitor is used to collect information about schema variable
pairs occurring within the same substitution operator within a
taclet.
|
class |
SyntacticalReplaceVisitor |
class |
TacletSchemaVariableCollector
Collects all schemavariables occurring in the
\find, \assumes part or goal description of a taclet. |
class |
TacletVariableSVCollector
This class is used to collect all appearing SchemaVariables that are bound in a
Taclet.
|
Modifier and Type | Class and Description |
---|---|
class |
ConstraintAwareSyntacticalReplaceVisitor
In KeY 1.x we supported a free variable calculus based on meta variables.
|
Modifier and Type | Class and Description |
---|---|
protected static class |
SymbolicExecutionSideProofUtil.ContainsIrrelevantThingsVisitor
Utility class used by
QuerySideProofRule#containsIrrelevantThings(Services, SequentFormula, Set) . |
protected static class |
SymbolicExecutionSideProofUtil.ContainsModalityOrQueryVisitor
Utility method used by
QuerySideProofRule#containsModalityOrQuery(Term) . |
Modifier and Type | Class and Description |
---|---|
class |
TacletVisitor |
Copyright © 2003-2019 The KeY-Project.