Add math example

[saulshanabrook]

This:

• Includes recent upstream changes
• Adds math smt example based on Update Math Demo egraphs-good/egglog#757
• Adds start of readme for this project to this readme
• Adds way to run and log SMT queries, which is fun!
• Adds a few more needed primitives, included a way to choose a smaller SMT expression by tree size

[Copilot]

Pull request overview

This PR adds SMT (Satisfiability Modulo Theories) support and related functionality to egglog-experimental. It's based on work from upstream egglog PR #757 and includes a calculus/math example demonstrating SMT-based symbolic reasoning. The changes enable SMT-backed term rewriting and analysis, which allows for more powerful equality reasoning using an external Z3 solver.

Key Changes:

• Adds comprehensive SMT infrastructure with support for real numbers, integers, booleans, bitvectors, and uninterpreted functions
• Introduces the get-size! primitive for querying e-graph node counts, useful for controlling rewrite explosion
• Updates the egglog dependency to a specific revision (33f7994) for compatibility

Reviewed changes

Copilot reviewed 16 out of 18 changed files in this pull request and generated 5 comments.

Show a summary per file

File	Description
tests/web-demo/node-limit.egg	New test demonstrating node limit control using get-size! with :until guards
tests/web-demo/get-size.egg	New test demonstrating the get-size! primitive functionality
tests/smt-real.egg	Updated to use renamed smt-= primitive instead of smt-real-= for consistency; adds uninterpreted function test
tests/smt-math.svg	Generated visualization file (SVG) for the math example
tests/smt-math.egg	New comprehensive test port of egg's math example using SMT for symbolic differentiation and integration
tests/polynomials/polynomial-smt.egg	Updated to use renamed smt-= primitive
tests/polynomials/factor-rat.egg	Updated to use renamed smt-= primitive
tests/polynomials/benchmark/polynomial-smt-rules.egg	Updated to use renamed smt-= primitive
tests/integration_test.rs	Added Rust integration test for get-size! primitive
src/smt_real.rs	Added AST size calculation, uninterpreted function support (SMTUFReal), and min-by-ast-size merge primitive
src/smt_bitvec.rs	Added AST size calculation for bitvector values
src/smt.rs	Major additions: SMT logging, exists quantifier, uninterpreted functions for Real type, AST size tracking, unified smt-= primitive
src/size.rs	New module implementing the get-size! primitive for querying e-graph sizes
src/scheduling.rs	Fixed :until condition logic to properly check for query matches
src/lib.rs	Integrated get-size! primitive and added size module; commented out run-schedule registration
README.md	Added SMT final project reproduction instructions
Cargo.toml	Pinned egglog dependencies to specific revision 33f7994
Cargo.lock	Updated dependencies to match pinned revision

---

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

[Copilot]

The repository URL in the README points to a fork ("RockingMat/egglog-smt") rather than the canonical repository ("egraphs-good/egglog-experimental"). This should be updated to use the correct repository URL to avoid confusion.

Suggested change

	git clone git@github.com:RockingMat/egglog-smt.git
	cd egglog-smt
	git clone git@github.com:egraphs-good/egglog-experimental.git
	cd egglog-experimental

[Copilot]

Grammar issue in comment: "Need to table for all" should be "Need to track all" or "Need a table for all"

Suggested change

	; Need to table for all math expressions since egglog does not allow unbound variables
	; Need to track all math expressions since egglog does not allow unbound variables

[Copilot]

Typo in comment: "samller" should be "smaller"

Suggested change

	// Returns the SMT term with the samller AST size. It biases towards the first argument in case of a tie.
	// Returns the SMT term with the smaller AST size. It biases towards the first argument in case of a tie.

[Copilot]

These lines are commented out code. If the run-schedule command is no longer needed, this code should be removed entirely rather than left as commented code. If it's still needed, it should be uncommented or documented with an explanation of why it's disabled.

Suggested change

	// egraph
	// .add_command("run-schedule".into(), Arc::new(RunExtendedSchedule))
	// .unwrap();