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

improve model printing so it's more smtlib2.6 compatible

Browse source
This commit is contained in:
Simon Cruanes 2022-10-15 23:15:42 -04:00
parent 4546b7cff2
commit 24bbcb3fbb
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
1 changed files with 2 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/smtlib/model.ml
View file

@ -41,7 +41,7 @@ let rec eval t (self : t) : value option =
let pp out (self : t) = let pp out (self : t) =
if is_empty self then if is_empty self then
Fmt.string out "(model)" Fmt.string out "()"
else ( else (
let rec pp_entries out = function let rec pp_entries out = function
| [] -> () | [] -> ()
@ -72,6 +72,5 @@ let pp out (self : t) =
(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)
in in
Fmt.fprintf out "(@[<hv>model@ %a@])" (Util.pp_iter pp_fun) Fmt.fprintf out "(@[<hv>%a@])" (Util.pp_iter pp_fun) (TM.to_iter self.m)
(TM.to_iter self.m)
) )