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

debug

Browse source
This commit is contained in:
Simon Cruanes 2022-02-15 16:57:25 -05:00
parent f3947f2237
commit 5b0a2ad4a4
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
1 changed files with 5 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -853,6 +853,7 @@ module Make(A : ARG)
f self.si f self.si
~add:(fun t u -> ~add:(fun t u ->
if not (M.mem model t) then ( if not (M.mem model t) then (
Log.debugf 20 (fun k->k "(@[smt.model-complete@ %a@ :with-val %a@])" Term.pp t Term.pp u);
M.replace model t u M.replace model t u
)); ));
in in
@ -869,7 +870,10 @@ module Make(A : ARG)
(* try each model hook *) (* try each model hook *)
let rec try_hooks_ = function let rec try_hooks_ = function
| [] -> N.term repr | [] ->
let t = N.term repr in
Log.debugf 20 (fun k->k "(@[smt.model.default-to-repr@ %a@])" Term.pp t);
t
| h :: hooks -> | h :: hooks ->
begin match h ~recurse:(fun _ n -> val_for_class n) self.si repr with begin match h ~recurse:(fun _ n -> val_for_class n) self.si repr with
| None -> try_hooks_ hooks | None -> try_hooks_ hooks