Added Sentence-accepting CNFSentence ctor. A step on the road to a bi…

…t more flexibility for consumers in exactly how conversion to CNF is carried out.

src/SCFirstOrderLogic/CNFClause.cs

@@ -28,9 +28,9 @@ public CNFClause(IEnumerable<Literal> literals)
     /// <summary>
     /// Initialises a new instance of the <see cref="CNFClause"/> class from a sentence that is a disjunction of literals (a literal being a predicate or a negated predicate).
     /// </summary>
-    /// <param name="sentence">The clause, represented as a <see cref="Sentence"/>. An <see cref="ArgumentException"/> exception will be thrown if it is not a disjunction of literals.</param>
-    public CNFClause(Sentence sentence)
-        : this(ConstructionVisitor.GetLiterals(sentence))
+    /// <param name="cnfClause">The clause, represented as a <see cref="Sentence"/>. An <see cref="ArgumentException"/> exception will be thrown if it is not a disjunction of literals.</param>
+    public CNFClause(Sentence cnfClause)
+        : this(ConstructionVisitor.GetLiterals(cnfClause))
     {
     }
 

src/SCFirstOrderLogic/CNFSentence.cs

@@ -1,6 +1,7 @@
 // Copyright (c) 2021-2024 Simon Condon.
 // You may use this file in accordance with the terms of the MIT license.
 using SCFirstOrderLogic.SentenceFormatting;
+using SCFirstOrderLogic.SentenceManipulation;
 using System;
 using System.Collections.Generic;
 
@@ -23,6 +24,18 @@ public CNFSentence(IEnumerable<CNFClause> clauses)
     {
     }
 
+    /// <summary>
+    /// Initialises a new instance of the <see cref="CNFSentence"/> class from a <see cref="Sentence"/> that is a conjunction of disjunctions of literals (a literal being a predicate or a negated predicate).
+    /// </summary>
+    /// <param name="cnfSentence">
+    /// The sentence, in CNF but represented as a <see cref="Sentence"/>. An <see cref="ArgumentException"/> exception will be thrown if it is not a conjunction of disjunctions of literals.
+    /// In other words, conversion to CNF is NOT carried out by this constructor.
+    /// </param>
+    public CNFSentence(Sentence cnfSentence)
+        : this(ConstructionVisitor.GetClauses(cnfSentence))
+    {
+    }
+
     // NB: We *could* actually use an immutable type to stop unscrupulous users from making it mutable by casting,
     // but this is a very low-level class, so I've opted to be lean and mean.
     internal CNFSentence(HashSet<CNFClause> clauses) => this.clauses = clauses;
@@ -66,4 +79,33 @@ public override int GetHashCode()
     {
         return ClausesEqualityComparer.GetHashCode(clauses);
     }
+
+    private class ConstructionVisitor : RecursiveSentenceVisitor
+    {
+        private readonly HashSet<CNFClause> clauses = new();
+
+        public static HashSet<CNFClause> GetClauses(Sentence sentence)
+        {
+            var visitor = new ConstructionVisitor();
+            visitor.Visit(sentence);
+            return visitor.clauses;
+        }
+
+        /// <inheritdoc />
+        public override void Visit(Sentence sentence)
+        {
+            if (sentence is Conjunction conjunction)
+            {
+                // The sentence is already in CNF - so the root down until the individual clauses will all be Conjunctions - we just skip past those.
+                Visit(conjunction);
+            }
+            else
+            {
+                // We've hit a clause.
+                // Afterwards, we don't need to look any further down the tree for the purposes of this class (though the CNFClause ctor that
+                // we invoke here does so to figure out the details of the clause). So we can just return rather than invoking base.Visit.
+                clauses.Add(new CNFClause(sentence));
+            }
+        }
+    }
 }

src/SCFirstOrderLogic/SentenceFormatting/SentenceFormatter.cs

@@ -15,7 +15,7 @@ namespace SCFirstOrderLogic.SentenceFormatting;
 // Will need precedence list in here - then presumably not too tough to include brackets or not based on the relative priority
 // of current op and child.
 // TODO-BREAKING-FEATURE: Allow for configuration of whether zero-arity functions (and predicates?) should have brackets or not.
-// Or roll into labeller (perhaps renamed - or separate interface - or perhaps some broader refactoring to do here) so can be by identifier? 
+// Or roll into labeller (perhaps renamed - or separate interface - some broader refactoring to do here, anyway) so can be by identifier? 
 public class SentenceFormatter
 {
     private const char PrecedenceBracketL = '[';

src/SCFirstOrderLogic/SentenceManipulation/Normalisation/NormalisationExtensions.cs

@@ -15,7 +15,7 @@ public static class NormalisationExtensions
     /// Converts this sentence to conjunctive normal form.
     /// </summary>
     /// <returns>A new <see cref="CNFSentence"/> object.</returns>
-    public static CNFSentence ToCNF(this Sentence sentence) => new(CNFSentenceConstructionVisitor.GetClauses(sentence));
+    public static CNFSentence ToCNF(this Sentence sentence) => new(CNFConversion.ApplyTo(sentence));
 
     /// <summary>
     /// Constructs and returns a clause that is the same as this one, except for the
@@ -64,36 +64,4 @@ public static CNFDefiniteClause Restandardise(this CNFDefiniteClause clause)
     {
         return new(Restandardise((CNFClause)clause));
     }
-
-    /// <summary>
-    /// Sentence visitor that constructs a set of <see cref="CNFClause"/> objects from a <see cref="Sentence"/> in CNF.
-    /// </summary>
-    private class CNFSentenceConstructionVisitor : RecursiveSentenceVisitor
-    {
-        private readonly HashSet<CNFClause> clauses = new();
-
-        public static HashSet<CNFClause> GetClauses(Sentence sentence)
-        {
-            var visitor = new CNFSentenceConstructionVisitor();
-            visitor.Visit(CNFConversion.ApplyTo(sentence));
-            return visitor.clauses;
-        }
-
-        /// <inheritdoc />
-        public override void Visit(Sentence sentence)
-        {
-            if (sentence is Conjunction conjunction)
-            {
-                // The expression is already in CNF - so the root down until the individual clauses will all be Conjunctions - we just skip past those.
-                Visit(conjunction);
-            }
-            else
-            {
-                // We've hit a clause.
-                // Afterwards, we don't need to look any further down the tree for the purposes of this class (though the CNFClause ctor that
-                // we invoke here does so to figure out the details of the clause). So we can just return rather than invoking base.Visit.
-                clauses.Add(new CNFClause(sentence));
-            }
-        }
-    }
 }