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

feat(model): improve printing of smtlib models

Browse source
This commit is contained in:
Simon Cruanes 2022-10-18 22:47:33 -04:00
parent 09d569ee68
commit 297615b61b
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/smtlib/model.ml
View file

@ -52,9 +52,9 @@ let pp out (self : t) =
| [] -> ()
| [ t ] -> Fmt.fprintf out "(@[= x0 %a@])" Term.pp t
| _ ->
Fmt.fprintf out "(@[and@ ";
Fmt.fprintf out "(@[and";
List.iteri
(fun i t -> Fmt.fprintf out "(@[= x%d %a@])" i Term.pp t)
(fun i t -> Fmt.fprintf out "@ (@[= x%d %a@])" i Term.pp t)
vs;
Fmt.fprintf out "@])"
in
@ -68,7 +68,7 @@ let pp out (self : t) =
| Some (args, v) ->
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
(Util.pp_list ~sep:"" pp_arg)
(Util.pp_list ~sep:" " pp_arg)
(List.mapi (fun i v -> i, Term.ty v) args)
Term.pp (Term.ty v) pp_entries (TL_map.to_list entries)
in