4012 evaluate pattern pruning - #4020

Open

geo2a wants to merge 14 commits into

4012-evaluate-pattern-pruning

Commits on Aug 21, 2024

Derive Show for SMT result types
geo2a
committed
a313ce8
Check consistency of the pattern's constraints before evaluating it
geo2a
committed
0c0e203
Check pattern consistency before starting rewriting in `"execute"`
geo2a
committed
5999a66
Fix frontend warning in collectiontest.k
geo2a
committed
2f75bc2
Invert `--no-fallback-simplify` and `--no-post-exec-simplify` (new default: no simplification)

jberthold
authored and
geo2a
committed
0de9517
Update integration tests
geo2a
committed
41e93b1
Correct typos and test description
geo2a
committed
2359ddc
Make Z3 call optional in evaluatePattern
geo2a
committed
998eb07
Fix unit tests
geo2a
committed
598a00c
Don't check initial constraints when "assume-state-defined"
geo2a
committed
9c07a05
Rename "assume-state-define" to "assume-defined"
geo2a
committed
39e6abc
Return vacuous on undefined concrete terms
geo2a
committed
df4cfae
Rename parameter in integration tests
geo2a
committed
e155e58
Reorganize tests
geo2a
committed
586589f