more shuffling around of source files (in alternatives and benchmarks)

src/SCFirstOrderLogic.Alternatives/SentenceManipulation/CNFClause_WithTypeSwitchCtorVisitors.cs → src/SCFirstOrderLogic.Alternatives/CNFClause_WithTypeSwitchCtorVisitors.cs

@@ -34,7 +34,7 @@ public CNFClause_WithTypeSwitchCtorVisitors(Sentence sentence)
     /// Initialises a new instance of the <see cref="CNFClause_WithTypeSwitchCtorVisitors"/> class from an enumerable of literals (removing any mutually-negating literals and duplicates as it does so).
     /// </summary>
     /// <param name="literals">The set of literals to be included in the clause.</param>
-    public CNFClause_WithTypeSwitchCtorVisitors(IEnumerable<CNFLiteral_WithTypeSwitchCtorVisitors> literals)
+    public CNFClause_WithTypeSwitchCtorVisitors(IEnumerable<Literal_WithTypeSwitchCtorVisitors> literals)
     {
         // We *could* actually use an immutable type to stop unscrupulous users from making it mutable by casting, but
         // its a super low-level class and I'd rather err on the side of using the simplest/smallest implementation possible.
@@ -45,12 +45,12 @@ public CNFClause_WithTypeSwitchCtorVisitors(IEnumerable<CNFLiteral_WithTypeSwitc
     /// <summary>
     /// Gets an instance of the empty clause.
     /// </summary>
-    public static CNFClause_WithTypeSwitchCtorVisitors Empty { get; } = new CNFClause_WithTypeSwitchCtorVisitors(Array.Empty<CNFLiteral_WithTypeSwitchCtorVisitors>());
+    public static CNFClause_WithTypeSwitchCtorVisitors Empty { get; } = new CNFClause_WithTypeSwitchCtorVisitors(Array.Empty<Literal_WithTypeSwitchCtorVisitors>());
 
     /// <summary>
     /// Gets the collection of literals that comprise this clause.
     /// </summary>
-    public IReadOnlyCollection<CNFLiteral_WithTypeSwitchCtorVisitors> Literals { get; }
+    public IReadOnlyCollection<Literal_WithTypeSwitchCtorVisitors> Literals { get; }
 
     /// <summary>
     /// <para>
@@ -140,7 +140,7 @@ public override int GetHashCode()
 
     private class ClauseConstructor : RecursiveSentenceVisitor_WithTypeSwitch
     {
-        public HashSet<CNFLiteral_WithTypeSwitchCtorVisitors> Literals { get; } = new();
+        public HashSet<Literal_WithTypeSwitchCtorVisitors> Literals { get; } = new();
 
         public override void Visit(Sentence sentence)
         {
@@ -154,7 +154,7 @@ public override void Visit(Sentence sentence)
                 // Assume we've hit a literal. NB will throw if its not actually a literal.
                 // Afterwards, we don't need to look any further down the tree for the purposes of this class (though the CNFLiteral ctor that
                 // we invoke here does so to figure out the details of the literal). So we can just return rather than invoking base.Visit.
-                Literals.Add(new CNFLiteral_WithTypeSwitchCtorVisitors(sentence));
+                Literals.Add(new Literal_WithTypeSwitchCtorVisitors(sentence));
             }
         }
     }

src/SCFirstOrderLogic.Alternatives/SentenceManipulation/CNFLiteral_WithTypeSwitchCtorVisitors.cs → src/SCFirstOrderLogic.Alternatives/Literal_WithTypeSwitchCtorVisitors.cs

@@ -11,13 +11,13 @@ namespace SCFirstOrderLogic.SentenceManipulation;
 /// <remarks>
 /// NB: Yes, literals are a meaningful notion regardless of CNF, but we only use THIS type within our CNF representation. Hence this type being called CNFLiteral and residing in this namespace.
 /// </remarks>
-public class CNFLiteral_WithTypeSwitchCtorVisitors : IEquatable<CNFLiteral_WithTypeSwitchCtorVisitors>
+public class Literal_WithTypeSwitchCtorVisitors : IEquatable<Literal_WithTypeSwitchCtorVisitors>
 {
     /// <summary>
     /// Initialises a new instance of the <see cref="AltCNFLiteral_WithTypeSwitchCtorVisitors"/> class.
     /// </summary>
     /// <param name="sentence">The literal, represented as a <see cref="Sentence"/> object. An exception will be thrown if it is neither a predicate nor a negated predicate.</param>
-    public CNFLiteral_WithTypeSwitchCtorVisitors(Sentence sentence)
+    public Literal_WithTypeSwitchCtorVisitors(Sentence sentence)
     {
         if (sentence is Negation negation)
         {
@@ -40,7 +40,7 @@ public CNFLiteral_WithTypeSwitchCtorVisitors(Sentence sentence)
     /// </summary>
     /// <param name="predicate">The atomic sentence to which this literal refers.</param>
     /// <param name="isNegated">A value indicating whether the atomic sentence is negated.</param>
-    public CNFLiteral_WithTypeSwitchCtorVisitors(Predicate predicate, bool isNegated)
+    public Literal_WithTypeSwitchCtorVisitors(Predicate predicate, bool isNegated)
     {
         Predicate = predicate;
         IsNegated = isNegated;
@@ -82,10 +82,10 @@ public CNFLiteral_WithTypeSwitchCtorVisitors(Predicate predicate, bool isNegated
     ////public override string ToString() => new SentenceFormatter().Print(this);
 
     /// <inheritdoc />
-    public override bool Equals(object? obj) => obj is CNFLiteral_WithTypeSwitchCtorVisitors literal && Equals(literal);
+    public override bool Equals(object? obj) => obj is Literal_WithTypeSwitchCtorVisitors literal && Equals(literal);
 
     /// <inheritdoc />
-    public bool Equals(CNFLiteral_WithTypeSwitchCtorVisitors? other)
+    public bool Equals(Literal_WithTypeSwitchCtorVisitors? other)
     {
         return other != null && other.Predicate.Equals(Predicate) && other.IsNegated.Equals(IsNegated);
     }
@@ -106,11 +106,11 @@ public Sentence ToSentence()
     /// Defines the (explicit) conversion of a <see cref="Sentence"/> instance to a <see cref="CNFLiteral_WithoutTypeSwitch"/>. NB: This conversion is explicit because it can fail (if the sentence isn't actually a literal).
     /// </summary>
     /// <param name="sentence">The sentence to convert.</param>
-    public static explicit operator CNFLiteral_WithTypeSwitchCtorVisitors(Sentence sentence)
+    public static explicit operator Literal_WithTypeSwitchCtorVisitors(Sentence sentence)
     {
         try
         {
-            return new CNFLiteral_WithTypeSwitchCtorVisitors(sentence);
+            return new Literal_WithTypeSwitchCtorVisitors(sentence);
         }
         catch (ArgumentException e)
         {
@@ -122,5 +122,5 @@ public static explicit operator CNFLiteral_WithTypeSwitchCtorVisitors(Sentence s
     /// Defines the (implicit) conversion of a <see cref="Predicate"/> instance to a <see cref="Literal"/>. NB: This conversion is implicit because it is always valid.
     /// </summary>
     /// <param name="sentence">The predicate to convert.</param>
-    public static implicit operator CNFLiteral_WithTypeSwitchCtorVisitors(Predicate predicate) => new(predicate);
+    public static implicit operator Literal_WithTypeSwitchCtorVisitors(Predicate predicate) => new(predicate);
 }

src/SCFirstOrderLogic.Alternatives/SentenceManipulation/Unification/LiteralUnifier_FromAIaMA.cs → src/SCFirstOrderLogic.Alternatives/SentenceManipulation/VariableManipulation/Unifier_FromAIaMA.cs

@@ -10,7 +10,7 @@ namespace SCFirstOrderLogic.SentenceManipulation.Unification;
 /// For learning and benchmarking only - obviously this is a terrible way to 
 /// implement this in C#.
 /// </summary>
-public static class LiteralUnifier_FromAIaMA
+public static class Unifier_FromAIaMA
 {
     /*
      * function UNIFY(x, y, θ) returns a substitution to make x and y identical

src/SCFirstOrderLogic.Alternatives/SentenceManipulation/Unification/LiteralUnifier_OptimisedFromAIaMA.cs → src/SCFirstOrderLogic.Alternatives/SentenceManipulation/VariableManipulation/Unifier_OptimisedFromAIaMA.cs

@@ -7,9 +7,9 @@ namespace SCFirstOrderLogic.SentenceManipulation.Unification;
 /// <summary>
 /// Most general unifier logic - optimised from the version presented in the source material,
 /// but operating on entire sentences, as opposed to literals. More powerful, but slower.
-/// This class is intended as a more realistic baseline than <see cref="LiteralUnifier_FromAIaMA"/>.
+/// This class is intended as a more realistic baseline than <see cref="Unifier_FromAIaMA"/>.
 /// </summary>
-public static class LiteralUnifier_OptimisedFromAIaMA
+public static class Unifier_OptimisedFromAIaMA
 {
     public static bool TryUnify(Sentence x, Sentence y, [NotNullWhen(returnValue: true)] out IDictionary<VariableReference, Term>? unifier)
     {

src/SCFirstOrderLogic.Alternatives/SentenceManipulation/Unification/LiteralUnifier_WithOccursCheckAsTransformation.cs → src/SCFirstOrderLogic.Alternatives/SentenceManipulation/VariableManipulation/Unifier_WithOccursCheckAsTransformation.cs

@@ -13,7 +13,7 @@ namespace SCFirstOrderLogic.SentenceManipulation.Unification;
 /// Differs from production version by using an occurs check that is a SentenceTransformation.
 /// </para>
 /// </summary>
-public static class LiteralUnifier_WithOccursCheckAsTransformation
+public static class Unifier_WithOccursCheckAsTransformation
 {
     /// <summary>
     /// Attempts to create the most general unifier for two literals.

src/SCFirstOrderLogic.Benchmarks/SentenceManipulation/Unification/UnificationBenchmarks.cs → src/SCFirstOrderLogic.Benchmarks/SentenceManipulation/VariableManipulation/UnificationBenchmarks.cs

@@ -27,35 +27,35 @@ public class UnificationBenchmarks
     public static bool Unify1_Actual() => Unifier.TryCreate(JohnKnowsX_Literal, JohnKnowsJane_Literal, out _);
 
     [Benchmark]
-    public static bool Unify1_OccursCheckTransform() => LiteralUnifier_WithOccursCheckAsTransformation.TryCreate(JohnKnowsX_Literal, JohnKnowsJane_Literal, out _);
+    public static bool Unify1_OccursCheckTransform() => Unifier_WithOccursCheckAsTransformation.TryCreate(JohnKnowsX_Literal, JohnKnowsJane_Literal, out _);
 
     [Benchmark]
-    public static bool Unify1_Sentence() => LiteralUnifier_OptimisedFromAIaMA.TryUnify(JohnKnowsX, JohnKnowsJane, out _);
+    public static bool Unify1_Sentence() => Unifier_OptimisedFromAIaMA.TryUnify(JohnKnowsX, JohnKnowsJane, out _);
 
     [Benchmark]
-    public static LiteralUnifier_FromAIaMA.Substitution Unify1_SentenceRaw() => LiteralUnifier_FromAIaMA.Unify(JohnKnowsX, JohnKnowsJane, null);
+    public static Unifier_FromAIaMA.Substitution Unify1_SentenceRaw() => Unifier_FromAIaMA.Unify(JohnKnowsX, JohnKnowsJane, null);
 
     [Benchmark]
     public static bool Unify2_Actual() => Unifier.TryCreate(JohnKnowsX_Literal, YKnowsJane_Literal, out _);
 
     [Benchmark]
-    public static bool Unify2_OccursCheckTransform() => LiteralUnifier_WithOccursCheckAsTransformation.TryCreate(JohnKnowsX_Literal, YKnowsJane_Literal, out _);
+    public static bool Unify2_OccursCheckTransform() => Unifier_WithOccursCheckAsTransformation.TryCreate(JohnKnowsX_Literal, YKnowsJane_Literal, out _);
 
     [Benchmark]
-    public static bool Unify2_Sentence() => LiteralUnifier_OptimisedFromAIaMA.TryUnify(JohnKnowsX, YKnowsJane, out _);
+    public static bool Unify2_Sentence() => Unifier_OptimisedFromAIaMA.TryUnify(JohnKnowsX, YKnowsJane, out _);
 
     [Benchmark]
-    public static LiteralUnifier_FromAIaMA.Substitution Unify2_SentenceRaw() => LiteralUnifier_FromAIaMA.Unify(JohnKnowsX, YKnowsJane, null);
+    public static Unifier_FromAIaMA.Substitution Unify2_SentenceRaw() => Unifier_FromAIaMA.Unify(JohnKnowsX, YKnowsJane, null);
 
     [Benchmark]
     public static bool Unify3_Actual() => Unifier.TryCreate(JohnKnowsX_Literal, YKnowsMotherOfY_Literal, out _);
 
     [Benchmark]
-    public static bool Unify3_OccursCheckTransform() => LiteralUnifier_WithOccursCheckAsTransformation.TryCreate(JohnKnowsX_Literal, YKnowsMotherOfY_Literal, out _);
+    public static bool Unify3_OccursCheckTransform() => Unifier_WithOccursCheckAsTransformation.TryCreate(JohnKnowsX_Literal, YKnowsMotherOfY_Literal, out _);
 
     [Benchmark]
-    public static bool Unify3_Sentence() => LiteralUnifier_OptimisedFromAIaMA.TryUnify(JohnKnowsX, YKnowsMotherOfY, out _);
+    public static bool Unify3_Sentence() => Unifier_OptimisedFromAIaMA.TryUnify(JohnKnowsX, YKnowsMotherOfY, out _);
 
     [Benchmark]
-    public static LiteralUnifier_FromAIaMA.Substitution Unify3_SentenceRaw() => LiteralUnifier_FromAIaMA.Unify(JohnKnowsX, YKnowsMotherOfY, null);
+    public static Unifier_FromAIaMA.Substitution Unify3_SentenceRaw() => Unifier_FromAIaMA.Unify(JohnKnowsX, YKnowsMotherOfY, null);
 }