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

Witness generation: Make CSV export work even if the solver fails #1407

Open
georgwiese opened this issue May 29, 2024 · 1 comment
Open

Comments

@georgwiese
Copy link
Collaborator

When the solver fails (e.g. due to missing constraints, missing hints, or contradictions in the constraints), it can be pretty daunting to figure out why. Often, this involves inspecting the trace log.

I think one thing that could help would be to just "dump" the current state. We already have the CSV export, so we could use it to dump a partial witness in the case of failure.

This won't be simple, because for example a machine that doesn't complete (which can happen also during a successful run) discards the partial block, so we'd have to keep it around in case we need to dump the current state.

@qwang98
Copy link
Collaborator

qwang98 commented May 29, 2024

Oh that's why my --export-csv didn't export when debugging ;)

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

No branches or pull requests

2 participants