Merge pull request #637 from vprover/term-ordering-diagrams

Term ordering diagrams refactor

CMakeLists.txt

@@ -223,7 +223,9 @@ set(VAMPIRE_KERNEL_SOURCES
     Kernel/MLMatcherSD.cpp
     Kernel/MLVariant.cpp
     Kernel/Ordering.cpp
+    Kernel/OrderingComparator.cpp
     Kernel/Ordering_Equality.cpp
+    Kernel/PartialOrdering.cpp
     Kernel/Problem.cpp
     Kernel/Renaming.cpp
     Kernel/RobSubstitution.cpp
@@ -237,6 +239,7 @@ set(VAMPIRE_KERNEL_SOURCES
     Kernel/Substitution.cpp
     Kernel/Term.cpp
     Kernel/TermIterators.cpp
+    Kernel/TermPartialOrdering.cpp
     Kernel/TermTransformer.cpp
     Kernel/Theory.cpp
     Kernel/Signature.cpp
@@ -270,6 +273,8 @@ set(VAMPIRE_KERNEL_SOURCES
     Kernel/MLMatcher.hpp
     Kernel/MLVariant.hpp
     Kernel/Ordering.hpp
+    Kernel/OrderingComparator.hpp
+    Kernel/PartialOrdering.hpp
     Kernel/Problem.hpp
     Kernel/RCClauseStack.hpp
     Kernel/Renaming.hpp
@@ -285,6 +290,7 @@ set(VAMPIRE_KERNEL_SOURCES
     Kernel/Substitution.hpp
     Kernel/Term.hpp
     Kernel/TermIterators.hpp
+    Kernel/TermPartialOrdering.hpp
     Kernel/TermTransformer.hpp
     Kernel/Theory.hpp
     Kernel/Signature.hpp

Forwards.hpp

@@ -105,6 +105,7 @@ class Ordering;
 typedef Lib::SmartPtr<Ordering> OrderingSP;
 struct OrderingComparator;
 typedef std::unique_ptr<OrderingComparator> OrderingComparatorUP;
+class PartialOrdering;
 
 typedef unsigned SplitLevel;
 typedef const SharedSet<SplitLevel> SplitSet;

Indexing/Index.hpp

@@ -27,6 +27,7 @@
 #include "ResultSubstitution.hpp"
 #include "Kernel/UnificationWithAbstraction.hpp"
 #include "Lib/Allocator.hpp"
+#include "Kernel/OrderingComparator.hpp"
 
 /**
  * Indices are parametrized by a LeafData, i.e. the bit of data you want to store in the index.
@@ -116,8 +117,10 @@ struct TermLiteralClause
 struct DemodulatorData
 {
   DemodulatorData(TypedTermList term, TermList rhs, Clause* clause, bool preordered, const Ordering& ord)
-    : term(term), rhs(rhs), clause(clause), preordered(preordered), comparator(ord.createComparator(term, rhs))
+    : term(term), rhs(rhs), clause(clause), preordered(preordered), comparator(ord.createComparator())
   {
+    // insert pointer to owner as non-null value representing success
+    comparator->insert({ { term, rhs, Ordering::GREATER } }, this);
 #if VDEBUG
     ASS(term.containsAllVariablesOf(rhs));
     ASS(!preordered || ord.compare(term,rhs)==Ordering::GREATER);

Inferences/BackwardDemodulation.cpp

@@ -143,7 +143,7 @@ struct BackwardDemodulation::ResultFn
 
     TermList lhsS=qr.data->term;
 
-    if (!_ordering.isGreater(AppliedTerm(lhsS), AppliedTerm(rhs,&appl,true))) {
+    if (_ordering.compareUnidirectional(AppliedTerm(lhsS), AppliedTerm(rhs,&appl,true))!=Ordering::GREATER) {
       return BwSimplificationRecord(0);
     }
 

Inferences/ForwardDemodulation.cpp

@@ -162,22 +162,28 @@ bool ForwardDemodulationImpl<combinatorySupSupport>::perform(Clause* cl, Clause*
           }
         }
 
-        TermList rhs = qr.data->rhs;
-        bool preordered = qr.data->preordered;
-
         auto subs = qr.unifier;
         ASS(subs->isIdentityOnQueryWhenResultBound());
 
         ApplicatorWithEqSort applWithEqSort(subs.ptr(), eqSortSubs);
         Applicator applWithoutEqSort(subs.ptr());
         auto appl = lhs.isVar() ? (SubstApplicator*)&applWithEqSort : (SubstApplicator*)&applWithoutEqSort;
 
+        AppliedTerm rhsApplied(qr.data->rhs,appl,true);
+        bool preordered = qr.data->preordered;
+
         if (_precompiledComparison) {
-          if (!preordered && (_preorderedOnly || !qr.data->comparator->check(appl))) {
+#if VDEBUG
+          auto dcomp = ordering.compareUnidirectional(trm,rhsApplied);
+#endif
+          qr.data->comparator->init(appl);
+          if (!preordered && (_preorderedOnly || !qr.data->comparator->next())) {
+            ASS_NEQ(dcomp,Ordering::GREATER);
             continue;
           }
+          ASS_EQ(dcomp,Ordering::GREATER);
         } else {
-          if (!preordered && (_preorderedOnly || !ordering.isGreater(AppliedTerm(trm),AppliedTerm(rhs,appl,true)))) {
+          if (!preordered && (_preorderedOnly || ordering.compareUnidirectional(trm,rhsApplied)!=Ordering::GREATER)) {
             continue;
           }
         }
@@ -194,10 +200,7 @@ bool ForwardDemodulationImpl<combinatorySupSupport>::perform(Clause* cl, Clause*
           }
         }
 
-        TermList rhsS = subs->applyToBoundResult(rhs);
-        if (lhs.isVar()) {
-          rhsS = eqSortSubs.apply(rhsS, 0);
-        }
+        TermList rhsS = rhsApplied.apply();
 
         if (redundancyCheck && !_helper.isPremiseRedundant(cl, lit, trm, rhsS, lhs, appl)) {
           continue;

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;
@@ -874,14 +874,9 @@ Ordering::Result KBO::isGreaterOrEq(AppliedTerm tl1, AppliedTerm tl2) const
   return res;
 }
 
-bool KBO::isGreater(AppliedTerm lhs, AppliedTerm rhs) const
+OrderingComparatorUP KBO::createComparator() const
 {
-  return isGreaterOrEq(lhs,rhs)==GREATER;
-}
-
-OrderingComparatorUP KBO::createComparator(TermList lhs, TermList rhs) const
-{
-  return make_unique<KBOComparator>(lhs, rhs, *this);
+  return make_unique<KBOComparator>(*this);
 }
 
 int KBO::symbolWeight(const Term* t) const

Kernel/KBO.hpp

@@ -161,15 +161,15 @@ class KBO
   Result compare(TermList tl1, TermList tl2) const override;
 
   Result compare(AppliedTerm t1, AppliedTerm t2) const override;
-  bool isGreater(AppliedTerm t1, AppliedTerm t2) const override;
-  OrderingComparatorUP createComparator(TermList lhs, TermList rhs) const override;
+  Result compareUnidirectional(AppliedTerm t1, AppliedTerm t2) const override;
+  OrderingComparatorUP createComparator() const override;
 
 protected:
-  Result isGreaterOrEq(AppliedTerm tt1, AppliedTerm tt2) const;
   unsigned computeWeight(AppliedTerm tt) const;
 
   Result comparePredicates(Literal* l1, Literal* l2) const override;
 
+  friend struct OrderingComparator;
   friend class KBOComparator;
 
   // int functionSymbolWeight(unsigned fun) const;