Package | Description |
---|---|
de.uka.ilkd.key.logic |
provides a representation for the term and sequent
structure.
|
de.uka.ilkd.key.proof.io |
Classes related to loading and saving proof files.
|
de.uka.ilkd.key.proof.io.intermediate | |
de.uka.ilkd.key.strategy |
This package contains classes implementing the proof search strategies of KeY.
|
de.uka.ilkd.key.strategy.termProjection | |
de.uka.ilkd.key.symbolic_execution.util |
Modifier and Type | Method and Description |
---|---|
PosInTerm |
PosInTerm.down(int i)
returns the position for the
i -th subterm of the subterm described by this position |
PosInTerm |
PosInTerm.firstN(int n)
returns the position of the
depth-n parent term |
static PosInTerm |
PosInTerm.getTopLevel()
returns the instance representing the top level position
|
static PosInTerm |
PosInTerm.parseReverseString(java.lang.String s)
create a position from the string
The string contains a comma separated list of integers.
|
PosInTerm |
PosInOccurrence.posInTerm()
The usage of this method is strongly discouraged, use
PosInOccurrence.iterator() instead. |
PosInTerm |
PosInTerm.up()
returns the position of the enclosing term
|
Modifier and Type | Method and Description |
---|---|
static PosInOccurrence |
PosInOccurrence.findInSequent(Sequent seq,
int formulaNumber,
PosInTerm pos) |
boolean |
PosInTerm.isPrefixOf(PosInTerm pit)
Checks whether this pit is the prefix of a given pit.
|
Term |
TermBuilder.replace(Term term,
PosInTerm pos,
Term replacement)
Replaces a child term by another one.
|
Constructor and Description |
---|
PiTIterator(PosInTerm p,
boolean order) |
PosInOccurrence(SequentFormula sequentFormula,
PosInTerm posInTerm,
boolean inAntec) |
Modifier and Type | Method and Description |
---|---|
static java.lang.String |
OutputStreamProofSaver.posInTerm2Proof(PosInTerm pos) |
Modifier and Type | Method and Description |
---|---|
ImmutableList<Pair<java.lang.Integer,PosInTerm>> |
BuiltInAppIntermediate.getBuiltInIfInsts() |
Pair<java.lang.Integer,PosInTerm> |
BuiltInAppIntermediate.getPosInfo() |
Pair<java.lang.Integer,PosInTerm> |
TacletAppIntermediate.getPosInfo() |
Constructor and Description |
---|
BuiltInAppIntermediate(java.lang.String ruleName,
Pair<java.lang.Integer,PosInTerm> pos,
java.lang.String contract,
ImmutableList<Pair<java.lang.Integer,PosInTerm>> builtInIfInsts,
ImmutableList<Name> newNames) |
BuiltInAppIntermediate(java.lang.String ruleName,
Pair<java.lang.Integer,PosInTerm> pos,
java.lang.String contract,
ImmutableList<Pair<java.lang.Integer,PosInTerm>> builtInIfInsts,
ImmutableList<Name> newNames) |
MergeAppIntermediate(java.lang.String ruleName,
Pair<java.lang.Integer,PosInTerm> pos,
int id,
java.lang.String joinProc,
int nrPartners,
ImmutableList<Name> newNames,
java.lang.String distinguishingFormula,
java.lang.Class<? extends AbstractPredicateAbstractionLattice> predAbstrLatticeType,
java.lang.String abstractionPredicates,
java.lang.String userChoices)
Constructs a new join rule.
|
MergePartnerAppIntermediate(java.lang.String ruleName,
Pair<java.lang.Integer,PosInTerm> pos,
int mergeNodeId,
ImmutableList<Name> newNames)
Constructs a new close-merge-partner intermediate application.
|
TacletAppIntermediate(java.lang.String tacletName,
Pair<java.lang.Integer,PosInTerm> posInfo,
java.util.LinkedList<java.lang.String> insts,
ImmutableList<java.lang.String> ifSeqFormulaList,
ImmutableList<java.lang.String> ifDirectFormulaList,
ImmutableList<Name> newNames)
Constructs a new intermediate taclet application.
|
Modifier and Type | Method and Description |
---|---|
protected static ProjectionToTerm |
StaticFeatureCollection.subAt(ProjectionToTerm t,
PosInTerm pit) |
Modifier and Type | Method and Description |
---|---|
static ProjectionToTerm |
SubtermProjection.create(ProjectionToTerm completeTerm,
PosInTerm pit) |
Modifier and Type | Method and Description |
---|---|
static PosInTerm |
SymbolicExecutionUtil.findModalityWithMaxSymbolicExecutionLabelId(Term term)
Searches the modality
PosInTerm with the maximal SymbolicExecutionTermLabel ID
SymbolicExecutionTermLabel.getId() in the given Term . |
static PosInTerm |
SymbolicExecutionUtil.findModalityWithMinSymbolicExecutionLabelId(Term term)
Searches the modality
PosInTerm with the minimal SymbolicExecutionTermLabel ID
SymbolicExecutionTermLabel.getId() in the given Term . |
Copyright © 2003-2019 The KeY-Project.