Adds json model parsing

src/solvers/model.ml

@@ -101,13 +101,40 @@ let to_smtlib_string model =
 
 module Parse = struct
   module Json = struct
+    open Result
+    module Json = Yojson.Basic
+
+    let from_json json =
+      let symbols = Json.Util.member "model" json |> Json.Util.to_assoc in
+      let tbl = Hashtbl.create 16 in
+      let* () =
+        Result.list_iter
+          (fun (symbol, json) ->
+            let ty = Json.Util.member "ty" json |> Json.Util.to_string in
+            let* ty = Ty.of_string ty in
+            let value =
+              (* FIXME: this is a bit hackish in order to reuse the previous code *)
+              match Json.Util.member "value" json with
+              | `Bool x -> Bool.to_string x
+              | `Float x -> Float.to_string x
+              | `Int x -> Int.to_string x
+              | `String x -> x
+              | _ -> assert false
+            in
+            let+ value = Value.of_string ty value in
+            let key = Symbol.make ty symbol in
+            Hashtbl.add tbl key value )
+          symbols
+      in
+      Ok tbl
+
+    let from_string s = Json.from_string s |> from_json
+
+    let from_channel chan = Json.from_channel chan |> from_json
 
-
-    let from_string _s = assert false
-
-    let from_channel _chan = assert false
-
-    let from_file _file = assert false
+    let from_file file =
+      let file = Fpath.to_string file in
+      Json.from_file ~fname:file file |> from_json
   end
 
   module Scfg = struct

src/solvers/model.mli

@@ -19,30 +19,43 @@ val pp : ?no_values:bool -> t Fmt.t
 val to_string : t -> string
 
 val to_json : t -> Yojson.t
+
 val to_json_string : t -> string
 
 val to_scfg : t -> Scfg.Types.config
+
 val to_scfg_string : t -> string
 
 (* TODO:
-val to_smtlib : t -> ?
+   val to_smtlib : t -> ?
 *)
 val to_smtlib_string : t -> string
 
 module Parse : sig
   module Json : sig
     val from_string : string -> (t, string) Result.t
+
     val from_channel : in_channel -> (t, string) Result.t
+
     val from_file : Fpath.t -> (t, string) Result.t
   end
+
   module Scfg : sig
     val from_string : string -> (t, string) Result.t
+
     val from_channel : in_channel -> (t, string) Result.t
+
     val from_file : Fpath.t -> (t, string) Result.t
   end
+
   module Smtlib : sig
     val from_string : string -> (t, string) Result.t
+    [@@alert unsafe "not implemented"]
+
     val from_channel : in_channel -> (t, string) Result.t
+    [@@alert unsafe "not implemented"]
+
     val from_file : Fpath.t -> (t, string) Result.t
+    [@@alert unsafe "not implemented"]
   end
 end

test/unit/test_model.ml

@@ -18,6 +18,23 @@ let () =
 
 (* Parsing *)
 
+(* json *)
+let () =
+  let open Result in
+  let model_str =
+    {|
+      {
+        "model" : {
+          "x_0" : { "ty" : "int", "value" : 42 },
+          "x_1" : { "ty" : "bool", "value" : true },
+          "x_2" : { "ty" : "f32", "value" : 42.42 }
+        }
+      }
+    |}
+  in
+  let model = Model.Parse.Json.from_string model_str in
+  assert (match model with Ok _ -> true | _ -> false)
+
 (* scfg *)
 let () =
   let open Result in