Henrik Böving d24dfa1031 perf: add a cache to bv_decide's reflection procedure (#7644) ... This PR adds a cache to the reflection procedure of bv_decide. This was motivated by the following profile on QF_BV SMTLIB problem `sage/app12/bench_3564.smt2`: https://share.firefox.dev/4iTG8KX. After this change we roughly get a 10x speedup and `simp` is the bottleneck again: https://share.firefox.dev/4iuezYT		2025-03-23 13:56:00 +00:00
..
bin	feat: API to avoid deadlocks from dropped promises (#6958)	2025-02-07 15:33:10 +00:00
cmake	fix: Windows stage0 linking (#6622)	2025-01-14 09:09:50 +01:00
include/lean	feat: socket support using LibUV (#6683)	2025-03-19 13:54:51 +00:00
Init	feat: model-based theory combination in grind (#7641)	2025-03-23 04:06:09 +00:00
initialize	fix: explicitly initialize Std in lean_initialize (#4668)	2024-07-06 13:17:30 +00:00
kernel	fix: bv_omega to use -implicitDefEqProofs (#7387)	2025-03-09 00:13:14 +00:00
lake	refactor: lake: unified configuration (#7504)	2025-03-23 02:49:57 +00:00
Lean	perf: add a cache to bv_decide's reflection procedure (#7644)	2025-03-23 13:56:00 +00:00
library	chore: fix interpreter lean_assert	2025-03-21 09:38:50 +01:00
runtime	chore: revert "perf: avoid taking mutex on task deactivation" (#7590)	2025-03-20 07:04:50 +00:00
shell	chore: avoid rebuilding leanmanifest in each build (#5057)	2024-08-15 14:55:36 +00:00
Std	perf: bv_decide don't drop the expression level cache (#7636)	2025-03-23 13:05:01 +00:00
util	perf: remove most remaining async blockers in Init.Data.List.Sublist (#7500)	2025-03-15 15:26:06 +00:00
cadical.mk	feat: ship cadical (#4325)	2024-08-23 09:13:27 +00:00
CMakeLists.txt	chore: CI: USE_LAKE secondary build job (#7505)	2025-03-20 12:16:53 +00:00
config.h.in
githash.h.in
Init.lean	feat: allow async elab tasks to contribute to info trees reported to linters and request handlers (#7457)	2025-03-13 15:09:00 +00:00
lakefile.toml.in	chore: lake: revert use of Lake plugin (#7608)	2025-03-21 00:59:43 +00:00
lean-toolchain
Lean.lean	feat: use realizeConst for all equation, unfold, induction, and partial fixpoint theorems (#7261)	2025-03-06 15:38:04 +00:00
lean.mk.in	chore: USE_LAKE: integrate into CMake (#4466)	2025-03-15 08:58:01 +00:00
Leanc.lean	feat: expose flags for the bundled C compiler (#4477)	2024-06-22 01:23:33 +00:00
Std.lean	feat: Std.Net.Addr (#6563)	2025-01-09 09:33:03 +00:00
stdlib.make.in	chore: lake: revert use of Lake plugin (#7608)	2025-03-21 00:59:43 +00:00
stdlib_flags.h	chore: remove comment from src/stdlib_flags.h (#7531)	2025-03-17 18:07:58 +00:00
version.h.in	feat: language reference links and examples in docstrings (#7240)	2025-03-12 09:17:27 +00:00