Skip to content

Make literal picker independent of theory explanation order - #14

Merged
dewert99 merged 8 commits into
mainfrom
detirministic
Mar 20, 2024
Merged

dewert99 merged 8 commits into
mainfrom
detirministic

Conversation

@dewert99

Copy link
Copy Markdown
Owner

While working on #11 I noticed that some of the performance changes were caused by differences in the literal picking order which themselves were cause by the explanations having different orders (even though they were always the same set). For this PR I modified batsat's literal picker to ignore the explanation order so that #11 could be better compared.

@codspeed

codspeed Bot commented Mar 14, 2024

Copy link
Copy Markdown

CodSpeed Performance Report

Merging #14 will degrade performances by 29.75%

Comparing detirministic (6a184d4) with main (c12dce5)

Summary

⚡ 13 improvements
❌ 6 (👁 6) regressions
✅ 61 untouched benchmarks

Benchmarks breakdown

Benchmark main detirministic Change
benches/starexec/incremental/QF_UF/2018-Goel-hwbench/QF_UF_brp.5.prop1_ab_core_max.smt2 559.1 ms 469.4 ms +19.11%
👁 benches/starexec/incremental/QF_UF/2018-Goel-hwbench/QF_UF_brp.6.prop1_ab_min_max.smt2 326.1 ms 464.3 ms -29.75%
benches/starexec/incremental/QF_UF/2018-Goel-hwbench/QF_UF_brp2.4.prop2_ab_min_max.smt2 423.7 ms 384.3 ms +10.25%
benches/starexec/incremental/QF_UF/2018-Goel-hwbench/QF_UF_cambridge.6.prop2_ab_min_max.smt2 1.4 s 1.1 s +18.84%
benches/starexec/incremental/QF_UF/2018-Goel-hwbench/QF_UF_elevator.3.prop1_ab_core_max.smt2 109.6 ms 91.4 ms +19.89%
benches/starexec/incremental/QF_UF/2018-Goel-hwbench/QF_UF_gear.1.prop3_ab_core_max.smt2 2.5 s 1.3 s +85.32%
benches/starexec/incremental/QF_UF/2018-Goel-hwbench/QF_UF_gear.1.prop4_ab_core_max.smt2 1,330.6 ms 959.6 ms +38.67%
👁 benches/starexec/incremental/QF_UF/2018-Goel-hwbench/QF_UF_lamport.3.prop1_ab_min_max.smt2 290.7 ms 329.5 ms -11.77%
👁 benches/starexec/incremental/QF_UF/2018-Goel-hwbench/QF_UF_leader_election.2.prop1_ab_min_max.smt2 702.9 ms 871.7 ms -19.36%
👁 benches/starexec/incremental/QF_UF/2018-Goel-hwbench/QF_UF_leader_election.5.prop1_ab_min_max.smt2 813.4 ms 1,020.7 ms -20.31%
benches/starexec/incremental/QF_UF/2018-Goel-hwbench/QF_UF_msmie.4.prop1_ab_core_max.smt2 1.8 s 1 s +82.39%
benches/starexec/incremental/QF_UF/2018-Goel-hwbench/QF_UF_pgm_protocol.2.prop1_ab_core_max.smt2 2.1 s 1.1 s +95.84%
👁 benches/starexec/incremental/QF_UF/2018-Goel-hwbench/QF_UF_pgm_protocol.7.prop5_ab_min_max.smt2 525 ms 657.7 ms -20.17%
👁 benches/starexec/incremental/QF_UF/2018-Goel-hwbench/QF_UF_pgm_protocol.8.prop1_ab_min_max.smt2 955.8 ms 1,221.5 ms -21.76%
benches/starexec/incremental/QF_UF/2018-Goel-hwbench/QF_UF_plc.4.prop2_ab_core_max.smt2 20.5 s 1.6 s ×13
benches/starexec/incremental/QF_UF/2018-Goel-hwbench/QF_UF_rether.2.prop1_ab_core_max.smt2 1,012.5 ms 390.3 ms ×2.6
benches/starexec/incremental/QF_UF/2018-Goel-hwbench/QF_UF_telephony.1.prop1_ab_core_max.smt2 1,018.9 ms 608.5 ms +67.45%
benches/starexec/incremental/QF_UF/2018-Goel-hwbench/QF_UF_telephony.7.prop1_ab_core_max.smt2 2.7 s 1.2 s ×2.2
benches/starexec/incremental/QF_UF/2018-Goel-hwbench/QF_UF_train-gate.5.prop1_ab_core_max.smt2 711.3 ms 458.2 ms +55.24%

@dewert99
dewert99 merged commit dedff0a into main Mar 20, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant