Skip to content

Commit 6b61aac

Browse files
Happypig375Happypig375
authored
Display not equals in Latexise, simplify Notf(Andf) and Notf(Orf) (#653)
1 parent c70101b commit 6b61aac

8 files changed

Lines changed: 92 additions & 59 deletions

File tree

‎Sources/AngouriMath/Convenience/MathS.cs‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5575,7 +5575,7 @@ public sealed record NewtonSetting
55755575
// Weigh provided predicates much less but nested provideds heavy
55765576
Providedf(var inner, var predicate) =>
55775577
DefaultCriteria(inner) + 0.1 * DefaultCriteria(predicate) + ExtraHeavyWeight * (inner.Nodes.Count(n => n is Providedf) + predicate.Nodes.Count(n => n is Providedf)),
5578-
Entity.Piecewise { Cases: var cases } =>
5578+
Piecewise { Cases: var cases } =>
55795579
cases.Sum(@case =>
55805580
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))),
55815581
Variable => Weight, // Number of variables
@@ -5586,6 +5586,7 @@ public sealed record NewtonSetting
55865586
Phif => ExtraHeavyWeight + expr.DirectChildren.Sum(DefaultCriteria), // Number of phi functions
55875587
Real { IsNegative: true } => MajorWeight + expr.DirectChildren.Sum(DefaultCriteria), // Number of negative reals
55885588
ComparisonSign when expr.DirectChildren[0] == 0 => Weight + expr.DirectChildren.Sum(DefaultCriteria), // 0 < x is bad. x > 0 is good.
5589+
Notf (Equalsf eq) => -Weight + DefaultCriteria(eq), // (not x = 0) is equally complex as (x = 0)
55895590
_ => expr.DirectChildren.Sum(DefaultCriteria)
55905591
} + Weight; // Number of nodes
55915592
return DefaultCriteria(expr);

‎Sources/AngouriMath/Functions/Output/Latex/Latex.Discrete.Classes.cs‎

Lines changed: 39 additions & 43 deletions
Original file line numberDiff line numberDiff line change
@@ -20,62 +20,58 @@ partial record Notf
2020
{
2121
/// <inheritdoc/>
2222
public override string Latexise()
23-
=> $@"\neg{{{Argument.Latexise(Argument.Priority < Priority)}}}";
23+
=> Argument is Equalsf(var left, var right)
24+
? $@"{left.Latexise(left.Priority <= Priority.Equal)} \neq {right.Latexise(right.Priority <= Priority.Equal)}"
25+
: $@"\neg{{{Argument.Latexise(Argument.Priority < Priority)}}}";
2426
}
2527

