abstract class ReplaceAndRegisterMethod
extends java.lang.Object
Modifier and Type | Class and Description |
---|---|
private static class |
ReplaceAndRegisterMethod.QuantifiableVariableVisitor |
Constructor and Description |
---|
ReplaceAndRegisterMethod() |
Modifier and Type | Method and Description |
---|---|
(package private) static java.util.HashSet<QuantifiableVariable> |
collectQuantifiableVariables(Term term) |
(package private) void |
register(Function f,
Services services) |
(package private) void |
register(ImmutableList<ProgramVariable> pvs,
Services services) |
(package private) void |
register(ProgramVariable pv,
Services services) |
(package private) InfFlowSpec[] |
replace(ImmutableList<InfFlowSpec> termss,
StateVars origVars,
StateVars poVars,
TermBuilder tb) |
(package private) InfFlowSpec |
replace(InfFlowSpec terms,
StateVars origVars,
StateVars poVars,
TermBuilder tb) |
(package private) Term[] |
replace(Term[] terms,
StateVars origVars,
StateVars poVars,
TermBuilder tb) |
(package private) Term |
replace(Term term,
ProofObligationVars origVars,
ProofObligationVars poVars,
TermBuilder tb) |
(package private) Term |
replace(Term term,
StateVars origVars,
StateVars poVars,
TermBuilder tb) |
(package private) Term |
replace(Term term,
Term[] origVars,
Term[] poVars,
TermBuilder tb) |
(package private) static Term |
replaceQuantifiableVariables(Term term,
java.util.HashSet<QuantifiableVariable> qvs,
Services services) |
final Term replace(Term term, ProofObligationVars origVars, ProofObligationVars poVars, TermBuilder tb)
final Term replace(Term term, StateVars origVars, StateVars poVars, TermBuilder tb)
final Term[] replace(Term[] terms, StateVars origVars, StateVars poVars, TermBuilder tb)
final InfFlowSpec replace(InfFlowSpec terms, StateVars origVars, StateVars poVars, TermBuilder tb)
final InfFlowSpec[] replace(ImmutableList<InfFlowSpec> termss, StateVars origVars, StateVars poVars, TermBuilder tb)
final Term replace(Term term, Term[] origVars, Term[] poVars, TermBuilder tb)
final void register(ProgramVariable pv, Services services)
final void register(ImmutableList<ProgramVariable> pvs, Services services)
static final Term replaceQuantifiableVariables(Term term, java.util.HashSet<QuantifiableVariable> qvs, Services services)
static final java.util.HashSet<QuantifiableVariable> collectQuantifiableVariables(Term term)