Refactoring models representation

alt-ergo-lib.opam

@@ -26,6 +26,7 @@ depends: [
   "fmt" {>= "0.9.0"}
   "stdlib-shims"
   "ppx_blob" {>= "0.7.2"}
+  "ppx_deriving"
   "camlzip" {>= "1.07"}
   "odoc" {with-doc}
   "ppx_deriving"

dune-project

@@ -86,6 +86,7 @@ See more details on http://alt-ergo.ocamlpro.com/"
   (fmt (>= 0.9.0))
   stdlib-shims
   (ppx_blob (>= 0.7.2))
+  ppx_deriving
   (camlzip (>= 1.07))
   (odoc :with-doc)
   ppx_deriving

src/bin/common/solving_loop.ml

@@ -181,7 +181,8 @@ let main () =
         begin
           let mdl = Model ((module SAT), partial_model) in
           if Options.(get_interpretation () && get_dump_models ()) then begin
-            FE.print_model (Options.Output.get_fmt_models ()) partial_model
+            Fmt.pf (Options.Output.get_fmt_models ()) "%a@."
+              FE.print_model partial_model
           end;
           Sat mdl
         end
@@ -193,7 +194,8 @@ let main () =
             Printer.print_fmt (Options.Output.get_fmt_diagnostic ())
               "@[<v 0>Returned unknown reason = %a@]"
               Sat_solver_sig.pp_ae_unknown_reason_opt ur;
-            FE.print_model (Options.Output.get_fmt_models ()) partial_model
+            Fmt.pf (Options.Output.get_fmt_models ()) "%a@."
+              FE.print_model partial_model
           end;
           Unknown (Some mdl)
         end
@@ -927,7 +929,8 @@ let main () =
           let () = match State.get partial_model_key st with
             | Some (Model ((module SAT), env)) ->
               let module FE = Frontend.Make (SAT) in
-              FE.print_model (Options.Output.get_fmt_regular ()) env
+              Fmt.pf (Options.Output.get_fmt_regular ()) "%a@."
+                FE.print_model env
             | None ->
               (* TODO: add the location of the statement. *)
               recoverable_error "No model produced."

src/lib/dune

@@ -55,7 +55,7 @@
     ; structures
     Commands Errors Explanation Fpa_rounding
     Parsed Profiling Satml_types Symbols
-    Expr Var Ty Typed Xliteral ModelMap Objective
+    Expr Var Ty Typed Xliteral ModelMap Id Objective
     ; util
     Emap Gc_debug Hconsing Hstring Heap Lists Loc
     MyUnix Numbers

src/lib/frontend/d_cnf.ml

@@ -39,7 +39,6 @@ module SM = Sy.Map
 
 module DE = DStd.Expr
 module DT = DE.Ty
-module Id = DStd.Id
 module B = DStd.Builtin
 
 let unsupported msg =
@@ -194,7 +193,7 @@ let builtin_term t = Dl.Typer.T.builtin_term t
 let builtin_ty t = Dl.Typer.T.builtin_ty t
 
 let ty name ty =
-  Id.Map.add { name = DStd.Name.simple name; ns = Sort } @@
+  DStd.Id.Map.add { name = DStd.Name.simple name; ns = Sort } @@
   fun env s ->
   builtin_ty @@
   Dolmen_type.Base.app0 (module Dl.Typer.T) env s ty
@@ -214,10 +213,11 @@ let builtin_enum = function
     let add_cstrs map =
       List.fold_left (fun map ((c : DE.term_cst), _) ->
           let name = get_basename c.path in
-          Id.Map.add { name = DStd.Name.simple name; ns = Term } (fun env _ ->
-              builtin_term @@
-              Dolmen_type.Base.term_app_cst
-                (module Dl.Typer.T) env c) map)
+          DStd.Id.Map.add { name = DStd.Name.simple name; ns = Term }
+            (fun env _ ->
+               builtin_term @@
+               Dolmen_type.Base.term_app_cst
+                 (module Dl.Typer.T) env c) map)
         map cstrs
     in
     Cache.store_ty (DE.Ty.Const.hash ty_cst) ty_;
@@ -238,19 +238,19 @@ module Const = struct
   let bv2nat =
     with_cache (fun n ->
         let name = "bv2nat" in
-        Id.mk ~name ~builtin:(BV2Nat n)
+        DE.Id.mk ~name ~builtin:(BV2Nat n)
           (DStd.Path.global name) Ty.(arrow [bitv n] int))
 
   let int2bv =
     with_cache (fun n ->
         let name = "int2bv" in
-        Id.mk ~name ~builtin:(Int2BV n)
+        DE.Id.mk ~name ~builtin:(Int2BV n)
           (DStd.Path.global name) Ty.(arrow [int] (bitv n)))
 
   let smt_round =
     with_cache (fun (n, m) ->
         let name = "ae.round" in
-        Id.mk
+        DE.Id.mk
           ~name
           ~builtin:(AERound (n, m))
           (DStd.Path.global name)
@@ -299,7 +299,7 @@ let bv_builtins env s =
     equivalent *)
 let inject_ae_to_smt2 id =
   match id with
