Repository navigation
Highlights
prove_equal(..., max_expressions=N): total-work budget across both bidirectional-BFS frontiers. Un-provable queries that previously exhausted the full depth-bounded reachable set now returnNonein bounded time. Measured impact: an un-provable boolean case went from 20,174 ms to 363 ms withmax_expressions=2000.minimize()default flipped toinclude_unidirectional=True: the old default silently ignored every=>rule, producing "no improvement found" on expressions with obvious unidirectional simplifications. Passinclude_unidirectional=Falseto restrict to strict reversible equivalences.- Experiments directory with runnable benchmarks that validate correctness against theory (
n! × Catalan(n-1)class sizes under associativity + commutativity) and measure timing across proof, enumeration, minimize, and random-walk features. - Expanded docs: new Equivalence & Proof guide, new API reference sections, new worked examples, and a
CHANGELOG.md.
Breaking changes
minimize()default forinclude_unidirectionalchanged fromFalsetoTrue. See above.OptimizationResult.improvement_ratiosemantics changed in 0.4.0; usecost_ratiofor the old behavior. (This landed in a prior commit but is worth re-flagging for anyone who skipped 0.4.)
Added
prove_equal(..., max_expressions=N)work budget.experiments/features_benchmark.py(7 probes) andexperiments/scaling.py.docs/equivalence.md, new API and examples sections, README section for equivalence and optimization.CHANGELOG.md.
Fixed
- Removed dead
check_intersection()helper inprove_equal(). - Collapsed a dead if/else branch in
equivalents(). - Replaced 7 stringly-typed
"failed"sentinel checks withwrap_bindings(). __version__inrerum/__init__.pyis no longer stale.
Tests
449 tests passing (up from 443 in 0.4.0). New test classes: TestProveEqualMaxExpressions, plus new regression tests for the minimize() default.
Install
pip install -U rerumFull changelog: CHANGELOG.md
🤖 Generated with Claude Code