v1.2.1

Metatheory v1.2.1

Diff since v1.2.0

• Fixed application of DynamicRules in egraph rewriting

v1.2.0

Metatheory v1.2.0

Diff since v1.1.0

• Fixes when printing patterns
• Can pass custom similarterm to SaturationParams by using SaturationParams.simterm.

v1.1.0

Metatheory v1.1.0

Diff since v1.0.0

• Fixes for SymbolicUtils integration
• Egraph pattern matcher can now match against symbol and function objects at the same time

Closed issues:

• AC Rules/Loop Prevention for MatchCore rewriting backend (#9)
• Document analyses and AbstractAnalysis (#16)
• Knuth-Bendix Completion for Classical Backend (#35)
• How to write your own Analysis/Scheduler tutorials (#42)
• UPDATE DOCUMENTATION (#67)
• Full compatibility of rules syntax with SymbolicUtils.jl rule syntax (#68)
• Symbolics rules macro is broken (#79)
• Downstream CI (#81)

Merged pull requests:

• Fixes for Symbolics (#80) (@shashi)

v1.0.0

Metatheory v1.0.0

Diff since v0.6.0

Metatheory.jl + SymbolicUtils.jl = ❤️

• Metatheory.jl now supports the same syntax as SymbolicUtils.jl for the rule definition DSL!
• The classical pattern matcher has been redesigned, and it is a port of SymbolicUtils.jl's pattern matcher. Now Metatheory.jl can be used in place of SU's rewriting backend.
• Performance improvements: caching of ground terms when doing e-matching in equality saturation.
• Dynamic Rules do not use RuntimeGeneratedFunctions when not needed.
• Improved manual.
• Removed @metatheory_init
• Rules now support type and function predicates as in SymbolicUtils.jl
• Redesigned the library
• Introduced @timerewrite to time the execution of classical rewriting systems.

Closed issues:

• Is @metatheory_init really needed? (#45)
• Experiment conditional rules (#52)
• Move over repository to JuliaSymbolics (#76)

Merged pull requests:

• [WIP] Import and unify the rule syntax and classical pattern matching system from SymbolicUtils.jl (#77) (@0x0f0f0f)
• Broken links due to move to JuliaSymbolics (#78) (@jlperla)

v0.6.0

Metatheory v0.6.0

Diff since v0.5.0

• Faster e-matching! 🚀
• Updated TermInterface.jl and pattern matchers to support exprhead.

Closed issues:

• Match on :: and ... (and optionally where) without triggering special ematching functions. (#12)
• @when macro for conditional dynamic rules (#26)
• Metatheory incorrectly merges e-classes? (#74)

Merged pull requests:

• Improve pattern display. (#73) (@MrVPlusOne)

v0.5.0

Metatheory v0.5.0

Diff since v0.4.1

• Goodbye MatchCore.jl, welcome Rewriters.jl. One can now define rewrite strategies as in SymbolicUtils.jl
• Rule-by-Rule timing reports like in SymbolicUtils thanks to TimerOutputs.jl
• No more global ematching cache. Rule objects now contain their own cache.
• Rules are callable functions!
• No more confusing passing of modules around functions. Everything runs in its definition module (static scoping).
• Rule is now AbstractRule.
• Tests now reside each one in its own module
• Various fixes and speedups, fixed parallelism thanks to @MrVPlusOne .
• Refactoring and cleaner codebase.
• Updated some dependencies, mostly TermInterface.jl.
• Temporary hack: If you have custom expression types where TermInterface.operation(x::MyType) is not a :call, you can still match on :call by setting Metatheory.iscall(x::MyType) = true. Defaults to false. This needs to be revised.

Closed issues:

• Use TimerOutputs.jl (#65)
• Use SafeTestsets.jl (#66)

Merged pull requests:

• Rename patterns.jl to pattern.jl for dev on case insensitive filesystems (#63) (@gpeairs)
• Fix equality saturation when threaded=true. Improve search performance. (#70) (@MrVPlusOne)
• Fix inform! for ScoredScheduler. (#71) (@MrVPlusOne)

v0.4.1

Metatheory v0.4.1

Diff since v0.4.0

Dollar interpolation in @theory macro. Initial support for TermInterface.jl package

Closed issues:

• interpolation of objects in theory macro with $ (#62)

v0.4.0

Metatheory v0.4.0

Diff since v0.3.2

Completely renewed the pattern matcher! MT is now dozens of times faster than before. Added reports about equality saturation results, many more parameters, improved schedulers. Completely changed the metadata system. Added a new interface for rewriting on custom types, and added a custom interface for building patterns and rules programmatically.

Closed issues:

• Optimize the E-Graph Pattern Matcher (#6)
• Use a Term-like interface instead of Expr (#18)
• Testing Rule eqivalence with == (#30)
• A custom type for specifying goals (#47)
• Bugs when function calls have no arguments (#54)
• Parametrize the metadata field type in ENodes. (#56)
• Using the interface to work on Syms (presumably correctly) gives wrong answers (#58)
• overlap with symbolics.jl? (#61)

Merged pull requests:

• Examples of the ZX-calculus (#55) (@ChenZhao44)
• Changed eval to resolve in pattern syntax. (#57) (@femtomc)

v0.3.2

0.3.2 release

v0.3.1

Metatheory v0.3.1

Diff since v0.3.0