Incremental smt2 #371
Incremental smt2 #371
Conversation
ACoquereau
force-pushed
the
incremental-smt2
branch
from
9701ee5 to
275465f
Compare
ACoquereau
force-pushed
the
incremental-smt2
branch
from
7361962 to
e1c12d6
Compare
…nd fix unit facts cache for tableaux sat solver
…the same smt file with push/pop commands
…the same smt file with push/pop commands in the functional sat solver
There was a problem hiding this comment.
-
I don't know if I wrote it somewhere: Can
--timeout-per-goaloption be used in incremental mode ? -
Another question related to save/replay used-context: an extra work is probably needed. This is probably already done for native-lang's multi-goals feature, and we could adapt it for push/pop
Yes, it works pretty well
I did not look into this issue but you're right we need to fix this |
There was a problem hiding this comment.
There are probably other refs inside or outside fun_sat.ml and satml_frontend.ml that need to be saved (on push) and restored (on pop). Like for instance,
- steps counter
- fied
model_gen_modein fun_sat.ml - other local refs related to model generation in fun_sat.ml
let all_models_sat_env = ref None
let latest_saved_env = ref None
let terminated_normally = ref false
In fun_sat for instances, we should probably have a function similar to reset_refs () to save/restore refs. The data can probably be directly stored in incremental.stack_guard. A similar solution should also work for satml_frontend.
src/lib/reasoners/fun_sat.ml
Outdated
| @@ -1794,7 +1878,8 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct | |||
| inst = Inst.add_predicate env.inst gf dep } | |||
| else | |||
| begin | |||
| assert (not (ME.mem a_t env.ground_preds)); | |||
| if Stack.is_empty env.incremental.stack_guard then | |||
There was a problem hiding this comment.
pred_def (of ground and non-ground predicates), should take guards into account (see detailed commented in satml_frontend.ml)
…d a fresh expr to use as a guard in the satml_frontend
some code was duplicated in fun_sat.ml and satml_frontend.ml. Moving the env (and the detection of ground preds) to instances.ml allows to refactor it.
The following example is now handled correctly: (declare-fun y () Bool) (assert (= y true)) (push 1) (define-fun x ((u Int)) Bool false) (assert (= (x 1) y)) (check-sat) (pop 1) (push 1) (define-fun x ((u Int)) Bool true) (assert (= (x 1) y)) (check-sat) (pop 1)
* Add smt-lib2 incremental (push/pop commands) support through Alt-Ergo Co-authored-by: OriginLabs-Iguernlala <mohamed.iguernlala@origin-labs.com>
No description provided.