Skip to content

Commit

Permalink
Minor Unifier tweaks - trivial performance improvement when working w…
Browse files Browse the repository at this point in the history 
…ith Predicates.
  • Loading branch information
@sdcondon
sdcondon committed Aug 27, 2024
1 parent e95fed4 commit e06195c
Showing 1 changed file with 102 additions and 62 deletions.
164 changes: 102 additions & 62 deletions src/SCFirstOrderLogic/SentenceManipulation/VariableManipulation/Unifier.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -52,6 +52,72 @@ public static bool TryCreate(Literal x, Literal y, [MaybeNullWhen(returnValue: f
return TryUpdateInPlace(x, y, unifierAttempt) ? unifierAttempt.CopyAsReadOnly() : null;
}

/// <summary>
/// Attempts to create the most general unifier for two predicates.
/// </summary>
/// <param name="x">One of the two predicates to attempt to create a unifier for.</param>
/// <param name="y">One of the two predicates to attempt to create a unifier for.</param>
/// <param name="unifier">If the predicates can be unified, this out parameter will be the unifier.</param>
/// <returns>True if the two predicates can be unified, otherwise false.</returns>
public static bool TryCreate(Predicate x, Predicate y, [MaybeNullWhen(returnValue: false)] out VariableSubstitution unifier)
{
var unifierAttempt = new MutableVariableSubstitution();

if (TryUpdateInPlace(x, y, unifierAttempt))
{
unifier = unifierAttempt.CopyAsReadOnly();
return true;
}

unifier = null;
return false;
}

/// <summary>
/// Attempts to create the most general unifier for two predicates.
/// </summary>
/// <param name="x">One of the two predicates to attempt to create a unifier for.</param>
/// <param name="y">One of the two predicates to attempt to create a unifier for.</param>
/// <returns>The unifier if the predicates can be unified, otherwise null.</returns>
public static VariableSubstitution? TryCreate(Predicate x, Predicate y)
{
var unifierAttempt = new MutableVariableSubstitution();
return TryUpdateInPlace(x, y, unifierAttempt) ? unifierAttempt.CopyAsReadOnly() : null;
}

/// <summary>
/// Attempts to create the most general unifier for two terms.
/// </summary>
/// <param name="x">One of the two terms to attempt to create a unifier for.</param>
/// <param name="y">One of the two terms to attempt to create a unifier for.</param>
/// <param name="unifier">If the terms can be unified, this out parameter will be the unifier.</param>
/// <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 MutableVariableSubstitution();

if (TryUpdateInPlace(x, y, unifierAttempt))
{
unifier = unifierAttempt.CopyAsReadOnly();
return true;
}

unifier = null;
return false;
}

/// <summary>
/// Attempts to create the most general unifier for two terms.
/// </summary>
/// <param name="x">One of the two terms to attempt to create a unifier for.</param>
/// <param name="y">One of the two terms to attempt to create a unifier for.</param>
/// <returns>The unifier if the terms can be unified, otherwise null.</returns>
public static VariableSubstitution? TryCreate(Term x, Term y)
{
var unifierAttempt = new MutableVariableSubstitution();
return TryUpdateInPlace(x, y, unifierAttempt) ? unifierAttempt.CopyAsReadOnly() : null;
}

/// <summary>
/// Attempts to update a unifier so that it (also) unifies two given literals.
/// </summary>
Expand Down Expand Up @@ -107,29 +173,6 @@ public static bool TryUpdate(Literal x, Literal y, ref VariableSubstitution unif
return TryUpdateInPlace(x, y, unifierAttempt) ? unifierAttempt.CopyAsReadOnly() : null;
}

/// <summary>
/// Attempts to create the most general unifier for two predicates.
/// </summary>
/// <param name="x">One of the two predicates to attempt to create a unifier for.</param>
/// <param name="y">One of the two predicates to attempt to create a unifier for.</param>
/// <param name="unifier">If the predicates can be unified, this out parameter will be the unifier.</param>
/// <returns>True if the two predicates can be unified, otherwise false.</returns>
public static bool TryCreate(Predicate x, Predicate y, [MaybeNullWhen(returnValue: false)] out VariableSubstitution unifier)
{
return TryCreate((Literal)x, (Literal)y, out unifier);
}

/// <summary>
/// Attempts to create the most general unifier for two predicates.
/// </summary>
/// <param name="x">One of the two predicates to attempt to create a unifier for.</param>
/// <param name="y">One of the two predicates to attempt to create a unifier for.</param>
/// <returns>The unifier if the predicates can be unified, otherwise null.</returns>
public static VariableSubstitution? TryCreate(Predicate x, Predicate y)
{
return TryCreate((Literal)x, (Literal)y);
}

/// <summary>
/// Attempts to update a unifier so that it (also) unifies two given predicates.
/// </summary>
Expand All @@ -140,7 +183,16 @@ public static bool TryCreate(Predicate x, Predicate y, [MaybeNullWhen(returnValu
/// <returns>True if the two predicates can be unified, otherwise false.</returns>
public static bool TryUpdate(Predicate x, Predicate y, VariableSubstitution unifier, [MaybeNullWhen(false)] out VariableSubstitution updatedUnifier)
{
return TryUpdate((Literal)x, (Literal)y, unifier, out updatedUnifier);
var potentialUpdatedUnifier = unifier.CopyAsMutable();

if (TryUpdateInPlace(x, y, potentialUpdatedUnifier))
{
updatedUnifier = potentialUpdatedUnifier.CopyAsReadOnly();
return true;
}

updatedUnifier = null;
return false;
}

/// <summary>
Expand All @@ -152,51 +204,27 @@ public static bool TryUpdate(Predicate x, Predicate y, VariableSubstitution unif
/// <returns>True if the two predicates can be unified, otherwise false.</returns>
public static bool TryUpdate(Predicate x, Predicate y, ref VariableSubstitution unifier)
{
return TryUpdate((Literal)x, (Literal)y, ref unifier);
}

/// <summary>
/// Attempts to update a unifier so that it (also) unifies two given predicates.
/// </summary>
/// <param name="x">One of the two predicates to attempt to unify.</param>
/// <param name="y">One of the two predicates to attempt to unify.</param>
/// <param name="unifier">The unifier to update.</param>
/// <returns>The unifier if the predicates can be unified, otherwise null.</returns>
public static VariableSubstitution? TryUpdate(Predicate x, Predicate y, VariableSubstitution unifier)
{
return TryUpdate((Literal)x, (Literal)y, unifier);
}

/// <summary>
/// Attempts to create the most general unifier for two terms.
/// </summary>
/// <param name="x">One of the two terms to attempt to create a unifier for.</param>
/// <param name="y">One of the two terms to attempt to create a unifier for.</param>
/// <param name="unifier">If the terms can be unified, this out parameter will be the unifier.</param>
/// <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 MutableVariableSubstitution();
var updatedUnifier = unifier.CopyAsMutable();

if (TryUpdateInPlace(x, y, unifierAttempt))
if (TryUpdateInPlace(x, y, updatedUnifier))
{
unifier = unifierAttempt.CopyAsReadOnly();
unifier = updatedUnifier.CopyAsReadOnly();
return true;
}

unifier = null;
return false;
}

/// <summary>
/// Attempts to create the most general unifier for two terms.
/// Attempts to update a unifier so that it (also) unifies two given predicates.
/// </summary>
/// <param name="x">One of the two terms to attempt to create a unifier for.</param>
/// <param name="y">One of the two terms to attempt to create a unifier for.</param>
/// <returns>The unifier if the terms can be unified, otherwise null.</returns>
public static VariableSubstitution? TryCreate(Term x, Term y)
/// <param name="x">One of the two predicates to attempt to unify.</param>
/// <param name="y">One of the two predicates to attempt to unify.</param>
/// <param name="unifier">The unifier to update.</param>
/// <returns>The unifier if the predicates can be unified, otherwise null.</returns>
public static VariableSubstitution? TryUpdate(Predicate x, Predicate y, VariableSubstitution unifier)
{
var unifierAttempt = new MutableVariableSubstitution();
var unifierAttempt = unifier.CopyAsMutable();
return TryUpdateInPlace(x, y, unifierAttempt) ? unifierAttempt.CopyAsReadOnly() : null;
}

Expand Down Expand Up @@ -255,16 +283,27 @@ public static bool TryUpdate(Term x, Term y, ref VariableSubstitution unifier)
return TryUpdateInPlace(x, y, unifierAttempt) ? unifierAttempt.CopyAsReadOnly() : null;
}

// NB: not public because it can partially update the unifier on failure
private static bool TryUpdateInPlace(Literal x, Literal y, MutableVariableSubstitution unifier)
{
if (x.IsNegated != y.IsNegated
|| !x.Predicate.Identifier.Equals(y.Predicate.Identifier)
|| x.Predicate.Arguments.Count != y.Predicate.Arguments.Count)
if (x.IsNegated != y.IsNegated)
{
return false;
}

return TryUpdateInPlace(x.Predicate, y.Predicate, unifier);
}

// NB: not public because it can partially update the unifier on failure
private static bool TryUpdateInPlace(Predicate x, Predicate y, MutableVariableSubstitution unifier)
{
if (!x.Identifier.Equals(y.Identifier)
|| x.Arguments.Count != y.Arguments.Count)
{
return false;
}

foreach (var args in x.Predicate.Arguments.Zip(y.Predicate.Arguments, (x, y) => (x, y)))
foreach (var args in x.Arguments.Zip(y.Arguments, (x, y) => (x, y)))
{
if (!TryUpdateInPlace(args.x, args.y, unifier))
{
Expand All @@ -275,6 +314,7 @@ private static bool TryUpdateInPlace(Literal x, Literal y, MutableVariableSubsti
return true;
}

// NB: not public because it can partially update the unifier on failure
private static bool TryUpdateInPlace(Term x, Term y, MutableVariableSubstitution unifier)
{
return (x, y) switch
Expand Down

0 comments on commit e06195c

Please sign in to comment.