perf: update to cadical 2.2.0 #7942
Draft
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
|
Mathlib CI status (docs):
|
|
!bench |
|
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. |
|
Here are the benchmark results for commit 65cb246. |
|
This seems to be an actual cadical bug. |
65cb246 to
ea4259c
Compare
|
Narrator: It was in fact not a cadical bug |
|
!bench |
|
Here are the benchmark results for commit ea4259c. 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_mo
9111
d 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 σ) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
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.smt2from 5:20 to 2:41.TODO: