simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-06 03:05:31 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

wip: try to restore old model construction

Browse source
This commit is contained in:
Simon Cruanes 2022-07-22 22:16:04 -04:00
parent 2922cca78f
commit 4a6237191e
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
1 changed files with 27 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

25
src/smt-solver/Sidekick_smt_solver.ml
View file

@ -627,16 +627,28 @@ module Make (A : ARG) :
(** {2 Model construction and theory combination} *) (** {2 Model construction and theory combination} *)
(* make model from the congruence closure *) (* make model from the congruence closure *)
let mk_model_ (self : t) : Model.t = let mk_model_ (self : t) (lits : lit Iter.t) : Model.t =
Log.debug 1 "(smt.solver.mk-model)"; Log.debug 1 "(smt.solver.mk-model)";
Profile.with_ "smt-solver.mk-model" @@ fun () -> Profile.with_ "smt-solver.mk-model" @@ fun () ->
let module M = Term.Tbl in let module M = Term.Tbl in
let { cc = (lazy cc); model_ask = model_ask_hooks; model_complete; _ } = let {
cc = (lazy cc);
tst;
model_ask = model_ask_hooks;
model_complete;
_;
} =
self self
in in
let model = M.create 128 in let model = M.create 128 in
(* first, add all literals to the model using the given propositional model
[lits]. *)
lits (fun lit ->
let t, sign = Lit.signed_term lit in
M.replace model t (Term.bool tst sign));
(* populate with information from the CC *) (* populate with information from the CC *)
(* FIXME (* FIXME
CC.get_model_for_each_class cc (fun (_, ts, v) -> CC.get_model_for_each_class cc (fun (_, ts, v) ->
@ -681,6 +693,8 @@ module Make (A : ARG) :
in in
let t_val = let t_val =
try_hooks_ model_ask_hooks
(* FIXME: the more complete version?
match match
(* look for a value in the model for any term in the class *) (* look for a value in the model for any term in the class *)
N.iter_class repr N.iter_class repr
@ -688,6 +702,7 @@ module Make (A : ARG) :
with with
| Some v -> v | Some v -> v
| None -> try_hooks_ model_ask_hooks | None -> try_hooks_ model_ask_hooks
*)
in in
M.replace model (N.term repr) t_val; M.replace model (N.term repr) t_val;
@ -708,7 +723,7 @@ module Make (A : ARG) :
(* do theory combination using the congruence closure. Each theory (* do theory combination using the congruence closure. Each theory
can merge classes, *) can merge classes, *)
let check_th_combination_ (self : t) (acts : theory_actions) : let check_th_combination_ (self : t) (_acts : theory_actions) lits :
(Model.t, th_combination_conflict) result = (Model.t, th_combination_conflict) result =
(* FIXME (* FIXME
@ -733,7 +748,7 @@ module Make (A : ARG) :
Ok m Ok m
with Semantic_conflict c -> Error c with Semantic_conflict c -> Error c
*) *)
let m = mk_model_ self in let m = mk_model_ self lits in
Ok m Ok m
(* call congruence closure, perform the actions it scheduled *) (* call congruence closure, perform the actions it scheduled *)
@ -772,7 +787,7 @@ module Make (A : ARG) :
List.iter (fun f -> f self acts lits) self.on_final_check; List.iter (fun f -> f self acts lits) self.on_final_check;
check_cc_with_acts_ self acts; check_cc_with_acts_ self acts;
(match check_th_combination_ self acts with (match check_th_combination_ self acts lits with
| Ok m -> self.last_model <- Some m | Ok m -> self.last_model <- Some m
| Error { lits; semantic } -> | Error { lits; semantic } ->
(* bad model, we add a clause to remove it *) (* bad model, we add a clause to remove it *)