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

feat(smtlib.model): improve printing of deeply nested ite

Browse source
This commit is contained in:
Simon Cruanes 2022-10-19 22:29:19 -04:00
parent 082bfdd43a
commit 61f1854b80
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/smtlib/model.ml
View file

@ -59,7 +59,7 @@ let pp out (self : t) =
Fmt.fprintf out "@])" Fmt.fprintf out "@])"
in in
Fmt.fprintf out "(@[ite %a@ %a@ %a@])" pp_guard () Term.pp v pp_entries Fmt.fprintf out "@[(ite %a@ %a@ %a)@]" pp_guard () Term.pp v pp_entries
tl tl
in in
let pp_fun out (f, entries) = let pp_fun out (f, entries) =
@ -67,7 +67,7 @@ let pp out (self : t) =
| None -> () | None -> ()
| Some (args, v) -> | Some (args, v) ->
let pp_arg out (i, ty) = Fmt.fprintf out "(@[x%d %a@])" i Term.pp ty in let pp_arg out (i, ty) = Fmt.fprintf out "(@[x%d %a@])" i Term.pp ty in
Fmt.fprintf out "(@[<1>define-fun %a (@[%a@])@ %a@ %a@])" Term.pp f Fmt.fprintf out "(@[<1>define-fun %a (@[%a@])@ %a@ @[%a@]@])" Term.pp f
(Util.pp_list ~sep:" " pp_arg) (Util.pp_list ~sep:" " pp_arg)
(List.mapi (fun i v -> i, Term.ty v) args) (List.mapi (fun i v -> i, Term.ty v) args)
Term.pp (Term.ty v) pp_entries (TL_map.to_list entries) Term.pp (Term.ty v) pp_entries (TL_map.to_list entries)