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

chore: debug msg

Browse source
This commit is contained in:
Simon Cruanes 2018-08-18 15:04:29 -05:00
parent 8ea844a5a0
commit 2b2765c67f
1 changed files with 17 additions and 16 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

33
src/smt/Congruence_closure.ml
View file

@ -525,8 +525,25 @@ let final_check cc : unit =
Log.debug 5 "(CC.final_check)"; Log.debug 5 "(CC.final_check)";
update_tasks cc update_tasks cc
let pp_full out (cc:t) : unit =
let pp_next out n =
if n==n.n_root then Fmt.string out " :is-root"
else Fmt.fprintf out "@ :next %a" N.pp n.n_root in
let pp_root out n =
let u = find cc n in if n==u||n.n_root==u then () else Fmt.fprintf out "@ :root %a" N.pp u in
let pp_n out n =
Fmt.fprintf out "(@[%a%a%a@])" Term.pp n.n_term pp_next n pp_root n
and pp_sig_e out (s,n) =
Fmt.fprintf out "(@[<1>%a@ -> %a%a%a@])" Signature.pp s N.pp n pp_next n pp_root n
in
Fmt.fprintf out
"(@[@{<yellow>cc.state@}@ (@[<hv>:nodes@ %a@])@ (@[<hv>:sig@ %a@])@])"
(Util.pp_seq ~sep:" " pp_n) (Term.Tbl.values cc.tbl)
(Util.pp_seq ~sep:" " pp_sig_e) (Sig_tbl.to_seq cc.signatures_tbl)
(* model: map each uninterpreted equiv class to some ID *) (* model: map each uninterpreted equiv class to some ID *)
let mk_model (cc:t) (m:Model.t) : Model.t = let mk_model (cc:t) (m:Model.t) : Model.t =
Log.debugf 15 (fun k->k "(@[cc.mk_model@ %a@])" pp_full cc);
(* populate [repr -> value] table *) (* populate [repr -> value] table *)
let t_tbl = N.Tbl.create 32 in let t_tbl = N.Tbl.create 32 in
(* type -> default value *) (* type -> default value *)
@ -605,22 +622,6 @@ let mk_model (cc:t) (m:Model.t) : Model.t =
in in
Model.add_funs funs m Model.add_funs funs m
let pp_full out (cc:t) : unit =
let pp_next out n =
if n==n.n_root then Fmt.string out " :is-root"
else Fmt.fprintf out "@ :next %a" N.pp n.n_root in
let pp_root out n =
let u = find cc n in if n==u||n.n_root==u then () else Fmt.fprintf out "@ :root %a" N.pp u in
let pp_n out n =
Fmt.fprintf out "(@[%a%a%a@])" Term.pp n.n_term pp_next n pp_root n
and pp_sig_e out (s,n) =
Fmt.fprintf out "(@[<1>%a@ -> %a%a%a@])" Signature.pp s N.pp n pp_next n pp_root n
in
Fmt.fprintf out
"(@[@{<yellow>cc.state@}@ (@[<hv>:nodes@ %a@])@ (@[<hv>:sig@ %a@])@])"
(Util.pp_seq ~sep:" " pp_n) (Term.Tbl.values cc.tbl)
(Util.pp_seq ~sep:" " pp_sig_e) (Sig_tbl.to_seq cc.signatures_tbl)
let check_invariants_ (cc:t) = let check_invariants_ (cc:t) =
Log.debug 5 "(cc.check-invariants)"; Log.debug 5 "(cc.check-invariants)";
Log.debugf 15 (fun k-> k "%a" pp_full cc); Log.debugf 15 (fun k-> k "%a" pp_full cc);