OperatorType class for types of predicate and function symbols; perfe…

…ctly hashed

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;

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++){

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);

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);
 

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; }

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);

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;

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;

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);

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);
   }