Q: Metatheory.jl code optimization for multivariate polynomial expressions?

[Audrius-St]

Hello,

After going through the Metatheory.jl documentation, there are a number of concepts that are novel and unfamilair to me, so I'm unable to discern if the package can do the following:

It is possible to use Metatheory.jl for code optimization in the sense of reducing the number of basic operations {+, -, x, /, ^} for large multivariate polynomial and polynomial-like expressions?

I'm currently using FORM 4.2.1 which performs a stochastic local search via stochastic hill climbing to find the near-minimal number of operations for a multivariate Horner scheme combined with CSEE [Common Subexpression Elimination]. FORM reduces the number of basic operations by about a factor of eight.

Is it possible to use Metatheory.jl to do the same or equivalent? It would be both useful and much simpler, from a coding perspective, to have an all-Julia solution.

[0x0f0f0f]

Yes.

You have to:

1. Define a rewrite rule set with @theory
2. Define a cost function (or use the default astsize)
3. (Optionally) tweak the strategy with SaturationParams
4. Make an EGraph with the input expression and saturate! it.
5. Run extract! and get your optimized output expression.

The challenges you may encounter are the handling of associative-commutative equality rules (e.g. @rule ~a + (~b + ~c) == (~a + ~b) + ~c), as they may "blow up" the e-graph.

You can check the test/integration folder for a bunch of examples

[0x0f0f0f]

test/integration/cas.jl may be a good example :)

[Audrius-St]

Thank you for the instructions and pointer to the example.