more fun with equality evaluation

ModelWriter · Nov 16, 2017 · bca75e9 · bca75e9
1 parent 64e76c4
commit bca75e9
Showing 1 changed file with 37 additions and 27 deletions.
diff --git a/Kernel/InterpretedLiteralEvaluator.cpp b/Kernel/InterpretedLiteralEvaluator.cpp
@@ -49,29 +49,9 @@ class InterpretedLiteralEvaluator::Evaluator
 
   virtual ~Evaluator() {}
 
-  virtual bool canEvaluateFunc(unsigned func)
-  {
-    CALL("InterpretedLiteralEvaluator::Evaluator::canEvaluateFunc");
-
-    if (!theory->isInterpretedFunction(func)) {
-      return false;
-    }
-    Interpretation interp = theory->interpretFunction(func);
-    return canEvaluate(interp);
-  }
-
-  virtual bool canEvaluatePred(unsigned pred)
-  {
-    CALL("InterpretedLiteralEvaluator::Evaluator::canEvaluatePred");
+  virtual bool canEvaluateFunc(unsigned func) { return false; }
+  virtual bool canEvaluatePred(unsigned pred) { return false; }
 
-    if (!theory->isInterpretedPredicate(pred)) {
-      return false;
-    }
-    Interpretation interp = theory->interpretPredicate(pred);
-    return canEvaluate(interp);
-  }
-
-  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; }
 };
@@ -140,7 +120,6 @@ class InterpretedLiteralEvaluator::EqualityEvaluator
     }
 
   }
-
 };
 
 /**
@@ -151,10 +130,14 @@ class InterpretedLiteralEvaluator::ConversionEvaluator
   : public Evaluator
 {
 public:
-  virtual bool canEvaluate(Interpretation interp)
+  bool canEvaluateFunc(unsigned func) override
   {
-    CALL("InterpretedLiteralEvaluator::ConversionEvaluator::canEvaluate");
-    return theory->isConversionOperation(interp);
+    CALL("InterpretedLiteralEvaluator::ConversionEvaluator::canEvaluateFunc");
+
+    if (!theory->isInterpretedFunction(func)) {
+      return false;
+    }
+    return theory->isConversionOperation(theory->interpretFunction(func));
   }
 
   virtual bool tryEvaluateFunc(Term* trm, TermList& res)
@@ -272,7 +255,7 @@ class InterpretedLiteralEvaluator::TypedEvaluator : public Evaluator
     // This is why we cannot evaluate Equality here... we cannot determine its sort
     if (!theory->hasSingleSort(interp)) { return false; } //To skip conversions and EQUAL
 
-    if (theory->isPolymorphic(interp)) {return false; } // typed evaulator not for polymorphic stuff
+    if (theory->isPolymorphic(interp)) { return false; } // typed evaulator not for polymorphic stuff
 
     unsigned opSort = theory->getOperationSort(interp);
     return opSort==T::getSort();
@@ -400,6 +383,33 @@ class InterpretedLiteralEvaluator::TypedEvaluator : public Evaluator
     }
 
   }
+
+  bool canEvaluateFunc(unsigned func) override
+  {
+    CALL("InterpretedLiteralEvaluator::TypedEvaluator::canEvaluateFunc");
+
+    if (!theory->isInterpretedFunction(func)) {
+      return false;
+    }
+    Interpretation interp = theory->interpretFunction(func);
+    return canEvaluate(interp);
+  }
+
+  bool canEvaluatePred(unsigned pred) override
+  {
+    CALL("InterpretedLiteralEvaluator::TypedEvaluator::canEvaluatePred");
+
+    if (pred == 0) { // these guyes don't do it for equality
+      return false;
+    }
+
+    if (!theory->isInterpretedPredicate(pred)) {
+      return false;
+    }
+    Interpretation interp = theory->interpretPredicate(pred);
+    return canEvaluate(interp);
+  }
+
 protected:
   virtual bool tryEvaluateUnaryFunc(Interpretation op, const T& arg, T& res)
   { return false; }