Skip to content

Split octagon autotuner to separate octagonAnalysis and octagonVars autotuners#1952

Open
karoliineh wants to merge 2 commits intomasterfrom
issue-1449
Open

Split octagon autotuner to separate octagonAnalysis and octagonVars autotuners#1952
karoliineh wants to merge 2 commits intomasterfrom
issue-1449

Conversation

@karoliineh
Copy link
Member

Solves #1449

@karoliineh karoliineh added cleanup Refactoring, clean-up usability sv-comp SV-COMP (analyses, results), witnesses precision relational Relational analyses (Apron, affeq, lin2var) labels Mar 5, 2026
@karoliineh karoliineh marked this pull request as ready for review March 5, 2026 15:16
@karoliineh karoliineh requested a review from sim642 March 5, 2026 15:16
Copy link
Member

@michael-schwarz michael-schwarz left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We should start to document what these autotuners do somehow. Maybe we can have some way they are registered and a command line option to get the description of all autotuners like you can get one for the analyses?

@sim642
Copy link
Member

sim642 commented Mar 9, 2026

We should start to document what these autotuners do somehow. Maybe we can have some way they are registered and a command line option to get the description of all autotuners like you can get one for the analyses?

We don't actually have the analysis descriptions available at runtime. They exist as module documentation in the API docs for now (which isn't too user-friendly but better than none at all).
The command line listing exists for options, but we have so many that it's probably unusable compared to the schema itself.

But documenting the autotuners would definitely be a good idea.
I think for a start there could be a documentation comment in the code, e.g. on its main function that is used in the list of available autotuners.

A separate next step would be to split autotune.ml into individual files (while maintaining git blame history) like the analyses, but that requires a bit of trickery.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

cleanup Refactoring, clean-up precision relational Relational analyses (Apron, affeq, lin2var) sv-comp SV-COMP (analyses, results), witnesses usability

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants