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

update model construction function

Browse source
This commit is contained in:
Simon Cruanes 2022-02-15 12:23:04 -05:00
parent 7f45cc6967
commit f3947f2237
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
1 changed files with 14 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -838,7 +838,8 @@ module Make(A : ARG)
Profile.with_ "smt-solver.mk-model" @@ fun () ->
let module M = Term.Tbl in
let model = M.create 128 in
let {Solver_internal.tst; cc=lazy cc; model_ask; model_complete; _} = self.si in
let {Solver_internal.tst; cc=lazy cc;
model_ask=model_ask_hooks; model_complete; _} = self.si in
(* first, add all literals to the model using the given propositional model
[lits]. *)
@ -867,16 +868,25 @@ module Make(A : ARG)
| None ->
(* try each model hook *)
let rec aux = function
let rec try_hooks_ = function
| [] -> N.term repr
| h :: hooks ->
begin match h ~recurse:(fun _ n -> val_for_class n) self.si repr with
| None -> aux hooks
| None -> try_hooks_ hooks
| Some t -> t
end
in
let t_val = aux model_ask in
let t_val =
match
(* look for a value in the model for any term in the class *)
N.iter_class repr
|> Iter.find_map (fun n -> M.get model (N.term n))
with
| Some v -> v
| None -> try_hooks_ model_ask_hooks
in
M.replace model (N.term repr) t_val; (* be sure to cache the value *)
t_val
in