Update Math Demo

[saulshanabrook]

This PR updates the math demo to more closely resemble the one from egglog at https://github.com/egraphs-good/egg/blob/main/tests/math.rs:

• Replace i64 with f64
• Adds node pruning with subsumption on another ruleset that always fires afterword
• Removes evals-to and replaces with just directly unioning the const
• Removes is-sym and replaces by just inlining Var pattern
• Adds all checks from egg
• Changes cost to match egg

This also runs quite quickly now on my machine!

[Copilot]

Pull request overview

This PR updates the math demo to closely match the egg implementation from https://github.com/egraphs-good/egg/blob/main/tests/math.rs. The changes improve performance and align the implementation with the reference design.

• Replaces i64 with f64 for floating-point constants throughout
• Implements node pruning using subsumption in a separate prune ruleset
• Simplifies constant handling by replacing the evals-to relation with direct constant folding rewrites
• Replaces the is-sym relation with inline Var pattern matching
• Adds comprehensive test cases from egg covering differentiation, integration, and simplification
• Updates cost model to match egg (adds :cost 100 to Diff and Integral)

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

[chatgpt-codex-connector]

Avoid tagging all non‑zero literals as proven non‑zero

The new is-not-zero rule now asserts is-not-zero x for every MathU term except the literal (Const 0.0). That makes conditional rewrites such as (Div a a) -> (Const 1.0) and (Pow x (Const 0.0)) -> (Const 1.0) fire for any symbolic variable, so Div (Var "x") (Var "x") now rewrites to 1 even when x could be zero. The previous evals-to-based predicate only marked values proven non‑zero; this broad rule introduces unsound equalities for zero inputs.

Useful? React with 👍 / 👎.

[saulshanabrook]

FWIW I updated the rule to be this because the egg rule is also unsound like this and that behavior is actually tested

[codspeed-hq]

CodSpeed Performance Report

Merging #757 will not alter performance

_{Comparing saulshanabrook:math-update (e37c620) with main (818e4ac)}

Summary

✅ 20 untouched
⏩ 190 skipped¹

Footnotes

1. 190 benchmarks were skipped, so the baseline results were used instead. If they were deleted from the codebase, click here and archive them to remove them from the performance reports. ↩

[oflatt]

Maybe we want to keep both? I thought the other math file was meant to be more natural egglog demonstrating evals-to

[saulshanabrook]

Sounds good, moved it to a new file

[yihozhang]

Maybe we should just keep one in the web-demo and move the other one out?