Added Ordinalise(Sentence) and Ordinalise(Literal) to VariableManipul…

…ationExtensions.

src/SCFirstOrderLogic/SentenceManipulation/VariableManipulation/VariableIdIgnorantEqualityComparer.cs

@@ -1,4 +1,6 @@
-using System;
+// Copyright © 2023-2024 Simon Condon.
+// You may use this file in accordance with the terms of the MIT license.
+using System;
 using System.Collections.Generic;
 using System.Diagnostics.CodeAnalysis;
 using System.Linq;
@@ -11,8 +13,8 @@ namespace SCFirstOrderLogic.SentenceManipulation.VariableManipulation;
 /// That is, an equality comparer that considers P(x, y) equal to P(a, b) (but of course distinct from P(x, x)).
 /// </para>
 /// <para>
-/// NB: of course, such comparison is non-trivial in terms of performance. When an unambiguous ordering of 
-/// literals can be established, instead consider prior transformation via <see cref="VariableManipulationExtensions.Ordinalise(Term)"/>,
+/// NB: of course, such comparison is sub-optimal in terms of performance. When an unambiguous ordering of literals
+/// can be established, instead consider prior transformation via <see cref="VariableManipulationExtensions.Ordinalise(Literal)"/>,
 /// followed by equality comparison using plain old <see cref="object.Equals(object?)"/>.
 /// </para>
 /// </summary>

src/SCFirstOrderLogic/SentenceManipulation/VariableManipulation/VariableManipulationExtensions.cs

@@ -72,6 +72,42 @@ public static bool UnifiesWithAnyOf(this CNFClause thisClause, IEnumerable<CNFCl
         return clauses.Any(c => thisClause.TryUnifyWith(c));
     }
 
+    /// <summary>
+    /// <para>
+    /// Ordinalises a sentence; replacing all variable identifiers with the (zero-based) ordinal of where they
+    /// first appear in a depth-first traversal of the sentence.
+    /// </para>
+    /// <para>
+    /// This is useful because it makes the original identifiers irrelevant but preserves distinctness, so that 
+    /// e.g. P(X, X) is transformed to a sentence that is identical to the transformation of P(Y, Y), but different
+    /// to the transformation of P(X, Y). Making the original identifier irrelevant is useful when e.g. indexing.
+    /// </para>
+    /// </summary>
+    /// <param name="sentence">The sentence to ordinalise.</param>
+    /// <returns>The ordinalised sentence.</returns>
+    public static Sentence Ordinalise(this Sentence sentence)
+    {
+        return sentence.Accept(new VariableOrdinalisation());
+    }
+
+    /// <summary>
+    /// <para>
+    /// Ordinalises a literal; replacing all variable identifiers with the (zero-based) ordinal of where they
+    /// first appear in a depth-first traversal of the literal.
+    /// </para>
+    /// <para>
+    /// This is useful because it makes the original identifiers irrelevant but preserves distinctness, so that 
+    /// e.g. P(X, X) is transformed to a literal that is identical to the transformation of P(Y, Y), but different
+    /// to the transformation of P(X, Y). Making the original identifier irrelevant is useful when e.g. indexing.
+    /// </para>
+    /// </summary>
+    /// <param name="literal">The literal to ordinalise.</param>
+    /// <returns>The ordinalised literal.</returns>
+    public static Literal Ordinalise(this Literal literal)
+    {
+        return new VariableOrdinalisation().ApplyTo(literal);
+    }
+
     /// <summary>
     /// <para>
     /// Ordinalises a term; replacing all variable identifiers with the (zero-based) ordinal of where they
@@ -162,6 +198,11 @@ private class VariableOrdinalisation : RecursiveSentenceTransformation
     {
         private readonly Dictionary<object, VariableDeclaration> variableIdMap = new();
 
+        public Literal ApplyTo(Literal literal)
+        {
+            return new((Predicate)ApplyTo(literal.Predicate), literal.IsNegated);
+        }
+
         /// <inheritdoc/>
         public override VariableDeclaration ApplyTo(VariableDeclaration variable)
         {