structured inpretretations done differently

ModelWriter · Nov 15, 2017 · 5acc529 · 5acc529
1 parent 44240ce
commit 5acc529
Show file tree

Hide file tree

Showing 12 changed files with 374 additions and 641 deletions.
diff --git a/Kernel/InterpretedLiteralEvaluator.cpp b/Kernel/InterpretedLiteralEvaluator.cpp
@@ -281,13 +281,6 @@ class InterpretedLiteralEvaluator::TypedEvaluator : public Evaluator
   virtual bool canEvaluate(Interpretation interp)
   {
     CALL("InterpretedLiteralEvaluator::TypedEvaluator::canEvaluate");
-
-    //only interpreted operations with non-single argument sort are array operations
-    if (theory->isArrayOperation(interp))
-    {
-        unsigned opSort = theory->getArrayOperationSort(interp);
-        return opSort==T::getSort();
-    }
 
     // This is why we cannot evaluate Equality here... we cannot determine its sort
     if (!theory->hasSingleSort(interp)) { return false; } //To skip conversions and EQUAL

diff --git a/Kernel/Signature.cpp b/Kernel/Signature.cpp
@@ -261,69 +261,6 @@ Signature::~Signature ()
   }
 } // Signature::~Signature
 
-/**
- * Add interpreted function
- */
-unsigned Signature::addInterpretedFunction(Interpretation interpretation, const vstring& name)
-{
-  CALL("Signature::addInterpretedFunction");
-  ASS(Theory::isFunction(interpretation));
-
-  unsigned res;
-  if (_iSymbols.find(interpretation,res)) { // already declared
-    if (name!=functionName(res)) {
-      USER_ERROR("Interpreted function '"+functionName(res)+"' has the same interpretation as '"+name+"' should have");
-    }
-    return res;
-  }
-
-  vstring symbolKey = name+"_i"+Int::toString(interpretation);
-  ASS(!_funNames.find(symbolKey));
-
-  unsigned fnNum = _funs.length();
-  InterpretedSymbol* sym = new InterpretedSymbol(name, interpretation);
-  _funs.push(sym);
-  _funNames.insert(symbolKey, fnNum);
-  ALWAYS(_iSymbols.insert(interpretation, fnNum));
-  OperatorType* fnType = Theory::getOperationType(interpretation);
-  ASS(fnType->isFunctionType());
-  sym->setType(fnType);
-  return fnNum;
-} // Signature::addInterpretedFunction
-
-/**
- * Add interpreted predicate
- */
-unsigned Signature::addInterpretedPredicate(Interpretation interpretation, const vstring& name)
-{
-  CALL("Signature::addInterpretedPredicate");
-  ASS(!Theory::isFunction(interpretation));
-
-  unsigned res;
-  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;
-  }
-
-  vstring symbolKey = name+"_i"+Int::toString(interpretation);
-
-  ASS(!_predNames.find(symbolKey));
-
-  unsigned predNum = _preds.length();
-  InterpretedSymbol* sym = new InterpretedSymbol(name, interpretation);
-  _preds.push(sym);
-  _predNames.insert(symbolKey,predNum);
-  ALWAYS(_iSymbols.insert(interpretation, predNum));
-  if (predNum!=0) {
-    OperatorType* predType = Theory::getOperationType(interpretation);
-    ASS_REP(!predType->isFunctionType(), predType->toString());
-    sym->setType(predType);
-  }
-  return predNum;
-} // Signature::addInterpretedPredicate
-
 /**
  * Add an integer constant to the signature. If defaultSort is true, treat it as
  * a term of the default sort, otherwise as an interepreted integer value.
@@ -475,19 +412,88 @@ unsigned Signature::addRealConstant(const RealConstantType& value)
   return result;
 }
 
+/**
+ * Add interpreted function
+ */
+unsigned Signature::addInterpretedFunction(Interpretation interpretation, OperatorType* type, const vstring& name)
+{
+  CALL("Signature::addInterpretedFunction(Interpretation,OperatorType*,const vstring&)");
+  ASS(Theory::isFunction(interpretation));
+
+  Theory::MonomorphisedInterpretation mi = std::make_pair(interpretation,type);
+
+  unsigned res;
+  if (_iSymbols.find(mi,res)) { // already declared
+    if (name!=functionName(res)) {
+      USER_ERROR("Interpreted function '"+functionName(res)+"' has the same interpretation as '"+name+"' should have");
+    }
+    return res;
+  }
+
+  vstring symbolKey = name+"_i"+Int::toString(interpretation)+(Theory::isPolymorphic(interpretation) ? type->toString() : "");
+  ASS(!_funNames.find(symbolKey));
+
+  unsigned fnNum = _funs.length();
+  InterpretedSymbol* sym = new InterpretedSymbol(name, interpretation);
+  _funs.push(sym);
+  _funNames.insert(symbolKey, fnNum);
+  ALWAYS(_iSymbols.insert(mi, fnNum));
+
+  OperatorType* fnType = Theory::getNonpolymorphicOperatorType(interpretation);
+  ASS(fnType->isFunctionType());
+  sym->setType(fnType);
+  return fnNum;
+} // Signature::addInterpretedFunction
+
+/**
+ * Add interpreted predicate
+ */
+unsigned Signature::addInterpretedPredicate(Interpretation interpretation, OperatorType* type, const vstring& name)
+{
+  CALL("Signature::addInterpretedPredicate(Interpretation,OperatorType*,const vstring&)");
+  ASS(!Theory::isFunction(interpretation));
+
+  Theory::MonomorphisedInterpretation mi = std::make_pair(interpretation,type);
+
+  unsigned res;
+  if (_iSymbols.find(mi,res)) { // already declared
+    if (name!=predicateName(res)) {
+      USER_ERROR("Interpreted predicate '"+predicateName(res)+"' has the same interpretation as '"+name+"' should have");
+    }
+    return res;
+  }
+
+  vstring symbolKey = name+"_i"+Int::toString(interpretation)+(Theory::isPolymorphic(interpretation) ? type->toString() : "");
+
+  ASS(!_predNames.find(symbolKey));
+
+  unsigned predNum = _preds.length();
+  InterpretedSymbol* sym = new InterpretedSymbol(name, interpretation);
+  _preds.push(sym);
+  _predNames.insert(symbolKey,predNum);
+  ALWAYS(_iSymbols.insert(mi, predNum));
+  if (predNum!=0) {
+    OperatorType* predType = Theory::getNonpolymorphicOperatorType(interpretation);
+    ASS_REP(!predType->isFunctionType(), predType->toString());
+    sym->setType(predType);
+  }
+  return predNum;
+} // Signature::addInterpretedPredicate
+
+
 /**
  * Return number of symbol that is interpreted by Interpretation @b interp.
  *
  * If no such symbol exists, it is created.
  */
