incremental mode vs multi-goals: currently, work is done twice #382
Labels
Comments
|
When the handling in main_text is simplfied, a particular attention should be given for check and cut commands |
bclement-ocp
added a commit
to bclement-ocp/alt-ergo
that referenced
this issue
Oct 13, 2023
This patch adds support for `(set-option :sat-solver)` in the SMT-LIB frontend. The patch mostly lifts SAT-independent bits out of `Frontend.Make`, allowing to use a first-class module stored on the Dolmen state to provide access to the frontend. Changing solvers is only allowed in the initial state (before any assertions are made) as a forward-compatibility measure: it would currently be possible to switch solvers on the fly because we merely accumulate commands in the context and only call the solver on `(check-sat)`, but allowing solver changes anywhere would make it harder to remove the command stack, which we will probably do at some point (see also OCamlPro#382).
bclement-ocp
added a commit
to bclement-ocp/alt-ergo
that referenced
this issue
Oct 13, 2023
This patch adds support for `(set-option :sat-solver)` in the SMT-LIB frontend. The patch mostly lifts SAT-independent bits out of `Frontend.Make`, allowing to use a first-class module stored on the Dolmen state to provide access to the frontend. Changing solvers is only allowed in the initial state (before any assertions are made) as a forward-compatibility measure: it would currently be possible to switch solvers on the fly because we merely accumulate commands in the context and only call the solver on `(check-sat)`, but allowing solver changes anywhere would make it harder to remove the command stack, which we will probably do at some point (see also OCamlPro#382).
bclement-ocp
added a commit
to bclement-ocp/alt-ergo
that referenced
this issue
Oct 13, 2023
This patch adds support for `(set-option :sat-solver)` in the SMT-LIB frontend. The patch mostly lifts SAT-independent bits out of `Frontend.Make`, allowing to use a first-class module stored on the Dolmen state to provide access to the frontend. Changing solvers is only allowed in the initial state (before any assertions are made) as a forward-compatibility measure: it would currently be possible to switch solvers on the fly because we merely accumulate commands in the context and only call the solver on `(check-sat)`, but allowing solver changes anywhere would make it harder to remove the command stack, which we will probably do at some point (see also OCamlPro#382).
bclement-ocp
added a commit
that referenced
this issue
Oct 13, 2023
This patch adds support for `(set-option :sat-solver)` in the SMT-LIB frontend. The patch mostly lifts SAT-independent bits out of `Frontend.Make`, allowing to use a first-class module stored on the Dolmen state to provide access to the frontend. Changing solvers is only allowed in the initial state (before any assertions are made) as a forward-compatibility measure: it would currently be possible to switch solvers on the fly because we merely accumulate commands in the context and only call the solver on `(check-sat)`, but allowing solver changes anywhere would make it harder to remove the command stack, which we will probably do at some point (see also #382).
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Once #371 is merged, Alt-Ergo will support SMT2 incremental mode (push/pop).
But the way things are done in
check-satandcheck-sat-assumingcommands togoal)is not optimal.
The main loop in main_text should be improved.
The text was updated successfully, but these errors were encountered: