Polymorphic arrays

Indexing/TermSharing.cpp

@@ -152,36 +152,33 @@ void TermSharing::computeAndSetSharedSortData(AtomicSort* sort)
 
   TIME_TRACE("sort sharing");
 
-    if(sort->isArraySort()){
-      _arraySorts.insert(TermList(sort));
+  unsigned weight = 1;
+  unsigned vars = 0;
+
+  for (TermList* tt = sort->args(); ! tt->isEmpty(); tt = tt->next()) {
+    if (tt->isVar()) {
+      ASS(tt->isOrdinaryVar());
+      vars++;
+      weight += 1;
     }
-    unsigned weight = 1;
-    unsigned vars = 0;
+    else {
+      ASS_REP(tt->term()->shared(), tt->term()->toString());
+
+      Term* r = tt->term();
 
-    for (TermList* tt = sort->args(); ! tt->isEmpty(); tt = tt->next()) {
-      if (tt->isVar()) {
-        ASS(tt->isOrdinaryVar());
-        vars++;
-        weight += 1;
-      }
-      else {
-        ASS_REP(tt->term()->shared(), tt->term()->toString());
-
-        Term* r = tt->term();
-
-        vars += r->numVarOccs();
-        weight += r->weight();
-      }
-    }
-    sort->markShared();
-    sort->setId(_sorts.size());
-    sort->setNumVarOccs(vars);
-    sort->setWeight(weight);
-
-    ASS_REP(SortHelper::allTopLevelArgsAreSorts(sort), sort->toString());
-    if (!SortHelper::allTopLevelArgsAreSorts(sort)){
-      USER_ERROR("Immediate subterms of sort "+sort->toString()+" are not all sorts as mandated in rank-1 polymorphism!");      
+      vars += r->numVarOccs();
+      weight += r->weight();
     }
+  }
+  sort->markShared();
+  sort->setId(_sorts.size());
+  sort->setNumVarOccs(vars);
+  sort->setWeight(weight);
+
+  ASS_REP(SortHelper::allTopLevelArgsAreSorts(sort), sort->toString());
+  if (!SortHelper::allTopLevelArgsAreSorts(sort)){
+    USER_ERROR("Immediate subterms of sort "+sort->toString()+" are not all sorts as mandated in rank-1 polymorphism!");      
+  }
 } // TermSharing::computeAndSetSharedSortData
 
 /** same as `TermSharing::computeAndSetSharedTermData(Term*)` but for literals 

Indexing/TermSharing.hpp

@@ -18,7 +18,6 @@
 #define __TermSharing__
 
 #include "Lib/Set.hpp"
-#include "Lib/DHSet.hpp"
 #include "Kernel/Term.hpp"
 
 using namespace Lib;
@@ -60,10 +59,6 @@ class TermSharing
         [&](auto i){ return *l2->nthArgument(i); }, 
         l2->arity(), someIf(l2->isTwoVarEquality(), [&](){ return l2->twoVarEqSort(); })); }
 
-  DHSet<TermList>* getArraySorts(){
-    return &_arraySorts;
-  }
-
   struct OpLitWrapper {
     OpLitWrapper(Literal* l) : l(l) {}
     Literal* l;
@@ -103,10 +98,6 @@ class TermSharing
   Set<Literal*,TermSharing> _literals;
   /** The set storing all sorts */
   Set<AtomicSort*,TermSharing> _sorts;
-  /* Set containing all array sorts. 
-   * Can be deleted once array axioms are made truly poltmorphic
-   */  
-  DHSet<TermList> _arraySorts;
 
   bool _poly;
   bool _wellSortednessCheckingDisabled;

Inferences/PolynomialEvaluation.cpp

@@ -110,8 +110,6 @@ Option<LitSimplResult> PolynomialEvaluation::tryEvalPredicate(Literal* orig, Pol
 
       /* integer predicates */
       HANDLE_CASE(INT_DIVIDES)
-      case Interpretation::ARRAY_BOOL_SELECT:
-        return Option<LitSimplResult>();
 
       case ANY_INTERPRETED_FUNCTION: 
       case Kernel::Theory::INVALID_INTERPRETATION: 

Inferences/TheoryInstAndSimp.cpp

@@ -169,7 +169,6 @@ bool TheoryInstAndSimp::isSupportedFunction(Term* trm) {
 
 bool TheoryInstAndSimp::isSupportedFunction(Theory::Interpretation itp) {
   switch (itp) {
-    case Theory::ARRAY_BOOL_SELECT:
     case Theory::ARRAY_SELECT:
     case Theory::ARRAY_STORE:
     case Theory::INT_SUCCESSOR:

Kernel/InferenceStore.cpp

@@ -1137,7 +1137,6 @@ struct InferenceStore::Smt2ProofCheckPrinter
       case Theory::REAL_QUOTIENT: out << "/"; return;
 
       // array functions
-      case Theory::ARRAY_BOOL_SELECT:
       case Theory::ARRAY_SELECT: out << "select"; return;
       case Theory::ARRAY_STORE: out << "store"; return;
 
@@ -1240,7 +1239,6 @@ struct InferenceStore::Smt2ProofCheckPrinter
       case Theory::INT_REMAINDER_E:                                                       \
       case Theory::INT_FLOOR:                                                             \
       case Theory::REAL_QUOTIENT:                                                         \
-      case Theory::ARRAY_BOOL_SELECT:                                                     \
       case Theory::ARRAY_SELECT:                                                          \
       case Theory::ARRAY_STORE
 

Kernel/Signature.cpp

@@ -260,7 +260,7 @@ Signature::Signature ():
 void Signature::addEquality()
 {
   // initialize equality
-  addInterpretedPredicate(Theory::EQUAL, OperatorType::getPredicateType(2), "=");
+  addInterpretedPredicate(Theory::EQUAL, "=");
   ASS_EQ(predicateName(0), "="); //equality must have number 0
   getPredicate(0)->markSkip();
 }
@@ -285,29 +285,28 @@ Signature::~Signature ()
 /**
  * Add interpreted function
  */
-unsigned Signature::addInterpretedFunction(Interpretation interpretation, OperatorType* type, const std::string& name)
+unsigned Signature::addInterpretedFunction(Interpretation interpretation, const std::string& name)
 {
   ASS(Theory::isFunction(interpretation));
 
-  Theory::MonomorphisedInterpretation mi = std::make_pair(interpretation,type);
-
   unsigned res;
-  if (_iSymbols.find(mi,res)) { // already declared
+  if (_iSymbols.find(interpretation,res)) { // already declared
     // TODO should this really be done in release mode?
     if (name!=functionName(res)) {
       USER_ERROR("Interpreted function '"+functionName(res)+"' has the same interpretation as '"+name+"' should have");
     }
     return res;
   }
 
+  auto type = Theory::getOperatorType(interpretation);
   auto symbolKey = SymbolKey(std::make_pair(interpretation, type));
   ASS_REP(!_funNames.find(symbolKey), name);
 
   unsigned fnNum = _funs.length();
   InterpretedSymbol* sym = new InterpretedSymbol(name, interpretation);
   _funs.push(sym);
   _funNames.insert(symbolKey, fnNum);
-  ALWAYS(_iSymbols.insert(mi, fnNum));
+  ALWAYS(_iSymbols.insert(interpretation, fnNum));
 
   OperatorType* fnType = type;
   ASS(fnType->isFunctionType());
@@ -318,22 +317,21 @@ unsigned Signature::addInterpretedFunction(Interpretation interpretation, Operat
 /**
  * Add interpreted predicate
  */
-unsigned Signature::addInterpretedPredicate(Interpretation interpretation, OperatorType* type, const std::string& name)
+unsigned Signature::addInterpretedPredicate(Interpretation interpretation, const std::string& name)
 {
   ASS(!Theory::isFunction(interpretation));
 
   // cout << "addInterpretedPredicate " << (type ? type->toString() : "nullptr") << " " << name << endl;
 
-  Theory::MonomorphisedInterpretation mi = std::make_pair(interpretation,type);
-
   unsigned res;
-  if (_iSymbols.find(mi,res)) { // already declared
+  if (_iSymbols.find(interpretation,res)) { // already declared
     if (name!=predicateName(res)) {
       USER_ERROR("Interpreted predicate '"+predicateName(res)+"' has the same interpretation as '"+name+"' should have");
     }
     return res;
   }
 
+  auto type = Theory::getOperatorType(interpretation);
   auto symbolKey = SymbolKey(std::make_pair(interpretation, type));
 
   // cout << "symbolKey " << symbolKey << endl;
@@ -344,7 +342,7 @@ unsigned Signature::addInterpretedPredicate(Interpretation interpretation, Opera
   InterpretedSymbol* sym = new InterpretedSymbol(name, interpretation);
   _preds.push(sym);
   _predNames.insert(symbolKey,predNum);
-  ALWAYS(_iSymbols.insert(mi, predNum));
+  ALWAYS(_iSymbols.insert(interpretation, predNum));
   if (predNum!=0) {
     OperatorType* predType = type;
     ASS_REP(!predType->isFunctionType(), predType->toString());
@@ -359,12 +357,10 @@ unsigned Signature::addInterpretedPredicate(Interpretation interpretation, Opera
  *
  * If no such symbol exists, it is created.
  */
-unsigned Signature::getInterpretingSymbol(Interpretation interp, OperatorType* type)
+unsigned Signature::getInterpretingSymbol(Interpretation interp)
 {
-  Theory::MonomorphisedInterpretation mi = std::make_pair(interp,type);
-
   unsigned res;
-  if (_iSymbols.find(mi, res)) {
+  if (_iSymbols.find(interp, res)) {
     return res;
   }
 
@@ -379,7 +375,7 @@ unsigned Signature::getInterpretingSymbol(Interpretation interp, OperatorType* t
       }
       name=name+Int::toString(i);
     }
-    addInterpretedFunction(interp, type, name);
+    addInterpretedFunction(interp, name);
   }
   else {
     if (predicateExists(name, arity)) {
@@ -389,11 +385,11 @@ unsigned Signature::getInterpretingSymbol(Interpretation interp, OperatorType* t
       }
       name=name+Int::toString(i);
     }
-    addInterpretedPredicate(interp, type, name);
+    addInterpretedPredicate(interp, name);
   }
 
   //we have now registered a new function, so it should be present in the map
-  return _iSymbols.get(mi);
+  return _iSymbols.get(interp);
 }
 
 const std::string& Signature::functionName(int number)

Kernel/Signature.hpp

@@ -593,36 +593,14 @@ class Signature
     }
   }
 
-
-  unsigned addInterpretedFunction(Interpretation itp, OperatorType* type, const std::string& name);
-  unsigned addInterpretedFunction(Interpretation itp, const std::string& name)
-  {
-    ASS(!Theory::isPolymorphic(itp));
-    return addInterpretedFunction(itp,Theory::getNonpolymorphicOperatorType(itp),name);
-  }
-
-  unsigned addInterpretedPredicate(Interpretation itp, OperatorType* type, const std::string& name);
-  unsigned addInterpretedPredicate(Interpretation itp, const std::string& name)
-  {
-    ASS(!Theory::isPolymorphic(itp));
-    return addInterpretedPredicate(itp,Theory::getNonpolymorphicOperatorType(itp),name);
-  }
-
-  unsigned getInterpretingSymbol(Interpretation interp, OperatorType* type);
-  unsigned getInterpretingSymbol(Interpretation interp)
-  {
-    ASS(!Theory::isPolymorphic(interp));
-    return getInterpretingSymbol(interp,Theory::getNonpolymorphicOperatorType(interp));
-  }
+  unsigned addInterpretedFunction(Interpretation itp, const std::string& name);
+  unsigned addInterpretedPredicate(Interpretation itp, const std::string& name);
+  unsigned getInterpretingSymbol(Interpretation interp);
 
   /** Return true iff there is a symbol interpreted by Interpretation @b interp */
-  bool haveInterpretingSymbol(Interpretation interp, OperatorType* type) const {
-    return _iSymbols.find(std::make_pair(interp,type));
-  }
-  bool haveInterpretingSymbol(Interpretation interp)
+  bool hasInterpretingSymbol(Interpretation interp) const
   {
-    ASS(!Theory::isPolymorphic(interp));
-    return haveInterpretingSymbol(interp,Theory::getNonpolymorphicOperatorType(interp));
+    return _iSymbols.find(interp);
   }
 
   /** return the name of a function with a given number */
@@ -1037,13 +1015,13 @@ class Signature
   bool _distinctGroupsAddedTo;
 
   /**
-   * Map from MonomorphisedInterpretation values to function and predicate symbols representing them
+   * Map from Interpretation values to function and predicate symbols representing them
    *
    * We mix here function and predicate symbols, but it is not a problem, as
-   * the MonomorphisedInterpretation value already determines whether we deal with a function
+   * the Interpretation value already determines whether we deal with a function
    * or a predicate.
    */
-  DHMap<Theory::MonomorphisedInterpretation, unsigned> _iSymbols;
+  DHMap<Theory::Interpretation, unsigned> _iSymbols;
 
   /** the number of string constants */
   unsigned _strings;

Kernel/Term.cpp

@@ -554,7 +554,7 @@ std::string Term::headToString() const
         auto bindingLhs = binding->literal()->termArg(0).term();
 
         std::string type;
-        if (Theory::tuples()->isConstructor(bindingLhs)) {
+        if (Theory::isTupleConstructor(bindingLhs)) {
           type += "[";
           for (unsigned i = 0; i < bindingLhs->numTermArguments(); i++) {
             auto arg = bindingLhs->termArg(i);
@@ -614,7 +614,7 @@ std::string Term::headToString() const
     }
   } else {
     unsigned proj;
-    if (!isSort() && Theory::tuples()->findProjection(functor(), isLiteral(), proj)) {
+    if (!isSort() && Theory::findTupleProjection(functor(), isLiteral(), proj)) {
       return "$proj(" + Int::toString(proj) + ", ";
     }
     std::string name = "";
@@ -889,7 +889,7 @@ std::string Literal::toString(bool reverseEquality) const
   }
 
   unsigned proj;
-  if (Theory::tuples()->findProjection(functor(), true, proj)) {
+  if (Theory::findTupleProjection(functor(), true, proj)) {
     return s + "$proj(" + Int::toString(proj) + ", " + args()->asArgsToString();
   }
   s += predicateName();