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.
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.