diff --git a/Sources/AngouriMath/Convenience/MathS.cs b/Sources/AngouriMath/Convenience/MathS.cs index 41ed419f4..858d06ba5 100644 --- a/Sources/AngouriMath/Convenience/MathS.cs +++ b/Sources/AngouriMath/Convenience/MathS.cs @@ -5575,7 +5575,7 @@ public sealed record NewtonSetting // Weigh provided predicates much less but nested provideds heavy Providedf(var inner, var predicate) => DefaultCriteria(inner) + 0.1 * DefaultCriteria(predicate) + ExtraHeavyWeight * (inner.Nodes.Count(n => n is Providedf) + predicate.Nodes.Count(n => n is Providedf)), - Entity.Piecewise { Cases: var cases } => + Piecewise { Cases: var cases } => cases.Sum(@case => DefaultCriteria(@case.Expression) + 0.1 * DefaultCriteria(@case.Predicate) + ExtraHeavyWeight * (@case.Expression.Nodes.Count(n => n is Providedf) + @case.Predicate.Nodes.Count(n => n is Providedf))), Variable => Weight, // Number of variables @@ -5586,6 +5586,7 @@ public sealed record NewtonSetting Phif => ExtraHeavyWeight + expr.DirectChildren.Sum(DefaultCriteria), // Number of phi functions Real { IsNegative: true } => MajorWeight + expr.DirectChildren.Sum(DefaultCriteria), // Number of negative reals ComparisonSign when expr.DirectChildren[0] == 0 => Weight + expr.DirectChildren.Sum(DefaultCriteria), // 0 < x is bad. x > 0 is good. + Notf (Equalsf eq) => -Weight + DefaultCriteria(eq), // (not x = 0) is equally complex as (x = 0) _ => expr.DirectChildren.Sum(DefaultCriteria) } + Weight; // Number of nodes return DefaultCriteria(expr); diff --git a/Sources/AngouriMath/Functions/Output/Latex/Latex.Discrete.Classes.cs b/Sources/AngouriMath/Functions/Output/Latex/Latex.Discrete.Classes.cs index 9c1b2a915..131794d1b 100644 --- a/Sources/AngouriMath/Functions/Output/Latex/Latex.Discrete.Classes.cs +++ b/Sources/AngouriMath/Functions/Output/Latex/Latex.Discrete.Classes.cs @@ -20,7 +20,9 @@ partial record Notf { /// public override string Latexise() - => $@"\neg{{{Argument.Latexise(Argument.Priority < Priority)}}}"; + => Argument is Equalsf(var left, var right) + ? $@"{left.Latexise(left.Priority <= Priority.Equal)} \neq {right.Latexise(right.Priority <= Priority.Equal)}" + : $@"\neg{{{Argument.Latexise(Argument.Priority < Priority)}}}"; } partial record Andf @@ -28,54 +30,48 @@ partial record Andf /// public override string Latexise() { - // Detect patterns like (a < b) ∧ (b < c) ∧ (c < d) and returns the chain of comparisons - List? comparisons = null; - void GatherComparisons(Entity e) // Recursively gather all comparisons connected by AND + var result = new System.Text.StringBuilder(); + Entity? left = null; + bool first = true; + foreach (var child in LinearChildren(this)) { - switch (e) + switch (child) { - case Andf(var left, var right): - GatherComparisons(left); - GatherComparisons(right); + // Detect chained comparisons like (a < b) ∧ (b < c) ∧ (c < d) and display as a < b < c < d + case ComparisonSign: + var renew = left != child.DirectChildren[0]; + if (!first && renew) result.Append(@" \land "); + first = false; + if (first || renew) result.Append(child.DirectChildren[0].Latexise(child.DirectChildren[0].Priority <= child.Priority)); + renew = false; + result.Append(child switch { + Equalsf => " = ", + Greaterf => " > ", + GreaterOrEqualf => @" \geq ", + Lessf => " < ", + LessOrEqualf => @" \leq ", + _ => throw new Core.Exceptions.AngouriBugException("Unexpected comparison sign in Andf.Latexise") + }).Append(child.DirectChildren[1].Latexise(child.DirectChildren[1].Priority <= child.Priority)); + left = child.DirectChildren[1]; break; - case ComparisonSign comp: - comparisons ??= []; - comparisons.Add(comp); + case Notf (Equalsf eq): + renew = left != eq.Left; + if (!first && renew) result.Append(@" \land "); + first = false; + if (first || renew) result.Append(eq.Left.Latexise(eq.Left.Priority <= eq.Priority)); + renew = false; + result.Append(@" \neq ").Append(eq.Right.Latexise(eq.Right.Priority <= eq.Priority)); + left = eq.Right; + break; + default: + if (!first) result.Append(" \\land "); + left = null; + first = false; + result.Append(child.Latexise(child.Priority < Priority)); break; } } - GatherComparisons(this); - - // Check if comparisons form a valid chain: right side of each must equal left side of next - if (comparisons is { Count: >= 2 }) - for (int i = 0; i < comparisons.Count - 1; i++) - if (comparisons[i].DirectChildren[1] != comparisons[i + 1].DirectChildren[0]) - goto fallback; // Not a valid chain - - // Try to detect chained comparisons: (a < b) ∧ (b < c) → a < b < c - if (comparisons is { Count: > 1 } chain) - { - var result = new System.Text.StringBuilder(chain[0].DirectChildren[0].Latexise(chain[0].DirectChildren[0].Priority < chain[0].Priority)); - foreach (var comparison in chain) - { - var op = comparison switch - { - Equalsf => " = ", - Greaterf => " > ", - GreaterOrEqualf => @" \geq ", - Lessf => " < ", - LessOrEqualf => @" \leq ", - _ => null - }; - if (op is null) - goto fallback; - result.Append(op).Append(comparison.DirectChildren[1].Latexise(comparison.DirectChildren[1].Priority < comparison.Priority)); - } - return result.ToString(); - } - - fallback: - return $@"{Left.Latexise(Left.Priority < Priority)} \land {Right.Latexise(Right.Priority < Priority)}"; + return result.ToString(); } } diff --git a/Sources/AngouriMath/Functions/Simplification/Patterns/Patterns.Boolean.cs b/Sources/AngouriMath/Functions/Simplification/Patterns/Patterns.Boolean.cs index 0eee9fc59..6a15801cb 100644 --- a/Sources/AngouriMath/Functions/Simplification/Patterns/Patterns.Boolean.cs +++ b/Sources/AngouriMath/Functions/Simplification/Patterns/Patterns.Boolean.cs @@ -5,6 +5,7 @@ // Website: https://am.angouri.org. // +using HonkSharp.Functional; using static AngouriMath.Entity; using static AngouriMath.Entity.Boolean; @@ -13,7 +14,7 @@ namespace AngouriMath.Functions internal static partial class Patterns { private static bool IsLogic(Entity a) - => a is Statement or Variable; + => a is Statement or Variable or Providedf; private static bool IsLogic(Entity a, Entity b) => IsLogic(a) && IsLogic(b); @@ -23,7 +24,7 @@ private static bool IsLogic(Entity a, Entity b, Entity c) internal static Entity BooleanRules(Entity x) => x switch { - Impliesf(var ass, _) when ass == False && IsLogic(ass) => True, + Impliesf(var ass, var other) when ass == False && IsLogic(other) => True.Provided(other.DomainCondition), Andf(Notf(var any1), Notf(var any2)) when IsLogic(any1, any2) => !(any1 | any2), Orf(Notf(var any1), Notf(var any2)) when IsLogic(any1, any2) => !(any1 & any2), Orf(Notf(var any1), var any1a) when any1 == any1a && IsLogic(any1) => True, @@ -31,11 +32,11 @@ private static bool IsLogic(Entity a, Entity b, Entity c) Andf(var any1, var any1a) when any1 == any1a && IsLogic(any1) => any1, Orf(var any1, var any1a) when any1 == any1a && IsLogic(any1) => any1, Impliesf(var any1, var any1a) when any1 == any1a && IsLogic(any1) => True, - Xorf(var any1, var any1a) when any1 == any1a && IsLogic(any1) => False, + Xorf(var any1, var any1a) when any1 == any1a && IsLogic(any1) => False.Provided(any1.DomainCondition), Notf(Notf(var any1)) when IsLogic(any1) => any1, - Orf(var any1, var any2) when (any1 == True || any2 == True) && IsLogic(any1, any2) => True, - Andf(var any1, var any2) when (any1 == False || any2 == False) && IsLogic(any1, any2) => False, + Orf(var any1, var any2) when (any1 == True || any2 == True) && IsLogic(any1, any2) => True.Provided(any1.DomainCondition).Provided(any2.DomainCondition), + Andf(var any1, var any2) when (any1 == False || any2 == False) && IsLogic(any1, any2) => False.Provided(any1.DomainCondition).Provided(any2.DomainCondition), Orf(Andf(var any1, var any2), Andf(var any1a, var any3)) when any1 == any1a && IsLogic(any1, any2, any3) => any1 & (any2 | any3), Andf(Orf(var any1, var any2), Orf(var any1a, var any3)) when any1 == any1a && IsLogic(any1, any2, any3) => any1 | (any2 & any3), diff --git a/Sources/AngouriMath/Functions/Simplification/Patterns/Patterns.EqualityInequality.cs b/Sources/AngouriMath/Functions/Simplification/Patterns/Patterns.EqualityInequality.cs index fe336e5d6..dc747f928 100644 --- a/Sources/AngouriMath/Functions/Simplification/Patterns/Patterns.EqualityInequality.cs +++ b/Sources/AngouriMath/Functions/Simplification/Patterns/Patterns.EqualityInequality.cs @@ -5,8 +5,10 @@ // Website: https://am.angouri.org. // +using System; using static AngouriMath.Entity; using static AngouriMath.Entity.Boolean; +using static Antlr4.Runtime.Atn.SemanticContext; namespace AngouriMath.Functions { @@ -55,12 +57,20 @@ private static bool OppositeSigns(ComparisonSign left, ComparisonSign right) Notf(Lessf(var any1, var any2)) => any1 >= any2, Notf(GreaterOrEqualf(var any1, var any2)) => any1 < any2, Notf(LessOrEqualf(var any1, var any2)) => any1 > any2, + // If we have a bunch of comparison operators combined with AND/OR and NOT outside, we can push the NOT inside and flip all the operators. + // For complexity to not increase, maximum one AND/OR component can be something other than a comparison operator to propagate NOT into. + // e.g. not (a > b and b = c) becomes (a <= b or not b = c) + // Note that Notf(Equalsf) has the same complexity as Equalsf in ComplexityCriteria, so it can be treated as a comparison operator here. + Notf(Andf a) when Andf.LinearChildren(a).Count(n => n is not (ComparisonSign or Notf or Orf)) <= 1 => + Andf.LinearChildren(a).Select(e => InequalityEqualityRules(e switch { Notf(var n) => n, var n => new Notf(n) })).Aggregate((a, b) => a | b), + Notf(Orf a) when Orf.LinearChildren(a).Count(n => n is not (ComparisonSign or Notf or Andf)) <= 1 => + Orf.LinearChildren(a).Select(e => InequalityEqualityRules(e switch { Notf(var n) => n, var n => new Notf(n) })).Aggregate((a, b) => a & b), Impliesf(Andf(Greaterf(var any1, var any2), Greaterf(var any2a, var any3)), Greaterf(var any1a, var any3a)) - when any1 == any1a && any2 == any2a && any3 == any3a => True, + when any1 == any1a && any2 == any2a && any3 == any3a => True.Provided(any1.DomainCondition).Provided(any2.DomainCondition).Provided(any3.DomainCondition), Impliesf(Andf(Lessf(var any1, var any2), Lessf(var any2a, var any3)), Lessf(var any1a, var any3a)) - when any1 == any1a && any2 == any2a && any3 == any3a => True, + when any1 == any1a && any2 == any2a && any3 == any3a => True.Provided(any1.DomainCondition).Provided(any2.DomainCondition).Provided(any3.DomainCondition), Equalsf(var zero, var anyButZero) when IsZero(zero) && !IsZero(anyButZero) => anyButZero.Equalizes(zero), Greaterf(var zero, var anyButZero) when IsZero(zero) && !IsZero(anyButZero) => anyButZero < zero, @@ -129,10 +139,10 @@ private static bool OppositeSigns(ComparisonSign left, ComparisonSign right) // a! = 0 Equalsf(Factorialf({ DomainCondition: var condition }), var zeroEnt) when IsZero(zeroEnt) => False.Provided(condition), - Greaterf(var any1, var any1a) when any1 == any1a => false, - Lessf(var any1, var any1a) when any1 == any1a => false, - GreaterOrEqualf(var any1, var any1a) when any1 == any1a => true, - LessOrEqualf(var any1, var any1a) when any1 == any1a => true, + Greaterf(var any1, var any1a) when any1 == any1a => False.Provided(any1.DomainCondition), + Lessf(var any1, var any1a) when any1 == any1a => False.Provided(any1.DomainCondition), + GreaterOrEqualf(var any1, var any1a) when any1 == any1a => True.Provided(any1.DomainCondition), + LessOrEqualf(var any1, var any1a) when any1 == any1a => True.Provided(any1.DomainCondition), _ => x }; diff --git a/Sources/Tests/UnitTests/Convenience/LatexTest.cs b/Sources/Tests/UnitTests/Convenience/LatexTest.cs index ad2892e27..f1d796ec7 100644 --- a/Sources/Tests/UnitTests/Convenience/LatexTest.cs +++ b/Sources/Tests/UnitTests/Convenience/LatexTest.cs @@ -49,7 +49,7 @@ void TestSimplify(string expected, Entity actual) => [Fact] public void MultiplySimplify() => TestSimplify("{x}^{2}", x * x); [Fact] public void Divide() => Test(@"\frac{x}{x}", x / x); [Fact] public void DivideDivide() => Test(@"\frac{\frac{x}{x}}{x}", x / x / x); - [Fact] public void DivideSimplify() => TestSimplify(@"1 \quad \text{for} \quad \neg{x = 0}", x / x); + [Fact] public void DivideSimplify() => TestSimplify(@"1 \quad \text{for} \quad x \neq 0", x / x); [Fact] public void Greek1() => Test(@"\alpha", MathS.Var("alpha")); [Fact] public void Greek2() => Test(@"\beta", MathS.Var("beta")); [Fact] public void Greek3() => Test(@"a_{\beta}", MathS.Var("a_beta")); @@ -631,13 +631,17 @@ [Fact] public void EqualityInequalityChain() => Test(@"x \geq y = z < w", (x >= MathS.Var("y")) & (MathS.Var("y").Equalizes(MathS.Var("z"))) & (MathS.Var("z") < MathS.Var("w"))); [Fact] public void EqualityInequalityChainAlt() => Test(@"x \geq y = z < w", (x >= "y").Equalizes("z") < "w"); - [Fact] public void EqualityInequalityChainString() => Test(@"x \geq y = z < w", (Entity)"x>=y=z Test(@"x \geq y = z < w", (Entity)"(x>=y=z) Test(@"x \geq y = \left(z < w\right)", (Entity)"x>=y=z Test(@"x \geq \left(y = \left(z < w\right)\right)", new Entity.GreaterOrEqualf(x, new Entity.Equalsf("y", (Entity)"z" < "w"))); [Fact] public void ParenthesizedComparisons() => Test(@"\left(x < x\right) \geq \left(x > \left(\left(x = x\right) \leq x\right)\right)", #pragma warning disable 1718 // Disable self-comparison warning new Entity.GreaterOrEqualf(x < x, (x > new Entity.LessOrEqualf(new Entity.Equalsf(x, x), x)))); #pragma warning restore 1718 + [Fact] public void NotEqual() => Test(@"1 \neq 2", (Entity)"not 1 = 2"); + [Fact] public void ChainedNotEqual() => Test(@"1 \neq 2 \neq 3 = 4 \land 5", (Entity)"not 1 = 2 and not 2 = 3 and 3 = 4 and 5"); + [Fact] public void MixedChainedComparison() => Test(@"1 \land 2 > 3 < 4 \land \left(\top \lor \bot \right) \land 5 \neq x = x \land x", (Entity)"1 and 2 > 3 and 3 < 4 and (true or false) and not 5 = x and x = x and x"); [Fact] public void ImpliesChain() => Test(@"\left(\left(x \to y\right) \to z\right) \to x \to y \to z", x.Implies("y").Implies("z").Implies(x.Implies(MathS.Var("y").Implies("z")))); } diff --git a/Sources/Tests/UnitTests/PatternsTest/BooleanSimplify.cs b/Sources/Tests/UnitTests/PatternsTest/BooleanSimplify.cs index 6a1f1f8a4..65592dfd3 100644 --- a/Sources/Tests/UnitTests/PatternsTest/BooleanSimplify.cs +++ b/Sources/Tests/UnitTests/PatternsTest/BooleanSimplify.cs @@ -127,5 +127,26 @@ public void TestProvided(string expr, string? expected) var act = expr.ToEntity(); Assert.Equal(exp, act.Simplify()); } + [Theory] + [InlineData("not (not x)", "x")] + [InlineData("not (a = b and b = c)", "not a = b or not b = c")] + [InlineData("not (a <= b and b < c)", "a > b or b >= c")] + [InlineData("not (a > b and b >= c)", "a <= b or b < c")] + [InlineData("not (a <= b and b <= c and 1)", "not (1 and a <= b and b <= c)")] + [InlineData("not (a = b or b = c)", "not a = b and not b = c")] + [InlineData("not (a <= b or b < c)", "a > b and b >= c")] + [InlineData("not (a > b or b >= c)", "a <= b and b < c")] + [InlineData("not (a <= b or b <= c or 1)", "not (1 or a <= b or b <= c)")] + [InlineData("not (a < b or c > d and e = f)", "a >= b and (c <= d or not e = f)")] + [InlineData("not (not (a > b and b >= c) and y)", "a > b and b >= c or not y")] + [InlineData("not (not (a = b and b = c) and y)", "a = b and b = c or not y")] + [InlineData("not (not (not a = b and not b = c) and y)", "not ((a = b or b = c) and y)")] + [InlineData("not (a < b and b < c and not c = d and not d and not (e and not (f or g = h)))", "a >= b or b >= c or c = d or d or e and not f and not g = h")] + public void NestedNot(string expr, string expected) + { + var exp = expected.ToEntity(); + var act = expr.ToEntity(); + Assert.Equal(exp, act.Simplify()); + } } } diff --git a/Sources/Tests/UnitTests/PatternsTest/SimplifyTest.cs b/Sources/Tests/UnitTests/PatternsTest/SimplifyTest.cs index 82a9994d6..f448e188a 100644 --- a/Sources/Tests/UnitTests/PatternsTest/SimplifyTest.cs +++ b/Sources/Tests/UnitTests/PatternsTest/SimplifyTest.cs @@ -48,7 +48,7 @@ [Fact] public void Patt2() => AssertSimplify( [Fact] public void Patt9() => AssertSimplify(MathS.Arccotan(x * 3) + MathS.Arctan(x * 6), MathS.Arccotan(3 * x) + MathS.Arctan(6 * x)); [Fact] public void Patt10() => AssertSimplify(MathS.Arcsin(x * 3) + MathS.Arccos(x * 1), MathS.Arcsin(3 * x) + MathS.Arccos(x)); [Fact] public void Patt11() => AssertSimplify(3 + x + 4 + x, 7 + 2 * x); - [Fact] public void Patt12() => AssertSimplify((x * y * a * b * c) / (c * b * a * x * x), "y / x provided not (c = 0 or a * b * c * x ^ 2 = 0)", 4); + [Fact] public void Patt12() => AssertSimplify((x * y * a * b * c) / (c * b * a * x * x), "y / x provided not c = 0 and not a * b * c * x ^ 2 = 0", 4); [Fact] public void Frac1() => AssertSimplify("x / (y / z)", "x * z / y"); [Fact] public void Frac2() => AssertSimplify("x / y / z", "x / (y * z)"); [Fact] public void Factorial2() => AssertSimplify(MathS.Factorial(2), 2); diff --git a/Sources/Tests/UnitTests/PatternsTest/SortSimplifyTest.cs b/Sources/Tests/UnitTests/PatternsTest/SortSimplifyTest.cs index 298753ac7..28ec8933f 100644 --- a/Sources/Tests/UnitTests/PatternsTest/SortSimplifyTest.cs +++ b/Sources/Tests/UnitTests/PatternsTest/SortSimplifyTest.cs @@ -21,7 +21,7 @@ public sealed class SortSimplifyTest // [InlineData("sin(arcsin(c x) + arccos(x c) + c)2 + a + b + sin(x) + 0 + cos(c - -arcsin(c x) - -arccos(-c x * (-1)))2", "1")] // [InlineData("sin(arcsin(c x) + arccos(x c) + c)2 + a + b + sin(x) + 0 + cos(c - -arcsin(c x) - -arccos(-c x * (-1)))2", ") ^ 2", false)] [InlineData("sec(x) + a + sin(x) + c + 1 + 0 + 3 + sec(x)", "4 + 2 * sec(x) + sin(x) + a + c")] - [InlineData("tan(x) * a * b / c / sin(h + 0.1) * cotan(x)", "a * b / (sin(h + 1/10) * c) provided not (sin(x) = 0 or cos(x) = 0)")] + [InlineData("tan(x) * a * b / c / sin(h + 0.1) * cotan(x)", "a * b / (sin(h + 1/10) * c) provided not sin(x) = 0 and not cos(x) = 0")] [InlineData("sin(x) * a * b / c / sin(h + 0.1) * cosec(x)", "a * b / (sin(h + 1/10) * c) provided not sin(x) = 0")] [InlineData("cos(x) * a * b / c / sin(h + 0.1) * sec(x)", "a * b / (sin(h + 1/10) * c) provided not cos(x) = 0")] [InlineData("sec(x) * a * b / c / sin(h + 0.1) * cos(x)", "a * b / (sin(h + 1/10) * c) provided not cos(x) = 0")]