-  | Id.{name = Simple n; _} ->
+  | DStd.Id.{name = Simple n; _} ->
     begin
       if String.equal n Fpa_rounding.fpa_rounding_mode_ae_type_name then
         (* Injecting the type name as the SMT2 Type name. *)
@@ -322,15 +322,15 @@ let inject_ae_to_smt2 id =
 let ae_fpa_builtins =
   let (->.) args ret = (args, ret) in
   let dterm name f =
-    Id.Map.add { name = DStd.Name.simple name; ns = Term } @@
+    DStd.Id.Map.add { name = DStd.Name.simple name; ns = Term } @@
     fun env s ->
     builtin_term @@
     Dolmen_type.Base.term_app1 (module Dl.Typer.T) env s f
   in
   let op ?(tyvars = []) name builtin (args, ret) =
     let ty = DT.pi tyvars @@ DT.arrow args ret in
     let cst = DE.Id.mk ~name ~builtin (DStd.Path.global name) ty in
-    Id.Map.add { name = DStd.Name.simple name; ns = Term } @@
+    DStd.Id.Map.add { name = DStd.Name.simple name; ns = Term } @@
     fun env _ ->
     builtin_term @@
     Dolmen_type.Base.term_app_cst
@@ -358,13 +358,13 @@ let ae_fpa_builtins =
   let float64 = float (DE.Term.int "53") (DE.Term.int "1074") in
   let float64d x = float64 (mode "NearestTiesToEven") x in
   let partial1 name f =
-    Id.Map.add { name = DStd.Name.simple name; ns = Term } @@
+    DStd.Id.Map.add { name = DStd.Name.simple name; ns = Term } @@
     fun env s ->
     builtin_term @@
     Dolmen_type.Base.term_app1 (module Dl.Typer.T) env s f
   in
   let partial2 name f =
-    Id.Map.add { name = DStd.Name.simple name; ns = Term } @@
+    DStd.Id.Map.add { name = DStd.Name.simple name; ns = Term } @@
     fun env s ->
     builtin_term @@
     Dolmen_type.Base.term_app2 (module Dl.Typer.T) env s f
@@ -380,7 +380,7 @@ let ae_fpa_builtins =
   in
   let fpa_builtins =
     let open DT in
-    Id.Map.empty
+    DStd.Id.Map.empty
 
     |> add_rounding_modes
 
@@ -454,7 +454,7 @@ let ae_fpa_builtins =
   fun env s ->
     let search_id id =
       try
-        Id.Map.find_exn id fpa_builtins env s
+        DStd.Id.Map.find_exn id fpa_builtins env s
       with Not_found -> `Not_found
     in
     match s with
@@ -469,7 +469,7 @@ let smt_fpa_builtins =
     Dolmen_type.Base.term_app2 (module Dl.Typer.T) env s f
   in
   let other_builtins =
-    Id.Map.empty
+    DStd.Id.Map.empty
     |> add_rounding_modes
   in
   fun env s ->
@@ -487,7 +487,7 @@ let smt_fpa_builtins =
         | exception Failure _ -> `Not_found
       end
     | Dl.Typer.T.Id id -> begin
-        match Id.Map.find_exn id other_builtins env s with
+        match DStd.Id.Map.find_exn id other_builtins env s with
         | e -> e
         | exception Not_found -> `Not_found
       end
@@ -1876,7 +1876,7 @@ let make dloc_file acc stmt =
             let ns = DStd.Namespace.Decl in
             let name = Ty.fresh_hypothesis_name goal_sort in
             let decl: _ Typer_Pipe.stmt = {
-              id = Id.mk ns name;
+              id = DStd.Id.mk ns name;
               contents = `Hyp t; loc; attrs; implicit
             }
             in
@@ -1893,7 +1893,7 @@ let make dloc_file acc stmt =
       assert false
 
     (* Axiom definitions *)
-    | { id = Id.{name = Simple name; _}; contents = `Hyp t; loc; attrs;
+    | { id = DStd.Id.{name = Simple name; _}; contents = `Hyp t; loc; attrs;
         implicit=_ } ->
       let dloc = DStd.Loc.(loc dloc_file stmt.loc) in
       let aloc = DStd.Loc.lexing_positions dloc in

src/lib/frontend/frontend.ml

@@ -520,5 +520,5 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
         Sat_solver_sig.pp_ae_unknown_reason_opt ur;
 
     | Some model ->
-      Models.output_concrete_model ppf model
+      Models.pp ppf model
 end