Skip to content

chore: add diagnostics#85

Merged
tdejager merged 5 commits intoprefix-dev:mainfrom
baszalmstra:misc/diagnostics
May 5, 2025
Merged

chore: add diagnostics#85
tdejager merged 5 commits intoprefix-dev:mainfrom
baszalmstra:misc/diagnostics

Conversation

@baszalmstra
Copy link
Copy Markdown
Contributor

This PR adds the use of segvec::SegVec to allocate clauses. This reduces the number of very large allocations performed by the library.

I also added functionality to report diagnostics to make it easier to debug what is going on.

@baszalmstra baszalmstra requested a review from wolfv November 28, 2024 09:03
@wolfv
Copy link
Copy Markdown
Member

wolfv commented Nov 28, 2024

Cool stuff! Did you benchmark that using segvec is beneficial?

The diagnostics are very nice.

@baszalmstra
Copy link
Copy Markdown
Contributor Author

I have not, I will run a benchmark at the end of the day.

@baszalmstra
Copy link
Copy Markdown
Contributor Author

But without it, I ran into issue with the solver trying to allocate 1.5GB in one go, which causes an OOM.

@baszalmstra
Copy link
Copy Markdown
Contributor Author

These are the timings results:

Untitled

There is no significant increase in outliers, but on average, the code became slightly slower.

Untitled-1

Ill try removing the segvec later and try again to see if thats the issue.

@tdejager tdejager changed the title chore: add diagnostics and segmented vector chore: add diagnostics May 5, 2025
@tdejager
Copy link
Copy Markdown
Contributor

tdejager commented May 5, 2025

Now prints something like:

Total number of solvables:  4
Total number of watches:    6 (512 B)
Total number of variables:  4 (108 B)
Total number of clauses:    5 (160 B)
- Requires:                 1
- Constrains:               0
- Lock:                     0
- Learned:                  0
- ForbidMultiple:           2
  - opentelemetry-api:      2

Removed SegVec cause it seems slower.

@tdejager tdejager merged commit 152e262 into prefix-dev:main May 5, 2025
9 checks passed
@baszalmstra baszalmstra mentioned this pull request May 5, 2025
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.

3 participants