Skip to content

Derived/non-competing solver presentation #204

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Closed
wintered wants to merge 61 commits into from
Closed

Derived/non-competing solver presentation #204

wintered wants to merge 61 commits into from

Conversation

@wintered
Copy link
Contributor

@wintered wintered commented Jul 30, 2025

No description provided.

Martin Jonáš and others added 26 commits July 6, 2025 08:40
Add generation of parallel benchmarks and test runs.
90cd20d
Do not use walltime killer anymore.
5452dd7
Use --continue-after-unknown.
bca1f08
Better status reporting.
6258316
Show contacts only of competitive solvers.
c635d8e
Generate more meaningful YML names.
680a97a
Update removed benchmarks.
ce5b4e7
Remove benchmarks also for non-AWS tracks.
e12e8a1
Revert "Do not use walltime killer anymore."
0402477 
This reverts commit 5452dd7.
Parse the single query/incremental results without scramble_id.
8800f20
@mpreiner
bitwuzla: Change options for parallel track. (#201)
b7c46ac 
* bitwuzla: Change options for parallel track.

Add additional configurations for lower CPU core counts.

* Make additional configurations non-competitive.
@zmylinxi99
submission: add additional configurations for lower CPU core counts. (#…
4fddcda 
…202)
Remove unused AWS infrastructure.
dde119e
fix: Use LazyFrame during selection of incremental benchmarks.
2c57e14
feat: Do not declare required machines for the parallel track.
f95717c
feat: Memory limit for parallel track.
76076e2
Change names of reduced-core parallel solvers.
f75b731
fix: Correctly recognize out of memory for incremental track.
96256c6
feat: Adapt parsing of Incremental results to new YML names.
8297d7f
fix: Add nb_answers to all results.
9ebce05
feat: Update year.
24a718f
feat: Better structure of generated result directories.
f4beace
@wintered
present derived solvers' increment over base solver
f4fa309
@wintered
cosmetics
9d64aee
@wintered
interim
8f1c054
@wintered
minor
b338b90
@wintered wintered changed the title Derived solver presentation Derived/non-competing solver presentation Jul 30, 2025
@wintered wintered marked this pull request as draft July 30, 2025 14:35
@github-actions
Copy link

github-actions bot commented Aug 2, 2025 •
edited
Loading

Summary of modified submissions

STP-Parti-Bitwuzla-16core

STP-Parti-Bitwuzla-64core

STP-Parti-Bitwuzla-8core

Z3-Parti-Z3pp-16core

Z3-Parti-Z3pp-32core

Z3-Parti-Z3pp-8core

Bitwuzla-16core

  • 2 authors
  • website: https://bitwuzla.github.io/
  • Participations
    • Parallel
      • Bitvec
        • all
      • Equality+MachineArith
        • ABV
        • ABVFP
        • ABVFPLRA
        • AUFBV
        • AUFBVFP
        • UFBV
        • UFBVFP
      • FPArith
        • all
      • QF_Bitvec
        • all
      • QF_Equality+Bitvec
        • QF_UFBVDT
      • QF_FPArith
        • QF_UFFPDTNIRA

Bitwuzla-32core

  • 2 authors
  • website: https://bitwuzla.github.io/
  • Participations
    • Parallel
      • Bitvec
        • all
      • Equality+MachineArith
        • ABV
        • ABVFP
        • ABVFPLRA
        • AUFBV
        • AUFBVFP
        • UFBV
        • UFBVFP
      • FPArith
        • all
      • QF_Bitvec
        • all
      • QF_Equality+Bitvec
        • QF_UFBVDT
      • QF_FPArith
        • QF_UFFPDTNIRA

wintered and others added 16 commits August 2, 2025 18:52
@wintered
establishing consistency among submissions with multiple cores
68cc10a
feat: Add preliminary results of UnsatCore track
ba23708
feat: Adapt unsat core validation to new YML format.
12c9977
fix: Remove join as there are no removed results.
e1e67d1
chore: Apply black.
eb0a5d3
feat: Remove non-competing divisions from results.
a17c198
fix: Remove debug prints.
62cf124
feat: Generate results of Parallel track.
4dd7dfd
feat: Add BestOverall ranking to certificates.
5aef59f
feat: Generate solver data for certificates automatically.
424c571
chore: Update year in certificates.
643a6e7
@wintered
2024 -> 2025
7468375
@wintered
2024 -> 2025
f4efacf
@wintered
target for cleaning up web results
7ef410f
@wintered
Merge remote-tracking branch 'origin/2025_final_execution' into prese…
8bc62ae 
…ntation-derived-solver
@wintered
feat: show legends for base and non-competing only when at least one
71e5365 
solver present
@wintered wintered closed this Aug 4, 2025
@wintered wintered deleted the presentation-derived-solver branch August 4, 2025 13:17
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

5 participants

@wintered @mpreiner @zmylinxi99 @Tomaqa