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

chore: minor debug msg

Browse source
This commit is contained in:
Simon Cruanes 2018-08-18 14:56:28 -05:00
parent 6d2d1c91e8
commit d5ca5c2c81
1 changed files with 3 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/smt/Congruence_closure.ml
View file

@ -608,7 +608,8 @@ let mk_model (cc:t) (m:Model.t) : Model.t =
let pp_full out (cc:t) : unit = let pp_full out (cc:t) : unit =
let pp_n out n = let pp_n out n =
let pp_next out n = let pp_next out n =
if n==n.n_root then () else Fmt.fprintf out "@ :next %a" N.pp n.n_root in 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 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 u = find cc n in if n==u||n.n_root==u then () else Fmt.fprintf out "@ :root %a" N.pp u in
Fmt.fprintf out "(@[%a%a%a@])" Term.pp n.n_term pp_next n pp_root n Fmt.fprintf out "(@[%a%a%a@])" Term.pp n.n_term pp_next n pp_root n
@ -616,7 +617,7 @@ let pp_full out (cc:t) : unit =
Fmt.fprintf out "(@[<1>%a@ -> %a@])" Signature.pp s N.pp n Fmt.fprintf out "(@[<1>%a@ -> %a@])" Signature.pp s N.pp n
in in
Fmt.fprintf out Fmt.fprintf out
"(@[cc.state@ (@[<hv>:nodes@ %a@])@ (@[<hv>:sig@ %a@])@])" "(@[@{<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_n) (Term.Tbl.values cc.tbl)
(Util.pp_seq ~sep:" " pp_sig_e) (Sig_tbl.to_seq cc.signatures_tbl) (Util.pp_seq ~sep:" " pp_sig_e) (Sig_tbl.to_seq cc.signatures_tbl)