2628
partial record Andf
2729
{
2830
/// <inheritdoc/>
2931
public override string Latexise()
3032
{
31-
// Detect patterns like (a < b) ∧ (b < c) ∧ (c < d) and returns the chain of comparisons
32-
List<ComparisonSign>? comparisons = null;
33-
void GatherComparisons(Entity e) // Recursively gather all comparisons connected by AND
33+
var result = new System.Text.StringBuilder();
34+
Entity? left = null;
35+
bool first = true;
36+
foreach (var child in LinearChildren(this))
3437
{
35-
switch (e)
38+
switch (child)
3639
{
37-
case Andf(var left, var right):
38-
GatherComparisons(left);
39-
GatherComparisons(right);
40+
// Detect chained comparisons like (a < b) ∧ (b < c) ∧ (c < d) and display as a < b < c < d
41+
case ComparisonSign:
42+
var renew = left != child.DirectChildren[0];
43+
if (!first && renew) result.Append(@" \land ");
44+
first = false;
45+
if (first || renew) result.Append(child.DirectChildren[0].Latexise(child.DirectChildren[0].Priority <= child.Priority));
46+
renew = false;
47+
result.Append(child switch {
48+
Equalsf => " = ",
49+
Greaterf => " > ",
50+
GreaterOrEqualf => @" \geq ",
51+
Lessf => " < ",
52+
LessOrEqualf => @" \leq ",
53+
_ => throw new Core.Exceptions.AngouriBugException("Unexpected comparison sign in Andf.Latexise")
54+
}).Append(child.DirectChildren[1].Latexise(child.DirectChildren[1].Priority <= child.Priority));
55+
left = child.DirectChildren[1];
4056
break;
41-
case ComparisonSign comp:
42-
comparisons ??= [];
43-
comparisons.Add(comp);
57+
case Notf (Equalsf eq):
58+
renew = left != eq.Left;
59+
if (!first && renew) result.Append(@" \land ");
60+
first = false;
61+
if (first || renew) result.Append(eq.Left.Latexise(eq.Left.Priority <= eq.Priority));
62+
renew = false;
63+
result.Append(@" \neq ").Append(eq.Right.Latexise(eq.Right.Priority <= eq.Priority));
64+
left = eq.Right;
65+
break;
66+
default:
67+
if (!first) result.Append(" \\land ");
68+
left = null;
69+
first = false;
70+
result.Append(child.Latexise(child.Priority < Priority));
4471
break;
4572
}
4673
}
47-
GatherComparisons(this);
48-
49-
// Check if comparisons form a valid chain: right side of each must equal left side of next
50-
if (comparisons is { Count: >= 2 })
51-
for (int i = 0; i < comparisons.Count - 1; i++)
52-
if (comparisons[i].DirectChildren[1] != comparisons[i + 1].DirectChildren[0])
53-
goto fallback; // Not a valid chain
54-
55-
// Try to detect chained comparisons: (a < b) ∧ (b < c) → a < b < c
56-
if (comparisons is { Count: > 1 } chain)
57-
{
58-
var result = new System.Text.StringBuilder(chain[0].DirectChildren[0].Latexise(chain[0].DirectChildren[0].Priority < chain[0].Priority));
59-
foreach (var comparison in chain)
60-
{
61-
var op = comparison switch
62-
{
63-
Equalsf => " = ",
64-
Greaterf => " > ",
65-
GreaterOrEqualf => @" \geq ",
66-
Lessf => " < ",
67-
LessOrEqualf => @" \leq ",
68-
_ => null
69-
};
70-
if (op is null)
71-
goto fallback;
72-
result.Append(op).Append(comparison.DirectChildren[1].Latexise(comparison.DirectChildren[1].Priority < comparison.Priority));
73-
}
74-
return result.ToString();
75-
}
76-
77-
fallback:
78-
return $@"{Left.Latexise(Left.Priority < Priority)} \land {Right.Latexise(Right.Priority < Priority)}";
74+
return result.ToString();
7975
}
8076
}
8177

‎Sources/AngouriMath/Functions/Simplification/Patterns/Patterns.Boolean.cs‎

Lines changed: 6 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@
55
// Website: https://am.angouri.org.
66
//
77

8+
using HonkSharp.Functional;
89
using static AngouriMath.Entity;
910
using static AngouriMath.Entity.Boolean;
1011

