Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

3.0 Release #185

Open
wants to merge 330 commits into
base: master
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
330 commits
Select commit Hold shift + click to select a range
f32e691
Fix merging of analysis data when one of them is nothing
gkronber Feb 25, 2024
94bc6b6
Changed definition of astsize and astsize_inv to simply count the num…
gkronber Feb 25, 2024
14f9944
Fixed syntax error.
gkronber Feb 26, 2024
a73a65b
Compare with first item (=min cost value) of cost tuple. The current …
gkronber Feb 26, 2024
55a6695
Merge pull request #191 from gkronber/3.0_fixes
0x0f0f0f Feb 27, 2024
e3d36e1
temp work
Feb 27, 2024
666618a
Revert "temp work"
Feb 28, 2024
98f9e17
Init new TIface
Feb 29, 2024
a97d3e9
Integrate more new terminterface
Mar 1, 2024
fcef108
all working with new terminterface
Mar 1, 2024
68d9df9
adjust doctest
Mar 1, 2024
0386096
adjust
Mar 1, 2024
571e34b
Fixed a bug that I introduced earlier.
gkronber Mar 2, 2024
c061425
optimizations
Mar 2, 2024
f8b5fce
Merge pull request #194 from gkronber/fix_astsizeinv
0x0f0f0f Mar 3, 2024
5c1942f
pretty printing; fix graphviz.jl
nmheim Mar 27, 2024
18992a1
minor fixes; some docstrings
nmheim Mar 27, 2024
abd23d4
some more doc strings
nmheim Mar 27, 2024
3f3e68f
update e-class printing
nmheim Mar 27, 2024
17dc6a7
include egraph type signature
nmheim Mar 27, 2024
07ef7b0
package extensions
nmheim Mar 27, 2024
056b058
update docs
nmheim Mar 27, 2024
506ec8b
update docs
nmheim Mar 27, 2024
4039796
update docs again
nmheim Mar 27, 2024
2f7e7f3
Apply suggestions from code review
0x0f0f0f Mar 28, 2024
f3f71f1
Merge pull request #195 from nmheim/nh/visuals
0x0f0f0f Mar 28, 2024
93798cd
adjust
Mar 28, 2024
0e008e8
Merge remote-tracking branch 'original/ale/3.0' into nh/pkg-ext
nmheim Mar 29, 2024
f06f570
svg with fixed labels
nmheim Mar 29, 2024
79aa461
Merge pull request #196 from nmheim/nh/pkg-ext
0x0f0f0f Mar 29, 2024
8254bd5
Merge remote-tracking branch 'origin/master' into ale/3.0
Apr 5, 2024
ccf2d52
Merge remote-tracking branch 'origin/master' into ale/3.0
Apr 6, 2024
6330cd7
Update docs
Apr 6, 2024
3059d52
cleanup
Apr 6, 2024
a5b7794
fix bug
Apr 6, 2024
3f40142
restore TODO
Apr 9, 2024
fd83a89
add second simple math benchmark
nmheim Apr 10, 2024
c7d1381
remove bench info
Apr 10, 2024
baa9b96
Merge pull request #198 from nmheim/nh/simpl2
0x0f0f0f Apr 10, 2024
dc9d0f7
fix test
Apr 10, 2024
f05c536
trigger ci
Apr 10, 2024
0a4ec2f
cleanup scheduler
Apr 10, 2024
93b9fec
minor optimization
Apr 10, 2024
5f61812
remove op_key
Apr 10, 2024
85991e1
adjust scheduler
Apr 10, 2024
8f7e10a
dont allocate
Apr 11, 2024
d04bf2b
avoid type convert
Apr 11, 2024
5e5dd24
ultra e-matching
Apr 20, 2024
3cbac25
ITS FKN WORKING
Apr 20, 2024
f4f08e0
add check-eq instruction
Apr 20, 2024
7f491e5
progress
Apr 20, 2024
d70bac4
works
Apr 21, 2024
ac63f60
no errors detected
Apr 21, 2024
0940e80
adjustments
Apr 21, 2024
428084e
next iteration
Apr 22, 2024
22f2e11
remove swearing
Apr 22, 2024
4fb0873
adjustments
Apr 24, 2024
e755a31
debug stuff
Apr 26, 2024
2093fb7
friday night
Apr 26, 2024
5370727
make tests pass
Apr 28, 2024
93eaf7e
remove old ematcher
Apr 28, 2024
a43213d
finalize
Apr 28, 2024
35d6e4b
trigger CI
Apr 28, 2024
06c4998
immutable eclass
Apr 28, 2024
3ae8173
cleanup
Apr 28, 2024
6278476
cleanup
Apr 28, 2024
24bc137
Merge pull request #199 from JuliaSymbolics/ale/ultra-ematcher
0x0f0f0f Apr 28, 2024
0e5bb1a
optimize extraction and application
Apr 29, 2024
e88996b
less allocations
Apr 29, 2024
c13867c
adjust type
Apr 29, 2024
c901fc2
Merge branch 'ale/3.0' into ale/immutable-eclass
Apr 29, 2024
410e0b3
cleanup and adjustments
Apr 30, 2024
acea4e1
benchmark mt vs. egg
nmheim May 1, 2024
33c2434
avoid using eval
May 1, 2024
0e38a88
addres comments; try to make action run on current pr
nmheim May 1, 2024
1b7d25c
remove deprecated set-output
nmheim May 1, 2024
24b122b
Update .github/workflows/benchmark_pr.yml
0x0f0f0f May 1, 2024
7648695
Merge pull request #201 from nmheim/nh/bench-action
0x0f0f0f May 1, 2024
5766fb5
benchmark pr
May 1, 2024
2bb73fb
Merge branch 'ale/3.0' into ale/ematch-dont-eval
May 1, 2024
83b8cca
more compiled stuffgs!
May 2, 2024
1ddf8f4
add match compiler
May 2, 2024
77b986b
compilation state
May 3, 2024
d6fc362
remove prints
May 4, 2024
aafa0dd
YOOOOOOOOOOOOOOOOOOOOOOOOOOOOOOOOOOOOOOOO even faster
May 4, 2024
a52c384
should be slightly faster
May 4, 2024
c42d746
buffer adjustments
May 4, 2024
dbb9d73
ultra optimize buffer memory
May 4, 2024
147c248
adjust method
May 4, 2024
592e92c
use less variables
May 5, 2024
5b96df8
optimize even further
May 5, 2024
8e1ae7b
compiler progress
May 6, 2024
ff266d7
use opt buffer for stacks
May 6, 2024
c6e2731
finalize static matchers
May 7, 2024
34e1493
things somehow work in index hell
May 7, 2024
9b041be
one remaining test
May 7, 2024
5783c82
ladies and gentleman compiled rewriting
May 8, 2024
71f4dba
make all tests pass
May 8, 2024
b1d8e87
adjust prop
May 8, 2024
c733091
ALL TESTS PASSING
May 8, 2024
3a6cf5e
use Base.@kwdef
May 8, 2024
891e16a
should pass CI
May 8, 2024
4041d90
Merge pull request #204 from JuliaSymbolics/ale/3.0-finalize-static-m…
0x0f0f0f May 8, 2024
ad836e2
Merge branch 'ale/3.0-finalize-static-matchers' into ale/3.0
May 8, 2024
097d49a
fix calc logic rules
nmheim May 9, 2024
9520668
prove in separate file
nmheim May 9, 2024
78e6264
fix tests/benchmarks
nmheim May 9, 2024
ecbb32f
include frege bench
nmheim May 9, 2024
be4bffc
Merge pull request #205 from nmheim/nh/calc-logic-fix
0x0f0f0f May 9, 2024
67781bc
adjust calc logic test file
May 9, 2024
6d73dac
calc logic
May 9, 2024
f11c5cd
comment out for CI
May 9, 2024
87f73df
format
May 9, 2024
79ee12e
Merge branch 'master' into ale/3.0
May 9, 2024
a86b0f2
Merge branch 'master' into ale/3.0
May 9, 2024
35abcc6
binarize!
May 12, 2024
d0a818a
improve KB
May 12, 2024
78871dc
adjust benchmark
May 12, 2024
5185eff
adjust knuth bendix and cas
May 13, 2024
8fd551d
remove dep
May 13, 2024
f135de6
simplify compiler
May 14, 2024
917509d
compact rules in single type
May 14, 2024
3893800
make all tests green
May 14, 2024
fbc42e9
update rules file
May 15, 2024
2c85584
rename
May 15, 2024
9c2c348
Merge pull request #206 from JuliaSymbolics/ale/3.0-new-compact-rule
0x0f0f0f May 15, 2024
11c279b
update
May 16, 2024
e7e56d9
print to correct IO
May 17, 2024
78e73e6
remove prints, make it pass
May 17, 2024
c0fc3d1
remove print
May 17, 2024
1599e0d
add unit tests folder
May 17, 2024
fe8d7ff
Merge pull request #207 from JuliaSymbolics/ale/3.0-named-rules
0x0f0f0f May 17, 2024
1608413
benchmark on 1.11
nmheim May 22, 2024
d216278
run bench workflow in MR
nmheim May 22, 2024
319ee7a
beta?
nmheim May 22, 2024
8b255ca
nightly?
nmheim May 22, 2024
b2164c9
1.11-beta
nmheim May 22, 2024
08ff618
beta1
nmheim May 22, 2024
6da15b6
issue comment does not work with forks
nmheim May 22, 2024
d5cc04b
fix lambda calc integration test; TODO: turn into tutorial
nmheim May 22, 2024
76c8e12
Merge pull request #208 from nmheim/nh/bench-1.11
0x0f0f0f May 23, 2024
07877e1
simplify
nmheim May 30, 2024
ee4cd0a
update to TermInterface 0.5
Jun 2, 2024
2b177d2
trigger CI
Jun 2, 2024
8f74503
Merge pull request #212 from JuliaSymbolics/ale/3.0-new-ti
0x0f0f0f Jun 2, 2024
840af79
get nested op
Jun 2, 2024
cdf82c8
Merge remote-tracking branch 'origin/ale/3.0' into ale/3.0
Jun 2, 2024
893afcf
resolve fully qualified function names
Jun 2, 2024
f5d2489
Merge branch 'ale/3.0' into nh/labmda-calc-2
nmheim Jun 3, 2024
d68899f
some words on lambda theory example; fix some smaller docs errors
nmheim Jun 3, 2024
a29c6f4
remove old lambda theory
nmheim Jun 3, 2024
f712d36
address comments
nmheim Jun 4, 2024
49690cc
add test for 2=S1
nmheim Jun 4, 2024
0d82eba
Merge pull request #216 from nmheim/nh/labmda-calc-2
0x0f0f0f Jun 5, 2024
df47537
autoformat
Jun 5, 2024
2e828e8
improvement on retrieving nested qualified functions
Jun 8, 2024
6965360
fully qualified function name improvements
Jun 8, 2024
fd502b8
remove unused, add test
Jun 8, 2024
b90a06a
remove old matchers
Jun 8, 2024
76065b1
make it pass
Jun 8, 2024
ded83f4
improve doc
Jun 8, 2024
fd267de
adjust docs
Jun 8, 2024
cb49aa6
cleanup and v bump
Jun 13, 2024
ed44417
remove base.meta import
Jun 13, 2024
b0bf132
fix comparison because == overrides BasicSymbolic of Bool
Jun 13, 2024
f4fa303
more isequal
Jun 13, 2024
2ad4e5a
test if works
0x0f0f0f Jun 18, 2024
085b55e
Update TermInterface
0x0f0f0f Jun 18, 2024
3fcb2ed
add direct function to convert EqualityRules
nmheim Jun 20, 2024
fbc4caa
isequal / rename functions
nmheim Jun 24, 2024
f8d6349
update TermInterface to 2.0
Jun 25, 2024
eec98d0
inversion works
Jun 25, 2024
542c46b
add docs
Jun 25, 2024
6a432fd
add docs
Jun 25, 2024
95e4c43
Merge pull request #220 from nmheim/nh/direct-conversion
0x0f0f0f Jun 25, 2024
360a29b
Merge remote-tracking branch 'origin/master' into ale/3.0
Jun 25, 2024
0068427
remove areequal
Jun 26, 2024
b36727d
adjust failing test on empty arrays
Jun 26, 2024
2b9ae8c
format
Jun 27, 2024
7328ea9
improvements to schedulers
Jun 27, 2024
07fb12d
add freeze scheduler
Jun 27, 2024
7709c90
remove merges buffer
Jun 28, 2024
8dc3283
typos
spaette Jul 4, 2024
dbdcdf5
Merge pull request #228 from vaerksted/ale/3.0
0x0f0f0f Jul 5, 2024
32be369
Squashed commit of the following:
gkronber Jul 5, 2024
d10173c
Merge pull request #229 from gkronber/225_hashcollision_squashed
0x0f0f0f Jul 6, 2024
f81371d
syntax improvements
Jul 6, 2024
6b34dfc
adjust syntax
Jul 6, 2024
cf05384
improve performance
Jul 6, 2024
2f3a032
minor optimizations
Jul 8, 2024
9e24b28
fix for niklas
Jul 22, 2024
a400c4d
Implement Base.iterate() for OptBuffer (for debug logging).
gkronber Jul 28, 2024
464660b
Fix comparison between 0 and zero(Id)
gkronber Jul 28, 2024
f061684
Fix incorrect usage of nothing value instead of :nothing symbol
gkronber Jul 28, 2024
d361144
Fix typo in docstring
gkronber Jul 28, 2024
83cb1a0
Add a unit test for a dynamic rule with a condition
gkronber Jul 28, 2024
8ad3c31
Merge pull request #230 from gkronber/ale/3.0
0x0f0f0f Jul 28, 2024
1726da7
Fix semantic analysis code for lambda theory unit test
gkronber Aug 16, 2024
d231fad
Bugfix in egraph semantic analysis update. We need to update the pare…
gkronber Aug 16, 2024
c1db759
Add assertions for semantic analysis values.
gkronber Aug 18, 2024
7629a9b
Add options to SaturationParams to enable assertions after rebuilding
gkronber Aug 20, 2024
30766c7
Rename kwargs.
gkronber Aug 20, 2024
c4a182e
Change comment to docstring and activate check_memo for lamda_theory …
gkronber Aug 20, 2024
e0fde97
run on all branches
Aug 21, 2024
a5d139e
trigger CI
Aug 21, 2024
82829ad
run on all MRs
Aug 22, 2024
7a8cb82
add column
Aug 22, 2024
d82aa04
Merge remote-tracking branch 'origin/master' into fix_lambda_theory_test
gkronber Aug 22, 2024
b4df50b
Implement the correct hash function.
gkronber Aug 23, 2024
f987d66
Fix upwards update of semantic analysis values.
gkronber Aug 23, 2024
313c5e8
Remove unused code
gkronber Aug 23, 2024
f14229d
Fix check_memo()
gkronber Aug 23, 2024
6b6522e
Fix an issue where enodes are not added to memo.
gkronber Aug 23, 2024
84d2e30
Simplify code
gkronber Aug 23, 2024
7adb07e
Add code to make sure we do not canonicalize vecexpr in memo
gkronber Aug 23, 2024
9b3d0e4
Make sure nodes in dictionaries (memo and pending) are cloned
gkronber Aug 23, 2024
6c7a56a
Use in!() instead of in() for UniqueQueue push!()
gkronber Aug 23, 2024
a4fe7a2
Comment runtime assertions
gkronber Aug 23, 2024
1dc53da
Merge pull request #236 from gkronber/fix_lambda_theory_test
0x0f0f0f Aug 23, 2024
b3bcd83
Merge remote-tracking branch 'origin/ale/3.0' into fix_enode_memo_2
gkronber Aug 24, 2024
d916a0d
Fix function call in in!()
gkronber Aug 24, 2024
d5dce5d
Remove unnecessary copies of VecExpr
gkronber Aug 24, 2024
fbdfc73
Improve add_class_by_op to use a single dictionary lookup
gkronber Aug 24, 2024
f74d552
Removed old commented code.
gkronber Aug 24, 2024
a3ebcb6
Move in!() outside of push!()
gkronber Aug 24, 2024
66ea780
Revert change in UniqueQueue as it does not work with Julia v1.8
gkronber Aug 25, 2024
0b2e6c9
Merge pull request #239 from gkronber/fix_enode_memo_2
0x0f0f0f Sep 3, 2024
7811095
Fix operation
gkronber Sep 10, 2024
8cc9c88
Add missing modify call after updating eclass analysis
gkronber Sep 10, 2024
2653075
Only update eclass analysis if the new analysis != nothing
gkronber Sep 10, 2024
4cb1dc6
Queue update of parents when analysis of eclass is updated (even when…
gkronber Sep 10, 2024
cd064e6
Move statement into bidirection conditional as it is only required fo…
gkronber Sep 10, 2024
f8d82eb
Fix access to ematch buffer elements
gkronber Sep 10, 2024
a6fcdf7
adjust benchmark target
Sep 12, 2024
39b0503
adjust benchmark
Sep 12, 2024
79c1a7b
Merge remote-tracking branch 'origin/master' into ale/3.0
Sep 12, 2024
ab07bde
Merge remote-tracking branch 'origin/master' into 3.0_minor_fixes_and…
Sep 12, 2024
22a10f3
Fix MU-puzzle rules and add more tests from original source.
gkronber Sep 13, 2024
dab995c
Merge pull request #247 from JuliaSymbolics/240_mu_puzzle
0x0f0f0f Sep 15, 2024
a252b32
Add a test case for dynamic rule predicates with where (mentioned in …
gkronber Sep 25, 2024
bce5fa3
Bugfix for new test case
gkronber Sep 25, 2024
3373cb6
Another fix required..
gkronber Sep 25, 2024
081a9e6
Merge pull request #243 from JuliaSymbolics/3.0_minor_fixes_and_impro…
0x0f0f0f Sep 29, 2024
ff76202
Mutable semantic analysis (data) for eclass
gkronber Oct 5, 2024
cd0ab88
Bugfix in diff(x^n, x) rule and prevent folding 0^0 as well as negati…
gkronber Oct 10, 2024
e9aefa6
Merge pull request #250 from JuliaSymbolics/mutable_eclass
0x0f0f0f Oct 10, 2024
5e5e912
Merge branch 'ale/3.0' into fix_broken_cas_tests
gkronber Oct 11, 2024
6814104
Merge pull request #252 from JuliaSymbolics/fix_broken_cas_tests
0x0f0f0f Oct 11, 2024
119e508
make UnionAll matchable as pattern operation
Jan 3, 2025
f0e6b91
retrigger CI
Jan 4, 2025
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 4 additions & 0 deletions NEWS.md
Original file line number Diff line number Diff line change
@@ -1,3 +1,6 @@
# 3.0
- Updated TermInterface to 1.0.1

# 2.0
- No longer dispatch against types, but instead dispatch against objects.
- Faster E-Graph Analysis
Expand All @@ -6,6 +9,7 @@
- New interface for e-graph extraction using `EGraphs.egraph_reconstruct_expression`
- Simplify E-Graph Analysis Interface. Use Symbols or functions for identifying Analyses.
- Remove duplicates in E-Graph analyses data.

## 1.2
- Fixes when printing patterns
- Can pass custom `similarterm` to `SaturationParams` by using `SaturationParams.simterm`.
Expand Down
14 changes: 9 additions & 5 deletions Project.toml
Original file line number Diff line number Diff line change
@@ -1,24 +1,28 @@
name = "Metatheory"
uuid = "e9d8d322-4543-424a-9be4-0cc815abe26c"
authors = ["Alessandro Cheli - 0x0f0f0f <[email protected]>"]
version = "2.0.2"
version = "3.0.0"

[deps]
AutoHashEquals = "15f4f7f2-30c1-5605-9d31-71845cf9641f"
DataStructures = "864edb3b-99cc-5e75-8d2d-829cb0a9cfe8"
DocStringExtensions = "ffbed154-4ef7-542d-bbb7-c09d3a79fcae"
Reexport = "189a3867-3050-52da-a836-e630ba90ab69"
TermInterface = "8ea1fca8-c5ef-4a55-8b96-4e9afe9c9a3c"
TimerOutputs = "a759f4b9-e2f1-59dc-863e-4aeb61b1ea8f"

[weakdeps]
GraphViz = "f526b714-d49f-11e8-06ff-31ed36ee7ee0"

[extensions]
Plotting = ["GraphViz"]

[compat]
AutoHashEquals = "2.1.0"
DataStructures = "0.18"
DocStringExtensions = "0.8, 0.9"
Reexport = "0.2, 1"
TermInterface = "0.3.3"
TermInterface = "2.0"
TimerOutputs = "0.5"
julia = "1.8"
julia = "1.9"

[extras]
Documenter = "e30172f5-a6a5-5a46-863b-614d45cd2de4"
Expand Down
154 changes: 136 additions & 18 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -18,36 +18,154 @@
[![status](https://joss.theoj.org/papers/3266e8a08a75b9be2f194126a9c6f0e9/status.svg)](https://joss.theoj.org/papers/3266e8a08a75b9be2f194126a9c6f0e9)
[![Zulip](https://img.shields.io/badge/Chat-Zulip-blue)](https://julialang.zulipchat.com/#narrow/stream/277860-metatheory.2Ejl)

**Metatheory.jl** is a general purpose term rewriting, metaprogramming and algebraic computation library for the Julia programming language, designed to take advantage of the powerful reflection capabilities to bridge the gap between symbolic mathematics, abstract interpretation, equational reasoning, optimization, composable compiler transforms, and advanced
homoiconic pattern matching features. The core features of Metatheory.jl are a powerful rewrite rule definition language, a vast library of functional combinators for classical term rewriting and an *e-graph rewriting*, a fresh approach to term rewriting achieved through an equality saturation algorithm. Metatheory.jl can manipulate any kind of
Julia symbolic expression type, as long as it satisfies the [TermInterface.jl](https://github.com/JuliaSymbolics/TermInterface.jl).
**Metatheory.jl** is a general purpose term rewriting, metaprogramming and
algebraic computation library for the Julia programming language, designed to
take advantage of the powerful reflection capabilities to bridge the gap between
symbolic mathematics, abstract interpretation, equational reasoning,
optimization, composable compiler transforms, and advanced homoiconic pattern
matching features. The core features of Metatheory.jl are a powerful rewrite
rule definition language, a vast library of functional combinators for classical
term rewriting and an *[e-graph](https://en.wikipedia.org/wiki/E-graph)
rewriting*, a fresh approach to term rewriting achieved through an equality
saturation algorithm. Metatheory.jl can manipulate any kind of Julia symbolic
expression type, as long as it satisfies [TermInterface.jl](https://github.com/JuliaSymbolics/TermInterface.jl).

Metatheory.jl provides:
- An eDSL (domain specific language) to define different kinds of symbolic rewrite rules.
- An eDSL (embedded domain specific language) to define different kinds of symbolic rewrite rules.
- A classical rewriting backend, derived from the [SymbolicUtils.jl](https://github.com/JuliaSymbolics/SymbolicUtils.jl) pattern matcher, supporting associative-commutative rules. It is based on the pattern matcher in the [SICM book](https://mitpress.mit.edu/sites/default/files/titles/content/sicm_edition_2/book.html).
- A flexible library of rewriter combinators.
- An e-graph rewriting (equality saturation) backend and pattern matcher, based on the [egg](https://egraphs-good.github.io/) library, supporting backtracking and non-deterministic term rewriting by using a data structure called *e-graph*, efficiently incorporating the notion of equivalence in order to reduce the amount of user effort required to achieve optimization tasks and equational reasoning.
- An [e-graph](https://en.wikipedia.org/wiki/E-graph) rewriting (equality saturation) engine, based on the [egg](https://egraphs-good.github.io/) library, supporting a backtracking pattern matcher and non-deterministic term rewriting by using a data structure called [e-graph](https://en.wikipedia.org/wiki/E-graph), efficiently incorporating the notion of equivalence in order to reduce the amount of user effort required to achieve optimization tasks and equational reasoning.
- `@capture` macro for flexible metaprogramming.

Intuitively, Metatheory.jl transforms Julia expressions
in other Julia expressions and can achieve such at both compile and run time. This allows Metatheory.jl users to perform customized and composable compiler optimizations specifically tailored to single, arbitrary Julia packages.
in other Julia expressions at both compile and run time.

This allows users to perform customized and composable compiler optimizations specifically tailored to single, arbitrary Julia packages.

Our library provides a simple, algebraically composable interface to help scientists in implementing and reasoning about semantics and all kinds of formal systems, by defining concise rewriting rules in pure, syntactically valid Julia on a high level of abstraction. Our implementation of equality saturation on e-graphs is based on the excellent, state-of-the-art technique implemented in the [egg](https://egraphs-good.github.io/) library, reimplemented in pure Julia.

## 2.0 is out!

Second stable version is out:
## 3.0 Alpha

- [ ] Rewrite integration test files in [Literate.jl](https://github.com/fredrikekre/Literate.jl) format, becoming narrative tutorials available in the docs.
- [ ] Proof production algorithm: explanations.
- [x] Using new TermInterface.
- [x] Performance optimization: use vectors of UInt to internally represent terms in e-graphs.
- [x] Comprehensive suite of benchmarks that are run automatically on PR.
- [x] Complete overhaul of the rebuilding algorithm.

---

## We need your help! - Practical and Research Contributions

There's lot of room for improvement for Metatheory.jl, by making it more performant and by extending its features.
Any contribution is welcome!

**Performance**:
- Improving the speed of the e-graph pattern matcher. [(Useful paper)](https://arxiv.org/abs/2108.02290)
- Reducing allocations used by Equality Saturation.
- [#50](https://github.com/JuliaSymbolics/Metatheory.jl/issues/50) - Goal-informed [rule schedulers](https://github.com/JuliaSymbolics/Metatheory.jl/blob/master/src/EGraphs/Schedulers.jl): develop heuristic algorithms that choose what rules to apply at each equality saturation iteration to prune space of possible rewrites.

**Features**:
- [#111](https://github.com/JuliaSymbolics/Metatheory.jl/issues/111) Introduce proof production capabilities for e-graphs. This can be based on the [egg implementation](https://github.com/egraphs-good/egg/blob/main/src/explain.rs).
- Common Subexpression Elimination when extracting from an e-graph [#158](https://github.com/JuliaSymbolics/Metatheory.jl/issues/158)
- Integer Linear Programming extraction of expressions.
- Pattern matcher enhancements: [#43 Better parsing of blocks](https://github.com/JuliaSymbolics/Metatheory.jl/issues/43), [#3 Support `...` variables in e-graphs](https://github.com/JuliaSymbolics/Metatheory.jl/issues/3), [#89 syntax for vectors](https://github.com/JuliaSymbolics/Metatheory.jl/issues/89)
- [#75 E-Graph intersection algorithm](https://github.com/JuliaSymbolics/Metatheory.jl/issues/75)

**Documentation**:
- Port more [integration tests](https://github.com/JuliaSymbolics/Metatheory.jl/tree/master/test/integration) to [tutorials](https://github.com/JuliaSymbolics/Metatheory.jl/tree/master/test/tutorials) that are rendered with [Literate.jl](https://github.com/fredrikekre/Literate.jl)
- Document [Functional Rewrite Combinators](https://github.com/JuliaSymbolics/Metatheory.jl/blob/master/src/Rewriters.jl) and add a tutorial.

## Real World Applications

Most importantly, there are many **practical real world applications** where Metatheory.jl could be used. Let's
work together to turn this list into some new Julia packages:


#### Integration with Symbolics.jl

Many features of this package, such as the classical rewriting system, have been ported from [SymbolicUtils.jl](https://github.com/JuliaSymbolics/SymbolicUtils.jl), and are technically the same. Integration between Metatheory.jl with Symbolics.jl **is currently
in-development**, as we recently released a new version of [TermInterface.jl](https://github.com/JuliaSymbolics/TermInterface.jl).

An integration between Metatheory.jl and [Symbolics.jl](https://github.com/JuliaSymbolics/Symbolics.jl) is possible and has previously been shown in the ["High-performance symbolic-numerics via multiple dispatch"](https://arxiv.org/abs/2105.03949) paper. Once we reach consensus for a shared symbolic term interface, Metatheory.jl can be used to:

- Rewrite Symbolics.jl expressions with **bi-directional equations** instead of simple directed rewrite rules.
- Search for the space of mathematically equivalent Symbolics.jl expressions for more computationally efficient forms to speed various packages like [ModelingToolkit.jl](https://github.com/SciML/ModelingToolkit.jl) that numerically evaluate Symbolics.jl expressions.
- When proof production is introduced in Metatheory.jl, automatically search the space of a domain-specific equational theory to prove that Symbolics.jl expressions are equal in that theory.
- Other scientific domains extending Symbolics.jl for system modeling.

#### Simplifying Quantum Algebras

[QuantumCumulants.jl](https://github.com/qojulia/QuantumCumulants.jl/) automates
the symbolic derivation of mean-field equations in quantum mechanics, expanding
them in cumulants and generating numerical solutions using state-of-the-art
solvers like [ModelingToolkit.jl](https://github.com/SciML/ModelingToolkit.jl)
and
[DifferentialEquations.jl](https://github.com/SciML/DifferentialEquations.jl). A
potential application for Metatheory.jl is domain-specific code optimization for
QuantumCumulants.jl, aiming to be the first symbolic simplification engine for
Fock algebras.


- New e-graph pattern matching system, relies on functional programming and closures, and is much more extensible than 1.0's virtual machine.
- No longer dispatch against types, but instead dispatch against objects.
- Faster E-Graph Analysis
- Better library macros
- Updated TermInterface to 0.3.3
- New interface for e-graph extraction using `EGraphs.egraph_reconstruct_expression`
- Simplify E-Graph Analysis Interface. Use Symbols or functions for identifying Analyses.
- Remove duplicates in E-Graph analyses data.
#### Automatic Floating Point Error Fixer


Many features have been ported from SymbolicUtils.jl. Metatheory.jl can be used in place of SymbolicUtils.jl when you have no need of manipulating mathematical expressions. The introduction of [TermInterface.jl](https://github.com/JuliaSymbolics/TermInterface.jl) has allowed for large potential in generalization of term rewriting and symbolic analysis and manipulation features. Integration between Metatheory.jl with Symbolics.jl, as it has been shown in the ["High-performance symbolic-numerics via multiple dispatch"](https://arxiv.org/abs/2105.03949) paper.
[Herbie](https://herbie.uwplse.org/) is a tool using equality saturation to automatically rewrites mathematical expressions to enhance
floating-point accuracy. Recently, Herbie's core has been rewritten using
[egg](https://egraphs-good.github.io/), with the tool originally implemented in
a mix of Racket, Scheme, and Rust. While effective, its usage involves multiple
languages, making it impractical for non-experts. The text suggests the theoretical
possibility of porting this technique to a pure Julia solution, seamlessly
integrating with the language, in a single macro `@fp_optimize` that fixes
floating-point errors in expressions just before code compilation and execution.

#### Automatic Theorem Proving in Julia

Metatheory.jl can be used to make a pure Julia Automated Theorem Prover (ATP)
inspired by the use of E-graphs in existing ATP environments like
[Z3](https://github.com/Z3Prover/z3), [Simplify](https://dl.acm.org/doi/10.1145/1066100.1066102) and [CVC4](https://en.wikipedia.org/wiki/CVC4),
in the context of [Satisfiability Modulo Theories (SMT)](https://en.wikipedia.org/wiki/Satisfiability_modulo_theories).

The two-language problem in program verification can be addressed by allowing users to define high-level
theories about their code, that are statically verified before executing the program. This holds potential for various applications in
software verification, offering a flexible and generic environment for proving
formulae in different logics, and statically verifying such constraints on Julia
code before it gets compiled (see
[Mixtape.jl](https://github.com/JuliaCompilerPlugins/Mixtape.jl)).

To develop such a package, Metatheory.jl needs:

- Introduction of Proof Production in equality saturation.
- SMT in conjunction with a SAT solver like [PicoSAT.jl](https://github.com/sisl/PicoSAT.jl)
- Experiments with various logic theories and software verification applications.

#### Other potential applications

Many projects that could potentially be ported to Julia are listed on the [egg website](https://egraphs-good.github.io/).
A simple search for ["equality saturation" on Google Scholar](https://scholar.google.com/scholar?hl=en&q="equality+saturation") shows many new articles that leverage the techniques used in this packages.

PLDI is a premier academic forum in the field of programming languages and programming systems research, which organizes an [e-graph symposium](https://pldi23.sigplan.org/home/egraphs-2023) where many interesting research and projects have been presented.

---

## Theoretical Developments

There's also lots of room for theoretical improvements to the e-graph data structure and equality saturation rewriting.

#### Associative-Commutative-Distributive e-matching

In classical rewriting SymbolicUtils.jl offers a mechanism for matching expressions with associative and commutative operations: [`@acrule`](https://docs.sciml.ai/SymbolicUtils/stable/manual/rewrite/#Associative-Commutative-Rules) - a special kind of rule that considers all permutations and combinations of arguments. In e-graph rewriting in Metatheory.jl, associativity and commutativity have to be explicitly defined as rules. However, the presence of such rules, together with distributivity, will likely cause equality saturation to loop infinitely. See ["Why reasonable rules can create infinite loops"](https://github.com/egraphs-good/egg/discussions/60) for an explanation.

Some workaround exists for ensuring termination of equality saturation: bounding the depth of search, or merge-only rewriting without introducing new terms (see ["Ensuring the Termination of EqSat over a Terminating Term Rewriting System"](https://effect.systems/blog/ta-completion.html)).

There's a few theoretical questions left:

- **What kind of rewrite systems terminate in equality saturation**?
- Can associative-commutative matching be applied efficiently to e-graphs while avoiding combinatory explosion?
- Can e-graphs be extended to include nodes with special algebraic properties, in order to mitigate the downsides of non-terminating systems?

---

## Recommended Readings - Selected Publications

Expand All @@ -72,7 +190,7 @@ You can install the stable version:
julia> using Pkg; Pkg.add("Metatheory")
```

Or you can install the developer version (recommended by now for latest bugfixes)
Or you can install the development version (recommended by now for latest bugfixes)
```julia
julia> using Pkg; Pkg.add(url="https://github.com/JuliaSymbolics/Metatheory.jl")
```
Expand Down
1 change: 1 addition & 0 deletions benchmark/tune.json
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
[{"Julia":"1.9.4","BenchmarkTools":"1.0.0"},[["BenchmarkGroup",{"data":{"logic":["BenchmarkGroup",{"data":{"prove1":["Parameters",{"gctrial":true,"time_tolerance":0.05,"evals_set":false,"samples":10000,"evals":1,"gcsample":false,"seconds":5.0,"overhead":0.0,"memory_tolerance":0.01}],"rewrite":["Parameters",{"gctrial":true,"time_tolerance":0.05,"evals_set":false,"samples":10000,"evals":1,"gcsample":false,"seconds":5.0,"overhead":0.0,"memory_tolerance":0.01}]},"tags":["egraph","logic"]}],"maths":["BenchmarkGroup",{"data":{"simpl1":["Parameters",{"gctrial":true,"time_tolerance":0.05,"evals_set":false,"samples":10000,"evals":1,"gcsample":false,"seconds":5.0,"overhead":0.0,"memory_tolerance":0.01}]},"tags":["egraphs"]}]},"tags":[]}]]]
1 change: 1 addition & 0 deletions docs/Project.toml
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
[deps]
Documenter = "e30172f5-a6a5-5a46-863b-614d45cd2de4"
Literate = "98b081ad-f1c9-55d3-8b20-4c87d4299306"
LiveServer = "16fef848-5104-11e9-1b77-fb7a48bbb589"
Metatheory = "e9d8d322-4543-424a-9be4-0cc815abe26c"
TermInterface = "8ea1fca8-c5ef-4a55-8b96-4e9afe9c9a3c"

Expand Down
27 changes: 27 additions & 0 deletions docs/liveserver.jl
Original file line number Diff line number Diff line change
@@ -0,0 +1,27 @@
#!/usr/bin/env julia

# Root of the repository
const repo_root = dirname(@__DIR__)

# Make sure docs environment is active
import Pkg
Pkg.activate(@__DIR__)
using Metatheory

# Communicate with docs/make.jl that we are running in live mode
push!(ARGS, "liveserver")

# Run LiveServer.servedocs(...)
import LiveServer
LiveServer.servedocs(;
# Documentation root where make.jl and src/ are located
foldername = joinpath(repo_root, "docs"),
skip_dirs = [
# exclude assets folder because it is modified by docs/make.jl
joinpath(repo_root, "docs", "src", "assets"),
# exclude tutorial .md files (auto-generated via Literate.jl)
abspath(joinpath(@__DIR__, "src", "tutorials"))
],
# include tutorial .jl files (generate .md files)
include_dirs=[joinpath(dirname(pathof(Metatheory)), "..", "test", "tutorials")]
)
20 changes: 11 additions & 9 deletions docs/src/api.md
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
# API Documentation


```
## Syntax

```@autodocs
Expand All @@ -25,26 +25,28 @@ Modules = [Metatheory.Rules]

---

## Rules
## Rewriters

```@autodocs
Modules = [Metatheory.Rules]
Modules = [Metatheory.Rewriters]
```

---

## Rewriters
## EGraphs

```@autodocs
Modules = [Metatheory.Rewriters]
Modules = [Metatheory.EGraphs]
```

---
## VecExprs (aka e-nodes)

## EGraphs
```@docs
Metatheory.VecExprModule.VecExpr
```

```@autodocs
Modules = [Metatheory.EGraphs]
Modules = [Metatheory.VecExprModule]
```

---
Expand All @@ -53,4 +55,4 @@ Modules = [Metatheory.EGraphs]

```@autodocs
Modules = [Metatheory.EGraphs.Schedulers]
```
```
Loading
Loading