Existential matching of simplification side conditions - #3942

Closed

geo2a wants to merge 9 commits into

georgy/existential-requires

Commits on Jun 14, 2024

Add `RewriteRule "ExistentialSimplifications"`
geo2a
committed
2a3cbad

Commits on Jun 15, 2024

Add simple matching for predicates with existentials
geo2a
committed
74eb49e
Draft existential side-condition heuristic
geo2a
committed
bf5f466

Commits on Jul 16, 2024

Merge remote-tracking branch 'origin/master' into georgy/existential-requires
geo2a
committed
6afcce0
Add LtInt
geo2a
committed
d5155bd
Fix LLVM integration tests
geo2a
committed
cc18b99

Commits on Jul 17, 2024

Add instantiateExistentialsMany, use in applyEquation
geo2a
committed
400d5b8
Add a test applying an existential simplifications
geo2a
committed
43e5d45
Internalise equations with existentials in requires
geo2a
committed
f957048