public class TermBuilder
extends java.lang.Object
Use this class if you intend to build complex terms by hand. It is more convenient than the @link{TermFactory} class.
Attention: some methods of this class try to simplify some terms. So if you want to be sure that the term looks exactly as you built it, you will have to use the TermFactory.
Modifier and Type | Field and Description |
---|---|
protected Services |
services |
static Transformer |
WD_ANY |
static Transformer |
WD_FORMULA |
Constructor and Description |
---|
TermBuilder(TermFactory tf,
Services services) |
Modifier and Type | Method and Description |
---|---|
Term |
acc(Term h,
Term s,
Term o1,
Term o2) |
Term |
add(Term t1,
Term t2) |
Term |
addLabel(Term term,
ImmutableArray<TermLabel> labels)
Adds labels to a term, removing any existing labels of the same type.
|
Term |
addLabel(Term term,
TermLabel label)
Adds a label to a term, removing any existing labels of the same type.
|
Term |
addLabelToAllSubs(Term term,
ImmutableArray<TermLabel> labels)
Applies the labels to the term and almost every (direct or indirect) sub-term recursively.
|
Term |
addLabelToAllSubs(Term term,
TermLabel label)
Applies the label to the term and almost every (direct or indirect) sub-term recursively.
|
Term |
all(java.lang.Iterable<QuantifiableVariable> qvs,
Term t) |
Term |
all(QuantifiableVariable qv,
Term t) |
Term |
allClose(Term t) |
Term |
allFields(Term o) |
Term |
allLocs() |
Term |
allObjects(Term f) |
Term |
and(java.lang.Iterable<Term> subTerms) |
Term |
and(Term... subTerms) |
Term |
and(Term t1,
Term t2) |
Term |
andPreserveLabels(java.lang.Iterable<Term> subTerms)
Similar behavior as
and(Iterable) but simplifications are not
performed if TermLabel s would be lost. |
Term |
andPreserveLabels(Term t1,
Term t2)
Similar behavior as
and(Term, Term) but simplifications are not
performed if TermLabel s would be lost. |
Term |
andSC(java.lang.Iterable<Term> subTerms) |
Term |
andSC(Term... subTerms) |
Term |
andSC(Term t1,
Term t2) |
Term |
anon(Term h1,
Term s,
Term h2) |
Term |
anonUpd(LocationVariable heap,
Term mod,
Term anonHeap) |
ImmutableList<Term> |
apply(Term update,
ImmutableList<Term> targets) |
Term |
apply(Term update,
Term target) |
Term |
apply(Term update,
Term target,
ImmutableArray<TermLabel> labels) |
ImmutableList<Term> |
applyElementary(Term heap,
java.lang.Iterable<Term> targets) |
Term |
applyElementary(Term heap,
Term target) |
Term |
applyElementary(Term loc,
Term value,
Term target) |
Term |
applyParallel(ImmutableList<Term> updates,
Term target) |
Term |
applyParallel(Term[] updates,
Term target) |
Term |
applyParallel(Term[] lhss,
Term[] values,
Term target) |
Term |
applySequential(ImmutableList<Term> updates,
Term target) |
Term |
applySequential(Term[] updates,
Term target) |
Term |
applyUpdatePairsSequential(ImmutableList<SVInstantiations.UpdateLabelPair> updates,
Term target) |
Term |
arr(Term idx) |
Term |
arrayRange(Term o,
Term lower,
Term upper) |
Term |
arrayStore(Term o,
Term i,
Term v) |
Term |
box(JavaBlock jb,
Term t) |
Term |
bprod(QuantifiableVariable qv,
Term a,
Term b,
Term t,
Services services)
Constructs a bounded product comprehension expression.
|
Term |
bsum(QuantifiableVariable qv,
Term a,
Term b,
Term t) |
Term |
cast(Sort s,
Term t) |
Term |
classErroneous(Sort classSort) |
Term |
classInitializationInProgress(Sort classSort) |
Term |
classInitialized(Sort classSort) |
Term |
classPrepared(Sort classSort) |
Term |
convertToBoolean(Term a)
For a formula a, convert it to a boolean expression.
|
Term |
convertToFormula(Term a)
If a is a boolean literal, the method returns the literal as a Formula.
|
Term |
create(Term h,
Term o) |
Term |
created(Term o) |
Term |
created(Term h,
Term o) |
Term |
createdInHeap(Term s,
Term h) |
Term |
createdLocs() |
Term |
cTerm(java.lang.String numberString) |
Term |
deepNonNull(Term o,
Term d)
The "deep non null" predicate arising from JML non_null types.
|
Term |
dia(JavaBlock jb,
Term t) |
Term |
disjoint(Term s1,
Term s2) |
Term |
dot(Sort asSort,
Term o,
Function f) |
Term |
dot(Sort asSort,
Term o,
LocationVariable field) |
Term |
dot(Sort asSort,
Term o,
Term f) |
Term |
dotArr(Term ref,
Term idx) |
Term |
dotLength(Term a) |
Term |
elementary(Term lhs,
Term rhs) |
Term |
elementary(UpdateableOperator lhs,
Term rhs) |
Term |
elementOf(Term o,
Term f,
Term s) |
Term |
empty() |
Term |
equals(Term t1,
Term t2)
Creates a term with the correct equality symbol for the sorts involved
|
Term |
ex(java.lang.Iterable<QuantifiableVariable> qvs,
Term t) |
Term |
ex(QuantifiableVariable qv,
Term t) |
Term |
exactInstance(Sort s,
Term t) |
LocationVariable |
excVar(IProgramMethod pm,
boolean makeNameUnique)
Creates a program variable for the thrown exception.
|
LocationVariable |
excVar(java.lang.String name,
IProgramMethod pm,
boolean makeNameUnique)
Creates a program variable for the thrown exception.
|
Term |
FALSE() |
Term |
ff() |
Term |
fieldStore(TermServices services,
Term o,
Function f,
Term v) |
Term |
forallHeaps(Services services,
Term t) |
Term |
frame(Term heapTerm,
java.util.Map<Term,Term> normalToAtPre,
Term mod) |
Term |
frameStrictlyEmpty(Term heapTerm,
java.util.Map<Term,Term> normalToAtPre)
Returns the framing condition that the resulting heap is identical (i.e.
|
Term |
freshLocs(Term h) |
Term |
func(Function f) |
Term |
func(Function f,
Term... s) |
Term |
func(Function f,
Term s) |
Term |
func(Function f,
Term[] s,
ImmutableArray<QuantifiableVariable> boundVars) |
Term |
func(Function f,
Term s1,
Term s2) |
Term |
func(IObserverFunction f,
Term... s) |
Term |
geq(Term t1,
Term t2) |
Term |
getBaseHeap() |
Function |
getMeasuredByEmpty() |
ImmutableList<Sort> |
getSorts(java.lang.Iterable<Term> terms)
|
static Term |
goBelowUpdates(Term term)
Removes leading updates from the passed term.
|
static Pair<ImmutableList<Term>,Term> |
goBelowUpdates2(Term term)
Removes leading updates from the passed term.
|
Term |
gt(Term t1,
Term t2) |
LocationVariable |
heapAtPreVar(java.lang.String baseName,
boolean makeNameUnique)
Creates a program variable for the atPre heap.
|
LocationVariable |
heapAtPreVar(java.lang.String baseName,
Sort sort,
boolean makeNameUnique)
Creates a program variable for the atPre heap.
|
Term |
ife(Term cond,
Term _then,
Term _else) |
Term |
ifEx(ImmutableList<QuantifiableVariable> qvs,
Term cond,
Term _then,
Term _else)
Construct a term with the \ifEx operator.
|
Term |
ifEx(QuantifiableVariable qv,
Term cond,
Term _then,
Term _else)
Construct a term with the \ifEx operator.
|
Term |
imp(Term t1,
Term t2) |
Term |
imp(Term t1,
Term t2,
ImmutableArray<TermLabel> labels) |
Term |
impPreserveLabels(Term t1,
Term t2)
Similar behavior as
imp(Term, Term) but simplifications are not
performed if TermLabel s would be lost. |
Term |
inByte(Term var) |
Term |
inChar(Term var) |
Term |
index() |
Term |
indexOf(Term s,
Term x)
Function representing the least index of an element x in a sequence s (or
underspecified)
|
Term |
infiniteUnion(QuantifiableVariable[] qvs,
Term s) |
Term |
infiniteUnion(QuantifiableVariable[] qvs,
Term guard,
Term s) |
Term |
inInt(Term var) |
Term |
initialized(Term o) |
Term |
inLong(Term var) |
Term |
inShort(Term var) |
Term |
instance(Sort s,
Term t) |
Term |
intersect(java.lang.Iterable<Term> subTerms) |
Term |
intersect(Term... subTerms) |
Term |
intersect(Term s1,
Term s2) |
Term |
inv(Term o) |
Term |
inv(Term[] h,
Term o) |
Term |
label(Term term,
ImmutableArray<TermLabel> labels)
Applies labels to a term, removing any existing labels.
|
Term |
label(Term term,
TermLabel label)
Applies a label to a term, removing any existing labels.
|
Term |
leq(Term t1,
Term t2) |
Term |
lt(Term t1,
Term t2) |
Term |
max(ImmutableList<? extends QuantifiableVariable> qvs,
Term range,
Term t,
TermServices services)
minimum operator
|
Term |
measuredBy(Term mby) |
Term |
measuredByCheck(Term mby) |
Term |
measuredByEmpty() |
Term |
min(ImmutableList<? extends QuantifiableVariable> qvs,
Term range,
Term t,
TermServices services)
minimum operator
|
java.lang.String |
newName(Sort sort)
Returns an available name constructed by affixing a counter to a self-
chosen base name for the passed sort.
|
java.lang.String |
newName(java.lang.String baseName)
Returns an available name constructed by affixing a counter to the passed
base name.
|
java.lang.String |
newName(java.lang.String baseName,
NamespaceSet localNamespace)
Returns an available name constructed by affixing a counter to the passed
base name.
|
Term |
not(Term t) |
Term |
notPreserveLabels(Term t)
|
Term |
NULL() |
Term |
one() |
Term |
open(Term formula)
Removes universal quantifiers from a formula.
|
Term |
or(java.lang.Iterable<Term> subTerms) |
Term |
or(Term... subTerms) |
Term |
or(Term t1,
Term t2) |
Term |
orPreserveLabels(java.lang.Iterable<Term> subTerms)
Similar behavior as
or(Iterable) but simplifications are not
performed if TermLabel s would be lost. |
Term |
orPreserveLabels(Term t1,
Term t2)
Similar behavior as
or(Term, Term) but simplifications are not
performed if TermLabel s would be lost. |
Term |
orSC(java.lang.Iterable<Term> subTerms) |
Term |
orSC(Term... subTerms) |
Term |
orSC(Term t1,
Term t2) |
Term |
pair(Term first,
Term second) |
Term |
parallel(ImmutableList<Term> updates) |
Term |
parallel(java.lang.Iterable<Term> lhss,
java.lang.Iterable<Term> values) |
Term |
parallel(Term... updates) |
Term |
parallel(Term[] lhss,
Term[] values) |
Term |
parallel(Term u1,
Term u2) |
ImmutableList<ProgramVariable> |
paramVars(IObserverFunction obs,
boolean makeNamesUnique)
Creates program variables for the parameters.
|
ImmutableList<ProgramVariable> |
paramVars(java.lang.String postfix,
IObserverFunction obs,
boolean makeNamesUnique)
Creates program variables for the parameters.
|
Term |
parseTerm(java.lang.String s)
Parses the given string that represents the term (or createTerm) using
the service's namespaces.
|
Term |
parseTerm(java.lang.String s,
NamespaceSet namespaces)
Parses the given string that represents the term (or createTerm) using
the provided namespaces.
|
Term |
permissionsFor(LocationVariable permHeap,
LocationVariable regularHeap) |
Term |
permissionsFor(Term permHeap,
Term regularHeap) |
Term |
prec(Term mby,
Term mbyAtPre) |
Term |
prod(ImmutableList<QuantifiableVariable> qvs,
Term range,
Term t,
TermServices services)
General (unbounded) product
|
Term |
prog(Modality mod,
JavaBlock jb,
Term t) |
Term |
prog(Modality mod,
JavaBlock jb,
Term t,
ImmutableArray<TermLabel> labels) |
Term |
reach(Term h,
Term s,
Term o1,
Term o2,
Term n) |
Term |
reachableValue(ProgramVariable pv) |
Term |
reachableValue(Term t,
KeYJavaType kjt) |
Term |
reachableValue(Term h,
Term t,
KeYJavaType kjt) |
Term |
replace(Term term,
PosInTerm pos,
Term replacement)
Replaces a child term by another one.
|
LocationVariable |
resultVar(IProgramMethod pm,
boolean makeNameUnique)
Creates a program variable for the result.
|
LocationVariable |
resultVar(java.lang.String name,
IProgramMethod pm,
boolean makeNameUnique)
Creates a program variable for the result with passed name.
|
Term |
select(Sort asSort,
Term h,
Term o,
LocationVariable field)
Get the select expression for a location variabe representing the field.
|
Term |
select(Sort asSort,
Term h,
Term o,
Term f) |
LocationVariable |
selfVar(IProgramMethod pm,
KeYJavaType kjt,
boolean makeNameUnique)
Creates a program variable for "self".
|
LocationVariable |
selfVar(IProgramMethod pm,
KeYJavaType kjt,
boolean makeNameUnique,
java.lang.String postfix)
Creates a program variable for "self".
|
LocationVariable |
selfVar(KeYJavaType kjt,
boolean makeNameUnique)
Creates a program variable for "self".
|
LocationVariable |
selfVar(KeYJavaType kjt,
boolean makeNameUnique,
java.lang.String postfix)
Creates a program variable for "self".
|
Term |
seq(ImmutableList<Term> terms) |
Term |
seq(Term... terms) |
Term |
seqConcat(Term s,
Term s2) |
Term |
seqDef(QuantifiableVariable qv,
Term a,
Term b,
Term t) |
Term |
seqEmpty() |
Term |
seqGet(Sort asSort,
Term s,
Term idx) |
Term |
seqLen(Term s) |
Term |
seqReverse(Term s) |
Term |
seqSingleton(Term x) |
Term |
seqSub(Term s,
Term from,
Term to) |
Term |
sequential(ImmutableList<Term> updates) |
Term |
sequential(Term[] updates) |
Term |
sequential(Term u1,
Term u2) |
Term |
setComprehension(QuantifiableVariable[] qvs,
Term o,
Term f) |
Term |
setComprehension(QuantifiableVariable[] qvs,
Term guard,
Term o,
Term f) |
Term |
setMinus(Term s1,
Term s2) |
java.lang.String |
shortBaseName(Sort s) |
Term |
shortcut(Term term) |
Term |
singleton(Term o,
Term f) |
Term |
skip() |
Term |
staticDot(Sort asSort,
Function f) |
Term |
staticDot(Sort asSort,
Term f) |
Term |
staticFieldStore(Function f,
Term v) |
Term |
staticInv(KeYJavaType t) |
Term |
staticInv(Term[] h,
KeYJavaType t) |
Term |
store(Term h,
Term o,
Term f,
Term v) |
Term |
strictlyNothing()
This value is only used as a marker for "\strictly_nothing" in JML.
|
Term |
subset(Term s1,
Term s2) |
Term |
subst(QuantifiableVariable substVar,
Term substTerm,
Term origTerm) |
Term |
subst(SubstOp op,
QuantifiableVariable substVar,
Term substTerm,
Term origTerm)
Creates a substitution term
|
Term |
sum(ImmutableList<QuantifiableVariable> qvs,
Term range,
Term t)
General (unbounded) sum
|
TermFactory |
tf() |
Term |
TRUE() |
Term |
tt() |
Term |
union(java.lang.Iterable<Term> subTerms) |
Term |
union(Term... subTerms) |
Term |
union(Term s1,
Term s2) |
ImmutableSet<Term> |
unionToSet(Term s) |
Term |
unlabel(Term term) |
Term |
unlabelRecursive(Term term) |
Term |
values() |
ImmutableList<Term> |
var(java.lang.Iterable<ProgramVariable> vs) |
Term |
var(LogicVariable v) |
Term |
var(ParsableVariable v) |
ImmutableList<Term> |
var(ProgramVariable... vs) |
Term |
var(ProgramVariable v) |
Term |
var(SchemaVariable v) |
ImmutableList<Term> |
wd(java.lang.Iterable<Term> l) |
Term |
wd(Term t) |
Term[] |
wd(Term[] l) |
Term |
wellFormed(LocationVariable heap) |
Term |
wellFormed(Term heap) |
Term |
zero() |
Term |
zTerm(long number) |
Term |
zTerm(java.lang.String numberString) |
protected final Services services
public static final Transformer WD_ANY
public static final Transformer WD_FORMULA
public TermBuilder(TermFactory tf, Services services)
public TermFactory tf()
public Term parseTerm(java.lang.String s) throws ParserException
s
- the String to parseParserException
public Term parseTerm(java.lang.String s, NamespaceSet namespaces) throws ParserException
s
- the String to parsenamespaces
- the namespaces used for name lookup.ParserException
public java.lang.String shortBaseName(Sort s)
public java.lang.String newName(java.lang.String baseName)
This method looks up the global NamespaceSet
to check whether the
Name
s is free. This can be problematic, since Namespace
s
are now local to goals. Use newName(String, NamespaceSet)
to
make sure that you have all the Name
s you need available.
baseName
- The base name (prefix) for the name to generate.newName(String, NamespaceSet)
public java.lang.String newName(java.lang.String baseName, NamespaceSet localNamespace)
Warning (DS): This method ignores the baseName if there are free name proposals. This can, for instance, cause troubles in loading proofs containing rule apps with more than one introduced (and saved) new name. In this case, the order of new names in the saved proof file matters (the first unused name is returned, regardless of the baseName).
baseName
- The base name (prefix) for the name to generate.localNamespace
- The local NamespaceSet
to check.public java.lang.String newName(Sort sort)
public LocationVariable selfVar(KeYJavaType kjt, boolean makeNameUnique)
public LocationVariable selfVar(KeYJavaType kjt, boolean makeNameUnique, java.lang.String postfix)
public LocationVariable selfVar(IProgramMethod pm, KeYJavaType kjt, boolean makeNameUnique, java.lang.String postfix)
public LocationVariable selfVar(IProgramMethod pm, KeYJavaType kjt, boolean makeNameUnique)
public ImmutableList<ProgramVariable> paramVars(IObserverFunction obs, boolean makeNamesUnique)
public ImmutableList<ProgramVariable> paramVars(java.lang.String postfix, IObserverFunction obs, boolean makeNamesUnique)
public LocationVariable resultVar(IProgramMethod pm, boolean makeNameUnique)
public LocationVariable resultVar(java.lang.String name, IProgramMethod pm, boolean makeNameUnique)
public LocationVariable excVar(IProgramMethod pm, boolean makeNameUnique)
public LocationVariable excVar(java.lang.String name, IProgramMethod pm, boolean makeNameUnique)
public LocationVariable heapAtPreVar(java.lang.String baseName, boolean makeNameUnique)
public LocationVariable heapAtPreVar(java.lang.String baseName, Sort sort, boolean makeNameUnique)
public Term var(LogicVariable v)
public Term var(ProgramVariable v)
public ImmutableList<Term> var(ProgramVariable... vs)
public ImmutableList<Term> var(java.lang.Iterable<ProgramVariable> vs)
public Term var(SchemaVariable v)
public Term var(ParsableVariable v)
public Term func(IObserverFunction f, Term... s)
public Term func(Function f, Term[] s, ImmutableArray<QuantifiableVariable> boundVars)
public Term ifEx(QuantifiableVariable qv, Term cond, Term _then, Term _else)
public Term ifEx(ImmutableList<QuantifiableVariable> qvs, Term cond, Term _then, Term _else)
public Term tt()
public Term ff()
public Term all(QuantifiableVariable qv, Term t)
public Term all(java.lang.Iterable<QuantifiableVariable> qvs, Term t)
public Term ex(QuantifiableVariable qv, Term t)
public Term ex(java.lang.Iterable<QuantifiableVariable> qvs, Term t)
public Term bsum(QuantifiableVariable qv, Term a, Term b, Term t)
public Term sum(ImmutableList<QuantifiableVariable> qvs, Term range, Term t)
public Term bprod(QuantifiableVariable qv, Term a, Term b, Term t, Services services)
public Term prod(ImmutableList<QuantifiableVariable> qvs, Term range, Term t, TermServices services)
public Term min(ImmutableList<? extends QuantifiableVariable> qvs, Term range, Term t, TermServices services)
public Term max(ImmutableList<? extends QuantifiableVariable> qvs, Term range, Term t, TermServices services)
public Term imp(Term t1, Term t2, ImmutableArray<TermLabel> labels)
public Term equals(Term t1, Term t2)
public Term subst(SubstOp op, QuantifiableVariable substVar, Term substTerm, Term origTerm)
substVar
- the QuantifiableVariable to be substitutedsubstTerm
- the Term that replaces substVarorigTerm
- the Term that is substitutedpublic Term subst(QuantifiableVariable substVar, Term substTerm, Term origTerm)
public Function getMeasuredByEmpty()
public Term measuredByEmpty()
public Term convertToFormula(Term a)
public Term convertToBoolean(Term a)
public Term elementary(UpdateableOperator lhs, Term rhs)
public Term skip()
public Term parallel(ImmutableList<Term> updates)
public Term sequential(ImmutableList<Term> updates)
public ImmutableList<Term> apply(Term update, ImmutableList<Term> targets)
public Term apply(Term update, Term target, ImmutableArray<TermLabel> labels)
public ImmutableList<Term> applyElementary(Term heap, java.lang.Iterable<Term> targets)
public Term applyParallel(ImmutableList<Term> updates, Term target)
public Term applySequential(ImmutableList<Term> updates, Term target)
public Term applyUpdatePairsSequential(ImmutableList<SVInstantiations.UpdateLabelPair> updates, Term target)
public Term TRUE()
public Term FALSE()
public Term zero()
public Term one()
public Term zTerm(java.lang.String numberString)
numberString
- String representing an integer with radix 10, may be negativejava.lang.NumberFormatException
- if numberString
is not a numberpublic Term zTerm(long number)
number
- an integerpublic Term cTerm(java.lang.String numberString)
numberString
- String containing the value of the char as a decimal numberjava.lang.NumberFormatException
- if numberString
is not a numberpublic Term index()
public Term strictlyNothing()
public Term empty()
public Term allLocs()
public Term infiniteUnion(QuantifiableVariable[] qvs, Term s)
public Term infiniteUnion(QuantifiableVariable[] qvs, Term guard, Term s)
public Term setComprehension(QuantifiableVariable[] qvs, Term o, Term f)
public Term setComprehension(QuantifiableVariable[] qvs, Term guard, Term o, Term f)
public Term createdLocs()
public ImmutableList<Term> wd(java.lang.Iterable<Term> l)
public Term NULL()
public Term deepNonNull(Term o, Term d)
public Term wellFormed(LocationVariable heap)
public Term permissionsFor(LocationVariable permHeap, LocationVariable regularHeap)
public Term staticInv(Term[] h, KeYJavaType t)
public Term staticInv(KeYJavaType t)
public Term select(Sort asSort, Term h, Term o, LocationVariable field)
public Term getBaseHeap()
public Term dot(Sort asSort, Term o, LocationVariable field)
public Term addLabelToAllSubs(Term term, ImmutableArray<TermLabel> labels)
The labels are not added to heap variables.
term
- term to label.labels
- the labels to apply.public Term addLabelToAllSubs(Term term, TermLabel label)
The label is not added to heap variables.
term
- term to label.label
- the label to apply.public Term addLabel(Term term, ImmutableArray<TermLabel> labels)
term
- the term.labels
- the labels to add.public Term addLabel(Term term, TermLabel label)
term
- the term.label
- the label to add.public Term label(Term term, ImmutableArray<TermLabel> labels)
term
- the term.labels
- the labels to apply.public Term label(Term term, TermLabel label)
term
- the term.label
- the label to apply.public Term fieldStore(TermServices services, Term o, Function f, Term v)
public Term reachableValue(Term h, Term t, KeYJavaType kjt)
public Term reachableValue(Term t, KeYJavaType kjt)
public Term reachableValue(ProgramVariable pv)
public Term frameStrictlyEmpty(Term heapTerm, java.util.Map<Term,Term> normalToAtPre)
frame(Term, Map, Term)
public Term anonUpd(LocationVariable heap, Term mod, Term anonHeap)
public Term indexOf(Term s, Term x)
public Term seqEmpty()
public Term seq(ImmutableList<Term> terms)
public Term replace(Term term, PosInTerm pos, Term replacement)
term
- the term in which to perform the replacement.pos
- the position at which to perform the replacement.replacement
- the replacement term.term
, with the child at pos
replaced by replacement
.public ImmutableSet<Term> unionToSet(Term s)
public static Term goBelowUpdates(Term term)
public static Pair<ImmutableList<Term>,Term> goBelowUpdates2(Term term)
public Term seqDef(QuantifiableVariable qv, Term a, Term b, Term t)
public Term values()
public ImmutableList<Sort> getSorts(java.lang.Iterable<Term> terms)
public Term impPreserveLabels(Term t1, Term t2)
imp(Term, Term)
but simplifications are not
performed if TermLabel
s would be lost.t1
- The left side.t2
- The right side.Term
.public Term andPreserveLabels(java.lang.Iterable<Term> subTerms)
and(Iterable)
but simplifications are not
performed if TermLabel
s would be lost.public Term andPreserveLabels(Term t1, Term t2)
and(Term, Term)
but simplifications are not
performed if TermLabel
s would be lost.t1
- The left side.t2
- The right side.Term
.public Term orPreserveLabels(java.lang.Iterable<Term> subTerms)
or(Iterable)
but simplifications are not
performed if TermLabel
s would be lost.Copyright © 2003-2019 The KeY-Project.