perf: update to cadical 2.2.0

[hargoniX]

This PR updates to Cadical 2.2.0.

We are particularly interested in this release as it implements congruence closure which alleviates the need to detect and encode XOR and ITE specially ourselves. Preliminary tests on a few SMTLIB problems show significant speedups here, for example Sage2/bench_8517.smt2 from 5:20 to 2:41.

TODO:

• Wait for an actual release
• Upgrade Nix dependency
• Evaluate on our benchmarks
• Evaluate on SMTLIB

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 069456ea9ca3971dbff7d11b5389f1ceeaf996b9 --onto deef1c2739a331899b0e536312e65e9815059014. You can force Mathlib CI using the force-mathlib-ci label. (2025-04-13 12:36:44)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 525fd2697c879c0144e5668c51aee11d1970346c --onto 020b8834c3e06da1cd1682431b6fa8d52206c8ec. You can force Mathlib CI using the force-mathlib-ci label. (2025-04-16 19:30:37)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e97c1505f05f12fefde0590106ab7e8241743a75 --onto a106ea053fec080a50204b0ad6dadc69bc3f0937. You can force Mathlib CI using the force-mathlib-ci label. (2025-11-20 23:49:05)

[hargoniX]

!bench

[hargoniX]

I don't know for sure if in this setup we already use the new cadical on the bench infra but let's see what happens.

[leanprover-bot]

Here are the benchmark results for commit 65cb246.
The entire run failed.
Found no significant differences.

[hargoniX]

This seems to be an actual cadical bug.

[hargoniX]

Narrator: It was in fact not a cadical bug

[hargoniX]

!bench

[leanprover-bot]

Here are the benchmark results for commit ea4259c.
There were significant changes against commit 525fd26:

  Benchmark                   Metric                  Change
  ======================================================================
- bv_decide_inequality.lean   branches                179.7%  (1567.5 σ)
- bv_decide_inequality.lean   instructions            197.5%  (1779.3 σ)
- bv_decide_inequality.lean   maxrss                  125.3%    (73.1 σ)
- bv_decide_inequality.lean   task-clock              236.4%    (40.4 σ)
- bv_decide_inequality.lean   wall-clock              232.6%    (39.8 σ)
- bv_decide_large_aig.lean    branches                  2.2%    (68.9 σ)
- bv_decide_large_aig.lean    instructions              2.4%    (84.9 σ)
+ bv_decide_mod               branches                -22.2%  (-322.7 σ)
+ bv_decide_mod               instructions            -23.3%  (-348.0 σ)
+ bv_decide_mod               maxrss                  -14.3%  (-153.1 σ)
+ bv_decide_mod               task-clock              -26.9%   (-33.9 σ)
+ bv_decide_mod               wall-clock              -26.9%   (-32.5 σ)
- bv_decide_mul               branches                  5.2%    (69.7 σ)
- bv_decide_mul               instructions              5.5%    (71.5 σ)
+ bv_decide_realworld         branches                -20.5% (-2307.8 σ)
+ bv_decide_realworld         instructions            -20.7% (-2046.9 σ)
+ bv_decide_realworld         task-clock              -17.2%   (-17.3 σ)
+ bv_decide_realworld         wall-clock               -9.6%   (-10.9 σ)
- channel.lean                bounded0_spsc             2.0%    (18.9 σ)
+ channel.lean                maxrss                  -15.0%   (-32.1 σ)
- ilean roundtrip             parse                     8.7%    (10.0 σ)
- ilean roundtrip             task-clock                3.2%    (16.9 σ)
- ilean roundtrip             wall-clock                3.2%    (16.7 σ)
+ liasolver                   maxrss                   -3.5%   (-10.2 σ)
+ nat_repr                    maxrss                   -3.5%   (-10.2 σ)
+ parser                      maxrss                   -3.5%   (-10.2 σ)
+ qsort                       maxrss                   -3.5%   (-10.2 σ)
- stdlib                      attribute application     2.9%    (14.9 σ)
- stdlib                      blocked                   3.6%   (160.1 σ)
- stdlib                      blocked (unaccounted)     3.7%    (16.9 σ)
- stdlib                      dsimp                     2.3%    (20.6 σ)
- stdlib                      task-clock                2.6%    (16.6 σ)
- stdlib                      type checking             3.0%    (49.5 σ)

[hargoniX]

!radar

[leanprover-radar]

Benchmark results for 8cf7053 against e97c150 are in! @hargoniX

Major changes (5)

• bv_decide_inequality.lean//instructions changed by +213.5% (🟥).
• bv_decide_large_aig.lean//instructions changed by +1.1% (🟥).
• bv_decide_mod//instructions changed by -29.3% (✅).
• bv_decide_mul//instructions changed by +11.2% (🟥).
• bv_decide_realworld//instructions changed by -25.8% (✅).

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase e97c1505f05f12fefde0590106ab7e8241743a75 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-11-20 23:49:06)