From a9b73b67e77d3eb623d0439aa77fa27fdc321a63 Mon Sep 17 00:00:00 2001 From: Simon Condon Date: Sun, 29 Sep 2024 14:03:51 +0100 Subject: [PATCH] Added Sentence-accepting CNFSentence ctor. A step on the road to a bit more flexibility for consumers in exactly how conversion to CNF is carried out. --- src/SCFirstOrderLogic/CNFClause.cs | 6 +-- src/SCFirstOrderLogic/CNFSentence.cs | 42 +++++++++++++++++++ .../SentenceFormatting/SentenceFormatter.cs | 2 +- .../Normalisation/NormalisationExtensions.cs | 34 +-------------- 4 files changed, 47 insertions(+), 37 deletions(-) diff --git a/src/SCFirstOrderLogic/CNFClause.cs b/src/SCFirstOrderLogic/CNFClause.cs index d3f2d916..ff3b1de7 100644 --- a/src/SCFirstOrderLogic/CNFClause.cs +++ b/src/SCFirstOrderLogic/CNFClause.cs @@ -28,9 +28,9 @@ public CNFClause(IEnumerable literals) /// /// Initialises a new instance of the class from a sentence that is a disjunction of literals (a literal being a predicate or a negated predicate). /// - /// The clause, represented as a . An exception will be thrown if it is not a disjunction of literals. - public CNFClause(Sentence sentence) - : this(ConstructionVisitor.GetLiterals(sentence)) + /// The clause, represented as a . An exception will be thrown if it is not a disjunction of literals. + public CNFClause(Sentence cnfClause) + : this(ConstructionVisitor.GetLiterals(cnfClause)) { } diff --git a/src/SCFirstOrderLogic/CNFSentence.cs b/src/SCFirstOrderLogic/CNFSentence.cs index 3c15b588..8892ed1d 100644 --- a/src/SCFirstOrderLogic/CNFSentence.cs +++ b/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 clauses) { } + /// + /// Initialises a new instance of the class from a that is a conjunction of disjunctions of literals (a literal being a predicate or a negated predicate). + /// + /// + /// The sentence, in CNF but represented as a . An 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. + /// + 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 clauses) => this.clauses = clauses; @@ -66,4 +79,33 @@ public override int GetHashCode() { return ClausesEqualityComparer.GetHashCode(clauses); } + + private class ConstructionVisitor : RecursiveSentenceVisitor + { + private readonly HashSet clauses = new(); + + public static HashSet GetClauses(Sentence sentence) + { + var visitor = new ConstructionVisitor(); + visitor.Visit(sentence); + return visitor.clauses; + } + + /// + 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)); + } + } + } } diff --git a/src/SCFirstOrderLogic/SentenceFormatting/SentenceFormatter.cs b/src/SCFirstOrderLogic/SentenceFormatting/SentenceFormatter.cs index fa6504ea..a9c1981f 100644 --- a/src/SCFirstOrderLogic/SentenceFormatting/SentenceFormatter.cs +++ b/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 = '['; diff --git a/src/SCFirstOrderLogic/SentenceManipulation/Normalisation/NormalisationExtensions.cs b/src/SCFirstOrderLogic/SentenceManipulation/Normalisation/NormalisationExtensions.cs index 8a4e3370..536b3d6d 100644 --- a/src/SCFirstOrderLogic/SentenceManipulation/Normalisation/NormalisationExtensions.cs +++ b/src/SCFirstOrderLogic/SentenceManipulation/Normalisation/NormalisationExtensions.cs @@ -15,7 +15,7 @@ public static class NormalisationExtensions /// Converts this sentence to conjunctive normal form. /// /// A new object. - public static CNFSentence ToCNF(this Sentence sentence) => new(CNFSentenceConstructionVisitor.GetClauses(sentence)); + public static CNFSentence ToCNF(this Sentence sentence) => new(CNFConversion.ApplyTo(sentence)); /// /// 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)); } - - /// - /// Sentence visitor that constructs a set of objects from a in CNF. - /// - private class CNFSentenceConstructionVisitor : RecursiveSentenceVisitor - { - private readonly HashSet clauses = new(); - - public static HashSet GetClauses(Sentence sentence) - { - var visitor = new CNFSentenceConstructionVisitor(); - visitor.Visit(CNFConversion.ApplyTo(sentence)); - return visitor.clauses; - } - - /// - 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)); - } - } - } } \ No newline at end of file