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

Support stacking decision scopes #20

Open
arbimo opened this issue Sep 24, 2021 · 0 comments
Open

Support stacking decision scopes #20

arbimo opened this issue Sep 24, 2021 · 0 comments
Labels
enhancement New feature or request I-solver

Comments

@arbimo
Copy link
Member

arbimo commented Sep 24, 2021

We should support defining new decision contexts that refine the current decision problem with assumptions.

The user should be able to set the current state as a virtual root of the solver.
In this new root, the user should be able to pose assumptions (modeled as decisions ?).
When the problem is found UNSAT, the solver that should return an explanation that is composed of the assumptions.

@arbimo arbimo added I-solver enhancement New feature or request labels Sep 24, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement New feature or request I-solver
Projects
None yet
Development

No branches or pull requests

1 participant