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 |
---|---|
private Term |
ff |
private static java.lang.String |
JAVA_LANG_THROWABLE |
protected Services |
services |
private TermFactory |
tf |
private Term |
tt |
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) |
Term |
addLabel(Term term,
TermLabel label) |
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) |
private Term |
elementary(Term heapTerm) |
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) |
Term |
label(Term term,
TermLabel label) |
Term |
leq(Term t1,
Term t2) |
Term |
lt(Term t1,
Term t2) |
Term |
max(ImmutableList<QuantifiableVariable> qvs,
Term range,
Term t,
TermServices services)
minimum operator
|
Term |
measuredBy(Term mby) |
Term |
measuredByCheck(Term mby) |
Term |
measuredByEmpty() |
Term |
min(ImmutableList<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() |
private Term |
numberTerm(java.lang.String numberString,
boolean containsChar)
Creates Z-/C-terms for ints/chars.
|
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) |
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) |
private static final java.lang.String JAVA_LANG_THROWABLE
private final TermFactory tf
private final Term tt
private final Term ff
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<QuantifiableVariable> qvs, Term range, Term t, TermServices services)
public Term max(ImmutableList<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()
private Term numberTerm(java.lang.String numberString, boolean containsChar)
numberString
- a string containing the number in a decimal representationcontainsChar
- true iff the number represents a charjava.lang.NumberFormatException
- if numberString
is not a numberpublic 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 addLabel(Term term, ImmutableArray<TermLabel> labels)
public Term label(Term term, ImmutableArray<TermLabel> labels)
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 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.