Skip to content
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.

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

BDD/Generator API #550

Merged
merged 6 commits into from
Oct 8, 2023
Merged

BDD/Generator API #550

merged 6 commits into from
Oct 8, 2023

Conversation

SSoelvsten
Copy link
Owner

@SSoelvsten SSoelvsten commented Oct 8, 2023

Deals with the breaking parts of #452 . The rest I will leave to be implemented another day.

  • Replaces the file-based input of bdd_restrict with a generator function / iterator.
  • Replaces the file-based inputs of bdd_eval with a generator function / iterator.

Furthermore,

  • Adds the domain_size() function to remove code duplication (treating no domain as 0).
  • Cleans up the logic for bdd_satmin and bdd_satmax that return a cube. Before this change, they put the entire assignment to the disk and then popped it off afterwards. Since the number of levels never exceed 8 MiB, we can just place the entire stack in internal memory.

With all of the above, we finally have removed all dependencies on the adiar::map_pair class (which seemed like a good idea that point in time, but really just is a mess) and the lifting of files from adiar::internal to adiar. This closes #538 .

@SSoelvsten SSoelvsten added ✨ feature New operation or other feature ✨ optimisation It's all about speed / space 📁 bdd Binary Decision Diagrams ❕ breaking version_number++ ✨ code quality Uncle Bob would be proud labels Oct 8, 2023
@SSoelvsten SSoelvsten self-assigned this Oct 8, 2023
In multiple places, we want to compare the domain size, where a missing
domain is treated as having size 0. We might as well just put this piece
of code in one place
…al memory stack

There is no need to make an external memory file for this algorithm. Adiar has a
minimum requirement of 128 MiB of memory, and even if all levels are present,
then they would only require up to 8 MiB of memory. This leaves enough space to
open all relevant streams and it will be considerably faster (since we do no
unecessary read/writes of tiny files to the disk)
The entire public API does not make use of Adiar's files (with the exception
of 'domain_get()' and one overload of 'domain_set(...)', both of which are
really only intended for an internal use-case anyway).
@codecov
Copy link

codecov bot commented Oct 8, 2023

Codecov Report

All modified lines are covered by tests ✅

Comparison is base (144a6d1) 96.648% compared to head (0b98531) 96.653%.

Additional details and impacted files
@@              Coverage Diff              @@
##              main      #550       +/-   ##
=============================================
+ Coverage   96.648%   96.653%   +0.006%     
=============================================
  Files           84        83        -1     
  Lines         5787      5767       -20     
=============================================
- Hits          5593      5574       -19     
+ Misses         194       193        -1     
Files Coverage Δ
src/adiar/bdd.h 100.000% <100.000%> (ø)
src/adiar/bdd/bdd.cpp 86.022% <100.000%> (ø)
src/adiar/bdd/count.cpp 100.000% <100.000%> (ø)
src/adiar/bdd/evaluate.cpp 100.000% <100.000%> (ø)
src/adiar/bdd/restrict.cpp 100.000% <100.000%> (ø)
src/adiar/domain.cpp 100.000% <100.000%> (ø)
src/adiar/domain.h 100.000% <ø> (ø)
src/adiar/functional.h 100.000% <100.000%> (ø)
src/adiar/internal/algorithms/substitution.h 94.737% <ø> (ø)
src/adiar/zdd/build.cpp 100.000% <100.000%> (ø)
... and 2 more

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

@SSoelvsten SSoelvsten merged commit e54d58f into main Oct 8, 2023
43 of 50 checks passed
@github-actions
Copy link

github-actions bot commented Oct 8, 2023

Benchmark Report 🟢

origin/bdd/generator-api is an improvement of 1.45% (compared to origin/main).

Minimum running time (s) for 9-Queens:

origin/main origin/bdd/generator-api
0.25 0.25
Raw Data

Running times (s) for 9-Queens:

origin/main origin/bdd/generator-api
0.25 0.26
0.26 0.26
0.26 0.26
0.26 0.25
0.26 0.25
0.26 0.25
0.26 0.26
0.31 0.26
0.26 0.26
0.26 0.25
0.29 0.26
0.27 0.32
0.26 0.26
0.31 0.26
0.26 0.26
0.26 0.26

@github-actions
Copy link

github-actions bot commented Oct 8, 2023

Benchmark Report 🟢

origin/bdd/generator-api is an improvement of 1.32% (compared to origin/main).

Minimum running time (s) for 12-Queens:

origin/main origin/bdd/generator-api
14.77 14.58
Raw Data

Running times (s) for 12-Queens:

origin/main origin/bdd/generator-api
14.77 14.90
15.12 14.63
15.01 14.62
15.13 14.58
15.01 14.70
15.06 15.05
15.16 14.91
15.08 14.71
15.04 14.71
15.09 14.64
15.01 14.64
15.01 14.62
14.97 14.92
15.57 14.73
15.22 14.80
15.09 15.08

@github-actions
Copy link

github-actions bot commented Oct 8, 2023

Benchmark Report 🟢

origin/bdd/generator-api is an improvement of 1.88% (compared to origin/main).

Minimum running time (s) for 14-Queens:

origin/main origin/bdd/generator-api
435.05 426.89
Raw Data

Running times (s) for 14-Queens:

origin/main origin/bdd/generator-api
568.56 432.16
439.71 428.42
445.03 426.89
435.05 430.96

@SSoelvsten SSoelvsten deleted the bdd/generator-api branch October 9, 2023 15:31
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
📁 bdd Binary Decision Diagrams ❕ breaking version_number++ ✨ code quality Uncle Bob would be proud ✨ feature New operation or other feature ✨ optimisation It's all about speed / space
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Remove <adiar/file.h> and <adiar/map_pair.h>
1 participant