Leonardo de Moura
|
c5314da28e
|
feat: add helper theorems for handling offsets in grind (#6584)
This PR adds helper theorems to implement offset constraints in grind.
|
2025-01-09 01:32:49 +00:00 |
|
Leonardo de Moura
|
6a839796fd
|
feat: add grind tactic (#6459)
This PR adds the (WIP) `grind` tactic. It currently generates a warning
message to make it clear that the tactic is not ready for production.
|
2024-12-27 03:48:01 +00:00 |
|
Leonardo de Moura
|
3cddae6492
|
feat: support for builtin grind propagators (#6448)
This PR declares the command `builtin_grind_propagator` for registering
equation propagator for `grind`. It also declares the auxiliary the
attribute.
|
2024-12-25 22:55:39 +00:00 |
|
Leonardo de Moura
|
ff37e5d512
|
feat: add grind core module (#4249)
|
2024-05-22 03:50:36 +00:00 |
|
Leonardo de Moura
|
f53b778c0d
|
feat: improve grind preprocessor (#4221)
|
2024-05-20 04:29:49 +00:00 |
|
Leonardo de Moura
|
d0e34aaed5
|
feat: add revertAll tactic for grind (#4167)
|
2024-05-14 23:22:54 +00:00 |
|
Leonardo de Moura
|
f3538dbdfa
|
feat: grind normalization theorems (#4164)
|
2024-05-14 19:19:38 +00:00 |
|