no interpreted distinct groups; should be done by InterpretedEvaluati…

…on + some polishing

Kernel/Signature.cpp

@@ -24,6 +24,7 @@
 #include "Lib/Environment.hpp"
 #include "Lib/Int.hpp"
 #include "Shell/Options.hpp"
+#include "Shell/DistinctGroupExpansion.hpp"
 
 #include "Signature.hpp"
 
@@ -32,10 +33,6 @@ using namespace Kernel;
 using namespace Shell;
 
 const unsigned Signature::STRING_DISTINCT_GROUP = 0;
-const unsigned Signature::INTEGER_DISTINCT_GROUP = 1;
-const unsigned Signature::RATIONAL_DISTINCT_GROUP = 2;
-const unsigned Signature::REAL_DISTINCT_GROUP = 3;
-const unsigned Signature::LAST_BUILT_IN_DISTINCT_GROUP = 3;
 
 /**
  * Standard constructor.
@@ -131,9 +128,10 @@ void Signature::Symbol::addToDistinctGroup(unsigned group,unsigned this_number)
   env.signature->_distinctGroupsAddedTo=true;
 
   Stack<unsigned>* members = env.signature->_distinctGroupMembers[group];
-  // see DistinctGroupExpansion::apply for why 141
-  if(members->size()<141 || env.options->bfnt()
-                       || env.options->saturationAlgorithm()==Options::SaturationAlgorithm::FINITE_MODEL_BUILDING){ 
+  if(members->size() <= DistinctGroupExpansion::EXPAND_UP_TO_SIZE || env.options->bfnt()
+                       || env.options->saturationAlgorithm()==Options::SaturationAlgorithm::FINITE_MODEL_BUILDING){
+    // we add one more than EXPAND_UP_TO_SIZE to signal to DistinctGroupExpansion::apply not to expand
+    // ... instead DistinctEqualitySimplifier will take over
     members->push(this_number);
   }
 
@@ -225,17 +223,8 @@ Signature::Signature ():
   getPredicate(0)->markSkip();
 
   unsigned aux;
-  // Warning! reordering or removing some of below may brake the code in
-  // DistinctGroupExpansion::apply(UnitList*& units)
   aux = createDistinctGroup();
   ASS_EQ(STRING_DISTINCT_GROUP, aux);
-  aux = createDistinctGroup();
-  ASS_EQ(INTEGER_DISTINCT_GROUP, aux);
-  aux = createDistinctGroup();
-  ASS_EQ(RATIONAL_DISTINCT_GROUP, aux);
-  aux = createDistinctGroup();
-  ASS_EQ(REAL_DISTINCT_GROUP, aux);
-
 } // Signature::Signature
 
 /**
@@ -277,10 +266,12 @@ unsigned Signature::addIntegerConstant(const vstring& number,bool defaultSort)
 
   result = _funs.length();
   Symbol* sym = new Symbol(name,0,false,false,true);
+  /*
   sym->addToDistinctGroup(INTEGER_DISTINCT_GROUP,result);
   if(defaultSort){ 
      sym->addToDistinctGroup(STRING_DISTINCT_GROUP,result); // numbers are disctinct from strings
   }
+  */
   _funs.push(sym);
   _funNames.insert(symbolKey,result);
   return result;
@@ -304,8 +295,9 @@ unsigned Signature::addIntegerConstant(const IntegerConstantType& value)
   Symbol* sym = new IntegerSymbol(value);
   _funs.push(sym);
   _funNames.insert(key,result);
+  /*
   sym->addToDistinctGroup(INTEGER_DISTINCT_GROUP,result);
-  //sym->addToDistinctGroup(STRING_DISTINCT_GROUP,result); // numbers are distinct from strings
+  */
   return result;
 } // addIntegerConstant
 
@@ -332,10 +324,12 @@ unsigned Signature::addRationalConstant(const vstring& numerator, const vstring&
   }
   result = _funs.length();
   Symbol* sym = new Symbol(name,0,false,false,true);
+  /*
   if(defaultSort){ 
     sym->addToDistinctGroup(STRING_DISTINCT_GROUP,result); // numbers are distinct from strings
   }
   sym->addToDistinctGroup(RATIONAL_DISTINCT_GROUP,result);
+  */
   _funs.push(sym);
   _funNames.insert(key,result);
   return result;
@@ -378,10 +372,12 @@ unsigned Signature::addRealConstant(const vstring& number,bool defaultSort)
   }
   result = _funs.length();
   Symbol* sym = new Symbol(value.toNiceString(),0,false,false,true);
+  /*
   if(defaultSort){ 
     sym->addToDistinctGroup(STRING_DISTINCT_GROUP,result); // numbers are distinct from strings
   }
   sym->addToDistinctGroup(REAL_DISTINCT_GROUP,result);
+  */
   _funs.push(sym);
   _funNames.insert(key,result);
   return result;

Kernel/Signature.hpp

@@ -467,10 +467,6 @@ class Signature
   unsigned reals() const {return _reals;}
 
   static const unsigned STRING_DISTINCT_GROUP;
-  static const unsigned INTEGER_DISTINCT_GROUP;
-  static const unsigned RATIONAL_DISTINCT_GROUP;
-  static const unsigned REAL_DISTINCT_GROUP;
-  static const unsigned LAST_BUILT_IN_DISTINCT_GROUP;
 
   unsigned getFoolConstantSymbol(bool isTrue){ 
     if(!_foolConstantsDefined){

Parse/TPTP.cpp

@@ -2492,7 +2492,7 @@ Formula* TPTP::createPredicateApplication(vstring name, unsigned arity)
         }
         env.signature->addToDistinctGroup(ts.term()->functor(),grpIdx);
       }
-      return new Formula(true); // we ignore it, it evalutes to true as we have recorded it elsewhere
+      return new Formula(true); // we ignore it, it evaluates to true as we have recorded it elsewhere
     }
   }
   // not equality or distinct

Shell/DistinctGroupExpansion.cpp

@@ -81,20 +81,8 @@ bool DistinctGroupExpansion::apply(UnitList*& units)
 
   for(unsigned i=0;i<group_members.size();i++){
     Stack<unsigned>* members = group_members[i];
-    if(i==Signature::STRING_DISTINCT_GROUP && !env.signature->strings()){ continue;} // If there are no strings do not expand group
-    if(members->size() > 0){
-      // If the non-empty distinct group represents numbers then we need to keep
-      // the distinct processing later as new numbers can be generated from the
-      // existing ones
-
-      Signature::Symbol* sym = env.signature->getFunction(members->top());
-      unsigned grp_sort = sym->fnType()->result();
-
-      if(grp_sort==Sorts::SRT_INTEGER || grp_sort==Sorts::SRT_RATIONAL || grp_sort==Sorts::SRT_REAL){ someLeft=true; }
-
-      // This 140 is a magic number, if it is changed then the corresponding
-      // 141 should be changed in Kernel::Signature::Symbol::addToDistinctGroup
-      if( members->size()>1 && (members->size() < 140 || expandEverything)){
+    if(members->size() > 0) {
+      if( members->size()>1 && (members->size() <= EXPAND_UP_TO_SIZE || expandEverything)) {
         added=true;
         Formula* expansion = expand(*members);
         if(env.options->showPreprocessing()){

Shell/DistinctGroupExpansion.hpp

@@ -35,6 +35,8 @@ using namespace Kernel;
  */
 class DistinctGroupExpansion {
 public:
+  static const unsigned EXPAND_UP_TO_SIZE = 140;
+
   DistinctGroupExpansion(){}
 
   void apply(Problem& prb);