EQUAL is back and it doesn't not make much difference

Inferences/Instantiation.cpp

@@ -157,11 +157,11 @@ void Instantiation::tryMakeLiteralFalse(Literal* lit, Stack<Substitution>& subs)
   CALL("Instantiation::tryMakeLiteralFalse");
 
   if(theory->isInterpretedPredicate(lit)){
-    Interpretation interpretation = theory->interpretPredicate(lit);
+    Interpretation itp = theory->interpretPredicate(lit);
     //unsigned sort = theory->getOperationSort(interpretation);
 
     //TODO, very limited consideration, expand
-    if (interpretation == Theory::INT_LESS || interpretation == Theory::RAT_LESS || interpretation == Theory::REAL_LESS || lit->isEquality() ) {
+    if (itp == Theory::EQUAL || itp == Theory::INT_LESS || itp == Theory::RAT_LESS || itp == Theory::REAL_LESS) {
       TermList* left = lit->nthArgument(0); TermList* right = lit->nthArgument(1);
       unsigned var;
       Term* t = 0;

Kernel/InterpretedLiteralEvaluator.cpp

@@ -71,7 +71,7 @@ class InterpretedLiteralEvaluator::EqualityEvaluator
   : public Evaluator
 {
   bool canEvaluatePred(unsigned pred) override {
-    return pred == 0; // the equality predicate
+    return Signature::isEqualityPredicate(pred);
   }
 
   template<typename T>
@@ -399,10 +399,6 @@ class InterpretedLiteralEvaluator::TypedEvaluator : public Evaluator
   {
     CALL("InterpretedLiteralEvaluator::TypedEvaluator::canEvaluatePred");
 
-    if (pred == 0) { // these guyes don't do it for equality
-      return false;
-    }
-
     if (!theory->isInterpretedPredicate(pred)) {
       return false;
     }
@@ -833,10 +829,8 @@ bool InterpretedLiteralEvaluator::balancable(Literal* lit)
   if(!theory->isInterpretedPredicate(lit->functor())) return false;
 
   // the perdicate must be binary
-  if (!lit->isEquality()) {
-    Interpretation ip = theory->interpretPredicate(lit->functor());
-    if(theory->getArity(ip)!=2) return false;
-  }
+  Interpretation ip = theory->interpretPredicate(lit->functor());
+  if(theory->getArity(ip)!=2) return false;
 
   // one side must be a constant and the other interpretted
   // the other side can contain at most one variable or uninterpreted subterm 

Kernel/Ordering.cpp

@@ -287,8 +287,8 @@ Ordering::Result PrecedenceOrdering::compare(Literal* l1, Literal* l2) const
 int PrecedenceOrdering::predicateLevel (unsigned pred) const
 {
   int basic=pred >= _predicates ? 1 : _predicateLevels[pred];
-  if(NONINTERPRETED_LEVEL_BOOST && !env.signature->getPredicate(pred)->interpreted()
-      && pred != 0) { // special case for equality - we don't call it interpreted anymore
+  if(NONINTERPRETED_LEVEL_BOOST && !env.signature->getPredicate(pred)->interpreted()) {
+    ASS(!Signature::isEqualityPredicate(pred)); //equality is always interpreted
     basic+=NONINTERPRETED_LEVEL_BOOST;
   }
   if(env.signature->predicateColored(pred)) {

Kernel/Signature.cpp

@@ -218,7 +218,7 @@ Signature::Signature ():
   CALL("Signature::Signature");
 
   // initialize equality
-  addPredicate("=", 2);
+  addInterpretedPredicate(Theory::EQUAL, OperatorType::getPredicateType(2), "=");
   ASS_EQ(predicateName(0), "="); //equality must have number 0
   getPredicate(0)->markSkip();
 

Kernel/Signature.hpp

@@ -434,6 +434,12 @@ class Signature
     return _preds[n];
   } // getPredicate
 
+  static inline bool isEqualityPredicate(unsigned p)
+  {
+    // we make sure equality is always 0
+    return (p == 0); // see the ASSERT in Signature::Signature
+  }
+
   Signature();
   ~Signature();
 

Kernel/Theory.cpp

@@ -590,6 +590,8 @@ unsigned Theory::getArity(Interpretation i)
 
     return 1;
 
+  case EQUAL:
+
   case INT_GREATER:
   case INT_GREATER_EQUAL:
   case INT_LESS:
@@ -802,6 +804,7 @@ bool Theory::hasSingleSort(Interpretation i)
   CALL("Theory::hasSingleSort");
 
   switch(i) {
+  case EQUAL:  // This not SingleSort because we don't know the sorts of its args
   case INT_TO_RAT:
   case INT_TO_REAL:
   case RAT_TO_INT:
@@ -828,6 +831,7 @@ bool Theory::isPolymorphic(Interpretation i)
   }
 
   switch(i) {
+  case EQUAL:
   case ARRAY_SELECT:
   case ARRAY_BOOL_SELECT:
   case ARRAY_STORE:
@@ -1452,7 +1456,7 @@ bool Theory::isInterpretedPredicate(unsigned pred)
 {
   CALL("Theory::isInterpretedPredicate(unsigned)");
 
-  return pred == 0 || env.signature->getPredicate(pred)->interpreted();
+  return env.signature->getPredicate(pred)->interpreted();
 }
 
 /**
@@ -1828,6 +1832,8 @@ vstring Theory::tryGetInterpretedLaTeXName(unsigned func, bool pred,bool polarit
   //TODO do we want special symbols for quotient, remainder, floor, ceiling, truncate, round?
 
   switch(i){
+  case EQUAL:return "a0 "+pol+"= a1";
+
   case INT_SUCCESSOR: return "a0++"; 
   case INT_UNARY_MINUS:
   case RAT_UNARY_MINUS:

Kernel/Theory.hpp

@@ -285,6 +285,8 @@ class Theory
   enum Interpretation
   {
     //predicates
+    EQUAL,
+
     INT_IS_INT,
     INT_IS_RAT,
     INT_IS_REAL,

Shell/InterpretedNormalizer.cpp

@@ -259,7 +259,7 @@ class InterpretedNormalizer::NLiteralTransformer : private TermTransformer
   {
     CALL("InterpretedNormalizer::NLiteralTransformer::apply");
 
-    if (!lit->isEquality() && theory->isInterpretedPredicate(lit)) // don't do this for equality which is interpreted, but does not have an interpretation
+    if (!lit->isEquality() && theory->isInterpretedPredicate(lit))
     {
       Interpretation itp = theory->interpretPredicate(lit);
       if(isTrivialInterpretation(itp)) {

Shell/Property.cpp

@@ -615,7 +615,7 @@ void Property::scanForInterpreted(Term* t)
   if (t->isLiteral()) {
     Literal* lit = static_cast<Literal*>(t);
     if (!theory->isInterpretedPredicate(lit)) { return; }
-    if(lit->isEquality()){
+    if (lit->isEquality()) {
       //cout << "this is interpreted equality " << t->toString() << endl;
       _hasInterpretedEquality=true;
       return;