-unsigned Signature::getInterpretingSymbol(Interpretation interp)
+unsigned Signature::getInterpretingSymbol(Interpretation interp, OperatorType* type)
 {
-  CALL("Signature::getInterpretingSymbol");
+  CALL("Signature::getInterpretingSymbol(Interpretation,OperatorType*)");
 
-  ASS(Theory::instance()->isValidInterpretation(interp));
-    
+  Theory::MonomorphisedInterpretation mi = std::make_pair(interp,type);
+
   unsigned res;
-  if (_iSymbols.find(interp, res)) {
+  if (_iSymbols.find(mi, res)) {
     return res;
   }
 
@@ -502,7 +508,7 @@ unsigned Signature::getInterpretingSymbol(Interpretation interp)
       }
       name=name+Int::toString(i);
     }
-    addInterpretedFunction(interp, name);
+    addInterpretedFunction(interp, type, name);
   }
   else {
     if (predicateExists(name, arity)) {
@@ -512,17 +518,11 @@ unsigned Signature::getInterpretingSymbol(Interpretation interp)
       }
       name=name+Int::toString(i);
     }
-    addInterpretedPredicate(interp, name);
+    addInterpretedPredicate(interp, type, name);
   }
 
   //we have now registered a new function, so it should be present in the map
-  return _iSymbols.get(interp);
-}
-
-unsigned Signature::getStructureInterpretationFunctor(unsigned theorySort, Theory::StructuredSortInterpretation ssi) {
-  CALL("Signature::getStructureInterpretationFunctor");
-  Interpretation i = Theory::instance()->getInterpretation(theorySort, ssi);
-  return env.signature->getInterpretingSymbol(i);
+  return _iSymbols.get(mi);
 }
 
 const vstring& Signature::functionName(int number)

diff --git a/Kernel/Signature.hpp b/Kernel/Signature.hpp
@@ -335,10 +335,6 @@ class Signature
   unsigned addNamePredicate(unsigned arity);
 
   // Interpreted symbol declarations
