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.Modifier and Type | Field and Description |
---|---|
private java.util.Map<Term,Term> |
cache |
private static ImmutableArray<Term> |
NO_SUBTERMS |
Constructor and Description |
---|
TermFactory() |
TermFactory(java.util.Map<Term,Term> cache) |
private static final ImmutableArray<Term> NO_SUBTERMS
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)
private ImmutableArray<Term> createSubtermArray(Term[] subs)
private Term doCreateTerm(Operator op, ImmutableArray<Term> subs, ImmutableArray<QuantifiableVariable> boundVars, JavaBlock javaBlock, ImmutableArray<TermLabel> labels)