3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-12 03:45:38 +00:00
Commit graph

7 commits

Author SHA1 Message Date
Nikolaj Bjorner
195f3c9110 update build dependencies 2025-07-07 16:50:35 +02:00
Nikolaj Bjorner
1b3c3c2716 initial pattern abstraction and move matching to src 2025-07-06 00:53:46 -07:00
Nikolaj Bjorner
644118660f list euf dependency in api cmakefile
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-05-07 15:47:03 -07:00
Nikolaj Bjorner
b52fd8d954 add EUF plugin framework.
plugin setting allows adding equality saturation within the E-graph propagation without involving externalizing theory solver dispatch. It makes equality saturation independent of SAT integration.
Add a special relation operator to support ad-hoc AC symbols.
2023-11-30 13:58:30 -08:00
Nikolaj Bjorner
4b6d7ca097 working on mam 2021-01-25 17:54:53 -08:00
Nikolaj Bjorner
680b185872 adding ematching engine, fixing seq_unicode 2021-01-22 17:10:45 -08:00
Nikolaj Bjorner
65e6d942ac euf
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-08-24 01:55:13 -07:00