Formula simplifier using e-graphs

[dariusf]

Here's a first attempt using egglog to remove temporary existentials, e.g.:

exists x. a=b/\res=x/\x=1
==>
a=b/\res=1

(datatype Value (Num i64))
(declare True Value)
(declare False Value)
(datatype VarType)
(datatype Term
    (Val Value)
    (Var VarType)
    (And Term Term)
    (Eq Term Term)
    (Ex VarType Term))
(function V (String) VarType)
(function From (Term) VarType)


(rewrite (And ?a ?b) (And ?b ?a))
(rewrite (Eq ?a ?b) (Eq ?b ?a))

(rewrite
  (Ex ?v (And (Eq (Var ?v) ?x) (Eq (Var ?v) ?y)))
  (Eq ?x ?y))

(let e1 (Ex (V "x") (And (Eq (Var (V "x")) (Val (Num 1))) (Eq (Var (V "x")) (Var (V "res"))))))

(push)

(run 4)
(check (= e1 (Eq (Var (V "res")) (Val (Num 1)))))
(extract e1)
(pop)

Dealing with binders

A simple solution (used above), where variables are represented with strings and assumed to be fresh, may be sufficient. If not, here are a few pointers.

• Blog post
• Sec 2 of this paper
• Slide 50

Next steps

• Figure out the full list of simplifications currently implemented
• Try above example using ego

[dariusf]

Here are some more simplifications which are currently implemented:

simplify_existential_locations:
  ex x; ens x->...; ex y; ens y->... ==> ex x; ens x->...; ex y; ens x->...
    if x=y appears somewhere

remove_temp_vars:
  ex x; ens x=c; S ==> ex x; S
    if x does not occur in S and c is a constant

optimize_existentials:
  ex x; S ==> S
    if x does not occur in S
  ex x; S; S1 ==> S; ex x; S1
    if x does not occur in S but occurs in S1

remove_vars_occurring_twice:
  ex x; ens x=0/\res=x ==> ex x; ens 0=0/\res=0

propagate_function_stage_equalities:
  ens b=(fun ...)/\a=b; a(...) ==> ens b=(fun ...); b(...)

simplify_pure:
  ens !(x=true) ==> ens x=false
  ens x=x ==> ens true
  ens c=c ==> ens true
  ens true/\P ==> ens P
  ens false/\P ==> ens false
  ens c+c ==> ens c1
    if c1=c+C