Added some Unifier.TryCreate/Update overloads that do not use ref/out…

… parameters.
sdcondon · May 26, 2024 · 9eef24f · 9eef24f
1 parent a02a379
commit 9eef24f
Showing 1 changed file with 55 additions and 3 deletions.
diff --git a/src/SCFirstOrderLogic/SentenceManipulation/Unification/Unifier.cs b/src/SCFirstOrderLogic/SentenceManipulation/Unification/Unifier.cs
@@ -8,10 +8,12 @@ namespace SCFirstOrderLogic.SentenceManipulation.Unification;
 
 /// <summary>
 /// <para>
-/// Utility class for creating unifiers.
+/// Utility class for creating unifiers - that is, variable substitutions that yield the same result when applied each of the expressions that they unify.
 /// </para>
 /// <para>
 /// This implementation includes an occurs check.
+/// </para>
+/// <para>
 /// See §9.2.2 ("Unification") of 'Artificial Intelligence: A Modern Approach' for an explanation of this algorithm.
 /// </para>
 /// </summary>
@@ -22,7 +24,7 @@ public static class Unifier
     /// </summary>
     /// <param name="x">One of the two literals to attempt to create a unifier for.</param>
     /// <param name="y">One of the two literals to attempt to create a unifier for.</param>
-    /// <param name="unifier">If the literals can be unified, this out parameter will be the unifier - a transformation that will yield identical results when applied to both literals.</param>
+    /// <param name="unifier">If the literals can be unified, this out parameter will be the unifier.</param>
     /// <returns>True if the two literals can be unified, otherwise false.</returns>
     public static bool TryCreate(Literal x, Literal y, [MaybeNullWhen(returnValue: false)] out VariableSubstitution unifier)
     {
@@ -38,6 +40,18 @@ public static bool TryCreate(Literal x, Literal y, [MaybeNullWhen(returnValue: f
         return false;
     }
 
+    /// <summary>
+    /// Attempts to create the most general unifier for two literals.
+    /// </summary>
+    /// <param name="x">One of the two literals to attempt to create a unifier for.</param>
+    /// <param name="y">One of the two literals to attempt to create a unifier for.</param>
+    /// <returns>The unifier if the literals can be unified, otherwise null.</returns>
+    public static VariableSubstitution? TryCreate(Literal x, Literal y)
+    {
+        var unifierAttempt = new VariableSubstitution();
+        return TryUpdateInPlace(x, y, unifierAttempt) ? unifierAttempt : null;
+    }
+
     /// <summary>
     /// Attempts to update a unifier so that it (also) unifies two given literals.
     /// </summary>
@@ -80,12 +94,25 @@ public static bool TryUpdate(Literal x, Literal y, ref VariableSubstitution unif
         return false;
     }
 
+    /// <summary>
+    /// Attempts to update a unifier so that it (also) unifies two given literals.
+    /// </summary>
+    /// <param name="x">One of the two literals to attempt to unify.</param>
+    /// <param name="y">One of the two literals to attempt to unify.</param>
+    /// <param name="unifier">The unifier to update.</param>
+    /// <returns>The unifier if the literals can be unified, otherwise null.</returns>
+    public static VariableSubstitution? TryUpdate(Literal x, Literal y, VariableSubstitution unifier)
+    {
+        var unifierAttempt = unifier.Clone();
+        return TryUpdateInPlace(x, y, unifierAttempt) ? unifierAttempt : null;
+    }
+
     /// <summary>
     /// Attempts to create the most general unifier for two terms.
     /// </summary>
     /// <param name="x">One of the two terms to attempt to create a unifier for.</param>
     /// <param name="y">One of the two terms to attempt to create a unifier for.</param>
-    /// <param name="unifier">If the terms can be unified, this out parameter will be the unifier - a transformation that will yield identical results when applied to both terms.</param>
+    /// <param name="unifier">If the terms can be unified, this out parameter will be the unifier.</param>
     /// <returns>True if the two terms can be unified, otherwise false.</returns>
     public static bool TryCreate(Term x, Term y, [MaybeNullWhen(false)] out VariableSubstitution unifier)
     {
@@ -101,6 +128,18 @@ public static bool TryCreate(Term x, Term y, [MaybeNullWhen(false)] out Variable
         return false;
     }
 
+    /// <summary>
+    /// Attempts to create the most general unifier for two terms.
+    /// </summary>
+    /// <param name="x">One of the two terms to attempt to create a unifier for.</param>
+    /// <param name="y">One of the two terms to attempt to create a unifier for.</param>
+    /// <returns>The unifier if the terms can be unified, otherwise null.</returns>
+    public static VariableSubstitution? TryCreate(Term x, Term y)
+    {
+        var unifierAttempt = new VariableSubstitution();
+        return TryUpdateInPlace(x, y, unifierAttempt) ? unifierAttempt : null;
+    }
+
     /// <summary>
     /// Attempts to update a unifier so that it (also) unifies two given terms.
     /// </summary>
@@ -143,6 +182,19 @@ public static bool TryUpdate(Term x, Term y, ref VariableSubstitution unifier)
         return false;
     }
 
+    /// <summary>
+    /// Attempts to update a unifier so that it (also) unifies two given terms.
+    /// </summary>
+    /// <param name="x">One of the two terms to attempt to unify.</param>
+    /// <param name="y">One of the two terms to attempt to unify.</param>
+    /// <param name="unifier">The unifier to update.</param>
+    /// <returns>The unifier if the literals can be unified, otherwise null.</returns>
+    public static VariableSubstitution? TryUpdate(Term x, Term y, VariableSubstitution unifier)
+    {
+        var unifierAttempt = unifier.Clone();
+        return TryUpdateInPlace(x, y, unifierAttempt) ? unifierAttempt : null;
+    }
+
     private static bool TryUpdateInPlace(Literal x, Literal y, VariableSubstitution unifier)
     {
         if (x.IsNegated != y.IsNegated