Code tree results: number equality sort variables first, as the compiler does

Indexing/CodeTreeInterfaces.hpp

@@ -17,6 +17,7 @@
 
 #include "Forwards.hpp"
 #include "Kernel/SubstHelper.hpp"
+#include "Kernel/SortHelper.hpp"
 #include "Kernel/Renaming.hpp"
 
 #include "LiteralCodeTree.hpp"
@@ -31,6 +32,29 @@ namespace Indexing
 using namespace Kernel;
 using namespace Lib;
 
+/**
+ * Make @c r number the variables of @c key the way the code tree's compiler does,
+ * since that is what the matcher's bindings are indexed by.
+ *
+ * For an equality literal this is NOT what Renaming::normalizeVariables(const Literal*)
+ * does: CodeTree::Compiler::compile visits the equality's sort before the arguments
+ * (and so does the flat term), the Renaming visits it after them.
+ * Keep this in sync with the compiler.
+ */
+template<class Key>
+void normalizeInCodeTreeOrder(Renaming& r, Key const& key)
+{
+  if constexpr (std::is_convertible<Key, const Literal*>::value) {
+    const Literal* lit = key;
+    if (lit->isEquality()) {
+      r.normalizeVariables(SortHelper::getEqualityArgumentSort(lit));
+    }
+    r.normalizeVariables(lit);
+  } else {
+    r.normalizeVariables(key);
+  }
+}
+
 template<class Data>
 class GenSubstitution
   : public SubstApplicator
@@ -92,7 +116,7 @@ class ResultIterator
     ASS(_found);
     if constexpr (!is_indexed_data_normalized<Data>::value) {
       _resultNormalizer->reset();
-      _resultNormalizer->normalizeVariables(_found->key());
+      normalizeInCodeTreeOrder(*_resultNormalizer, _found->key());
     }
     auto out = GenSubstitutionQR<Data>(_subst, _found);
     _found = nullptr;

UnitTests/tTermIndex.cpp

@@ -326,3 +326,33 @@ TEST_FUN(zero_arity_predicate_gen) {
   check_gen(  tree, a != a, Stack<Data>{});
 }
 
+
+// The code tree numbers the variables of an equality literal sort-first, so the Renaming
+// that translates the key's variables into binding slots must do the same.
+TEST_FUN(gen_equality_sort_variables_numbered_first) {
+
+  DECL_DEFAULT_VARS
+  DECL_DEFAULT_SORT_VARS
+  DECL_SORT(A)
+  DECL_SORT(B)
+  DECL_CONST(a, A)
+  DECL_CONST(b, B)
+  // k : !>[X0,X1]: X0 > X1, so in k(alpha,beta,x) = y the sort is beta, which is not
+  // the first variable met among the arguments
+  DECL_POLY_FUNC(k, 2, {alpha}, beta)
+
+  using Data = MyData<Literal*>;
+  CodeTreeLIS<Data> tree;
+  Literal* key = k(alpha, beta, x) == y;
+  Literal* query = k(A, B, a) == b;
+  tree.handle(Data(key, "k(alpha,beta,x) = y"), /*insert=*/true);
+
+  unsigned found = 0;
+  auto it = tree.getGeneralizations(query, /*complementary=*/false);
+  while (it.hasNext()) {
+    auto res = it.next();
+    ASS_EQ(res.unifier.apply(key), query)
+    found++;
+  }
+  ASS_EQ(found, 1u)
+}