[WIP] EGraphs optimization

[0x0f0f0f]

What has been added:

• Integration of Symbolic types with EGraph types (see types.jl)
• Moved down stuff from Symbolics pull 286
• Basic theory of equalities
• symbolicegraph function to construct an egraph prepared for <:Symbolic expressions.
• extraction from an egraph returns constructor-level optimized expressions
• internal function toterm to transform Add, Mul, Pow, etc... into Term{T}
• internal function unflatten that takes associative n-ary terms and turns them into their binary Term{T} representation (egraph rewriting works best with this representation)
• An egraph cost function that computes the cost of operations of terms in CPU cycles (See https://arxiv.org/abs/2105.03949).
• An optimize function that takes an expression and returns the optimized expression.
• similarterm for <:Symbolic types can now dispatch against a f::Symbol operation, resolving the corresponding function object. The egraph backend does not know whether it should use a function object or a symbol when choosing the operation to instantiate during substitution. In this case, it's left to the actual instantiation of the term type through similarterm to choose whether to use the Symbol or the function literal.

What is left to do:

• [ ] add more equalities to the theory
• [ ] add more operator costs to the cost function
• [ ] add more tests
• [ ] do more than optimizing. egraphs can also do simplification.
• [ ] evaluate the standard simplification ruleset in an egraph and see how it does
• [ ] Find the best SaturationParameters. Maybe an hyperparameter analysis/exploration package can help.
• [ ] Add tests to downstream

[0x0f0f0f]

When running

    ex = 2a + 2b - (a*(a + b))
    res = optimize(ex)
    @test res ≖ (a+b)*(2-a)

There's a problem. Sometimes it returns the correct result (a+b)*(2-a) and sometimes, even if it says that the egraph has saturated it still returns 2a + 2b - (a*(a + b)). Here's a breakdown of the returned egraphs in the two cases, pretty printed. The numbers in the expressions are the eclass ids of children if not explicitly annotated.

ex = 2a + 2b - (a*(a + b))

erroring with result 

julia> extract!(g, SymbolicUtils.costfun)
2a + 2b + (a + b)*(a)

 g.root = 12

1 => [2] # number 2, not eclass ID
2 => SymbolicUtils.Sym{Number, Nothing}[a]
4 => SymbolicUtils.Sym{Number, Nothing}[b]
8 => [-1] # number -1, not eclass ID
3 => [:(1 * 2)]                              # 2 * a
5 => [:(1 * 4)]                              # 2 * b
7 => [:(2 + 4)]                              # a + b
13 => [:(2 * 8), :(8 * 2), :(-2)]            # a * -1 == -1 * a == -a
14 => [:(7 * 13)]                            # (a + b) * -a
15 => [:(1 * 7), :(3 + 5)]                   # 2 * (a + b) ==  (2 * a) + (2 * b)
12 => [:(14 + 15), :(15 + 14)]               # -a(a+b) + 2(a+b) == 2(a+b) + -a(a+b)

--------------------------

Correct result with g.root = 13

julia> extract!(g, SymbolicUtils.costfun)
(a + b)*(2 - a)

1 => [2] # number 2, not ECLass ID
2 => SymbolicUtils.Sym{Number, Nothing}[a]
4 => SymbolicUtils.Sym{Number, Nothing}[b]
8 => [-1] # number -1, not EClass ID
12 => [:(15 + 17), :(17 + 15), :(1 * 14), :(14 * 1)]    # 2b + 2a == 2a + 2b == 2(a+b) == (a+b)2
15 => [:(4 * 1), :(1 * 4)]                              # b * 2 == 2 * b
14 => [:(4 + 2), :(2 + 4)]                              # a + b == b + a
16 => [:(2 * 8), :(8 * 2), :(-2)]                       # a * -1 == -1 * a == -a
24 => [:(1 - 2), :(1 + 16)]                             # 2 - a == 2 + (-a)
17 => [:(2 * 1), :(1 * 2)]                              # a * 2 == 2 * a
18 => [:(14 * 16)]                                      # (a + b) * -a  
13 => [:(12 + 18), :(14 * 24)]                          # 2(a+b) + -a(a+b) == (a+b)*(2-a)

This is not due to extraction. This error happens during saturation. Some rules are not applied (and apparently, don't even match since it reports that the egraph has saturated). This does not happen in the next example:

 ex = sin(a^2)/cos(a^2)
    res = optimize(ex)
    @test isequal(res, tan(a^2)) 

always returns the same result.

cc @shashi for help

[0x0f0f0f]

The issue may be caused by the fact that when calling similarterm to build the actual instantiated terms of RHS of rules, the optimized types (Add, Mul, ...) are constructed therefore the ordering of children is somehow lost in the way, depending on the ordering of application of rules. Trying a custom similarterm approach passed to saturate!() as a parameter to keep everything as a Term.

[0x0f0f0f]

The issue may be caused by the fact that when calling similarterm to build the actual instantiated terms of RHS of rules, the optimized types (Add, Mul, ...) are constructed therefore the ordering of children is somehow lost in the way, depending on the ordering of application of rules. Trying a custom similarterm approach passed to saturate!() as a parameter to keep everything as a Term.

Solved with a custom similarterm and a couple tweaks to preprocessing

[codecov-commenter]

Codecov Report

Merging #389 (847c86f) into master (ad5664a) will decrease coverage by 0.35%. The diff coverage is 78.04%.

@@            Coverage Diff             @@
##           master     #389      +/-   ##
==========================================
- Coverage   83.37%   83.01%   -0.36%     
==========================================
  Files          10       12       +2     
  Lines        1257     1319      +62     
==========================================
+ Hits         1048     1095      +47     
- Misses        209      224      +15     

Impacted Files	Coverage Δ
src/SymbolicUtils.jl	100.00% <ø> (ø)
src/polyform.jl	91.92% <0.00%> (-0.84%)	:arrow_down:
src/types.jl	83.60% <70.58%> (-1.39%)	:arrow_down:
src/egraph.jl	96.55% <96.55%> (ø)

---

Continue to review full report at Codecov.

Legend - Click here to learn more Δ = absolute <relative> (impact), ø = not affected, ? = missing data Powered by Codecov. Last update ad5664a...847c86f. Read the comment docs.

[0x0f0f0f]

All green. Creating PR in Symbolics.jl integrating those changes now