diff --git a/FMB/DefinitionIntroduction.hpp b/FMB/DefinitionIntroduction.hpp
index 8fd0ca1a96..104bdfefef 100644
--- a/FMB/DefinitionIntroduction.hpp
+++ b/FMB/DefinitionIntroduction.hpp
@@ -133,7 +133,7 @@ namespace FMB {
         if(!_introduced.find(t)){
           unsigned newConstant = env.signature->addFreshFunction(0,"fmbdef");
           unsigned srt = SortHelper::getResultSort(t);
-          env.signature->getFunction(newConstant)->setType(new FunctionType(srt));
+          env.signature->getFunction(newConstant)->setType(OperatorType::getConstantsType(srt));
           Term* c = Term::createConstant(newConstant); 
           _introduced.insert(t,c);
           if(term==t) retC=c;
diff --git a/FMB/FiniteModelMultiSorted.cpp b/FMB/FiniteModelMultiSorted.cpp
index eb592db239..61a9905383 100644
--- a/FMB/FiniteModelMultiSorted.cpp
+++ b/FMB/FiniteModelMultiSorted.cpp
@@ -70,7 +70,7 @@ FiniteModelMultiSorted::FiniteModelMultiSorted(DHMap<unsigned,unsigned> sizes) :
     unsigned arity=env.signature->functionArity(f);
     f_offsets[f]=offsets;
 
-    FunctionType* sig = env.signature->getFunction(f)->fnType();
+    OperatorType* sig = env.signature->getFunction(f)->fnType();
     unsigned add = _sizes.get(sig->result());
     for(unsigned i=0;i<arity;i++){ add*= _sizes.get(sig->arg(i)); }
     
@@ -84,7 +84,7 @@ FiniteModelMultiSorted::FiniteModelMultiSorted(DHMap<unsigned,unsigned> sizes) :
     unsigned arity=env.signature->predicateArity(p);
     p_offsets[p]=offsets;
 
-    PredicateType* sig = env.signature->getPredicate(p)->predType();
+    OperatorType* sig = env.signature->getPredicate(p)->predType();
     unsigned add = 1;
     for(unsigned i=0;i<arity;i++){ add*= _sizes.get(sig->arg(i)); }
 
@@ -126,7 +126,7 @@ void FiniteModelMultiSorted::addFunctionDefinition(unsigned f, const DArray<unsi
 
   unsigned var = f_offsets[f];
   unsigned mult = 1;
-  FunctionType* sig = env.signature->getFunction(f)->fnType();
+  OperatorType* sig = env.signature->getFunction(f)->fnType();
   for(unsigned i=0;i<args.size();i++){
     var += mult*(args[i]-1);
     mult *= _sizes.get(sig->arg(i));
@@ -160,7 +160,7 @@ void FiniteModelMultiSorted::addPredicateDefinition(unsigned p, const DArray<uns
 
   unsigned var = p_offsets[p];
   unsigned mult = 1;
-  PredicateType* sig = env.signature->getPredicate(p)->predType();
+  OperatorType* sig = env.signature->getPredicate(p)->predType();
   for(unsigned i=0;i<args.size();i++){
     var += mult*(args[i]-1);
     mult *=_sizes.get(sig->arg(i));
@@ -279,7 +279,7 @@ vstring FiniteModelMultiSorted::toString()
     if(!printIntroduced && env.signature->getFunction(f)->introduced()) continue;
     vstring name = env.signature->functionName(f);
 
-    FunctionType* sig = env.signature->getFunction(f)->fnType();
+    OperatorType* sig = env.signature->getFunction(f)->fnType();
     modelStm << "tff("<<prepend("declare_", name)<<",type,"<<name<<": ";
     for(unsigned i=0;i<arity;i++){
       modelStm << env.sorts->sortName(sig->arg(i));
@@ -366,7 +366,7 @@ vstring FiniteModelMultiSorted::toString()
     if(!printIntroduced && env.signature->getPredicate(f)->introduced()) continue;
     vstring name = env.signature->predicateName(f);
 
-    PredicateType* sig = env.signature->getPredicate(f)->predType();
+    OperatorType* sig = env.signature->getPredicate(f)->predType();
     modelStm << "tff("<<prepend("declare_", name)<<",type,"<<name<<": ";
     for(unsigned i=0;i<arity;i++){
       modelStm << env.sorts->sortName(sig->arg(i));
@@ -450,7 +450,7 @@ unsigned FiniteModelMultiSorted::evaluateGroundTerm(Term* term)
     if(args[i]==0) USER_ERROR("Could not evaluate "+term->toString());
   }
 
-  FunctionType* sig = env.signature->getFunction(term->functor())->fnType();
+  OperatorType* sig = env.signature->getFunction(term->functor())->fnType();
   unsigned var = f_offsets[term->functor()];
   unsigned mult = 1;
   for(unsigned i=0;i<args.size();i++){
@@ -494,7 +494,7 @@ bool FiniteModelMultiSorted::evaluateGroundLiteral(Literal* lit)
     else return !res;
   }
 
-  PredicateType* sig = env.signature->getPredicate(lit->functor())->predType();
+  OperatorType* sig = env.signature->getPredicate(lit->functor())->predType();
   unsigned var = p_offsets[lit->functor()];
   unsigned mult = 1;
   for(unsigned i=0;i<args.size();i++){
diff --git a/FMB/FiniteModelMultiSorted.hpp b/FMB/FiniteModelMultiSorted.hpp
index 63a679f8a6..5090a7de5e 100644
--- a/FMB/FiniteModelMultiSorted.hpp
+++ b/FMB/FiniteModelMultiSorted.hpp
@@ -100,7 +100,7 @@ class FiniteModelMultiSorted {
    if(_domainConstants.find(pair,t)) return t;
    vstring name = "domCon_"+env.sorts->sortName(srt)+"_"+Lib::Int::toString(c);
    unsigned f = env.signature->addFreshFunction(0,name.c_str()); 
-   env.signature->getFunction(f)->setType(new FunctionType(srt));
+   env.signature->getFunction(f)->setType(OperatorType::getConstantsType(srt));
    t = Term::createConstant(f);
    _domainConstants.insert(pair,t);
    _domainConstantsRev.insert(t,pair);
diff --git a/FMB/FunctionRelationshipInference.cpp b/FMB/FunctionRelationshipInference.cpp
index 4b36184e13..c5c467b646 100644
--- a/FMB/FunctionRelationshipInference.cpp
+++ b/FMB/FunctionRelationshipInference.cpp
@@ -217,7 +217,7 @@ ClauseList* FunctionRelationshipInference::getCheckingClauses()
   unsigned initial_functions = env.signature->functions();
   for(unsigned f=0; f < initial_functions; f++){
 
-    FunctionType* ftype = env.signature->getFunction(f)->fnType();
+    OperatorType* ftype = env.signature->getFunction(f)->fnType();
     unsigned ret_srt = ftype->result();
     unsigned arity = env.signature->functionArity(f);
 
diff --git a/FMB/Monotonicity.cpp b/FMB/Monotonicity.cpp
index ed5ea4adf6..76950ea87e 100644
--- a/FMB/Monotonicity.cpp
+++ b/FMB/Monotonicity.cpp
@@ -196,7 +196,7 @@ void Monotonicity::addSortPredicates(bool withMon, ClauseList*& clauses, DArray<
     if(!isMonotonic[s]){
       vstring name = "sortPredicate_"+env.sorts->sortName(s);
       unsigned p = env.signature->addFreshPredicate(1,name.c_str());
-      env.signature->getPredicate(p)->setType(new PredicateType({s}));
+      env.signature->getPredicate(p)->setType(OperatorType::getPredicateType({s}));
       sortPredicates[s] = p;
     }
     else{ sortPredicates[s]=0; }
@@ -236,7 +236,7 @@ void Monotonicity::addSortPredicates(bool withMon, ClauseList*& clauses, DArray<
 
     // Next the non-empty constraint
     unsigned skolemConstant = env.signature->addSkolemFunction(0);
-    env.signature->getFunction(skolemConstant)->setType(new FunctionType(s));
+    env.signature->getFunction(skolemConstant)->setType(OperatorType::getConstantsType(s));
     Literal* psk = Literal::create1(p,true,TermList(Term::createConstant(skolemConstant)));
     Clause* nonEmpty = new(1) Clause(1,Unit::InputType::AXIOM, new Inference(Inference::INPUT));
     (*nonEmpty)[0] = psk;
@@ -351,7 +351,7 @@ void Monotonicity::addSortFunctions(bool withMon, ClauseList*& clauses)
     if(!isMonotonic[s]){
       vstring name = "sortFunction_"+env.sorts->sortName(s);
       unsigned f = env.signature->addFreshFunction(1,name.c_str());
-      env.signature->getFunction(f)->setType(new FunctionType({s},s));
+      env.signature->getFunction(f)->setType(OperatorType::getFunctionType({s},s));
       sortFunctions[s] = f;
     }
     else{ sortFunctions[s]=0; }
diff --git a/FMB/SortInference.cpp b/FMB/SortInference.cpp
index 4621f27530..76e52a9fe1 100644
--- a/FMB/SortInference.cpp
+++ b/FMB/SortInference.cpp
@@ -117,7 +117,7 @@ void SortInference::doInference()
     for(unsigned f=0;f<env.signature->functions();f++){
       if(_del_f[f]) continue;
       unsigned arity = env.signature->functionArity(f);
-      FunctionType* ftype = env.signature->getFunction(f)->fnType();
+      OperatorType* ftype = env.signature->getFunction(f)->fnType();
       //cout << env.signature->functionName(f) << " : " << env.sorts->sortName(ftype->result()) << endl;;
       unsigned dsort = (*_sig->vampireToDistinct.get(ftype->result()))[0];
       //cout << env.signature->functionName(f) << " : " << dsort << endl;
@@ -134,7 +134,7 @@ void SortInference::doInference()
         unsigned dsort = (*_sig->vampireToDistinct.get(s))[0];
         if(_sig->sortedConstants[dsort].isEmpty()){
           unsigned fresh = env.signature->addFreshFunction(0,"fmbFreshConstant");
-          env.signature->getFunction(fresh)->setType(new FunctionType(s));
+          env.signature->getFunction(fresh)->setType(OperatorType::getConstantsType(s));
           _sig->sortedConstants[dsort].push(fresh);
         }
       }
@@ -145,7 +145,7 @@ void SortInference::doInference()
     for(unsigned f=0;f<env.signature->functions();f++){
       if(f < _del_f.size() && _del_f[f]) continue;
       unsigned arity = env.signature->functionArity(f);
-      FunctionType* ftype = env.signature->getFunction(f)->fnType();
+      OperatorType* ftype = env.signature->getFunction(f)->fnType();
       _sig->functionSignatures[f].ensure(arity+1);
       for(unsigned i=0;i<arity;i++){ 
         _sig->functionSignatures[f][i]=(*_sig->vampireToDistinct.get(ftype->arg(i)))[0]; 
@@ -156,7 +156,7 @@ void SortInference::doInference()
     for(unsigned p=1;p<env.signature->predicates();p++){
       if(_del_p[p]) continue;
       unsigned arity = env.signature->predicateArity(p);
-      PredicateType* ptype = env.signature->getPredicate(p)->predType();
+      OperatorType* ptype = env.signature->getPredicate(p)->predType();
       _sig->predicateSignatures[p].ensure(arity);
       for(unsigned i=0;i<arity;i++){ 
         _sig->predicateSignatures[p][i]=(*_sig->vampireToDistinct.get(ptype->arg(i)))[0]; 
@@ -504,7 +504,7 @@ void SortInference::doInference()
     _sig->functionSignatures[f][arity] = rangeSort;
 
     Signature::Symbol* fnSym = env.signature->getFunction(f);
-    FunctionType* fnType = fnSym->fnType();
+    OperatorType* fnType = fnSym->fnType();
     if(parentSet[rangeSort]){
 #if VDEBUG
       //cout << "FUNCTION " << env.signature->functionName(f) << endl;
@@ -563,7 +563,7 @@ void SortInference::doInference()
     unsigned srt = freshMap.get(f);
     unsigned dsrt = _sig->parents[srt];
     unsigned vsrt = (*_sig->distinctToVampire.get(dsrt))[0];
-    env.signature->getFunction(f)->setType(new FunctionType(vsrt));
+    env.signature->getFunction(f)->setType(OperatorType::getConstantsType(vsrt));
     env.signature->getFunction(f)->markIntroduced();
   }
 
@@ -583,7 +583,7 @@ void SortInference::doInference()
     _sig->predicateSignatures[p].ensure(arity);
 
     Signature::Symbol* prSym = env.signature->getPredicate(p);
-    PredicateType* prType = prSym->predType();
+    OperatorType* prType = prSym->predType();
 
     for(unsigned i=0;i<arity;i++){
       int argRoot = unionFind.root(offset_p[p]+i);
diff --git a/Forwards.hpp b/Forwards.hpp
index 8224422838..7efb888e47 100644
--- a/Forwards.hpp
+++ b/Forwards.hpp
@@ -68,6 +68,7 @@ template<class T> class RCPtr;
 template<typename T> class SingleParamEvent;
 template<class C> class DArray;
 template<class C> class Stack;
+template<class C> class Vector;
 template<typename T> class List;
 template<typename T, class Comparator> class BinaryHeap;
 template<typename T> class SharedSet;
diff --git a/Inferences/TermAlgebraReasoning.cpp b/Inferences/TermAlgebraReasoning.cpp
index 24987c39c6..b8044f062b 100644
--- a/Inferences/TermAlgebraReasoning.cpp
+++ b/Inferences/TermAlgebraReasoning.cpp
@@ -212,7 +212,7 @@ namespace Inferences {
     unsigned int _index; // between 0 and _length
     Literal* _lit;
     Clause* _clause;
-    FunctionType* _type; // type of f
+    OperatorType* _type; // type of f
   };
 
   struct InjectivityGIE::SubtermEqualityFn
@@ -252,7 +252,7 @@ namespace Inferences {
       Literal *lit = (*c)[i];
       if (sameConstructorsEquality(lit) && lit->isPositive()) {
         if (lit->nthArgument(0)->term()->arity() == 1) {
-          FunctionType *type = env.signature->getFunction(lit->nthArgument(0)->term()->functor())->fnType();
+          OperatorType *type = env.signature->getFunction(lit->nthArgument(0)->term()->functor())->fnType();
           Literal *newlit = Literal::createEquality(true,
                                                     *lit->nthArgument(0)->term()->nthArgument(0),
                                                     *lit->nthArgument(1)->term()->nthArgument(0),
@@ -273,7 +273,7 @@ namespace Inferences {
     Literal *lit = (*c)[i];
     if (sameConstructorsEquality(lit) && !lit->polarity()) {
       unsigned arity = lit->nthArgument(0)->term()->arity();
-      FunctionType *type = env.signature->getFunction(lit->nthArgument(0)->term()->functor())->fnType();
+      OperatorType *type = env.signature->getFunction(lit->nthArgument(0)->term()->functor())->fnType();
       for (unsigned j = 0; j < arity; j++) {
         Literal *l = Literal::createEquality(true,
                                              *lit->nthArgument(0)->term()->nthArgument(j),
@@ -303,7 +303,7 @@ namespace Inferences {
     for (int i = length - 1; i >= 0; i--) {
       if (litCondition(c, i)) {
         Literal *lit = (*c)[i];
-        FunctionType *type = env.signature->getFunction(lit->nthArgument(0)->term()->functor())->fnType();
+        OperatorType *type = env.signature->getFunction(lit->nthArgument(0)->term()->functor())->fnType();
         unsigned oldLength = c->length();
         unsigned arity = lit->nthArgument(0)->term()->arity();
         unsigned newLength = oldLength + arity - 1;
diff --git a/InstGen/ModelPrinter.cpp b/InstGen/ModelPrinter.cpp
index 8471671c6a..8761332f0c 100644
--- a/InstGen/ModelPrinter.cpp
+++ b/InstGen/ModelPrinter.cpp
@@ -57,12 +57,12 @@ bool ModelPrinter::haveNonDefaultSorts()
 
   unsigned funs = env.signature->functions();
   for(unsigned i=0; i<funs; i++) {
-    FunctionType* type = env.signature->getFunction(i)->fnType();
+    OperatorType* type = env.signature->getFunction(i)->fnType();
     if(!type->isAllDefault()) { return false; }
   }
   unsigned preds = env.signature->predicates();
   for(unsigned i=1; i<preds; i++) {
-    PredicateType* type = env.signature->getPredicate(i)->predType();
+    OperatorType* type = env.signature->getPredicate(i)->predType();
     if(!type->isAllDefault()) { return false; }
   }
   return true;
@@ -206,7 +206,7 @@ void ModelPrinter::generateNewInstances(Literal* base, TermStack& domain, DHSet<
   static DArray<TermList> args;
   static DArray<bool> variables;
   static DArray<unsigned> nextIndexes;
-  PredicateType* predType = env.signature->getPredicate(base->functor())->predType();
+  OperatorType* predType = env.signature->getPredicate(base->functor())->predType();
 
   args.ensure(arity);
   variables.ensure(arity);
@@ -343,7 +343,7 @@ void ModelPrinter::analyzeEqualityAndPopulateDomain()
     vstring firstTermStr = firstTerm.toString();
     unsigned eqClassSort = SortHelper::getResultSort(firstTerm.term());
     unsigned reprFunc = env.signature->addStringConstant(firstTermStr);
-    FunctionType* reprType = new FunctionType(eqClassSort);
+    OperatorType* reprType = OperatorType::getConstantsType(eqClassSort);
     env.signature->getFunction(reprFunc)->setType(reprType);
     TermList reprTerm = TermList(Term::create(reprFunc, 0, 0));
     _rewrites.insert(firstTerm, reprTerm);
diff --git a/Kernel/Signature.cpp b/Kernel/Signature.cpp
index b73503f9ba..b09bb069f7 100644
--- a/Kernel/Signature.cpp
+++ b/Kernel/Signature.cpp
@@ -155,7 +155,7 @@ void Signature::Symbol::addToDistinctGroup(unsigned group,unsigned this_number)
  * should be different from the default type, this function must be
  * called before any call to @c fnType() or @c predType().
  */
-void Signature::Symbol::setType(BaseType* type)
+void Signature::Symbol::setType(OperatorType* type)
 {
   CALL("Signature::Symbol::setType");
   ASS(!_type);
@@ -168,7 +168,7 @@ void Signature::Symbol::setType(BaseType* type)
  * This can be unsafe so should only be used when you know it is safe to
  * change the type i.e. nothing yet relies on the type of this symbol
  */
-void Signature::Symbol::forceType(BaseType* type)
+void Signature::Symbol::forceType(OperatorType* type)
 {
   CALL("Signature::Symbol::forceType");
   if(_type){ delete _type; }
@@ -181,14 +181,14 @@ void Signature::Symbol::forceType(BaseType* type)
  * If the @c setType() function was not called before, the function
  * symbol is assigned a default type.
  */
-FunctionType* Signature::Symbol::fnType() const
+OperatorType* Signature::Symbol::fnType() const
 {
   CALL("Signature::Symbol::fnType");
 
   if (!_type) {
-    _type = new FunctionType(arity(), (unsigned*)0, Sorts::SRT_DEFAULT);
+    _type = OperatorType::getFunctionType(arity(), (unsigned*)0, Sorts::SRT_DEFAULT);
   }
-  return static_cast<FunctionType*>(_type);
+  return _type;
 }
 
 /**
@@ -197,14 +197,14 @@ FunctionType* Signature::Symbol::fnType() const
  * If the @c setType() function was not called before, the function
  * symbol is assigned a default type.
  */
-PredicateType* Signature::Symbol::predType() const
+OperatorType* Signature::Symbol::predType() const
 {
   CALL("Signature::Symbol::predType");
 
   if (!_type) {
-    _type = new PredicateType(arity(), (unsigned*)0);
+    _type = OperatorType::getPredicateType(arity(), (unsigned*)0);
   }
-  return static_cast<PredicateType*>(_type);
+  return _type;
 }
 
 
@@ -285,7 +285,7 @@ unsigned Signature::addInterpretedFunction(Interpretation interpretation, const
   _funs.push(sym);
   _funNames.insert(symbolKey, fnNum);
   ALWAYS(_iSymbols.insert(interpretation, fnNum));
-  BaseType* fnType = Theory::getOperationType(interpretation);
+  OperatorType* fnType = Theory::getOperationType(interpretation);
   ASS(fnType->isFunctionType());
   sym->setType(fnType);
   return fnNum;
@@ -317,7 +317,7 @@ unsigned Signature::addInterpretedPredicate(Interpretation interpretation, const
   _predNames.insert(symbolKey,predNum);
   ALWAYS(_iSymbols.insert(interpretation, predNum));
   if (predNum!=0) {
-    BaseType* predType = Theory::getOperationType(interpretation);
+    OperatorType* predType = Theory::getOperationType(interpretation);
     ASS_REP(!predType->isFunctionType(), predType->toString());
     sym->setType(predType);
   }
diff --git a/Kernel/Signature.hpp b/Kernel/Signature.hpp
index be3f47614e..8421e7ab29 100644
--- a/Kernel/Signature.hpp
+++ b/Kernel/Signature.hpp
@@ -89,7 +89,7 @@ class Signature
     /** marks term algebra constructors */
     unsigned _termAlgebraCons : 1;
     /** Either a FunctionType of a PredicateType object */
-    mutable BaseType* _type;
+    mutable OperatorType* _type;
     /** List of distinct groups the constant is a member of, all members of a distinct group should be distinct from each other */
     List<unsigned>* _distinctGroups;
     /** number of times it is used in the problem */
@@ -198,10 +198,10 @@ class Signature
         Note that this should only be called on a constant **/
     void addToDistinctGroup(unsigned group,unsigned this_number);
 
-    void setType(BaseType* type);
-    void forceType(BaseType* type);
-    FunctionType* fnType() const;
-    PredicateType* predType() const;
+    void setType(OperatorType* type);
+    void forceType(OperatorType* type);
+    OperatorType* fnType() const;
+    OperatorType* predType() const;
 
     CLASS_NAME(Signature::Symbol);
     USE_ALLOCATOR(Symbol);
@@ -244,7 +244,7 @@ class Signature
     {
       CALL("IntegerSymbol");
 
-      setType(new FunctionType(Sorts::SRT_INTEGER));
+      setType(OperatorType::getConstantsType(Sorts::SRT_INTEGER));
     }
     CLASS_NAME(Signature::IntegerSymbol);
     USE_ALLOCATOR(IntegerSymbol);
@@ -264,7 +264,7 @@ class Signature
     {
       CALL("RationalSymbol");
 
-      setType(new FunctionType(Sorts::SRT_RATIONAL));
+      setType(OperatorType::getConstantsType(Sorts::SRT_RATIONAL));
     }
     CLASS_NAME(Signature::RationalSymbol);
     USE_ALLOCATOR(RationalSymbol);
@@ -284,7 +284,7 @@ class Signature
     {
       CALL("RealSymbol");
 
-      setType(new FunctionType(Sorts::SRT_REAL));
+      setType(OperatorType::getConstantsType(Sorts::SRT_REAL));
     }
     CLASS_NAME(Signature::RealSymbol);
     USE_ALLOCATOR(RealSymbol);
@@ -467,9 +467,9 @@ class Signature
   unsigned getFoolConstantSymbol(bool isTrue){ 
     if(!_foolConstantsDefined){
       _foolFalse = addFunction("$$false",0); 
-      getFunction(_foolFalse)->setType(new FunctionType(Sorts::SRT_BOOL));
+      getFunction(_foolFalse)->setType(OperatorType::getConstantsType(Sorts::SRT_BOOL));
       _foolTrue = addFunction("$$true",0);
-      getFunction(_foolTrue)->setType(new FunctionType(Sorts::SRT_BOOL));
+      getFunction(_foolTrue)->setType(OperatorType::getConstantsType(Sorts::SRT_BOOL));
       _foolConstantsDefined=true;
     }
     return isTrue ? _foolTrue : _foolFalse;
diff --git a/Kernel/SortHelper.cpp b/Kernel/SortHelper.cpp
index f145de6f73..ea5a885708 100644
--- a/Kernel/SortHelper.cpp
+++ b/Kernel/SortHelper.cpp
@@ -39,7 +39,7 @@ using namespace Kernel;
  * Return the type of a term or a literal @c t
  * @author Andrei Voronkov
  */
-BaseType& SortHelper::getType(Term* t)
+OperatorType& SortHelper::getType(Term* t)
 {
   CALL("SortHelper::getType(Term*)");
 
@@ -768,7 +768,7 @@ bool SortHelper::areImmediateSortsValid(Term* t)
     return true;
   }
 
-  BaseType& type = getType(t);
+  OperatorType& type = getType(t);
   unsigned arity = t->arity();
   for (unsigned i=0; i<arity; i++) {
     TermList arg = *t->nthArgument(i);
diff --git a/Kernel/SortHelper.hpp b/Kernel/SortHelper.hpp
index 6cdbd96ff9..150fbe0ffd 100644
--- a/Kernel/SortHelper.hpp
+++ b/Kernel/SortHelper.hpp
@@ -77,7 +77,7 @@ class SortHelper {
   static bool areSortsValid(Clause* cl);
   static bool areImmediateSortsValid(Term* t);
 
-  static BaseType& getType(Term* t);
+  static OperatorType& getType(Term* t);
 
   static bool areSortsValid(Term* t, DHMap<unsigned,unsigned>& varSorts);
 private:
diff --git a/Kernel/Sorts.cpp b/Kernel/Sorts.cpp
index 059041b421..f98f7cab17 100644
--- a/Kernel/Sorts.cpp
+++ b/Kernel/Sorts.cpp
@@ -223,122 +223,101 @@ const vstring& Sorts::sortName(unsigned idx) const
 } // Sorts::sortName
 
 /**
- * Initialise a base type. If @c sorts is is NULL, all arguments will be
- * initalised by the default sort, otherwise, by sorts from the array @c sorts
+ * Pre-initialise an OperatorKey.
+ *
+ * If @c sorts is is NULL, all arguments will be initalized by the default sort,
+ * otherwise, by sorts from the array @c sorts
  * @author Andrei Voronkov
  */
-BaseType::BaseType(unsigned arity, const unsigned* sorts)
+OperatorType::OperatorKey* OperatorType::setupKey(unsigned arity, const unsigned* sorts)
 {
-  CALL("BaseType::BaseType");
+  CALL("OperatorType::setupKey(unsigned,const unsigned*)");
 
-  if (!arity) {
-    _args = 0;
-    return;
-  }
+  OperatorKey* key = OperatorKey::allocate(arity+1);
 
-  _args = SortVector::allocate(arity);
   if (!sorts) {
     // initialise all argument types to the default type
     for (unsigned i = 0; i < arity; i++) {
-      (*_args)[i] = Sorts::SRT_DEFAULT;
+      (*key)[i] = Sorts::SRT_DEFAULT;
+    }
+  } else {
+    // initialise all the argument types to those taken from sorts
+    for (unsigned i = 0; i < arity; i++) {
+      (*key)[i] = sorts[i];
     }
-    return;
-  }
-  // initialise all the argument types to thos taken from sorts
-  for (unsigned i = 0; i < arity; i++) {
-    (*_args)[i] = sorts[i];
   }
-} // BaseType::BaseType
+  return key;
+}
 
 /**
- * Initialise a base type from an initializer list of sorts.
+ * Pre-initialise an OperatorKey from an initializer list of sorts.
  */
-BaseType::BaseType(std::initializer_list<unsigned> sorts)
+OperatorType::OperatorKey* OperatorType::setupKey(std::initializer_list<unsigned> sorts)
 {
-  CALL("BaseType::BaseType");
+  CALL("OperatorType::setupKey(std::initializer_list<unsigned>)");
 
-  if (sorts.size() == 0) {
-    _args = 0;
-    return;
-  }
+  OperatorKey* key = OperatorKey::allocate(sorts.size()+1);
 
-  _args = SortVector::allocate(sorts.size());
-  // initialise all the argument types to thos taken from sorts
+  // initialise all the argument types to those taken from sorts
   unsigned i = 0;
   for (auto sort : sorts) {
-    (*_args)[i++] = sort;
+    (*key)[i++] = sort;
   }
-} // BaseType::BaseType
+
+  return key;
+}
 
 /**
- * Destrory the type and deallocate its arguments, if any
- * @author Andrei Voronkov 
- */ 
-BaseType::~BaseType()
+ * Pre-initialise an OperatorKey from unsing a uniform range.
+ */
+OperatorType::OperatorKey* OperatorType::setupKeyUniformRange(unsigned arity, unsigned argsSort)
 {
-  CALL("BaseType::~BaseType");
+  CALL("OperatorType::setupKeyUniformRange");
+
+  OperatorKey* key = OperatorKey::allocate(arity+1);
 
-  if (_args) {
-    _args->deallocate();
+  static Stack<unsigned> argSorts;
+  argSorts.reset();
+  for (unsigned i=0; i<arity; i++) {
+    argSorts.push(argsSort);
   }
-} // BaseType::~BaseType
 
-/**
- * True if all arguments of this type have sort @c str.
- * @author Andrei Voronkov 
- */ 
-bool BaseType::isSingleSortType(unsigned srt) const
-{
-  CALL("BaseType::isAllDefault");
+  return key;
+}
 
-  unsigned len = arity();
-  for (unsigned i = 0; i <len; i++) {
-    if (arg(i) != srt) {
-      return false;
-    }
-  }
-  return true;
-} // isSingleSortType
+OperatorType::OperatorTypes OperatorType::_operatorTypes;
 
 /**
- * Return true if two types are equal. Two are are equal if their argument types
- * coincide and their return types coincide.
- * @author Andrei Voronkov
+ * Check if OperatorType corresponding to the given key
+ * already exists. If so return it, if not create new,
+ * store it for future retrieval and return it.
+ *
+ * Release key if not needed.
  */
-bool BaseType::operator==(const BaseType& o) const
+OperatorType* OperatorType::getTypeFromKey(OperatorType::OperatorKey* key)
 {
-  CALL("BaseType::operator==");
+  CALL("OperatorType::getTypeFromKey");
 
-  if (isFunctionType() != o.isFunctionType()) {
-    return false;
-  }
-  if (isFunctionType()) {
-    if (static_cast<const FunctionType&>(*this).result() != 
-	static_cast<const FunctionType&>(o).result()) {
-      return false;
-    }
-  }
-  unsigned len = arity();
-  if (len != o.arity()) {
-    return false;
-  }
-  for (unsigned i=0; i < len; i++) {
-    if (arg(i) != o.arg(i)) {
-      return false;
-    }
+  OperatorType* resultType;
+  if (_operatorTypes.find(key,resultType)) {
+    key->deallocate();
+    return resultType;
   }
-  return true;
-} // BaseType::operator==
 
-/** 
+  resultType = new OperatorType(key);
+  _operatorTypes.insert(key,resultType);
+  return resultType;
+}
+
+/**
  * Return the string representation of arguments of a non-atomic
  * functional or a predicate sort in the form (t1 * ... * tn)
  * @since 04/05/2013 bug fix (comma was used instead of *)
  * @author Andrei Voronkov
  */
-vstring BaseType::argsToString() const
+vstring OperatorType::argsToString() const
 {
-  CALL("BaseType::argsToString");
+  CALL("OperatorType::argsToString");
 
   vstring res = "(";
   unsigned ar = arity();
@@ -351,72 +330,38 @@ vstring BaseType::argsToString() const
   }
   res += ')';
   return res;
-} // BaseType::argsToString()
-
-/**
- * Return the TPTP string representation of the predicate type.
- * @author Andrei Voronkov
- */
-vstring PredicateType::toString() const
-{
-  CALL("PredicateType::toString");
-  return arity() ? argsToString() + " > $o" : "$o";
-} // PredicateType::toString
+} // OperatorType::argsToString()
 
 /**
- * Create a type of the form (argSort * ... * argSort) -> rangeSort
- * @author Evgeny Kotelnikov
+ * Return the TPTP string representation of the OpertorType.
  */
-PredicateType* PredicateType::makeTypeUniformRange(unsigned arity, unsigned argsSort)
+vstring OperatorType::toString() const
 {
-  CALL("PredicateType::makeTypeUniformRange");
-
-  static Stack<unsigned> argSorts;
-  argSorts.reset();
-  for (unsigned i=0; i<arity; i++) {
-    argSorts.push(argsSort);
-  }
-  return new PredicateType(arity, argSorts.begin());
-} // PredicateType::makeTypeUniformRange
+  CALL("OperatorType::toString");
 
+  return (arity() ? argsToString() + " > " : "") +
+      (isPredicateType() ? "$o" : env.sorts->sortName(result()));
+}
 
 /**
- * Return the TPTP string representation of the function type.
+ * True if all arguments of this type have sort @c str
+ * and so is the result sort if we are talking about a function type.
  * @author Andrei Voronkov
  */
-vstring FunctionType::toString() const
+bool OperatorType::isSingleSortType(unsigned srt) const
 {
-  CALL("FunctionType::toString");
-  return (arity() ? argsToString() + " > " : "") + env.sorts->sortName(result());
-} // FunctionType::toString
+  CALL("OperatorType::isAllDefault");
 
-/**
- * True if this function type has the form (srt * ... * srt) -> srt
- * @author Andrei Voronkov
- */
-bool FunctionType::isSingleSortType(unsigned srt) const
-{
-  CALL("FunctionType::isSingleSortType");
+  unsigned len = arity();
+  for (unsigned i = 0; i <len; i++) {
+    if (arg(i) != srt) {
+      return false;
+    }
+  }
 
-  if (result() != srt) {
+  if (isFunctionType() && result() != srt) {
     return false;
   }
-  return BaseType::isSingleSortType(srt);
-} // FunctionType::isSingleSortType
 
-/**
- * Create a type of the form (argSort * ... * argSort) -> rangeSort
- * @author Andrei Voronkov
- * @author Evgeny Kotelnikov, move to FunctionType
- */
-FunctionType* FunctionType::makeTypeUniformRange(unsigned arity, unsigned argsSort, unsigned rangeSort)
-{
-  CALL("FunctionType::makeTypeUniformRange");
-
-  static Stack<unsigned> argSorts;
-  argSorts.reset();
-  for (unsigned i=0; i<arity; i++) {
-    argSorts.push(argsSort);
-  }
-  return new FunctionType(arity, argSorts.begin(), rangeSort);
-} // FunctionType::makeTypeUniformRange
+  return true;
+} // isSingleSortType
diff --git a/Kernel/Sorts.hpp b/Kernel/Sorts.hpp
index 67bc0d224a..cd862cba93 100644
--- a/Kernel/Sorts.hpp
+++ b/Kernel/Sorts.hpp
@@ -206,81 +206,130 @@ class Sorts {
   Stack<SortInfo*> _sorts;
   /** true if there is a sort different from built-ins */
   bool _hasSort;
-
 };
 
-class BaseType
+/**
+ * The OperatorType class represents the predicate and function types (which are not sorts in first-order logic).
+ * These are determined by their kind (either PREDICATE or FUNCTION), arity, a corresponding list of argument sorts,
+ * and a return sort in the case of functions.
+ *
+ * The class stores all this data in one Vector<unsigned>*, of length arity+1,
+ * where the last element is the return sort for functions and "MAX_UNSIGNED" for predicates (which distinguishes the two kinds).
+ *
+ * The objects of this class are perfectly shared (so that equal predicate / function types correspond to equal pointers)
+ * and are obtained via static methods (to guarantee the sharing).
+ */
+class OperatorType
 {
 public:
-  CLASS_NAME(BaseType);
-  USE_ALLOCATOR(BaseType);
+  CLASS_NAME(OperatorType);
+  USE_ALLOCATOR(OperatorType);
 
-  virtual ~BaseType();
+private:
+  typedef Vector<unsigned> OperatorKey; // Vector of argument sorts together with "FFFF" appended for predicates and resultSort appended for functions
+  OperatorKey* _key;
 
-  unsigned arg(unsigned idx) const
-  {
-    CALL("BaseType::arg");
-    return (*_args)[idx];
+  // constructors kept private
+  OperatorType(OperatorKey* key) : _key(key) {}
+
+  /**
+   * Convenience functions for creating a key
+   */
+  static OperatorKey* setupKey(unsigned arity, const unsigned* sorts=0);
+  static OperatorKey* setupKey(std::initializer_list<unsigned> sorts);
+  static OperatorKey* setupKeyUniformRange(unsigned arity, unsigned argsSort);
+
+  typedef Map<OperatorKey*,OperatorType*,Hash> OperatorTypes;
+  // we should delete all the stored OperatorTypes inside at the end of the world, when this get destroyed
+  static OperatorTypes _operatorTypes;
+
+  static OperatorType* getTypeFromKey(OperatorKey* key);
+
+  static const unsigned PREDICATE_FLAG = std::numeric_limits<unsigned>::max();
+
+public:
+  ~OperatorType() { _key->deallocate(); }
+
+  static OperatorType* getPredicateType(unsigned arity, const unsigned* sorts=0) {
+    CALL("OperatorType::getPredicateType(unsigned,const unsigned*)");
+
+    OperatorKey* key = setupKey(arity,sorts);
+    (*key)[arity] = PREDICATE_FLAG;
+    return getTypeFromKey(key);
   }
 
-  unsigned arity() const { return _args ? _args->length() : 0; }
-  virtual bool isSingleSortType(unsigned sort) const;
-  bool isAllDefault() const { return isSingleSortType(Sorts::SRT_DEFAULT); }
+  static OperatorType* getPredicateType(std::initializer_list<unsigned> sorts) {
+    CALL("OperatorType::getPredicateType(std::initializer_list<unsigned>)");
 
-  virtual bool isFunctionType() const { return false; }
+    OperatorKey* key = setupKey(sorts);
+    (*key)[sorts.size()] = PREDICATE_FLAG;
+    return getTypeFromKey(key);
+  }
 
-  bool operator==(const BaseType& o) const;
-  bool operator!=(const BaseType& o) const { return !(*this==o); }
+  static OperatorType* getPredicateTypeUniformRange(unsigned arity, unsigned argsSort) {
+    CALL("OperatorType::getPredicateTypeUniformRange");
 
-  virtual vstring toString() const = 0;
-protected:
-  BaseType(unsigned arity, const unsigned* sorts=0);
-  BaseType(std::initializer_list<unsigned> sorts);
+    OperatorKey* key = setupKeyUniformRange(arity,argsSort);
+    (*key)[arity] = PREDICATE_FLAG;
+    return getTypeFromKey(key);
+  }
 
-  vstring argsToString() const;
-private:
-  typedef Vector<unsigned> SortVector;
-  SortVector* _args;
-};
+  static OperatorType* getFunctionType(unsigned arity, const unsigned* sorts, unsigned resultSort) {
+    CALL("OperatorType::getFunctionType");
 
-class PredicateType : public BaseType
-{
-public:
-  CLASS_NAME(PredicateType);
-  USE_ALLOCATOR(PredicateType);
+    OperatorKey* key = setupKey(arity,sorts);
+    (*key)[arity] = resultSort;
+    return getTypeFromKey(key);
+  }
 
-  PredicateType(unsigned arity, const unsigned* argumentSorts)
-   : BaseType(arity, argumentSorts) {}
-  PredicateType(std::initializer_list<unsigned> sorts) : BaseType(sorts) {}
+  static OperatorType* getFunctionType(std::initializer_list<unsigned> sorts, unsigned resultSort) {
+    CALL("OperatorType::getFunctionType(std::initializer_list<unsigned>)");
 
-  virtual vstring toString() const;
+    OperatorKey* key = setupKey(sorts);
+    (*key)[sorts.size()] = resultSort;
+    return getTypeFromKey(key);
+  }
 
-  static PredicateType* makeTypeUniformRange(unsigned arity, unsigned argsSort);
-};
+  static OperatorType* getFunctionTypeTypeUniformRange(unsigned arity, unsigned argsSort, unsigned resultSort) {
+    CALL("OperatorType::getFunctionTypeTypeUniformRange");
 
-class FunctionType : public BaseType
-{
-public:
-  CLASS_NAME(FunctionType);
-  USE_ALLOCATOR(FunctionType);
+    OperatorKey* key = setupKeyUniformRange(arity,argsSort);
+    (*key)[arity] = resultSort;
+    return getTypeFromKey(key);
+  }
 
-  FunctionType(unsigned arity, const unsigned* argumentSorts, unsigned resultSort)
-   : BaseType(arity, argumentSorts), _result(resultSort) {}
-  FunctionType(unsigned resultSort)
-   : BaseType(0, 0), _result(resultSort) {}
-  FunctionType(std::initializer_list<unsigned> argSorts, unsigned resultSort)
-   : BaseType(argSorts), _result(resultSort) {}
+  /**
+   * Convenience function for creating OperatorType for constants (as symbols).
+   * Constants are function symbols of 0 arity, so just provide the result sort.
+   */
+  static OperatorType* getConstantsType(unsigned resultSort) { return getFunctionType(0,nullptr,resultSort); }
+
+  unsigned arity() const { return _key->length()-1; }
+
+  unsigned arg(unsigned idx) const
+  {
+    CALL("OperatorType::arg");
+    return (*_key)[idx];
+  }
 
-  unsigned result() const { return _result; }
+  bool isPredicateType() const { return (*_key)[arity()] == PREDICATE_FLAG; };
+  bool isFunctionType() const { return (*_key)[arity()] != PREDICATE_FLAG; };
+  unsigned result() const {
+    CALL("OperatorType::result");
+    ASS(isFunctionType());
+    return (*_key)[arity()];
+  }
 
-  virtual bool isSingleSortType(unsigned sort) const;
-  virtual bool isFunctionType() const { return true; }
+  vstring toString() const;
 
-  virtual vstring toString() const;
+  bool isSingleSortType(unsigned sort) const;
+  bool isAllDefault() const { return isSingleSortType(Sorts::SRT_DEFAULT); }
+
+  bool operator==(const OperatorType& o) const { return _key == o._key; }
+  bool operator!=(const OperatorType& o) const { return !(*this==o); }
 
-  static FunctionType* makeTypeUniformRange(unsigned arity, unsigned argsSort, unsigned rangeSort);
 private:
-  unsigned _result;
+  vstring argsToString() const;
 };
 
 }
diff --git a/Kernel/Term.cpp b/Kernel/Term.cpp
index 0a12e2fd1d..bcc4c7c31b 100644
--- a/Kernel/Term.cpp
+++ b/Kernel/Term.cpp
@@ -419,8 +419,8 @@ vstring Term::headToString() const
         bool isPredicate = binding.isTerm() && binding.term()->isBoolean();
         vstring functor = isPredicate ? env.signature->predicateName(sd->getFunctor())
                                       : env.signature->functionName(sd->getFunctor());
-        BaseType* type = isPredicate ? (BaseType*)env.signature->getPredicate(sd->getFunctor())->predType()
-                                     : (BaseType*)env.signature->getFunction(sd->getFunctor())->fnType();
+        OperatorType* type = isPredicate ? env.signature->getPredicate(sd->getFunctor())->predType()
+                                         : env.signature->getFunction(sd->getFunctor())->fnType();
 
         const IntList* variables = sd->getVariables();
         vstring variablesList = "";
@@ -464,7 +464,7 @@ vstring Term::headToString() const
         unsigned tupleFunctor = sd->getFunctor();
         TermList binding = sd->getBinding();
 
-        FunctionType* fnType = env.signature->getFunction(tupleFunctor)->fnType();
+        OperatorType* fnType = env.signature->getFunction(tupleFunctor)->fnType();
 
         vstring symbolsList = "";
         for (unsigned i = 0; i < IntList::length(symbols); i++) {
diff --git a/Kernel/Theory.cpp b/Kernel/Theory.cpp
index 888d44396c..55b619605f 100644
--- a/Kernel/Theory.cpp
+++ b/Kernel/Theory.cpp
@@ -1179,8 +1179,8 @@ unsigned Theory::Tuples::getProjectionFunctor(unsigned proj, unsigned tupleSort)
 bool Theory::Tuples::findProjection(unsigned projFunctor, bool isPredicate, unsigned &proj) {
   CALL("Theory::Tuples::findProjection");
 
-  BaseType* projType = isPredicate ? static_cast<BaseType*>(env.signature->getPredicate(projFunctor)->predType())
-                                   : static_cast<BaseType*>(env.signature->getFunction(projFunctor)->fnType());
+  OperatorType* projType = isPredicate ? env.signature->getPredicate(projFunctor)->predType()
+                                       : env.signature->getFunction(projFunctor)->fnType();
 
   if (projType->arity() != 1) {
     return false;
@@ -1213,7 +1213,7 @@ bool Theory::Tuples::findProjection(unsigned projFunctor, bool isPredicate, unsi
  *
  * @c i must be a type conversion operation.
  */
-FunctionType* Theory::getConversionOperationType(Interpretation i)
+OperatorType* Theory::getConversionOperationType(Interpretation i)
 {
   CALL("Theory::getConversionOperationType");
 
@@ -1246,7 +1246,7 @@ FunctionType* Theory::getConversionOperationType(Interpretation i)
   default:
     ASSERTION_VIOLATION;
   }
-  return new FunctionType({from}, to);
+  return OperatorType::getFunctionType({from}, to);
 }
 
 Sorts::StructuredSort Theory::getInterpretedSort(StructuredSortInterpretation ssi) {
@@ -1388,7 +1388,7 @@ vstring Theory::getInterpretationName(Interpretation interp) {
   }
 }
 
-BaseType* Theory::getStructuredSortOperationType(Interpretation i) {
+OperatorType* Theory::getStructuredSortOperationType(Interpretation i) {
   CALL("Theory::getStructuredSortOperationType");
 
   ASS(theory->isStructuredSortInterpretation(i));
@@ -1404,13 +1404,13 @@ BaseType* Theory::getStructuredSortOperationType(Interpretation i) {
 
       switch (ssi) {
         case StructuredSortInterpretation::ARRAY_SELECT:
-          return new FunctionType({ theorySort, indexSort }, valueSort);
+          return OperatorType::getFunctionType({ theorySort, indexSort }, valueSort);
 
         case StructuredSortInterpretation::ARRAY_BOOL_SELECT:
-          return new PredicateType({ theorySort, indexSort });
+          return OperatorType::getPredicateType({ theorySort, indexSort });
 
         case StructuredSortInterpretation::ARRAY_STORE:
-          return new FunctionType({ theorySort, indexSort, innerSort }, valueSort);
+          return OperatorType::getFunctionType({ theorySort, indexSort, innerSort }, valueSort);
 
         default:
           ASSERTION_VIOLATION;
@@ -1424,7 +1424,7 @@ BaseType* Theory::getStructuredSortOperationType(Interpretation i) {
 /**
  * Return type of the function representing interpreted function/predicate @c i.
  */
-BaseType* Theory::getOperationType(Interpretation i)
+OperatorType* Theory::getOperationType(Interpretation i)
 {
   CALL("Theory::getOperationType");
   ASS_NEQ(i, EQUAL);
@@ -1447,9 +1447,9 @@ BaseType* Theory::getOperationType(Interpretation i)
   domainSorts.init(arity, sort);
 
   if (isFunction(i)) {
-    return new FunctionType(arity, domainSorts.array(), sort);
+    return OperatorType::getFunctionType(arity, domainSorts.array(), sort);
   } else {
-    return new PredicateType(arity, domainSorts.array());
+    return OperatorType::getPredicateType(arity, domainSorts.array());
   }
 }
 
@@ -1463,7 +1463,7 @@ void Theory::defineTupleTermAlgebra(unsigned arity, unsigned* sorts) {
   }
 
   unsigned functor = env.signature->addFreshFunction(arity, "tuple");
-  FunctionType* tupleType = new FunctionType(arity, sorts, tupleSort);
+  OperatorType* tupleType = OperatorType::getFunctionType(arity, sorts, tupleSort);
   env.signature->getFunction(functor)->setType(tupleType);
   env.signature->getFunction(functor)->markTermAlgebraCons();
 
@@ -1473,10 +1473,10 @@ void Theory::defineTupleTermAlgebra(unsigned arity, unsigned* sorts) {
     unsigned destructor;
     if (projSort == Sorts::SRT_BOOL) {
       destructor = env.signature->addFreshPredicate(1, "proj");
-      env.signature->getPredicate(destructor)->setType(new PredicateType({ tupleSort }));
+      env.signature->getPredicate(destructor)->setType(OperatorType::getPredicateType({ tupleSort }));
     } else {
       destructor = env.signature->addFreshFunction(1, "proj");
-      env.signature->getFunction(destructor)->setType(new FunctionType({ tupleSort }, projSort));
+      env.signature->getFunction(destructor)->setType(OperatorType::getFunctionType({ tupleSort }, projSort));
     }
     destructors[i] = destructor;
   }
diff --git a/Kernel/Theory.hpp b/Kernel/Theory.hpp
index b4d7e13ab7..5b0d87f590 100644
--- a/Kernel/Theory.hpp
+++ b/Kernel/Theory.hpp
@@ -451,8 +451,8 @@ class Theory
   static bool isFunction(Interpretation i);
   static bool isInequality(Interpretation i);
   static Sorts::StructuredSort getInterpretedSort(StructuredSortInterpretation ssi);
-  static BaseType* getOperationType(Interpretation i);
-  static BaseType* getStructuredSortOperationType(Interpretation i);
+  static OperatorType* getOperationType(Interpretation i);
+  static OperatorType* getStructuredSortOperationType(Interpretation i);
   static bool hasSingleSort(Interpretation i);
   static unsigned getOperationSort(Interpretation i);
   static bool isConversionOperation(Interpretation i);
@@ -568,7 +568,7 @@ class Theory
   Term* representRealConstant(vstring str);
 private:
   Theory();
-  static FunctionType* getConversionOperationType(Interpretation i);
+  static OperatorType* getConversionOperationType(Interpretation i);
 
   DHMap<unsigned,unsigned> _arraySkolemFunctions;
 
diff --git a/Lib/Hash.hpp b/Lib/Hash.hpp
index c3546d5b27..f55cbebe86 100644
--- a/Lib/Hash.hpp
+++ b/Lib/Hash.hpp
@@ -55,6 +55,18 @@ struct StackHash {
   }
 };
 
+template<class ElementHash>
+struct VectorHash {
+  template<typename T>
+  static unsigned hash(const Vector<T>& s) {
+    unsigned res = 2166136261u;
+    for (unsigned i = 0; i < s.length(); i++) {
+      res = HashUtils::combine(res, ElementHash::hash(s[i]));
+    }
+    return res;
+  }
+};
+
 /**
  * Hash functions for various types.
  */
@@ -78,6 +90,10 @@ class Hash
   static unsigned hash(Stack<T> obj)
   { return StackHash<Hash>::hash(obj); }
 
+  template<typename T>
+  static unsigned hash(Vector<T>* obj)
+  { return VectorHash<Hash>::hash(*obj); }
+
   // Careful: using this default on structs may cause big trouble!
   // Even when all fields are properly initialized, there can remain "holes"
   // within the "sizeof" bytes containing garbage, due to alignment politics!
diff --git a/Parse/SMTLIB.cpp b/Parse/SMTLIB.cpp
index ef52d3bf1f..590ef4888b 100644
--- a/Parse/SMTLIB.cpp
+++ b/Parse/SMTLIB.cpp
@@ -306,7 +306,7 @@ void SMTLIB::doSortDeclarations()
   }
 }
 
-BaseType* SMTLIB::getSymbolType(const FunctionInfo& fnInfo)
+OperatorType* SMTLIB::getSymbolType(const FunctionInfo& fnInfo)
 {
   CALL("SMTLIB::getSymbolType");
   
@@ -323,7 +323,7 @@ BaseType* SMTLIB::getSymbolType(const FunctionInfo& fnInfo)
     argSorts.push(getSort(argSortName));
   }
 
-  return new FunctionType(arity, argSorts.begin(), rangeSort);
+  return OperatorType::getFunctionType(arity, argSorts.begin(), rangeSort);
 }
 
 void SMTLIB::doFunctionDeclarations()
@@ -335,8 +335,8 @@ void SMTLIB::doFunctionDeclarations()
     FunctionInfo& fnInfo = _funcs[i];
     unsigned arity = fnInfo.argSorts.size();
     
-    BaseType* type = getSymbolType(fnInfo);
-    bool isPred = !type->isFunctionType();
+    OperatorType* type = getSymbolType(fnInfo);
+    bool isPred = type->isPredicateType();
 
     unsigned symNum;
     Signature::Symbol* sym;
@@ -518,7 +518,7 @@ void SMTLIB::ensureArgumentSorts(bool pred, unsigned symNum, TermList* args)
 {
   CALL("SMTLIB::ensureArgumentSorts");
 
-  BaseType* type;
+  OperatorType* type;
   if(pred) {
     type = env.signature->getPredicate(symNum)->predType();
   }
@@ -1192,7 +1192,7 @@ bool SMTLIB::tryReadDistinct(LExpr* e, Formula*& res)
   }
 
   bool added;
-  BaseType* type = PredicateType::makeTypeUniformRange(arity, sort);
+  OperatorType* type = OperatorType::getPredicateTypeUniformRange(arity, sort);
 
   //this is a bit of a quick hack, we need to come up with
   //a proper way to have a polymorphic $distinct predicate
@@ -1201,7 +1201,7 @@ bool SMTLIB::tryReadDistinct(LExpr* e, Formula*& res)
     env.signature->getPredicate(predNum)->setType(type);
   }
   else {
-    BaseType* prevType = env.signature->getPredicate(predNum)->predType();
+    OperatorType* prevType = env.signature->getPredicate(predNum)->predType();
     if(*type==*prevType) {
       delete type;
     }
@@ -1420,7 +1420,7 @@ Formula* SMTLIB::nameFormula(Formula* f, vstring fletVarName)
 
   fletVarName = StringUtils::sanitizeSuffix(fletVarName);
   unsigned predNum = env.signature->addFreshPredicate(varCnt, "sP", fletVarName.c_str());
-  BaseType* type = new PredicateType(varCnt, argSorts.begin());
+  OperatorType* type = OperatorType::getPredicateType(varCnt, argSorts.begin());
 
   Signature::Symbol* predSym = env.signature->getPredicate(predNum);
   predSym->setType(type);
diff --git a/Parse/SMTLIB.hpp b/Parse/SMTLIB.hpp
index 022abfd269..0eff76ad04 100644
--- a/Parse/SMTLIB.hpp
+++ b/Parse/SMTLIB.hpp
@@ -78,7 +78,7 @@ class SMTLIB {
    *
    * This function can be called if the mode is at least DECLARE_SORTS.
    */
-  BaseType* getSymbolType(const FunctionInfo& fnInfo);
+  OperatorType* getSymbolType(const FunctionInfo& fnInfo);
 
   /**
    * Return parsed formula.
diff --git a/Parse/SMTLIB2.cpp b/Parse/SMTLIB2.cpp
index 5d7bfc2516..36f574889e 100644
--- a/Parse/SMTLIB2.cpp
+++ b/Parse/SMTLIB2.cpp
@@ -766,14 +766,14 @@ SMTLIB2::DeclaredFunction SMTLIB2::declareFunctionOrPredicate(const vstring& nam
   bool added;
   unsigned symNum;
   Signature::Symbol* sym;
-  BaseType* type;
+  OperatorType* type;
 
   if (rangeSort == Sorts::SRT_BOOL) { // predicate
     symNum = env.signature->addPredicate(name, argSorts.size(), added);
 
     sym = env.signature->getPredicate(symNum);
 
-    type = new PredicateType(argSorts.size(),argSorts.begin());
+    type = OperatorType::getPredicateType(argSorts.size(),argSorts.begin());
 
     LOG1("declareFunctionOrPredicate-Predicate");
   } else { // proper function
@@ -785,7 +785,7 @@ SMTLIB2::DeclaredFunction SMTLIB2::declareFunctionOrPredicate(const vstring& nam
 
     sym = env.signature->getFunction(symNum);
 
-    type = new FunctionType(argSorts.size(), argSorts.begin(), rangeSort);
+    type = OperatorType::getFunctionType(argSorts.size(), argSorts.begin(), rangeSort);
 
     LOG1("declareFunctionOrPredicate-Function");
   }
@@ -978,7 +978,7 @@ TermAlgebraConstructor* SMTLIB2::buildTermAlgebraConstructor(vstring constrName,
   unsigned functor = env.signature->addFunction(constrName, arity, added);
   ASS(added);
 
-  BaseType* constructorType = new FunctionType(arity, argSorts.begin(), taSort);
+  OperatorType* constructorType = OperatorType::getFunctionType(arity, argSorts.begin(), taSort);
   env.signature->getFunction(functor)->setType(constructorType);
   env.signature->getFunction(functor)->markTermAlgebraCons();
 
@@ -1001,8 +1001,8 @@ TermAlgebraConstructor* SMTLIB2::buildTermAlgebraConstructor(vstring constrName,
                                              : env.signature->addFunction(destructorName,  1, added);
     ASS(added);
 
-    BaseType* destructorType = isPredicate ? (BaseType*) new PredicateType(1, &taSort)
-                                           : (BaseType*) new FunctionType(1, &taSort, destructorSort);
+    OperatorType* destructorType = isPredicate ? OperatorType::getPredicateType(1, &taSort)
+                                           : OperatorType::getFunctionType(1, &taSort, destructorSort);
 
     LOG1("build destructor "+destructorName+": "+destructorType->toString());
 
@@ -1296,14 +1296,14 @@ void SMTLIB2::parseLetPrepareLookup(LExpr* exp)
     TermList trm;
     if (sort == Sorts::SRT_BOOL) {
       unsigned symb = env.signature->addFreshPredicate(0,"sLP");
-      PredicateType* type = new PredicateType(0, nullptr);
+      OperatorType* type = OperatorType::getPredicateType(0, nullptr);
       env.signature->getPredicate(symb)->setType(type);
 
       Formula* atom = new AtomicFormula(Literal::create(symb,0,true,false,nullptr));
       trm = TermList(Term::createFormula(atom));
     } else {
       unsigned symb = env.signature->addFreshFunction (0,"sLF");
-      FunctionType* type = new FunctionType(0, nullptr, sort);
+      OperatorType* type = OperatorType::getFunctionType(0, nullptr, sort);
       env.signature->getFunction(symb)->setType(type);
 
       trm = TermList(Term::createConstant(symb));
@@ -1497,8 +1497,7 @@ bool SMTLIB2::parseAsUserDefinedSymbol(const vstring& id,LExpr* exp)
 
   Signature::Symbol* symbol = isTrueFun ? env.signature->getFunction(symbIdx)
                                         : env.signature->getPredicate(symbIdx);
-  BaseType* type = isTrueFun ? static_cast<BaseType*>(symbol->fnType())
-                             : static_cast<BaseType*>(symbol->predType());
+  OperatorType* type = isTrueFun ? symbol->fnType() : symbol->predType();
 
   unsigned arity = symbol->arity();
 
@@ -2044,7 +2043,7 @@ void SMTLIB2::parseRankedFunctionApplication(LExpr* exp)
             bool added;
             unsigned pred = env.signature->addPredicate(c->discriminatorName(), 1, added);
             ASS(added);
-            PredicateType* type = new PredicateType({ sort });
+            OperatorType* type = OperatorType::getPredicateType({ sort });
             env.signature->getPredicate(pred)->setType(type);
             c->addDiscriminator(pred);
             // this predicate is not declare for the parser as it has a reserved name
diff --git a/Parse/TPTP.cpp b/Parse/TPTP.cpp
index bda72cbd53..c7fc21d4ce 100644
--- a/Parse/TPTP.cpp
+++ b/Parse/TPTP.cpp
@@ -1889,10 +1889,10 @@ void TPTP::endBinding() {
                                       : env.signature->addFreshFunction (arity,name.c_str());
 
   if (isPredicate) {
-    PredicateType* type = new PredicateType(arity, argSorts.begin());
+    OperatorType* type = OperatorType::getPredicateType(arity, argSorts.begin());
     env.signature->getPredicate(symbolNumber)->setType(type);
   } else {
-    FunctionType* type = new FunctionType(arity, argSorts.begin(), bindingSort);
+    OperatorType* type = OperatorType::getFunctionType(arity, argSorts.begin(), bindingSort);
     env.signature->getFunction(symbolNumber)->setType(type);
   }
 
@@ -1954,10 +1954,10 @@ void TPTP::endTupleBinding() {
     unsigned symbol;
     if (isPredicate) {
       symbol = env.signature->addFreshPredicate(0, name.c_str());
-      env.signature->getPredicate(symbol)->setType(new PredicateType(0, 0));
+      env.signature->getPredicate(symbol)->setType(OperatorType::getPredicateType(0, 0));
     } else {
       symbol = env.signature->addFreshFunction(0, name.c_str());
-      env.signature->getFunction(symbol)->setType(new FunctionType(sort));
+      env.signature->getFunction(symbol)->setType(OperatorType::getConstantsType(sort));
     }
 
     IntList::push(symbol, constants);
@@ -2499,7 +2499,7 @@ Formula* TPTP::createPredicateApplication(vstring name, unsigned arity)
   }
   // not equality or distinct
   Literal* lit = new(arity) Literal(pred,arity,true,false);
-  PredicateType* type = env.signature->getPredicate(pred)->predType();
+  OperatorType* type = env.signature->getPredicate(pred)->predType();
   bool safe = true;
   for (int i = arity-1;i >= 0;i--) {
     unsigned sort = type->arg(i);
@@ -2543,7 +2543,7 @@ TermList TPTP::createFunctionApplication(vstring name, unsigned arity)
   }
   Term* t = new(arity) Term;
   t->makeSymbol(fun,arity);
-  FunctionType* type = env.signature->getFunction(fun)->fnType();
+  OperatorType* type = env.signature->getFunction(fun)->fnType();
   bool safe = true;
   for (int i = arity-1;i >= 0;i--) {
     unsigned sort = type->arg(i);
@@ -3052,7 +3052,7 @@ void TPTP::endTff()
     if (!added) {
       USER_ERROR("Function symbol type is declared after its use: " + name);
     }
-    env.signature->getFunction(fun)->setType(new FunctionType(sortNumber));
+    env.signature->getFunction(fun)->setType(OperatorType::getConstantsType(sortNumber));
     return;
   }
 
@@ -3099,7 +3099,7 @@ void TPTP::endTff()
       USER_ERROR("Predicate symbol type is declared after its use: " + name);
     }
     symbol = env.signature->getPredicate(pred);
-    symbol->setType(new PredicateType(arity, sorts.begin()));
+    symbol->setType(OperatorType::getPredicateType(arity, sorts.begin()));
   }
   else {
     unsigned fun = arity == 0
@@ -3109,7 +3109,7 @@ void TPTP::endTff()
       USER_ERROR("Function symbol type is declared after its use: " + name);
     }
     symbol = env.signature->getFunction(fun);
-    symbol->setType(new FunctionType(arity, sorts.begin(), returnSortNumber));
+    symbol->setType(OperatorType::getFunctionType(arity, sorts.begin(), returnSortNumber));
   }
 } // endTff
 
@@ -3866,7 +3866,7 @@ unsigned TPTP::addIntegerConstant(const vstring& name, Set<vstring>& overflow, b
     if (added) {
       overflow.insert(name);
       Signature::Symbol* symbol = env.signature->getFunction(fun);
-      symbol->setType(new FunctionType(defaultSort ? Sorts::SRT_DEFAULT : Sorts::SRT_INTEGER));
+      symbol->setType(OperatorType::getConstantsType(defaultSort ? Sorts::SRT_DEFAULT : Sorts::SRT_INTEGER));
     }
     else if (!overflow.contains(name)) {
       USER_ERROR((vstring)"Cannot use name '" + name + "' as an atom name since it collides with an integer number");
@@ -3902,7 +3902,7 @@ unsigned TPTP::addRationalConstant(const vstring& name, Set<vstring>& overflow,
     if (added) {
       overflow.insert(name);
       Signature::Symbol* symbol = env.signature->getFunction(fun);
-      symbol->setType(new FunctionType(defaultSort ? Sorts::SRT_DEFAULT : Sorts::SRT_RATIONAL));
+      symbol->setType(OperatorType::getConstantsType(defaultSort ? Sorts::SRT_DEFAULT : Sorts::SRT_RATIONAL));
     }
     else if (!overflow.contains(name)) {
       USER_ERROR((vstring)"Cannot use name '" + name + "' as an atom name since it collides with an rational number");
@@ -3934,7 +3934,7 @@ unsigned TPTP::addRealConstant(const vstring& name, Set<vstring>& overflow, bool
     if (added) {
       overflow.insert(name);
       Signature::Symbol* symbol = env.signature->getFunction(fun);
-      symbol->setType(new FunctionType(defaultSort ? Sorts::SRT_DEFAULT : Sorts::SRT_REAL));
+      symbol->setType(OperatorType::getConstantsType(defaultSort ? Sorts::SRT_DEFAULT : Sorts::SRT_REAL));
     }
     else if (!overflow.contains(name)) {
       USER_ERROR((vstring)"Cannot use name '" + name + "' as an atom name since it collides with an real number");
diff --git a/Shell/AnswerExtractor.cpp b/Shell/AnswerExtractor.cpp
index 02a2fc1a84..7e811b4709 100644
--- a/Shell/AnswerExtractor.cpp
+++ b/Shell/AnswerExtractor.cpp
@@ -71,7 +71,7 @@ void AnswerExtractor::tryOutputAnswer(Clause* refutation)
       InterpretedLiteralEvaluator eval;
       unsigned p = env.signature->addFreshPredicate(1,"p"); 
       unsigned sort = SortHelper::getResultSort(aLit.term());
-      PredicateType* type = new PredicateType({sort});
+      OperatorType* type = OperatorType::getPredicateType({sort});
       env.signature->getPredicate(p)->setType(type);
       Literal* l = Literal::create1(p,true,aLit); 
       Literal* res =0;
@@ -355,7 +355,7 @@ Literal* AnswerLiteralManager::getAnswerLiteral(Formula::VarList* vars,Formula*
   unsigned vcnt = litArgs.size();
   unsigned pred = env.signature->addFreshPredicate(vcnt,"ans");
   Signature::Symbol* predSym = env.signature->getPredicate(pred);
-  predSym->setType(new PredicateType(sorts.size(), sorts.begin()));
+  predSym->setType(OperatorType::getPredicateType(sorts.size(), sorts.begin()));
   predSym->markAnswerPredicate();
   return Literal::create(pred, vcnt, true, false, litArgs.begin());
 }
diff --git a/Shell/EqualityProxy.cpp b/Shell/EqualityProxy.cpp
index e6519414f4..aab21d2f3b 100644
--- a/Shell/EqualityProxy.cpp
+++ b/Shell/EqualityProxy.cpp
@@ -180,7 +180,7 @@ void EqualityProxy::addAxioms(UnitList*& units)
  * equalities.
  */
 bool EqualityProxy::getArgumentEqualityLiterals(unsigned cnt, LiteralStack& lits,
-    Stack<TermList>& vars1, Stack<TermList>& vars2, BaseType* symbolType, bool skipSortsWithoutEquality)
+    Stack<TermList>& vars1, Stack<TermList>& vars2, OperatorType* symbolType, bool skipSortsWithoutEquality)
 {
   CALL("EqualityProxy::getArgumentEqualityLiterals");
   ASS_EQ(cnt, symbolType->arity());
@@ -229,7 +229,7 @@ void EqualityProxy::addCongruenceAxioms(UnitList*& units)
     if (arity == 0) {
       continue;
     }
-    FunctionType* fnType = fnSym->fnType();
+    OperatorType* fnType = fnSym->fnType();
     getArgumentEqualityLiterals(arity, lits, vars1, vars2, fnType, false);
     Term* t1 = Term::create(i, arity, vars1.begin());
     Term* t2 = Term::create(i, arity, vars2.begin());
@@ -359,7 +359,7 @@ unsigned EqualityProxy::getProxyPredicate(unsigned sort)
   }
   unsigned newPred = env.signature->addFreshPredicate(2,"sQ","eqProxy");
   Signature::Symbol* predSym = env.signature->getPredicate(newPred);
-  BaseType* predType = new PredicateType({sort, sort});
+  OperatorType* predType = OperatorType::getPredicateType({sort, sort});
   predSym->setType(predType);
   predSym->markEqualityProxy();
 
diff --git a/Shell/EqualityProxy.hpp b/Shell/EqualityProxy.hpp
index 403191d10a..4aff572ac2 100644
--- a/Shell/EqualityProxy.hpp
+++ b/Shell/EqualityProxy.hpp
@@ -74,7 +74,7 @@ class EqualityProxy
   void addAxioms(UnitList*& units);
   void addCongruenceAxioms(UnitList*& units);
   bool getArgumentEqualityLiterals(unsigned cnt, LiteralStack& lits, Stack<TermList>& vars1,
-      Stack<TermList>& vars2, BaseType* symbolType, bool skipSortsWithoutEquality);
+      Stack<TermList>& vars2, OperatorType* symbolType, bool skipSortsWithoutEquality);
   Literal* apply(Literal* lit);
   Literal* makeProxyLiteral(bool polarity, TermList arg0, TermList arg1, unsigned sort);
 
diff --git a/Shell/FOOLElimination.cpp b/Shell/FOOLElimination.cpp
index b933f35984..9ab4130e83 100644
--- a/Shell/FOOLElimination.cpp
+++ b/Shell/FOOLElimination.cpp
@@ -924,11 +924,11 @@ unsigned FOOLElimination::introduceFreshSymbol(Context context, const char* pref
   CALL("FOOLElimination::introduceFreshSymbol");
 
   unsigned arity = (unsigned)sorts.size();
-  BaseType* type;
+  OperatorType* type;
   if (context == FORMULA_CONTEXT) {
-    type = new PredicateType(arity, sorts.begin());
+    type = OperatorType::getPredicateType(arity, sorts.begin());
   } else {
-    type = new FunctionType(arity, sorts.begin(), resultSort);
+    type = OperatorType::getFunctionType(arity, sorts.begin(), resultSort);
   }
 
   unsigned symbol;
diff --git a/Shell/GeneralSplitting.cpp b/Shell/GeneralSplitting.cpp
index b12c43a2cc..a4e7a6f719 100644
--- a/Shell/GeneralSplitting.cpp
+++ b/Shell/GeneralSplitting.cpp
@@ -242,7 +242,7 @@ bool GeneralSplitting::apply(Clause*& cl, UnitList*& resultStack)
 
 
   unsigned namingPred=env.signature->addNamePredicate(minDeg);
-  BaseType* npredType = new PredicateType(minDeg, argSorts.begin());
+  OperatorType* npredType = OperatorType::getPredicateType(minDeg, argSorts.begin());
   env.signature->getPredicate(namingPred)->setType(npredType);
 
   if(mdvColor!=COLOR_TRANSPARENT && otherColor!=COLOR_TRANSPARENT) {
diff --git a/Shell/Grounding.cpp b/Shell/Grounding.cpp
index 156943ed50..2ddc398ba9 100644
--- a/Shell/Grounding.cpp
+++ b/Shell/Grounding.cpp
@@ -180,7 +180,7 @@ ClauseList* Grounding::getEqualityAxioms(bool otherThanReflexivity)
 	continue;
       }
 
-      PredicateType* predType = env.signature->getPredicate(pred)->predType();
+      OperatorType* predType = env.signature->getPredicate(pred)->predType();
 
       args.ensure(arity);
       for(unsigned i=0;i<arity;i++) {
diff --git a/Shell/InequalitySplitting.cpp b/Shell/InequalitySplitting.cpp
index 89e7876ff1..d3ff5368d8 100644
--- a/Shell/InequalitySplitting.cpp
+++ b/Shell/InequalitySplitting.cpp
@@ -161,7 +161,7 @@ Literal* InequalitySplitting::splitLiteral(Literal* lit, Unit::InputType inpType
 
   unsigned predNum=env.signature->addNamePredicate(1);
   unsigned srt = SortHelper::getEqualityArgumentSort(lit);
-  BaseType* type = new PredicateType({srt});
+  OperatorType* type = OperatorType::getPredicateType({srt});
 
   Signature::Symbol* predSym = env.signature->getPredicate(predNum);
   predSym->setType(type);
diff --git a/Shell/Naming.cpp b/Shell/Naming.cpp
index fb003d173e..0f3988c7f4 100644
--- a/Shell/Naming.cpp
+++ b/Shell/Naming.cpp
@@ -1161,7 +1161,7 @@ Literal* Naming::getDefinitionLiteral(Formula* f, Formula::VarList* freeVars) {
     predArgs.push(TermList(uvar, false));
   }
 
-  predSym->setType(new PredicateType(length, domainSorts.begin()));
+  predSym->setType(OperatorType::getPredicateType(length, domainSorts.begin()));
 
   return Literal::create(pred, length, true, false, predArgs.begin());
 }
diff --git a/Shell/NewCNF.cpp b/Shell/NewCNF.cpp
index 160355b95d..a6afe30a02 100644
--- a/Shell/NewCNF.cpp
+++ b/Shell/NewCNF.cpp
@@ -556,7 +556,7 @@ TermList NewCNF::eliminateLet(Term::SpecialTermData *sd, TermList contents)
     IntList* symbols = sd->getTupleSymbols();
     unsigned bodySort = sd->getSort();
 
-    FunctionType* tupleType = env.signature->getFunction(tupleFunctor)->fnType();
+    OperatorType* tupleType = env.signature->getFunction(tupleFunctor)->fnType();
 
     Term* bindingTuple = binding.term()->getSpecialData()->getTupleTerm();
     unsigned arity = IntList::length(symbols);
@@ -595,13 +595,13 @@ TermList NewCNF::eliminateLet(Term::SpecialTermData *sd, TermList contents)
     IntList* symbols = sd->getTupleSymbols();
     unsigned bodySort = sd->getSort();
 
-    FunctionType* tupleType = env.signature->getFunction(tupleFunctor)->fnType();
+    OperatorType* tupleType = env.signature->getFunction(tupleFunctor)->fnType();
     unsigned tupleSort = tupleType->result();
 
     ASS_EQ(tupleType->arity(), IntList::length(symbols));
 
     unsigned tuple = env.signature->addFreshFunction(0, "tuple");
-    env.signature->getFunction(tuple)->setType(new FunctionType(tupleSort));
+    env.signature->getFunction(tuple)->setType(OperatorType::getConstantsType(tupleSort));
 
     TermList tupleTerm = TermList(Term::createConstant(tuple));
 
@@ -740,11 +740,11 @@ TermList NewCNF::nameLetBinding(unsigned symbol, Formula::VarList* bindingVariab
     }
 
     if (isPredicate) {
-      PredicateType* type = new PredicateType(nameArity, sorts.begin());
+      OperatorType* type = OperatorType::getPredicateType(nameArity, sorts.begin());
       freshSymbol = env.signature->addFreshPredicate(nameArity, "lG");
       env.signature->getPredicate(freshSymbol)->setType(type);
     } else {
-      FunctionType* type = new FunctionType(nameArity, sorts.begin(), nameSort);
+      OperatorType* type = OperatorType::getFunctionType(nameArity, sorts.begin(), nameSort);
       freshSymbol = env.signature->addFreshFunction(nameArity, "lG");
       env.signature->getFunction(freshSymbol)->setType(type);
     }
@@ -1095,7 +1095,7 @@ Literal* NewCNF::createNamingLiteral(Formula* f, List<unsigned>* free)
     predArgs.push(TermList(uvar, false));
   }
 
-  predSym->setType(new PredicateType(length, domainSorts.begin()));
+  predSym->setType(OperatorType::getPredicateType(length, domainSorts.begin()));
 
   return Literal::create(pred, length, true, false, predArgs.begin());
 }
diff --git a/Shell/Property.cpp b/Shell/Property.cpp
index 51eff89c62..521b5d673c 100644
--- a/Shell/Property.cpp
+++ b/Shell/Property.cpp
@@ -531,7 +531,7 @@ void Property::scan(Literal* lit, int polarity, unsigned cLen, bool goal)
       pred->markInGoal();
     }
 
-    PredicateType* type = pred->predType();
+    OperatorType* type = pred->predType();
     for (int i=0; i<arity; i++) {
       scanSort(type->arg(i));
     }
@@ -597,7 +597,7 @@ void Property::scan(TermList ts,bool unit,bool goal)
     if(goal){ func->markInGoal();}
 
     int arity = t->arity();
-    FunctionType* type = func->fnType();
+    OperatorType* type = func->fnType();
     for (int i = 0; i < arity; i++) {
       scanSort(type->arg(i));
     }
diff --git a/Shell/Skolem.cpp b/Shell/Skolem.cpp
index aed97529ea..d8936a8851 100644
--- a/Shell/Skolem.cpp
+++ b/Shell/Skolem.cpp
@@ -139,7 +139,7 @@ unsigned Skolem::addSkolemFunction(unsigned arity, unsigned* domainSorts,
 
   unsigned fun = env.signature->addSkolemFunction(arity, suffix);
   Signature::Symbol* fnSym = env.signature->getFunction(fun);
-  fnSym->setType(new FunctionType(arity, domainSorts, rangeSort));
+  fnSym->setType(OperatorType::getFunctionType(arity, domainSorts, rangeSort));
   return fun;
 }
 
@@ -163,7 +163,7 @@ unsigned Skolem::addSkolemPredicate(unsigned arity, unsigned* domainSorts, const
 
   unsigned pred = env.signature->addSkolemPredicate(arity, suffix);
   Signature::Symbol* pSym = env.signature->getPredicate(pred);
-  pSym->setType(new PredicateType(arity, domainSorts));
+  pSym->setType(OperatorType::getPredicateType(arity, domainSorts));
   return pred;
 }
 
diff --git a/Shell/TPTPPrinter.cpp b/Shell/TPTPPrinter.cpp
index 3ff0b98417..15258e039b 100644
--- a/Shell/TPTPPrinter.cpp
+++ b/Shell/TPTPPrinter.cpp
@@ -201,7 +201,7 @@ void TPTPPrinter::outputSymbolTypeDefinitions(unsigned symNumber, bool function)
 
   Signature::Symbol* sym = function ?
       env.signature->getFunction(symNumber) : env.signature->getPredicate(symNumber);
-  BaseType* type = function ? static_cast<BaseType*>(sym->fnType()) : static_cast<BaseType*>(sym->predType());
+  OperatorType* type = function ? sym->fnType() : sym->predType();
 
   if(type->isAllDefault()) {
     return;
@@ -258,13 +258,13 @@ void TPTPPrinter::ensureNecesarySorts()
   }
   unsigned i;
   List<unsigned> *_usedSorts(0);
-  BaseType* type;
+  OperatorType* type;
   Signature::Symbol* sym;
   unsigned sorts = env.sorts->count();
   //check the sorts of the function symbols and collect information about used sorts
   for (i = 0; i < env.signature->functions(); i++) {
     sym = env.signature->getFunction(i);
-    type = static_cast<BaseType*>(sym->fnType());
+    type = sym->fnType();
     unsigned arity = sym->arity();
     if (arity > 0) {
       for (unsigned i = 0; i < arity; i++) {
@@ -276,7 +276,7 @@ void TPTPPrinter::ensureNecesarySorts()
   //check the sorts of the predicates and collect information about used sorts
   for (i = 0; i < env.signature->predicates(); i++) {
     sym = env.signature->getPredicate(i);
-    type = static_cast<BaseType*>(sym->predType());
+    type = sym->predType();
     unsigned arity = sym->arity();
     if (arity > 0) {
       for (unsigned i = 0; i < arity; i++) {
diff --git a/Shell/TermAlgebra.cpp b/Shell/TermAlgebra.cpp
index 5220c0e852..89d655ae70 100644
--- a/Shell/TermAlgebra.cpp
+++ b/Shell/TermAlgebra.cpp
@@ -141,7 +141,7 @@ unsigned TermAlgebra::getSubtermPredicate() {
     // declare a binary predicate subterm
     Stack<unsigned> args;
     args.push(_sort); args.push(_sort);
-    env.signature->getPredicate(s)->setType(new PredicateType(args.size(),args.begin()));
+    env.signature->getPredicate(s)->setType(OperatorType::getPredicateType(args.size(),args.begin()));
   }
 
   return s;
diff --git a/Shell/TermAlgebra.hpp b/Shell/TermAlgebra.hpp
index 7cf024ecab..3b4f0fad6d 100644
--- a/Shell/TermAlgebra.hpp
+++ b/Shell/TermAlgebra.hpp
@@ -25,6 +25,7 @@
 #include "Lib/List.hpp"
 #include "Lib/Array.hpp"
 #include "Lib/VString.hpp"
+#include "Kernel/Sorts.hpp"
 
 namespace Shell {
   class TermAlgebraConstructor {
@@ -59,7 +60,7 @@ namespace Shell {
     Lib::vstring discriminatorName();
     
   private:
-    Kernel::FunctionType* _type;
+    Kernel::OperatorType* _type;
     unsigned _functor;
     bool _hasDiscriminator;
     unsigned _discriminator;
diff --git a/Shell/TheoryAxioms.cpp b/Shell/TheoryAxioms.cpp
index b12fbc50e5..e9c997a5b8 100644
--- a/Shell/TheoryAxioms.cpp
+++ b/Shell/TheoryAxioms.cpp
@@ -587,7 +587,7 @@ void TheoryAxioms::addIntegerDividesAxioms(Interpretation divides, Interpretatio
   // create a skolem function with signature srt*srt>srt
   unsigned skolem = env.signature->addSkolemFunction(2);
   Signature::Symbol* sym = env.signature->getFunction(skolem);
-  sym->setType(new FunctionType({srt,srt},srt));
+  sym->setType(OperatorType::getFunctionType({srt,srt},srt));
   TermList skXY(Term::create2(skolem,n,y));
   TermList msxX(Term::create2(mulFun,skXY,n));
   Literal* msxXeqY = Literal::createEquality(true,msxX,y,srt);
diff --git a/Shell/UIHelper.cpp b/Shell/UIHelper.cpp
index a7664113c3..a880b2420c 100644
--- a/Shell/UIHelper.cpp
+++ b/Shell/UIHelper.cpp
@@ -594,7 +594,7 @@ void UIHelper::outputSymbolTypeDeclarationIfNeeded(ostream& out, bool function,
     }
   }
 
-  BaseType* type = function ? static_cast<BaseType*>(sym->fnType()) : sym->predType();
+  OperatorType* type = function ? sym->fnType() : sym->predType();
 
   if (type->isAllDefault()) {
     return;