diff --git a/src/SCFirstOrderLogic/SentenceManipulation/VariableManipulation/VariableIdIgnorantEqualityComparer.cs b/src/SCFirstOrderLogic/SentenceManipulation/VariableManipulation/VariableIdIgnorantEqualityComparer.cs index a0609f60..7aebd92f 100644 --- a/src/SCFirstOrderLogic/SentenceManipulation/VariableManipulation/VariableIdIgnorantEqualityComparer.cs +++ b/src/SCFirstOrderLogic/SentenceManipulation/VariableManipulation/VariableIdIgnorantEqualityComparer.cs @@ -1,4 +1,6 @@ -using System; +// Copyright © 2023-2024 Simon Condon. +// You may use this file in accordance with the terms of the MIT license. +using System; using System.Collections.Generic; using System.Diagnostics.CodeAnalysis; using System.Linq; @@ -11,8 +13,8 @@ namespace SCFirstOrderLogic.SentenceManipulation.VariableManipulation; /// That is, an equality comparer that considers P(x, y) equal to P(a, b) (but of course distinct from P(x, x)). /// /// -/// NB: of course, such comparison is non-trivial in terms of performance. When an unambiguous ordering of -/// literals can be established, instead consider prior transformation via , +/// NB: of course, such comparison is sub-optimal in terms of performance. When an unambiguous ordering of literals +/// can be established, instead consider prior transformation via , /// followed by equality comparison using plain old . /// /// diff --git a/src/SCFirstOrderLogic/SentenceManipulation/VariableManipulation/VariableManipulationExtensions.cs b/src/SCFirstOrderLogic/SentenceManipulation/VariableManipulation/VariableManipulationExtensions.cs index cc76f255..aed15e0d 100644 --- a/src/SCFirstOrderLogic/SentenceManipulation/VariableManipulation/VariableManipulationExtensions.cs +++ b/src/SCFirstOrderLogic/SentenceManipulation/VariableManipulation/VariableManipulationExtensions.cs @@ -72,6 +72,42 @@ public static bool UnifiesWithAnyOf(this CNFClause thisClause, IEnumerable thisClause.TryUnifyWith(c)); } + /// + /// + /// Ordinalises a sentence; replacing all variable identifiers with the (zero-based) ordinal of where they + /// first appear in a depth-first traversal of the sentence. + /// + /// + /// This is useful because it makes the original identifiers irrelevant but preserves distinctness, so that + /// e.g. P(X, X) is transformed to a sentence that is identical to the transformation of P(Y, Y), but different + /// to the transformation of P(X, Y). Making the original identifier irrelevant is useful when e.g. indexing. + /// + /// + /// The sentence to ordinalise. + /// The ordinalised sentence. + public static Sentence Ordinalise(this Sentence sentence) + { + return sentence.Accept(new VariableOrdinalisation()); + } + + /// + /// + /// Ordinalises a literal; replacing all variable identifiers with the (zero-based) ordinal of where they + /// first appear in a depth-first traversal of the literal. + /// + /// + /// This is useful because it makes the original identifiers irrelevant but preserves distinctness, so that + /// e.g. P(X, X) is transformed to a literal that is identical to the transformation of P(Y, Y), but different + /// to the transformation of P(X, Y). Making the original identifier irrelevant is useful when e.g. indexing. + /// + /// + /// The literal to ordinalise. + /// The ordinalised literal. + public static Literal Ordinalise(this Literal literal) + { + return new VariableOrdinalisation().ApplyTo(literal); + } + /// /// /// Ordinalises a term; replacing all variable identifiers with the (zero-based) ordinal of where they @@ -162,6 +198,11 @@ private class VariableOrdinalisation : RecursiveSentenceTransformation { private readonly Dictionary variableIdMap = new(); + public Literal ApplyTo(Literal literal) + { + return new((Predicate)ApplyTo(literal.Predicate), literal.IsNegated); + } + /// public override VariableDeclaration ApplyTo(VariableDeclaration variable) {