Unreleased - ReleaseDate
0.9.4 - 2023-05-23
- [#253] Improved rebuilding algorithm using a queue.
- [#259] Fixed another overflow bug in proof size optimization.
- Various typo fixes (Thanks @nlewycky)
0.9.3 - 2023-02-06
- #215 Added a better intersection algorithms on two egraphs based on "Join Algorithms for the Theory of Uninterpreted Functions". The old intersection algorithm was not complete on the terms in both egraphs, but the new one is. Unfortunately, the new algorithm is quadratic.
- #230 Fixed a performance bug in
get_string_with_letthat caused printing let-bound proofs to be extremely inefficient.
0.9.2 - 2022-12-15
- #210 Fix crashes in proof generation due to proof size calculations overflowing.
0.9.1 - 2022-09-22
- #186 Added proof minimization (enabled by default), a greedy algorithm to find smaller proofs
- with and
without_explanation_length_optimizationfor turning this on and off
copy_without_unionsfor copying an egraph but without any equality information
id_to_exprfor getting an expression corresponding to a particular enode's id
- with and
- #197 Added
search_with_limit, so that matching also stops when it hits scheduling limits.
- Changed the
pre_unionhook to support explanations
- now provides the
Idof the two specific enodes that are merged, not canonical ids.
- It also provides the reason for the merge in the form of a
- now provides the
0.9.0 - 2022-06-12
- Added a way to update analysis data and have it propagate through the e-graph
- Improved documentation
- Updated dependencies
unionis now allowed when explanations are on
0.8.1 - 2022-05-04
- Improved documentation for features.
0.8.0 - 2022-04-28
- (#165) Unions now happen "instantly", restoring the pre-0.7 behavior.
- The tested MSRV is now 1.60.0.
- Several small documentation enhancements.
- (#162, #163)
Symbollogic into the
0.7.1 - 2021-12-14
This patch fixes a pretty bad e-matching bug introduced in 0.7.0. Please upgrade!
- (#143) Non-linear patterns e-match correctly again
- (#141) Loosen requirement on FromOp::Error
0.7.0 - 2021-11-23
It's a been a long time since a release! There's a lot in this one, hopefully I can cut releases more frequently in the future, because there are definitely more features coming :)
- The egraph now has an
EGraph::with_explanations_enabledmode that allows for explaining why two terms are equivalent in the egraph. In explanations mode, all unions must be done through
union_instantiationsin order to justify the union. Calling
Explanationwhich has both a
FlatExplanationform and a
TreeExplanationform. See #115 and #119 for more details.
BackoffScheduleris now more flexible.
EGraph::pre_unionallows inspection of unions, which can be useful for debugging.
- The dot printer is now more flexible.
Analysis::mergenow gets a
&mut self, so it can store data on the
Analysis::mergehas a different signature.
- Pattern compilation and execution is faster, especially when there are ground terms involved.
- All unions are now delayed until rebuilding, so
EGraph::rebuildbe called to observe effects.
apply_onefunction on appliers now needs to perform unions.
- The congruence closure algorithm now keeps the egraph congruent before
doing any analysis (calling
make). It does this by interleaving rebuilding and doing analysis.
EGraph::add_exprnow proceeds linearly through the given
RecExpr, which should be faster and include all e-nodes from the expression.
Rewritenow has public
applierfields and no
- (#61) Rebuilding is much improved! The new algorithm's congruence closure part is closer to Downey, Sethi, Tarjan, and the analysis data propagation is more precise with respect to merging. Overall, the algorithm is simpler, easier to reason about, and more than twice as fast!
Language::display_ophas been removed. Languages should implement
Displayto display the operator instead.
Language::from_op_strhas been replaced by a new
define_language!implements this trait automatically.
0.6.0 - 2020-07-16
Idis now a struct not a type alias. This should help prevent some bugs.
Runnerhooks allow you to modify the
Runnereach iteration and stop early if you want.
- Added a way to lookup an e-node without adding it.
define_language!now support variants with data and children.
- Added a tutorial in the documentation!
- Fixed a bug when making
- Improved the
0.5.0 - 2020-06-22
Symbols, a simple interned string that users can (and should) use in their
eggwill now warn you when you try to use
Rewrites with the same name.
- Rewrite creation will now fail if the searcher doesn't bind the right variables.
rewrite!macro supports bidirectional rewrites now.
define_language!now supports variable numbers of children with
rewrite!macro builds conditional rewrites in the correct order now.
0.4.1 - 2020-05-26
- Added various Debug and Display impls.
- Fixed the way applications were counted by the Runner.
0.4.0 - 2020-05-21
- The rebuilding algorithm is now precise meaning it avoid a lot of unnecessary work. This leads to across the board speedup by up to 2x.
Languageelements are now much more compact, leading to speed ups across the board.
Analysis, which can hold egraph-global data as well as per-eclass data.
- Fix: An eclass's metadata will now get updated by congruence. (commit)
BackoffSchedulerwill now fast-forward if all rules are banned. (commit)
- Improve benchmark reporting (commit)
- The egraph now skips irrelevant eclasses while searching for a ~40% search speed up. (PR)
0.3.0 - 2020-02-27
Runnercan now be configured with user-defined
- Reworked the
RunnerAPI. It's now a generic struct instead of a trait.
- Patterns are now compiled into a small virtual machine bytecode inspired by this paper. This gets about a 40% speed up.
0.2.0 - 2020-02-19
- A dumb little benchmarking system called
egg_benchthat can help benchmark tests.
- String interning for
QuestionMarkNames). This speeds up things by ~35%.
- Add a configurable time limit to
- Multi-matching patterns (ex:
?a...). They were a hack and undocumented. If we can come up with better way to do it, then we can put them back.
0.1.2 - 2020-02-14
This release completes the documentation (at least every public item is documented).
0.1.1 - 2020-02-13
- A lot of documentation
- The graphviz visualization now looks a lot better; enode argument come out from the "correct" position based on which argument they are.
0.1.0 - 2020-02-11
This is egg's first real release!
Hard to make a changelog on the first release, since basically everything has changed! But hopefully things will be a little more stable from here on out since the API is a lot nicer.