@@ -13,7 +14,7 @@ namespace AngouriMath.Functions
1314
internal static partial class Patterns
1415
{
1516
private static bool IsLogic(Entity a)
16-
=> a is Statement or Variable;
17+
=> a is Statement or Variable or Providedf;
1718

1819
private static bool IsLogic(Entity a, Entity b)
1920
=> IsLogic(a) && IsLogic(b);
@@ -23,19 +24,19 @@ private static bool IsLogic(Entity a, Entity b, Entity c)
2324

2425
internal static Entity BooleanRules(Entity x) => x switch
2526
{
26-
Impliesf(var ass, _) when ass == False && IsLogic(ass) => True,
27+
Impliesf(var ass, var other) when ass == False && IsLogic(other) => True.Provided(other.DomainCondition),
2728
Andf(Notf(var any1), Notf(var any2)) when IsLogic(any1, any2) => !(any1 | any2),
2829
Orf(Notf(var any1), Notf(var any2)) when IsLogic(any1, any2) => !(any1 & any2),
2930
Orf(Notf(var any1), var any1a) when any1 == any1a && IsLogic(any1) => True,
3031
Orf(Notf(var any1), var any2) when IsLogic(any1, any2) => any1.Implies(any2),
3132
Andf(var any1, var any1a) when any1 == any1a && IsLogic(any1) => any1,
3233
Orf(var any1, var any1a) when any1 == any1a && IsLogic(any1) => any1,
3334
Impliesf(var any1, var any1a) when any1 == any1a && IsLogic(any1) => True,
34-
Xorf(var any1, var any1a) when any1 == any1a && IsLogic(any1) => False,
35+
Xorf(var any1, var any1a) when any1 == any1a && IsLogic(any1) => False.Provided(any1.DomainCondition),
3536
Notf(Notf(var any1)) when IsLogic(any1) => any1,
3637

37-
Orf(var any1, var any2) when (any1 == True || any2 == True) && IsLogic(any1, any2) => True,
38-
Andf(var any1, var any2) when (any1 == False || any2 == False) && IsLogic(any1, any2) => False,
38+
Orf(var any1, var any2) when (any1 == True || any2 == True) && IsLogic(any1, any2) => True.Provided(any1.DomainCondition).Provided(any2.DomainCondition),
39+
Andf(var any1, var any2) when (any1 == False || any2 == False) && IsLogic(any1, any2) => False.Provided(any1.DomainCondition).Provided(any2.DomainCondition),
3940

4041
Orf(Andf(var any1, var any2), Andf(var any1a, var any3)) when any1 == any1a && IsLogic(any1, any2, any3) => any1 & (any2 | any3),
4142
Andf(Orf(var any1, var any2), Orf(var any1a, var any3)) when any1 == any1a && IsLogic(any1, any2, any3) => any1 | (any2 & any3),

‎Sources/AngouriMath/Functions/Simplification/Patterns/Patterns.EqualityInequality.cs‎

Lines changed: 16 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -5,8 +5,10 @@
55
// Website: https://am.angouri.org.
66
//
77

8+
using System;
89
using static AngouriMath.Entity;
910
using static AngouriMath.Entity.Boolean;
11+
using static Antlr4.Runtime.Atn.SemanticContext;
1012

1113
namespace AngouriMath.Functions
1214
{
@@ -55,12 +57,20 @@ private static bool OppositeSigns(ComparisonSign left, ComparisonSign right)
5557
Notf(Lessf(var any1, var any2)) => any1 >= any2,
5658
Notf(GreaterOrEqualf(var any1, var any2)) => any1 < any2,
5759
Notf(LessOrEqualf(var any1, var any2)) => any1 > any2,
60+
// 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.
61+
// For complexity to not increase, maximum one AND/OR component can be something other than a comparison operator to propagate NOT into.
62+
// e.g. not (a > b and b = c) becomes (a <= b or not b = c)
63+
// Note that Notf(Equalsf) has the same complexity as Equalsf in ComplexityCriteria, so it can be treated as a comparison operator here.
64+
Notf(Andf a) when Andf.LinearChildren(a).Count(n => n is not (ComparisonSign or Notf or Orf)) <= 1 =>
65+
Andf.LinearChildren(a).Select(e => InequalityEqualityRules(e switch { Notf(var n) => n, var n => new Notf(n) })).Aggregate((a, b) => a | b),
66+
Notf(Orf a) when Orf.LinearChildren(a).Count(n => n is not (ComparisonSign or Notf or Andf)) <= 1 =>
67+
Orf.LinearChildren(a).Select(e => InequalityEqualityRules(e switch { Notf(var n) => n, var n => new Notf(n) })).Aggregate((a, b) => a & b),
5868

5969
Impliesf(Andf(Greaterf(var any1, var any2), Greaterf(var any2a, var any3)), Greaterf(var any1a, var any3a))
60-
when any1 == any1a && any2 == any2a && any3 == any3a => True,
70+
when any1 == any1a && any2 == any2a && any3 == any3a => True.Provided(any1.DomainCondition).Provided(any2.DomainCondition).Provided(any3.DomainCondition),
6171

6272
Impliesf(Andf(Lessf(var any1, var any2), Lessf(var any2a, var any3)), Lessf(var any1a, var any3a))
63-
when any1 == any1a && any2 == any2a && any3 == any3a => True,
73+
when any1 == any1a && any2 == any2a && any3 == any3a => True.Provided(any1.DomainCondition).Provided(any2.DomainCondition).Provided(any3.DomainCondition),
6474

6575
Equalsf(var zero, var anyButZero) when IsZero(zero) && !IsZero(anyButZero) => anyButZero.Equalizes(zero),
6676
Greaterf(var zero, var anyButZero) when IsZero(zero) && !IsZero(anyButZero) => anyButZero < zero,
@@ -129,10 +139,10 @@ private static bool OppositeSigns(ComparisonSign left, ComparisonSign right)
129139
// a! = 0
130140
Equalsf(Factorialf({ DomainCondition: var condition }), var zeroEnt) when IsZero(zeroEnt) => False.Provided(condition),
131141

132-
Greaterf(var any1, var any1a) when any1 == any1a => false,
133-
Lessf(var any1, var any1a) when any1 == any1a => false,
134-
GreaterOrEqualf(var any1, var any1a) when any1 == any1a => true,
135-
LessOrEqualf(var any1, var any1a) when any1 == any1a => true,
142+
Greaterf(var any1, var any1a) when any1 == any1a => False.Provided(any1.DomainCondition),
143+
Lessf(var any1, var any1a) when any1 == any1a => False.Provided(any1.DomainCondition),
144+
GreaterOrEqualf(var any1, var any1a) when any1 == any1a => True.Provided(any1.DomainCondition),
145+
LessOrEqualf(var any1, var any1a) when any1 == any1a => True.Provided(any1.DomainCondition),
136146

137147
_ => x
138148
};

‎Sources/Tests/UnitTests/Convenience/LatexTest.cs‎

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -49,7 +49,7 @@ void TestSimplify(string expected, Entity actual) =>
4949
[Fact] public void MultiplySimplify() => TestSimplify("{x}^{2}", x * x);
5050
[Fact] public void Divide() => Test(@"\frac{x}{x}", x / x);
5151
[Fact] public void DivideDivide() => Test(@"\frac{\frac{x}{x}}{x}", x / x / x);
52-
[Fact] public void DivideSimplify() => TestSimplify(@"1 \quad \text{for} \quad \neg{x = 0}", x / x);
52+
[Fact] public void DivideSimplify() => TestSimplify(@"1 \quad \text{for} \quad x \neq 0", x / x);
5353
[Fact] public void Greek1() => Test(@"\alpha", MathS.Var("alpha"));
5454
[Fact] public void Greek2() => Test(@"\beta", MathS.Var("beta"));
5555
[Fact] public void Greek3() => Test(@"a_{\beta}", MathS.Var("a_beta"));
@@ -631,13 +631,17 @@ [Fact] public void EqualityInequalityChain()
631631
=> Test(@"x \geq y = z < w",
632632
(x >= MathS.Var("y")) & (MathS.Var("y").Equalizes(MathS.Var("z"))) & (MathS.Var("z") < MathS.Var("w")));
633633
[Fact] public void EqualityInequalityChainAlt() => Test(@"x \geq y = z < w", (x >= "y").Equalizes("z") < "w");
634-
[Fact] public void EqualityInequalityChainString() => Test(@"x \geq y = z < w", (Entity)"x>=y=z<w");
634+
[Fact] public void EqualityInequalityChainString() => Test(@"x \geq y = z < w", (Entity)"(x>=y=z)<w");
635+
[Fact] public void EqualityInequalityChainStringBug() => Test(@"x \geq y = \left(z < w\right)", (Entity)"x>=y=z<w"); // TODO: why does it parse this way? it's supposed to parse like the above test.
635636
[Fact] public void EqualityInequalityChainParenthesized() => Test(@"x \geq \left(y = \left(z < w\right)\right)", new Entity.GreaterOrEqualf(x, new Entity.Equalsf("y", (Entity)"z" < "w")));
636637
[Fact] public void ParenthesizedComparisons()
637638
=> Test(@"\left(x < x\right) \geq \left(x > \left(\left(x = x\right) \leq x\right)\right)",
638639
#pragma warning disable 1718 // Disable self-comparison warning
639640
new Entity.GreaterOrEqualf(x < x, (x > new Entity.LessOrEqualf(new Entity.Equalsf(x, x), x))));
640641
#pragma warning restore 1718
642+
[Fact] public void NotEqual() => Test(@"1 \neq 2", (Entity)"not 1 = 2");
643+
[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");
644+
[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");
641645
[Fact] public void ImpliesChain()
642646
=> 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"))));
643647
}

‎Sources/Tests/UnitTests/PatternsTest/BooleanSimplify.cs‎

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -127,5 +127,26 @@ public void TestProvided(string expr, string? expected)
127127
var act = expr.ToEntity();
128128
Assert.Equal(exp, act.Simplify());
129129
}
130+
[Theory]
131+
[InlineData("not (not x)", "x")]
132+
[InlineData("not (a = b and b = c)", "not a = b or not b = c")]
133+
[InlineData("not (a <= b and b < c)", "a > b or b >= c")]
134+
[InlineData("not (a > b and b >= c)", "a <= b or b < c")]
135+
[InlineData("not (a <= b and b <= c and 1)", "not (1 and a <= b and b <= c)")]
136+
[InlineData("not (a = b or b = c)", "not a = b and not b = c")]
137+
[InlineData("not (a <= b or b < c)", "a > b and b >= c")]
138+
[InlineData("not (a > b or b >= c)", "a <= b and b < c")]
139+
[InlineData("not (a <= b or b <= c or 1)", "not (1 or a <= b or b <= c)")]
140+
[InlineData("not (a < b or c > d and e = f)", "a >= b and (c <= d or not e = f)")]
141+
[InlineData("not (not (a > b and b >= c) and y)", "a > b and b >= c or not y")]
142+
[InlineData("not (not (a = b and b = c) and y)", "a = b and b = c or not y")]
143+
[InlineData("not (not (not a = b and not b = c) and y)", "not ((a = b or b = c) and y)")]
144+
[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")]
145+
public void NestedNot(string expr, string expected)
146+
{
147+
var exp = expected.ToEntity();
148+
var act = expr.ToEntity();
149+
Assert.Equal(exp, act.Simplify());
150+
}
130151
}
131152
}

‎Sources/Tests/UnitTests/PatternsTest/SimplifyTest.cs‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -48,7 +48,7 @@ [Fact] public void Patt2() => AssertSimplify(
4848
[Fact] public void Patt9() => AssertSimplify(MathS.Arccotan(x * 3) + MathS.Arctan(x * 6), MathS.Arccotan(3 * x) + MathS.Arctan(6 * x));
4949
[Fact] public void Patt10() => AssertSimplify(MathS.Arcsin(x * 3) + MathS.Arccos(x * 1), MathS.Arcsin(3 * x) + MathS.Arccos(x));
5050
[Fact] public void Patt11() => AssertSimplify(3 + x + 4 + x, 7 + 2 * x);
51-
[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);
51+
[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);
5252
[Fact] public void Frac1() => AssertSimplify("x / (y / z)", "x * z / y");
5353
[Fact] public void Frac2() => AssertSimplify("x / y / z", "x / (y * z)");
5454
[Fact] public void Factorial2() => AssertSimplify(MathS.Factorial(2), 2);

‎Sources/Tests/UnitTests/PatternsTest/SortSimplifyTest.cs‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,7 @@ public sealed class SortSimplifyTest
2121
// [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")]
2222
// [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)]
2323
[InlineData("sec(x) + a + sin(x) + c + 1 + 0 + 3 + sec(x)", "4 + 2 * sec(x) + sin(x) + a + c")]
24-
[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)")]
24+
[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")]
2525
[InlineData("sin(x) * a * b / c / sin(h + 0.1) * cosec(x)", "a * b / (sin(h + 1/10) * c) provided not sin(x) = 0")]
2626
[InlineData("cos(x) * a * b / c / sin(h + 0.1) * sec(x)", "a * b / (sin(h + 1/10) * c) provided not cos(x) = 0")]
2727
[InlineData("sec(x) * a * b / c / sin(h + 0.1) * cos(x)", "a * b / (sin(h + 1/10) * c) provided not cos(x) = 0")]

0 commit comments

Comments
 (0)