fix lpo literal precedence

ModelWriter · Nov 7, 2017 · f054a67 · f054a67
1 parent 07f710c
commit f054a67
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 4 deletions.
diff --git a/Kernel/LPO.cpp b/Kernel/LPO.cpp
@@ -28,7 +28,7 @@ using namespace Shell;
  * Compare arguments of literals l1 and l2 and return the result
  * of the comparison.
  */
-Ordering::Result LPO::compare(Literal* l1, Literal* l2) const
+Ordering::Result LPO::compare(Literal* l1, Literal *l2) const
 {
   CALL("LPO::compare(Literal*...)");
   ASS(l1->shared());
@@ -48,6 +48,7 @@ Ordering::Result LPO::compare(Literal* l1, Literal* l2) const
   }
 
   if (p1 == p2) {
+    ASS_EQ(l1->isNegative(), l1->isNegative())
     if(l1->isEquality()) {
       ASS(l2->isEquality());
       return compareEqualities(l1, l2);
@@ -63,8 +64,8 @@ Ordering::Result LPO::compare(Literal* l1, Literal* l2) const
     return EQUAL;
   }
 
-  ASS_NEQ(_predicatePrecedences[p1], _predicatePrecedences[p2]); // precedence should be total
-  return (_predicatePrecedences[p1] > _predicatePrecedences[p2]) ? GREATER : LESS;
+  ASS_NEQ(predicatePrecedence(p1), predicatePrecedence(p2)); // precedence should be total
+  return (predicatePrecedence(p1) > predicatePrecedence(p2)) ? GREATER : LESS;
 } // LPO::compare()
 
 Ordering::Result LPO::compare(TermList tl1, TermList tl2) const

diff --git a/Kernel/LPO.hpp b/Kernel/LPO.hpp
@@ -18,7 +18,7 @@ namespace Kernel {
 using namespace Lib;
 
 /**
- * Class for instances of the Knuth-Bendix orderings
+ * Class for instances of the lexicographic path orderings
  */
 class LPO
 : public PrecedenceOrdering