-
-  unsigned addInterpretedFunction(Interpretation itp, const vstring& name);
-  unsigned addInterpretedPredicate(Interpretation itp, const vstring& name);
-
   unsigned addIntegerConstant(const vstring& number,bool defaultSort);
   unsigned addRationalConstant(const vstring& numerator, const vstring& denominator,bool defaultSort);
   unsigned addRealConstant(const vstring& number,bool defaultSort);
@@ -347,27 +343,40 @@ class Signature
   unsigned addRationalConstant(const RationalConstantType& number);
   unsigned addRealConstant(const RealConstantType& number);
 
-  vstring getInterpretationName(Interpretation interp);
-  unsigned getInterpretingSymbol(Interpretation interp);
-
-  unsigned getStructureInterpretationFunctor(unsigned theorySort, Theory::StructuredSortInterpretation ssi);
+  unsigned addInterpretedFunction(Interpretation itp, OperatorType* type, const vstring& name);
+  unsigned addInterpretedFunction(Interpretation itp, const vstring& name)
+  {
+    CALL("Signature::addInterpretedFunction(Interpretation,const vstring&)");
+    ASS(!Theory::isPolymorphic(itp));
+    return addInterpretedFunction(itp,Theory::getNonpolymorphicOperatorType(itp),name);
+  }
 
-  /** Return true iff there is a symbol interpreted by Interpretation @b interp */
-  bool haveInterpretingSymbol(Interpretation interp) const { return _iSymbols.find(interp); }
+  unsigned addInterpretedPredicate(Interpretation itp, OperatorType* type, const vstring& name);
+  unsigned addInterpretedPredicate(Interpretation itp, const vstring& name)
+  {
+    CALL("Signature::addInterpretedPredicate(Interpretation,const vstring&)");
+    ASS(!Theory::isPolymorphic(itp));
+    return addInterpretedPredicate(itp,Theory::getNonpolymorphicOperatorType(itp),name);
+  }
 
-  /**
-   * Return true iff we have any declared interpreted symbols
-   *
-   * The equality symbol is always present and is interpreted,
-   * so we return true only if we have any other interpreted
-   * symbols.
-   */
-  bool anyInterpretedSymbols() const
+  unsigned getInterpretingSymbol(Interpretation interp, OperatorType* type);
+  unsigned getInterpretingSymbol(Interpretation interp)
   {
-    CALL("Signature::anyInterpretedSymbols");
-    ASS_G(_iSymbols.size(),0); //we always have equality which is interpreted
+    CALL("Signature::getInterpretingSymbol(Interpretation)");
+    ASS(!Theory::isPolymorphic(interp));
+    return getInterpretingSymbol(interp,Theory::getNonpolymorphicOperatorType(interp));
+  }
 
-    return _iSymbols.size()!=1;
+  /** Return true iff there is a symbol interpreted by Interpretation @b interp */
+  bool haveInterpretingSymbol(Interpretation interp, OperatorType* type) const {
+    CALL("Signature::haveInterpretingSymbol(Interpretation, OperatorType*)");
+    return _iSymbols.find(std::make_pair(interp,type));
+  }
+  unsigned haveInterpretingSymbol(Interpretation interp)
+  {
+    CALL("Signature::haveInterpretingSymbol(Interpretation)");
+    ASS(!Theory::isPolymorphic(interp));
+    return haveInterpretingSymbol(interp,Theory::getNonpolymorphicOperatorType(interp));
   }
 
   /** return the name of a function with a given number */
@@ -533,13 +542,14 @@ class Signature
   bool _distinctGroupsAddedTo;
 
   /**
-   * Map from Interpretation values to function and predicate symbols representing them
+   * Map from MonomorphisedInterpretation values to function and predicate symbols representing them
    *
    * We mix here function and predicate symbols, but it is not a problem, as
-   * the Interpretation value already determines whether we deal with a function
+   * the MonomorphisedInterpretation value already determines whether we deal with a function
    * or a predicate.
    */
-  DHMap<Interpretation, unsigned> _iSymbols;
+  DHMap<Theory::MonomorphisedInterpretation, unsigned> _iSymbols;
+
   /** the number of string constants */
   unsigned _strings;
   /** the number of integer constants */

diff --git a/Kernel/Sorts.hpp b/Kernel/Sorts.hpp
@@ -61,8 +61,6 @@ class Sorts {
   enum class StructuredSort {
     /** The structured sort for arrays **/
     ARRAY,
-    /** The structured sort for lists, currently unused **/
-    LIST,
     /** The structured sort for tuples */
     TUPLE,
     /** not a real structured sort, it's here to denote the length of the StructuredSort enum */