## Refinement E-Graphs Oct 4, 2026 The idea of a refinement e-graph is to add a baked in a = {True} (ge dontcare false) ; dontcare also refines to false. {True, False} >= {False} (insert (ite x true dontcare)) ; insert starting term (run 5 :expand-le) (extract-le (ite x true dontcare)) ; can extract x because refining this dontcare to true enables a nice term` `Writing /tmp/circuit.sexp` `! refinement-microegg /tmp/circuit.sexp` There are also refinement rewrite rules available in the implementation, rewrite-le and rewrite-ge. Spiritually, (rewrite-le lhs rhs) represents the formula forall…