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

chore: improve debug msg in check invariants

Browse source
This commit is contained in:
Simon Cruanes 2018-08-18 15:02:44 -05:00
parent d5ca5c2c81
commit 8ea844a5a0
1 changed files with 6 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/smt/Congruence_closure.ml
View file

@ -606,15 +606,15 @@ let mk_model (cc:t) (m:Model.t) : Model.t =
Model.add_funs funs m Model.add_funs funs m
let pp_full out (cc:t) : unit = 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 = let pp_n out n =
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
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
and pp_sig_e out (s,n) = and pp_sig_e out (s,n) =
Fmt.fprintf out "(@[<1>%a@ -> %a@])" Signature.pp s N.pp n Fmt.fprintf out "(@[<1>%a@ -> %a%a%a@])" Signature.pp s N.pp n pp_next n pp_root n
in in
Fmt.fprintf out Fmt.fprintf out
"(@[@{<yellow>cc.state@}@ (@[<hv>:nodes@ %a@])@ (@[<hv>:sig@ %a@])@])" "(@[@{<yellow>cc.state@}@ (@[<hv>:nodes@ %a@])@ (@[<hv>:sig@ %a@])@])"