VariableSubstitution stuff:

* Added MutableVariableSubstitution. Derives from VariableSubstitution and is modifiable in-place. Added `ToMutable` method to VariableSubstitution
* Added `CopyAndAdd` methods to VariableSubstitution.
* Breaking: renamed `VariableSubstitution.Clone()` to `VariableSubstitution.Copy()`. Didn't want to use the term "Clone" for the methods above, because "Clone" suggests no change more strongly than "Copy" does - "CloneAndAdd" is a bit awkward. So renaming this method for consistency. (..and not implementing ICloneable anyway..)

src/SCFirstOrderLogic.Tests/SentenceManipulation/VariableSubstitutionTests.cs

@@ -6,16 +6,16 @@ namespace SCFirstOrderLogic.SentenceManipulation;
 
 public static class VariableSubstitutionTests
 {
-    // NB: Application tested via Literalunifier tests - probably shouldn't be
+    // NB: Application of substitution tested via Unifier tests - probably shouldn't be
 
     private record EqualityTestCase(VariableSubstitution X, VariableSubstitution Y, bool ExpectedEquality);
 
     public static Test EqualityBehaviour => TestThat
         .GivenEachOf(() => new EqualityTestCase[]
         {
             new(
-                X: new(new Dictionary<VariableReference, Term>()),
-                Y: new(new Dictionary<VariableReference, Term>()),
+                X: new([]),
+                Y: new([]),
                 ExpectedEquality: true),
 
             new(

src/SCFirstOrderLogic/SentenceManipulation/MutableVariableSubstitution.cs

@@ -0,0 +1,45 @@
+using System.Collections.Generic;
+
+namespace SCFirstOrderLogic.SentenceManipulation;
+
+/// <summary>
+/// A <see cref="VariableSubstitution"/> that can be modified in-place.
+/// </summary>
+public class MutableVariableSubstitution : VariableSubstitution
+{
+    /// <summary>
+    /// Initializes a new instance of the <see cref="MutableVariableSubstitution"/> class that is empty.
+    /// </summary>
+    public MutableVariableSubstitution()
+        : base()
+    {
+    }
+
+    /// <summary>
+    /// Initializes a new instance of the <see cref="MutableVariableSubstitution"/> class that uses a given set of bindings.
+    /// </summary>
+    /// <param name="bindings">The bindings to use.</param>
+    public MutableVariableSubstitution(IEnumerable<KeyValuePair<VariableReference, Term>> bindings)
+        : base(bindings)
+    {
+    }
+
+    /// <summary>
+    /// Adds a binding.
+    /// </summary>
+    /// <param name="variable">A reference to the variable to be substituted out.</param>
+    /// <param name="term">The term to be substituted in.</param>
+    public void AddBinding(VariableReference variable, Term term)
+    {
+        bindings.Add(variable, term);
+    }
+
+    /// <summary>
+    /// Creates an immutable copy of this substitution.
+    /// </summary>
+    /// <returns>A new <see cref="VariableSubstitution"/> instance with the same bindings as this one.</returns>
+    public VariableSubstitution ToReadOnly()
+    {
+        return new VariableSubstitution(bindings);
+    }
+}

src/SCFirstOrderLogic/SentenceManipulation/Unification/Unifier.cs

@@ -28,11 +28,11 @@ public static class Unifier
     /// <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)
     {
-        var unifierAttempt = new VariableSubstitution();
+        var unifierAttempt = new MutableVariableSubstitution();
 
         if (TryUpdateInPlace(x, y, unifierAttempt))
         {
-            unifier = unifierAttempt;
+            unifier = unifierAttempt.ToReadOnly();
             return true;
         }
 
@@ -48,8 +48,8 @@ public static bool TryCreate(Literal x, Literal y, [MaybeNullWhen(returnValue: f
     /// <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;
+        var unifierAttempt = new MutableVariableSubstitution();
+        return TryUpdateInPlace(x, y, unifierAttempt) ? unifierAttempt.ToReadOnly() : null;
     }
 
     /// <summary>
@@ -62,11 +62,11 @@ public static bool TryCreate(Literal x, Literal y, [MaybeNullWhen(returnValue: f
     /// <returns>True if the two literals can be unified, otherwise false.</returns>
     public static bool TryUpdate(Literal x, Literal y, VariableSubstitution unifier, [MaybeNullWhen(false)] out VariableSubstitution updatedUnifier)
     {
-        var potentialUpdatedUnifier = unifier.Clone();
+        var potentialUpdatedUnifier = unifier.ToMutable();
 
         if (TryUpdateInPlace(x, y, potentialUpdatedUnifier))
         {
-            updatedUnifier = potentialUpdatedUnifier;
+            updatedUnifier = potentialUpdatedUnifier.ToReadOnly();
             return true;
         }
 
@@ -83,11 +83,11 @@ public static bool TryUpdate(Literal x, Literal y, VariableSubstitution unifier,
     /// <returns>True if the two literals can be unified, otherwise false.</returns>
     public static bool TryUpdate(Literal x, Literal y, ref VariableSubstitution unifier)
     {
-        var updatedUnifier = unifier.Clone();
+        var updatedUnifier = unifier.ToMutable();
 
         if (TryUpdateInPlace(x, y, updatedUnifier))
         {
-            unifier = updatedUnifier;
+            unifier = updatedUnifier.ToReadOnly();
             return true;
         }
 
@@ -103,8 +103,8 @@ public static bool TryUpdate(Literal x, Literal y, ref VariableSubstitution unif
     /// <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;
+        var unifierAttempt = unifier.ToMutable();
+        return TryUpdateInPlace(x, y, unifierAttempt) ? unifierAttempt.ToReadOnly() : null;
     }
 
     /// <summary>
@@ -176,11 +176,11 @@ public static bool TryUpdate(Predicate x, Predicate y, ref VariableSubstitution
     /// <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)
     {
-        var unifierAttempt = new VariableSubstitution();
+        var unifierAttempt = new MutableVariableSubstitution();
 
         if (TryUpdateInPlace(x, y, unifierAttempt))
         {
-            unifier = unifierAttempt;
+            unifier = unifierAttempt.ToReadOnly();
             return true;
         }
 
@@ -196,8 +196,8 @@ public static bool TryCreate(Term x, Term y, [MaybeNullWhen(false)] out Variable
     /// <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;
+        var unifierAttempt = new MutableVariableSubstitution();
+        return TryUpdateInPlace(x, y, unifierAttempt) ? unifierAttempt.ToReadOnly() : null;
     }
 
     /// <summary>
@@ -210,11 +210,11 @@ public static bool TryCreate(Term x, Term y, [MaybeNullWhen(false)] out Variable
     /// <returns>True if the two terms can be unified, otherwise false.</returns>
     public static bool TryUpdate(Term x, Term y, VariableSubstitution unifier, [MaybeNullWhen(false)] out VariableSubstitution updatedUnifier)
     {
-        var potentialUpdatedUnifier = unifier.Clone();
+        var potentialUpdatedUnifier = unifier.ToMutable();
 
         if (TryUpdateInPlace(x, y, potentialUpdatedUnifier))
         {
-            updatedUnifier = potentialUpdatedUnifier;
+            updatedUnifier = potentialUpdatedUnifier.ToReadOnly();
             return true;
         }
 
@@ -231,11 +231,11 @@ public static bool TryUpdate(Term x, Term y, VariableSubstitution unifier, [Mayb
     /// <returns>True if the two terms can be unified, otherwise false.</returns>
     public static bool TryUpdate(Term x, Term y, ref VariableSubstitution unifier)
     {
-        var updatedUnifier = unifier.Clone();
+        var updatedUnifier = unifier.ToMutable();
 
         if (TryUpdateInPlace(x, y, updatedUnifier))
         {
-            unifier = updatedUnifier;
+            unifier = updatedUnifier.ToReadOnly();
             return true;
         }
 
@@ -251,11 +251,11 @@ public static bool TryUpdate(Term x, Term y, ref VariableSubstitution unifier)
     /// <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;
+        var unifierAttempt = unifier.ToMutable();
+        return TryUpdateInPlace(x, y, unifierAttempt) ? unifierAttempt.ToReadOnly() : null;
     }
 
-    private static bool TryUpdateInPlace(Literal x, Literal y, VariableSubstitution unifier)
+    private static bool TryUpdateInPlace(Literal x, Literal y, MutableVariableSubstitution unifier)
     {
         if (x.IsNegated != y.IsNegated 
             || !x.Predicate.Identifier.Equals(y.Predicate.Identifier)
@@ -275,7 +275,7 @@ private static bool TryUpdateInPlace(Literal x, Literal y, VariableSubstitution
         return true;
     }
 
-    private static bool TryUpdateInPlace(Term x, Term y, VariableSubstitution unifier)
+    private static bool TryUpdateInPlace(Term x, Term y, MutableVariableSubstitution unifier)
     {
         return (x, y) switch
         {
@@ -289,7 +289,7 @@ private static bool TryUpdateInPlace(Term x, Term y, VariableSubstitution unifie
         };
     }
 
-    private static bool TryUpdateInPlace(VariableReference variable, Term other, VariableSubstitution unifier)
+    private static bool TryUpdateInPlace(VariableReference variable, Term other, MutableVariableSubstitution unifier)
     {
         if (variable.Equals(other))
         {
@@ -319,7 +319,7 @@ private static bool TryUpdateInPlace(VariableReference variable, Term other, Var
         }
     }
 
-    private static bool TryUpdateInPlace(Function x, Function y, VariableSubstitution unifier)
+    private static bool TryUpdateInPlace(Function x, Function y, MutableVariableSubstitution unifier)
     {
         if (!x.Identifier.Equals(y.Identifier) || x.Arguments.Count != y.Arguments.Count)
         {

src/SCFirstOrderLogic/SentenceManipulation/VariableSubstitution.cs

@@ -2,26 +2,29 @@
 // You may use this file in accordance with the terms of the MIT license.
 using System;
 using System.Collections.Generic;
+using System.Collections.ObjectModel;
+using System.Linq;
 
 namespace SCFirstOrderLogic.SentenceManipulation;
 
 /// <summary>
 /// Sentence transformation class that makes some substitutions for <see cref="VariableReference"/> instances.
-/// In addition to the <see cref="RecursiveSentenceTransformation.ApplyTo(Sentence)"/> method
-/// offered by the base class, this also offers an <see cref="ApplyTo(Literal)"/> method.
+/// In addition to the various method ApplyTo methods offered by the base class that operate on <see cref="Sentence"/>
+/// and <see cref="Term"/> subtypes, this class also offers an <see cref="ApplyTo(Literal)"/> method.
 /// </summary>
-// TODO-FEATURE/ROBUSTNESS: Make VariableSubstitution read-only (i.e. even internally),
-// and add MutableVariableSubstitution : VariableSubstitution.
 public class VariableSubstitution : RecursiveSentenceTransformation
 {
-    private readonly Dictionary<VariableReference, Term> bindings;
+    /// <summary>
+    /// The individual substitutions made by this substitution.
+    /// </summary>
+    protected readonly Dictionary<VariableReference, Term> bindings;
 
     /// <summary>
     /// Initializes a new instance of the <see cref="VariableSubstitution"/> class that is empty.
     /// </summary>
     public VariableSubstitution()
+        : this(Enumerable.Empty<KeyValuePair<VariableReference, Term>>())
     {
-        bindings = new();
     }
 
     /// <summary>
@@ -31,18 +34,40 @@ public VariableSubstitution()
     public VariableSubstitution(IEnumerable<KeyValuePair<VariableReference, Term>> bindings)
     {
         this.bindings = new(bindings);
+        Bindings = new ReadOnlyDictionary<VariableReference, Term>(this.bindings);
     }
 
     /// <summary>
-    /// Gets the substitutions applied by this transformation.
+    /// Gets the individuals substitutions applied by this substitution.
+    /// Gets a mapping from replaced variable reference to the term that replaces it.
     /// </summary>
-    public IReadOnlyDictionary<VariableReference, Term> Bindings => bindings;
+    public IReadOnlyDictionary<VariableReference, Term> Bindings { get; }
 
     /// <summary>
     /// Creates a copy of this substitution.
     /// </summary>
     /// <returns>A new <see cref="VariableSubstitution"/> instance with the same bindings as this one.</returns>
-    public VariableSubstitution Clone() => new(bindings);
+    public VariableSubstitution Copy() => new(bindings);
+
+    /// <summary>
+    /// Creates a copy of this substitution, with an additional binding.
+    /// </summary>
+    /// <param name="additionalBinding">The binding to add to the clone.</param>
+    /// <returns>A new <see cref="VariableSubstitution"/> instance with the same bindings as this one, plus the given additional one.</returns>
+    public VariableSubstitution CopyAndAdd(KeyValuePair<VariableReference, Term> additionalBinding) => new(bindings.Append(additionalBinding));
+
+    /// <summary>
+    /// Creates a copy of this substitution, with some additional bindings.
+    /// </summary>
+    /// <param name="additionalBindings">The bindings to add to the clone.</param>
+    /// <returns>A new <see cref="VariableSubstitution"/> instance with the same bindings as this one, plus the given additional ones.</returns>
+    public VariableSubstitution CopyAndAdd(IEnumerable<KeyValuePair<VariableReference, Term>> additionalBindings) => new(bindings.Concat(additionalBindings));
+
+    /// <summary>
+    /// Creates a mutable copy of this substitution.
+    /// </summary>
+    /// <returns>A new <see cref="MutableVariableSubstitution"/> instance with the same bindings as this one.</returns>
+    public MutableVariableSubstitution ToMutable() => new(bindings);
 
     /// <summary>
     /// Applies this substitution to a <see cref="Literal"/> instance.
@@ -227,14 +252,4 @@ public override int GetHashCode()
 
         return hashCode.ToHashCode();
     }
-
-    /// <summary>
-    /// Adds a binding.
-    /// </summary>
-    /// <param name="variable">A reference to the variable to be substituted out.</param>
-    /// <param name="term">The term to be substituted in.</param>
-    internal void AddBinding(VariableReference variable, Term term)
-    {
-        bindings.Add(variable, term);
-    }
 }

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

@@ -182,19 +182,19 @@ private static class InstanceUnifier
     {
         public static bool TryCreate(Term generalisation, Term instance, [MaybeNullWhen(false)] out VariableSubstitution unifier)
         {
-            var unifierAttempt = new VariableSubstitution();
+            var unifierAttempt = new MutableVariableSubstitution();
 
             if (TryUpdateInPlace(generalisation, instance, unifierAttempt))
             {
-                unifier = unifierAttempt;
+                unifier = unifierAttempt.ToReadOnly();
                 return true;
             }
 
             unifier = null;
             return false;
         }
 
-        private static bool TryUpdateInPlace(Term generalisation, Term instance, VariableSubstitution unifier)
+        private static bool TryUpdateInPlace(Term generalisation, Term instance, MutableVariableSubstitution unifier)
         {
             return (generalisation, instance) switch
             {
@@ -207,7 +207,7 @@ private static bool TryUpdateInPlace(Term generalisation, Term instance, Variabl
             };
         }
 
-        private static bool TryUpdateInPlace(VariableReference variable, Term instanceTerm, VariableSubstitution unifier)
+        private static bool TryUpdateInPlace(VariableReference variable, Term instanceTerm, MutableVariableSubstitution unifier)
         {
             if (variable.Equals(instanceTerm))
             {
@@ -226,7 +226,7 @@ private static bool TryUpdateInPlace(VariableReference variable, Term instanceTe
             }
         }
 
-        private static bool TryUpdateInPlace(Function x, Function y, VariableSubstitution unifier)
+        private static bool TryUpdateInPlace(Function x, Function y, MutableVariableSubstitution unifier)
         {
             if (!x.Identifier.Equals(y.Identifier) || x.Arguments.Count != y.Arguments.Count)
             {
@@ -244,9 +244,4 @@ private static bool TryUpdateInPlace(Function x, Function y, VariableSubstitutio
             return true;
         }
     }
-
-    private static class AsyncEnumerable
-    {
-
-    }
 }