Modifier and Type | Class and Description |
---|---|
class |
BooleanLattice
A simple lattice for booleans.
|
Modifier and Type | Class and Description |
---|---|
class |
AbstractPredicateAbstractionLattice
A super class for predicates abstraction lattices.
|
class |
ConjunctivePredicateAbstractionLattice
A lattice for all predicates accepting the given sort.
|
class |
DisjunctivePredicateAbstractionLattice
A lattice for all predicates accepting the given sort.
|
class |
SimplePredicateAbstractionLattice
A lattice for all predicates accepting the given sort.
|
Modifier and Type | Class and Description |
---|---|
class |
SignAnalysisLattice
A lattice for sign analysis of integers.
|
Modifier and Type | Method and Description |
---|---|
protected abstract AbstractDomainLattice |
MergeWithLatticeAbstraction.getAbstractDomainForSort(Sort s,
Services services)
Returns the abstract domain lattice for the given sort or null if there
has no lattice been specified for that sort.
|
AbstractDomainLattice |
MergeWithPredicateAbstraction.getAbstractDomainForSort(Sort s,
Services services) |
static AbstractDomainLattice |
MergeWithPredicateAbstraction.instantiateAbstractDomain(Sort s,
java.util.List<AbstractionPredicate> applicablePredicates,
java.lang.Class<? extends AbstractPredicateAbstractionLattice> latticeType,
Services services)
Instantiates the abstract domain lattice for the given sort or null if
there has no lattice been specified for that sort.
|
Copyright © 2003-2019 The KeY-Project.