Rename isGreaterOrEq to compareUnidirectional and document it properly

vprover · Jan 7, 2025 · 8833384 · 8833384
1 parent d565870
commit 8833384
Show file tree

Hide file tree

Showing 9 changed files with 26 additions and 15 deletions.
diff --git a/Inferences/BackwardDemodulation.cpp b/Inferences/BackwardDemodulation.cpp
@@ -143,7 +143,7 @@ struct BackwardDemodulation::ResultFn
 
     TermList lhsS=qr.data->term;
 
-    if (_ordering.isGreaterOrEq(AppliedTerm(lhsS), AppliedTerm(rhs,&appl,true))!=Ordering::GREATER) {
+    if (_ordering.compareUnidirectional(AppliedTerm(lhsS), AppliedTerm(rhs,&appl,true))!=Ordering::GREATER) {
       return BwSimplificationRecord(0);
     }
 

diff --git a/Inferences/ForwardDemodulation.cpp b/Inferences/ForwardDemodulation.cpp
@@ -174,7 +174,7 @@ bool ForwardDemodulationImpl<combinatorySupSupport>::perform(Clause* cl, Clause*
 
         if (_precompiledComparison) {
 #if VDEBUG
-          auto dcomp = ordering.isGreaterOrEq(trm,rhsApplied);
+          auto dcomp = ordering.compareUnidirectional(trm,rhsApplied);
 #endif
           qr.data->comparator->init(appl);
           if (!preordered && (_preorderedOnly || !qr.data->comparator->next())) {
@@ -183,7 +183,7 @@ bool ForwardDemodulationImpl<combinatorySupSupport>::perform(Clause* cl, Clause*
           }
           ASS_EQ(dcomp,Ordering::GREATER);
         } else {
-          if (!preordered && (_preorderedOnly || ordering.isGreaterOrEq(trm,rhsApplied)!=Ordering::GREATER)) {
+          if (!preordered && (_preorderedOnly || ordering.compareUnidirectional(trm,rhsApplied)!=Ordering::GREATER)) {
             continue;
           }
         }

diff --git a/Kernel/KBO.cpp b/Kernel/KBO.cpp
@@ -805,7 +805,7 @@ Ordering::Result KBO::compare(AppliedTerm tl1, AppliedTerm tl2) const
   return res;
 }
 
-Ordering::Result KBO::isGreaterOrEq(AppliedTerm tl1, AppliedTerm tl2) const
+Ordering::Result KBO::compareUnidirectional(AppliedTerm tl1, AppliedTerm tl2) const
 {
   if (tl1.equalsShallow(tl2)) {
     return EQUAL;

diff --git a/Kernel/KBO.hpp b/Kernel/KBO.hpp
@@ -161,7 +161,7 @@ class KBO
   Result compare(TermList tl1, TermList tl2) const override;
 
   Result compare(AppliedTerm t1, AppliedTerm t2) const override;
-  Result isGreaterOrEq(AppliedTerm t1, AppliedTerm t2) const override;
+  Result compareUnidirectional(AppliedTerm t1, AppliedTerm t2) const override;
   OrderingComparatorUP createComparator() const override;
 
 protected:

diff --git a/Kernel/LPO.cpp b/Kernel/LPO.cpp
@@ -96,7 +96,7 @@ Ordering::Result LPO::compare(AppliedTerm tl1, AppliedTerm tl2) const
   return clpo(tl1, tl2);
 }
 
-Ordering::Result LPO::isGreaterOrEq(AppliedTerm lhs, AppliedTerm rhs) const
+Ordering::Result LPO::compareUnidirectional(AppliedTerm lhs, AppliedTerm rhs) const
 {
   return lpo(lhs,rhs);
 }

diff --git a/Kernel/LPO.hpp b/Kernel/LPO.hpp
@@ -47,7 +47,7 @@ class LPO
   using PrecedenceOrdering::compare;
   Result compare(TermList tl1, TermList tl2) const override;
   Result compare(AppliedTerm tl1, AppliedTerm tl2) const override;
-  Result isGreaterOrEq(AppliedTerm tl1, AppliedTerm tl2) const override;
+  Result compareUnidirectional(AppliedTerm tl1, AppliedTerm tl2) const override;
   OrderingComparatorUP createComparator() const override;
 
   void showConcrete(std::ostream&) const override;

diff --git a/Kernel/Ordering.hpp b/Kernel/Ordering.hpp
@@ -87,9 +87,20 @@ class Ordering
   virtual Result compare(AppliedTerm lhs, AppliedTerm rhs) const
   { return compare(lhs.apply(), rhs.apply()); }
 
-  /** Optimised function used for checking that @b t1 is greater than @b t2,
-   * under some substitutions captured by @b AppliedTerm. */
-  virtual Result isGreaterOrEq(AppliedTerm t1, AppliedTerm t2) const
+  /** Unidirectional comparison of @b t1 and @b t2 under some
+   * substitutions captured by @b AppliedTerm which returns:
+   * (a) GREATER       if and only if  t1 ≻ t2,
+   * (b) EQUAL         if and only if  t1 = t2,
+   * (c) LESS                 only if  t1 ≺ t2,
+   * (d) INCOMPARABLE         only if  t1 ⪰̸ t2.
+   * That is, the function need not distinguish between t1 less
+   * than t2 and t1 and t2 being incomparable, which allows for
+   * some optimisations (see KBO and LPO implementation).
+   * 
+   * This is useful in simplifications such as demodulation where
+   * only the result being greater matters and in runtime specialized
+   * ordering checks (see OrderingComparator). */
+  virtual Result compareUnidirectional(AppliedTerm t1, AppliedTerm t2) const
   { return compare(t1, t2); }
 
   /** Creates optimised object for ordering checks. @see OrderingComparator. */

diff --git a/Kernel/OrderingComparator.cpp b/Kernel/OrderingComparator.cpp
@@ -64,7 +64,7 @@ void* OrderingComparator::next()
     Ordering::Result comp = Ordering::INCOMPARABLE;
     if (node->tag == Node::T_TERM) {
 
-      comp = _ord.isGreaterOrEq(
+      comp = _ord.compareUnidirectional(
         AppliedTerm(node->lhs, _appl, true),
         AppliedTerm(node->rhs, _appl, true));
 

diff --git a/UnitTests/tKBO.cpp b/UnitTests/tKBO.cpp
@@ -382,8 +382,8 @@ TEST_FUN(kbo_test23) {
 // isGreater tests
 
 bool isGreaterSymmetric(const KBO& ord, TermList t1, TermList t2) {
-  return ord.isGreaterOrEq(AppliedTerm(t1),AppliedTerm(t2))==Ordering::GREATER
-    && ord.isGreaterOrEq(AppliedTerm(t2),AppliedTerm(t1))!=Ordering::GREATER;
+  return ord.compareUnidirectional(AppliedTerm(t1),AppliedTerm(t2))==Ordering::GREATER
+    && ord.compareUnidirectional(AppliedTerm(t2),AppliedTerm(t1))!=Ordering::GREATER;
 }
 
 TEST_FUN(kbo_isGreater_test01) {
@@ -430,8 +430,8 @@ TEST_FUN(kbo_isGreater_test04) {
 
   auto ord = kbo(weights(make_pair(f, 10u)), weights());
 
-  ASS(ord.isGreaterOrEq(AppliedTerm(f(x)), AppliedTerm(g(g(g(g(g(y)))))))!=Ordering::GREATER);
-  ASS(ord.isGreaterOrEq(AppliedTerm(g(g(g(g(g(y)))))), AppliedTerm(f(x)))!=Ordering::GREATER);
+  ASS(ord.compareUnidirectional(AppliedTerm(f(x)), AppliedTerm(g(g(g(g(g(y)))))))!=Ordering::GREATER);
+  ASS(ord.compareUnidirectional(AppliedTerm(g(g(g(g(g(y)))))), AppliedTerm(f(x)))!=Ordering::GREATER);
 }
 
 TEST_FUN(kbo_isGreater_test05) {