remove Theory::Equalit from Interpretations

ModelWriter · Nov 15, 2017 · b1b0db6 · b1b0db6
1 parent edecd6c
commit b1b0db6
Show file tree

Hide file tree

Showing 6 changed files with 44 additions and 77 deletions.
diff --git a/Inferences/Instantiation.cpp b/Inferences/Instantiation.cpp
@@ -156,53 +156,44 @@ void Instantiation::tryMakeLiteralFalse(Literal* lit, Stack<Substitution>& subs)
 {
   CALL("Instantiation::tryMakeLiteralFalse");
 
-    if(theory->isInterpretedPredicate(lit)){ 
-      Interpretation interpretation = theory->interpretPredicate(lit);
-      //unsigned sort = theory->getOperationSort(interpretation);
-
-      //TODO, very limited consideration, expand
-      switch(interpretation){
-        case Theory::EQUAL:
-        case Theory::INT_LESS: // do these less_equal cases make sense?
-        case Theory::RAT_LESS:
-        case Theory::REAL_LESS:
-        {
-          TermList* left = lit->nthArgument(0); TermList* right = lit->nthArgument(1); 
-          unsigned var;
-          Term* t = 0;
-          if(left->isVar() && !right->isVar()){
-           t = right->term(); 
-           var = left->var();
-          }
-          if(right->isVar() && !left->isVar()){
-           t = left->term(); 
-           var = right->var();
-          }
-          if(t){
-            // do occurs check
-            VariableIterator vit(t);
-            while(vit.hasNext()) if(vit.next().var()==var) return;
-
-            // we are okay
-            Substitution s1;
-            s1.bind(var,t);
-            subs.push(s1);
-            if(lit->polarity()){
-             t = tryGetDifferentValue(t);
-             if(t){
-               Substitution s2;
-               s2.bind(var,t);
-               subs.push(s2);
-             }
-            }
-          }
-          break;
+  if(theory->isInterpretedPredicate(lit)){
+    Interpretation interpretation = 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() ) {
+      TermList* left = lit->nthArgument(0); TermList* right = lit->nthArgument(1);
+      unsigned var;
+      Term* t = 0;
+      if(left->isVar() && !right->isVar()){
+       t = right->term();
+       var = left->var();
+      }
+      if(right->isVar() && !left->isVar()){
+       t = left->term();
+       var = right->var();
+      }
+      if(t){
+        // do occurs check
+        VariableIterator vit(t);
+        while(vit.hasNext()) if(vit.next().var()==var) return;
+
+        // we are okay
+        Substitution s1;
+        s1.bind(var,t);
+        subs.push(s1);
+        if(lit->polarity()){
+         t = tryGetDifferentValue(t);
+         if(t){
+           Substitution s2;
+           s2.bind(var,t);
+           subs.push(s2);
+         }
         }
-        default: //TODO cover other cases
-          break;
       }
     }
-
+    // TODO cover other cases ...
+  }
 }
 
 Term* Instantiation::tryGetDifferentValue(Term* t)

diff --git a/Kernel/InterpretedLiteralEvaluator.cpp b/Kernel/InterpretedLiteralEvaluator.cpp
@@ -49,7 +49,7 @@ class InterpretedLiteralEvaluator::Evaluator
 
   virtual ~Evaluator() {}
 
-  bool canEvaluateFunc(unsigned func)
+  virtual bool canEvaluateFunc(unsigned func)
   {
     CALL("InterpretedLiteralEvaluator::Evaluator::canEvaluateFunc");
 
@@ -60,7 +60,7 @@ class InterpretedLiteralEvaluator::Evaluator
     return canEvaluate(interp);
   }
 
-  bool canEvaluatePred(unsigned pred)
+  virtual bool canEvaluatePred(unsigned pred)
   {
     CALL("InterpretedLiteralEvaluator::Evaluator::canEvaluatePred");
 
@@ -71,7 +71,7 @@ class InterpretedLiteralEvaluator::Evaluator
     return canEvaluate(interp);
   }
 
-  virtual bool canEvaluate(Interpretation interp) = 0;
+  virtual bool canEvaluate(Interpretation interp) { return false; }
   virtual bool tryEvaluateFunc(Term* trm, TermList& res) { return false; }
   virtual bool tryEvaluatePred(Literal* trm, bool& res)  { return false; }
 };
@@ -90,15 +90,8 @@ class InterpretedLiteralEvaluator::Evaluator
 class InterpretedLiteralEvaluator::EqualityEvaluator
   : public Evaluator
 {
-
-  virtual bool canEvaluate(Interpretation interp)
-  {
-    return interp==Interpretation::EQUAL; 
-  }
-
-  virtual bool tryEvaluateFunc(Term* trm, TermList& res)
-  {
-    ASSERTION_VIOLATION; // EQUAL is a predicate, not a function!
+  bool canEvaluatePred(unsigned pred) override {
+    return pred == 0; // the equality predicate
   }
 
   template<typename T>
@@ -123,14 +116,8 @@ class InterpretedLiteralEvaluator::EqualityEvaluator
   {
     CALL("InterpretedLiteralEvaluator::EqualityEvaluator::tryEvaluatePred");
 
-    // Return if this is not an equality between theory terms
-    if(!theory->isInterpretedPredicate(lit)){ return false; }
-
     try{
-
-      Interpretation itp = theory->interpretPredicate(lit);
-      ASS(itp==Interpretation::EQUAL);
-      ASS(theory->getArity(itp)==2);
+      ASS(lit->isEquality());
 
       // We try and interpret the equality as a number of different sorts
       // If it is not an equality between two constants of the same sort the

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

diff --git a/Kernel/Theory.cpp b/Kernel/Theory.cpp
@@ -590,8 +590,6 @@ unsigned Theory::getArity(Interpretation i)
 
     return 1;
 
-  case EQUAL:
-
   case INT_GREATER:
   case INT_GREATER_EQUAL:
   case INT_LESS:
@@ -729,8 +727,6 @@ bool Theory::isFunction(Interpretation i)
 
     return true;
 
-  case EQUAL:
-
   case INT_GREATER:
   case INT_GREATER_EQUAL:
   case INT_LESS:
@@ -806,7 +802,6 @@ 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:
@@ -829,7 +824,6 @@ bool Theory::isPolymorphic(Interpretation i)
   CALL("Theory::isPolymorphic");
 
   switch(i) {
-  case EQUAL:
   case ARRAY_SELECT:
   case ARRAY_BOOL_SELECT:
   case ARRAY_STORE:
@@ -1835,8 +1829,6 @@ vstring Theory::tryGetInterpretedLaTeXName(unsigned func, bool pred,bool polarit
   case RAT_UNARY_MINUS:
   case REAL_UNARY_MINUS: return "-a0";
 
-  case EQUAL:return "a0 "+pol+"= a1";
-
   case INT_GREATER: return "a0 "+pol+"> a1";
   case INT_GREATER_EQUAL: return "a0 "+pol+"\\geq a1";
   case INT_LESS: return "a0 "+pol+"< a1";

diff --git a/Kernel/Theory.hpp b/Kernel/Theory.hpp
@@ -285,9 +285,6 @@ class Theory
   enum Interpretation
   {
     //predicates
-
-    EQUAL,
-
     INT_IS_INT,
     INT_IS_RAT,
     INT_IS_REAL,

diff --git a/Shell/Property.cpp b/Shell/Property.cpp
@@ -615,12 +615,12 @@ void Property::scanForInterpreted(Term* t)
   if (t->isLiteral()) {
     Literal* lit = static_cast<Literal*>(t);
     if (!theory->isInterpretedPredicate(lit)) { return; }
-    itp = theory->interpretPredicate(lit);
-    if(itp==Theory::EQUAL){ 
+    if(lit->isEquality()){
       //cout << "this is interpreted equality " << t->toString() << endl;
       _hasInterpretedEquality=true;
       return; 
     }
+    itp = theory->interpretPredicate(lit);
   }
   else {
     if (!theory->isInterpretedFunction(t)) { return; }