public final class TermFactory
extends java.lang.Object
Term
. All other
classes of the system only know about terms what the Term
class
offers them.
This class is used to encapsulate knowledge about the internal term
structures.
See TermBuilder
for more convenient methods to
create terms.Constructor and Description |
---|
TermFactory() |
TermFactory(java.util.Map<Term,Term> cache) |
public Term createTerm(Operator op, ImmutableArray<Term> subs, ImmutableArray<QuantifiableVariable> boundVars, JavaBlock javaBlock, ImmutableArray<TermLabel> labels)
public Term createTerm(Operator op, ImmutableArray<Term> subs, ImmutableArray<QuantifiableVariable> boundVars, JavaBlock javaBlock)
public Term createTerm(Operator op, Term[] subs, ImmutableArray<QuantifiableVariable> boundVars, JavaBlock javaBlock)
public Term createTerm(Operator op, Term[] subs, ImmutableArray<QuantifiableVariable> boundVars, JavaBlock javaBlock, ImmutableArray<TermLabel> labels)
public Term createTerm(Operator op, Term[] subs, ImmutableArray<QuantifiableVariable> boundVars, JavaBlock javaBlock, TermLabel label)
public Term createTerm(Operator op, Term[] subs, ImmutableArray<TermLabel> labels)
public Term createTerm(Operator op, Term sub, ImmutableArray<TermLabel> labels)
public Term createTerm(Operator op, Term sub1, Term sub2, ImmutableArray<TermLabel> labels)
public Term createTerm(Operator op, ImmutableArray<TermLabel> labels)
@Nonnull public Term createTerm(@Nonnull Operator junctor, @Nonnull java.util.List<Term> terms)
((a op b) op c) op d
.junctor
- the left-associative operator to combine the terms togetherterms
- a list of non-null temrsCopyright © 2003-2019 The KeY-Project.