public class OpReplacer
extends java.lang.Object
Constructor and Description |
---|
OpReplacer(java.util.Map<? extends SVSubstitute,? extends SVSubstitute> map,
TermFactory tf)
Creates an
OpReplacer . |
OpReplacer(java.util.Map<? extends SVSubstitute,? extends SVSubstitute> map,
TermFactory tf,
Proof proof)
Creates an
OpReplacer . |
Modifier and Type | Method and Description |
---|---|
ImmutableArray<QuantifiableVariable> |
replace(ImmutableArray<QuantifiableVariable> vars)
Replaces in an ImmutableArray
|
ImmutableList<Term> |
replace(ImmutableList<Term> terms)
Replaces in a list of terms.
|
ImmutableSet<Term> |
replace(ImmutableSet<Term> terms)
Replaces in a set of terms.
|
java.util.Map<Operator,Term> |
replace(java.util.Map<Operator,Term> myMap)
Replaces in a map from Operator to Term.
|
Operator |
replace(Operator op)
Replaces in an operator.
|
static Term |
replace(Operator toReplace,
Operator with,
Term in,
TermFactory tf)
Replace an operator.
|
static Term |
replace(Operator toReplace,
Operator with,
Term in,
TermFactory tf,
Proof proof)
Replace an operator.
|
Term |
replace(Term term)
Replaces in a term.
|
static ImmutableList<Term> |
replace(Term toReplace,
Term with,
ImmutableList<Term> in,
TermFactory tf)
Replace a sub-term.
|
static ImmutableList<Term> |
replace(Term toReplace,
Term with,
ImmutableList<Term> in,
TermFactory tf,
Proof proof)
Replace a sub-term.
|
static Term |
replace(Term toReplace,
Term with,
Term in,
TermFactory tf)
Replace a sub-term.
|
static Term |
replace(Term toReplace,
Term with,
Term in,
TermFactory tf,
Proof proof)
Replace a sub-term.
|
ImmutableList<InfFlowSpec> |
replaceInfFlowSpec(ImmutableList<InfFlowSpec> terms)
Replaces in a list of triples of lists of terms.
|
public OpReplacer(java.util.Map<? extends SVSubstitute,? extends SVSubstitute> map, TermFactory tf)
Creates an OpReplacer
.
If there is a proof currently loaded, you may want to use
OpReplacer(Map, TermFactory, Proof)
as it correctly deals with
OriginTermLabels
and other proof-dependent features.
map
- map mapping from the operators/terms to be replaced to the ones to
replace them withtf
- a term factory.public OpReplacer(java.util.Map<? extends SVSubstitute,? extends SVSubstitute> map, TermFactory tf, Proof proof)
OpReplacer
.map
- map mapping from the operators/terms to be replaced to the ones to
replace them with.tf
- a term factory.proof
- the currently loaded proofpublic static Term replace(Term toReplace, Term with, Term in, TermFactory tf)
Replace a sub-term.
If there is a proof currently loaded, you may want to use
replace(Operator, Operator, Term, TermFactory, Proof)
as it correctly deals with
OriginTermLabels
and other proof-dependent features.
toReplace
- the sub-term to replace.with
- the replacement sub-term.in
- the term in which to perform the replacement.tf
- a term factory.public static ImmutableList<Term> replace(Term toReplace, Term with, ImmutableList<Term> in, TermFactory tf)
Replace a sub-term.
If there is a proof currently loaded, you may want to use
replace(Term, Term, ImmutableList, TermFactory, Proof)
as it correctly deals with
OriginTermLabels
and other proof-dependent features.
toReplace
- the sub-term to replace.with
- the replacement sub-term.in
- the terms in which to perform the replacement.tf
- a term factory.public static Term replace(Operator toReplace, Operator with, Term in, TermFactory tf)
Replace an operator.
If there is a proof currently loaded, you may want to use
replace(Operator, Operator, Term, TermFactory, Proof)
as it correctly deals with
OriginTermLabels
and other proof-dependent features.
toReplace
- the operator to replace.with
- the replacement operator.in
- the term in which to perform the replacement.tf
- a term factory.public static Term replace(Term toReplace, Term with, Term in, TermFactory tf, Proof proof)
Replace a sub-term.
toReplace
- the sub-term to replace.with
- the replacement sub-term.in
- the term in which to perform the replacement.tf
- a term factory.proof
- the currently loaded proof.public static ImmutableList<Term> replace(Term toReplace, Term with, ImmutableList<Term> in, TermFactory tf, Proof proof)
Replace a sub-term.
toReplace
- the sub-term to replace.with
- the replacement sub-term.in
- the terms in which to perform the replacement.tf
- a term factory.proof
- the currently loaded proof.public static Term replace(Operator toReplace, Operator with, Term in, TermFactory tf, Proof proof)
Replace an operator.
toReplace
- the operator to replace.with
- the replacement operator.in
- the term in which to perform the replacement.tf
- a term factory.proof
- the currently loaded proof.public Operator replace(Operator op)
op
- the operator in which to perform the replacement.public Term replace(Term term)
term
- the term in which to perform the replacement.public ImmutableList<Term> replace(ImmutableList<Term> terms)
terms
- the terms in which to perform the replacement.public ImmutableList<InfFlowSpec> replaceInfFlowSpec(ImmutableList<InfFlowSpec> terms)
terms
- the terms in which to perform the replacement.public ImmutableSet<Term> replace(ImmutableSet<Term> terms)
terms
- the terms in which to perform the replacement.public java.util.Map<Operator,Term> replace(java.util.Map<Operator,Term> myMap)
myMap
- the map in which to perform the replacement.public ImmutableArray<QuantifiableVariable> replace(ImmutableArray<QuantifiableVariable> vars)
vars
- the array in which to perform the replacement.Copyright © 2003-2019 The KeY-Project.