S
- the type of the elements to replace.T
- the type of the replacements.public interface ReplacementMap<S extends SVSubstitute,T>
extends java.util.Map<S,T>
OpReplacer
.
It maps operators that should be replaced to their replacements.Modifier and Type | Interface and Description |
---|---|
static class |
ReplacementMap.DefaultReplacementMap<S extends SVSubstitute,T>
The replacement map type to use if
TermLabelSettings.getUseOriginLabels() is false. |
static class |
ReplacementMap.NoIrrelevantLabelsReplacementMap<S extends SVSubstitute,T>
The replacement map type to use if
TermLabelSettings.getUseOriginLabels() is true. |
Modifier and Type | Method and Description |
---|---|
static <S extends SVSubstitute,T> |
create(TermFactory tf,
Proof proof)
Creates a new replacement map.
|
static <S extends SVSubstitute,T> |
create(TermFactory tf,
Proof proof,
java.util.Map<S,T> initialMappings)
Creates a new replacement map.
|
static <S extends SVSubstitute,T> ReplacementMap<S,T> create(TermFactory tf, Proof proof)
S
- the type of the elements to replace.T
- the type of the replacements.tf
- a term factory.proof
- the currently loaded proof, or null
if no proof is loaded.static <S extends SVSubstitute,T> ReplacementMap<S,T> create(TermFactory tf, Proof proof, java.util.Map<S,T> initialMappings)
S
- the type of the elements to replace.T
- the type of the replacements.tf
- a term factory.proof
- the currently loaded proof, or null
if no proof is loaded.initialMappings
- a map whose mapping should be added to the new replacement map.Copyright © 2003-2019 The KeY-Project.