Leonardo de Moura dd3652ecdc feat: cutsat preparations (#7097) ... This PR implements several modifications for the cutsat procedure in `grind`. - The maximal variable is now at the beginning of linear polynomials. - The old `LinearArith.Solver` was deleted, and the normalizer was moved to `Simp`. - cutsat first files were created, and basic infrastructure for representing divisibility constraints was added.		2025-02-16 02:52:14 +00:00
..
Arith	feat: cutsat preparations (#7097)	2025-02-16 02:52:14 +00:00
BuiltinSimprocs	feat: make BitVec.getElem the simp normal form and use it in ext (#5498)	2025-02-16 00:04:56 +00:00
Arith.lean	feat: cutsat preparations (#7097)	2025-02-16 02:52:14 +00:00
Attr.lean	refactor: mark the Simp.Context constructor as private	2024-11-13 14:12:55 +11:00
BuiltinSimprocs.lean	feat: simprocs for #[1,2,3,4,5][2] (#4765)	2024-07-17 03:05:17 +00:00
Diagnostics.lean	fix: add workaround for MessageData limitations (#6669)	2025-01-16 16:58:20 +00:00
Main.lean	feat: binderNameHint in congr (#7053)	2025-02-13 09:38:42 +00:00
RegisterCommand.lean	feat: attribute [simp ←] (#5870)	2024-10-29 11:07:08 +00:00
Rewrite.lean	feat: cutsat preparations (#7097)	2025-02-16 02:52:14 +00:00
SimpAll.lean	chore: avoid runtime array bounds checks (#6134)	2024-11-21 05:04:52 +00:00
SimpCongrTheorems.lean	feat: make it possible to use dot notation in m! strings (#5857)	2024-10-27 22:55:29 +00:00
Simproc.lean	fix: isDefEq, whnf, simp caching and configuration (#6053)	2024-11-18 01:17:26 +00:00
SimpTheorems.lean	refactor: simpMatch to not etaStruct (#6901)	2025-02-01 19:04:05 +00:00
Types.lean	chore: simp_arith has been deprecated (#7043)	2025-02-12 03:55:45 +00:00