A bit more file shuffling

src/SCFirstOrderLogic/SentenceManipulation/VariableManipulation/CNFClauseExtensions.cs

@@ -0,0 +1,108 @@
+using System.Collections.Generic;
+using System.Linq;
+
+namespace SCFirstOrderLogic.SentenceManipulation.VariableManipulation
+{
+    ////public static class CNFClauseExtensions
+    ////{
+    ////    /// <summary>
+    ////    /// <para>
+    ////    /// Gets a value indicating whether 'this' clause subsumes another.
+    ////    /// </para>
+    ////    /// <para>
+    ////    /// That is, whether the other clause is logically entailed by this one.
+    ////    /// </para>
+    ////    /// </summary>
+    ////    /// <param name="thisClause"></param>
+    ////    /// <param name="otherClause"></param>
+    ////    /// <returns>True if this clause subsumes the other; otherwise false.</returns>
+    ////    public static bool Subsumes(this CNFClause thisClause, CNFClause otherClause)
+    ////    {
+    ////        throw new NotImplementedException();
+    ////    }
+    ////
+    ////    /// <summary>
+    ////    /// <para>
+    ////    /// Gets a value indicating whether another clause subsumes this one.
+    ////    /// </para>
+    ////    /// <para>
+    ////    /// That is, whether this clause is logically entailed by the other.
+    ////    /// </para>
+    ////    /// </summary>
+    ////    /// <param name="thisClause"></param>
+    ////    /// <param name="otherClause"></param>
+    ////    /// <returns>True if the other clause subsumes this one; otherwise false.</returns>
+    ////    public static bool IsSubsumedBy(this CNFClause thisClause, CNFClause otherClause)
+    ////    {
+    ////        return otherClause.Subsumes(thisClause);
+    ////    }
+    ////}
+}
+
+namespace SCFirstOrderLogic.SentenceManipulation.Unification
+{
+    /// <summary>
+    /// <para>
+    /// Extension methods pertaining to the unification of clauses.
+    /// </para>
+    /// <para>
+    /// NB: Of course, these methods COULD just be added to <see cref="CNFClause"/>. It felt a little messy
+    /// to have CNFClause depend on code in the Unification namespace though. Perhaps a slightly idiosyncratic 
+    /// design decision (after all, I'm fine with CNFClause depending on SentenceManipulation), but I'm sticking by it.
+    /// </para>
+    /// </summary>
+    // TODO-BREAKING-V7: Merge me into class above
+    public static class CNFClauseExtensions
+    {
+        /// <summary>
+        /// <para>
+        /// Checks whether "this" clause unifies with any of an enumeration of other definite clauses.
+        /// </para>
+        /// </summary>
+        /// <param name="thisClause">"This" clause.</param>
+        /// <param name="clauses">The clauses to check for unification with.</param>
+        /// <returns>True if this clause unifies with any of the provided clauses; otherwise false.</returns>
+        public static bool UnifiesWithAnyOf(this CNFClause thisClause, IEnumerable<CNFClause> clauses)
+        {
+            return clauses.Any(c => thisClause.TryUnifyWith(c));
+        }
+
+        /// <summary>
+        /// Tries to unify "this" clause with another.
+        /// </summary>
+        /// <param name="thisClause">"This" clause.</param>
+        /// <param name="otherClause">The other clause.</param>
+        /// <returns>True if the two clauses were successfully unified, otherwise false.</returns>
+        private static bool TryUnifyWith(this CNFClause thisClause, CNFClause otherClause)
+        {
+            if (thisClause.Literals.Count != otherClause.Literals.Count)
+            {
+                return false;
+            }
+
+            return TryUnifyWith(thisClause.Literals, otherClause.Literals, new VariableSubstitution()).Any();
+        }
+
+        private static IEnumerable<VariableSubstitution> TryUnifyWith(IEnumerable<Literal> thisLiterals, IEnumerable<Literal> otherLiterals, VariableSubstitution unifier)
+        {
+            if (!thisLiterals.Any())
+            {
+                yield return unifier;
+            }
+            else
+            {
+                foreach (var otherLiteral in otherLiterals)
+                {
+                    if (Unifier.TryUpdate(thisLiterals.First(), otherLiteral, unifier, out var firstLiteralUnifier))
+                    {
+                        // TODO-PERFORMANCE: Ugh, skip is bad enough - Except is going to get slow, esp when nested. Important thing for now is that it works as a baseline..
+                        foreach (var restOfLiteralsUnifier in TryUnifyWith(thisLiterals.Skip(1), otherLiterals.Except(new[] { otherLiteral }), firstLiteralUnifier))
+                        {
+                            yield return restOfLiteralsUnifier;
+                        }
+                    }
+                }
+            }
+        }
+    }
+}

src/SCFirstOrderLogic/SentenceManipulation/Unification/Unifier.cs → src/SCFirstOrderLogic/SentenceManipulation/VariableManipulation/Unifier.cs

@@ -4,6 +4,7 @@
 using System.Diagnostics.CodeAnalysis;
 using System.Linq;
 
+// TODO-BREAKING-V7: Move to VariableManipulation
 namespace SCFirstOrderLogic.SentenceManipulation.Unification;
 
 /// <summary>

src/SCFirstOrderLogic/TermIndexing/(Internals)/DiscriminationTreeVariableBindings.cs

@@ -15,7 +15,7 @@ internal class DiscriminationTreeVariableBindings
     private DiscriminationTreeVariableBindings(IEnumerable<KeyValuePair<int, IDiscriminationTreeNodeKey[]>> content) => map = new(content);
 
     // Overall performance would perhaps be better with a tree instead of copying a dictionary
-    // Worth a test at some point perhaps (maybe after looking at substitution trees in general).
+    // Worth a test at some point perhaps (maybe after looking at substitution trees in general - something to add to SentenceManipulation.VariableManipulation, perhaps?).
     // Might not be worth the complexity though.
     public static bool TryAddOrMatchBinding(int ordinal, IDiscriminationTreeNodeKey[] value, ref DiscriminationTreeVariableBindings bindings)
     {