Nested associative-commutative pattern matching

[zengmao]

This PR enables full (nested) associative-commutative pattern matching for all sub-expressions with + or * operations, when the user passes an option fullac to the @rule macro. This solves the problem that @acrule only applies associativity-commutativity at the top level.

The algorithm is currently simplistic, meant to be a "minimum viable product" rather than an optimized implementation. The pattern matcher tries up to $n!$ permutations of $n$ arguments for any sub-expression with the operation + or *, when attempting to find matches. The core algorithm is implemented in matcher.jl in the function function term_matcher(term, fullac_flag = false).

Here are examples which show capabilities beyond those of @acrule:

@syms a b c
(@rule ~a + ~a*~b => ~a * (1+~b) fullac)(b + a*b) # result: b * (1+a)
(@rule ~a*~b + ~a*~c => ~a * (~b+~c) fullac)(a*b + b*c) # result: b * (a+c)

In these cases, @acrule return nothing because it fails to reorder the multiplication expressions to find a match.

[github-actions[bot]]

Benchmark Results

	master	a14a308fbe0066...	master/a14a308fbe0066...
overhead/acrule/a+2	0.76 ± 0.016 μs	0.749 ± 0.016 μs	1.01
overhead/acrule/a+2+b	0.744 ± 0.015 μs	0.723 ± 0.014 μs	1.03
overhead/acrule/a+b	0.257 ± 0.011 μs	0.255 ± 0.011 μs	1.01
overhead/acrule/noop:Int	25.1 ± 0.92 ns	26.5 ± 0.92 ns	0.944
overhead/acrule/noop:Sym	0.0364 ± 0.0053 μs	0.0408 ± 0.005 μs	0.892
overhead/rule/noop:Int	0.0439 ± 0.00067 μs	0.0451 ± 0.00075 μs	0.974
overhead/rule/noop:Sym	0.0561 ± 0.0024 μs	0.0561 ± 0.0026 μs	1
overhead/rule/noop:Term	0.0556 ± 0.0029 μs	0.0543 ± 0.0028 μs	1.02
overhead/ruleset/noop:Int	0.127 ± 0.0031 μs	0.133 ± 0.0025 μs	0.962
overhead/ruleset/noop:Sym	0.152 ± 0.0045 μs	0.146 ± 0.0045 μs	1.04
overhead/ruleset/noop:Term	3.09 ± 0.13 μs	3.1 ± 0.089 μs	0.994
overhead/simplify/noop:Int	0.138 ± 0.0024 μs	0.148 ± 0.0023 μs	0.934
overhead/simplify/noop:Sym	0.155 ± 0.0049 μs	0.159 ± 0.0058 μs	0.975
overhead/simplify/noop:Term	0.0366 ± 0.0019 ms	0.0396 ± 0.0021 ms	0.924
overhead/simplify/randterm (+, *):serial	0.0898 ± 0.002 s	0.0915 ± 0.0046 s	0.982
overhead/simplify/randterm (+, *):thread	0.052 ± 0.035 s	0.0577 ± 0.033 s	0.902
overhead/simplify/randterm (/, *):serial	0.215 ± 0.007 ms	0.221 ± 0.0055 ms	0.972
overhead/simplify/randterm (/, *):thread	0.243 ± 0.0084 ms	0.247 ± 0.0058 ms	0.984
overhead/substitute/a	0.0596 ± 0.0016 ms	0.0602 ± 0.0014 ms	0.99
overhead/substitute/a,b	0.0523 ± 0.0014 ms	0.0536 ± 0.0014 ms	0.976
overhead/substitute/a,b,c	16.9 ± 0.69 μs	19.1 ± 0.71 μs	0.884
polyform/easy_iszero	29.5 ± 1.8 μs	29.5 ± 1.5 μs	1
polyform/isone	3.1 ± 0.01 ns	3.1 ± 0.01 ns	1
polyform/iszero	1.12 ± 0.033 ms	1.13 ± 0.034 ms	0.988
polyform/simplify_fractions	1.63 ± 0.045 ms	1.6 ± 0.039 ms	1.02
time_to_load	2.15 ± 0.0093 s	2.13 ± 0.019 s	1.01

Benchmark Plots

A plot of the benchmark results have been uploaded as an artifact to the workflow run for this PR. Go to "Actions"->"Benchmark a pull request"->[the most recent run]->"Artifacts" (at the bottom).

[zengmao]

It would be useful to hear some feedback about:

• Since Metatheory.jl potentially can handle associativity-commutativity fully in the alternative e-graph approach, does SymbolicsUtil still need a classic term rewriter that's aware of associativity-commutativity beyond the top level? Or do you prefer to keep the classical rewriter in its current state, rather than adding features like this PR?
• Is the user interface, i.e. an extra option for @rule, acceptable? Or would it be better to make a new macro like @fullac_rule? I can also add an option for the user to specify custom functions, other than + and *, to be treated as AC.
• Is there a risk of a resource-intensive feature getting used too heavily by users and causing performance degradation? Maybe the users just need to be warned to prefer ordinary @rule and @acrule when possible.