model parsing draft

dune-project

@@ -73,6 +73,7 @@
   (prelude
    (>= "0.3"))
   rusage
+  scfg
   (yojson
    (>= "1.6.0"))
   (zarith

smtml.opam

@@ -31,6 +31,7 @@ depends: [
   "patricia-tree" {>= "0.10.0"}
   "prelude" {>= "0.3"}
   "rusage"
+  "scfg"
   "yojson" {>= "1.6.0"}
   "zarith" {>= "1.5"}
   "odoc" {with-doc}

src/ast/num.ml

@@ -14,6 +14,14 @@ type printer =
   | `Hexadecimal
   ]
 
+let type_of (n : t) =
+  match n with
+  | I8 _ -> Ty.(Ty_bitv 8)
+  | I32 _ -> Ty.(Ty_bitv 32)
+  | I64 _ -> Ty.(Ty_bitv 64)
+  | F32 _ -> Ty.(Ty_fp 32)
+  | F64 _ -> Ty.(Ty_fp 64)
+
 let compare n1 n2 =
   match (n1, n2) with
   | I8 i1, I8 i2 -> Int.compare i1 i2
@@ -62,12 +70,22 @@ let pp fmt v = !printer fmt v
 
 let to_string (n : t) : string = Fmt.str "%a" pp n
 
-let to_json (n : t) : Yojson.Basic.t = `String (to_string n)
+let of_string (cast : Ty.t) value =
+  match cast with
+  | Ty_bitv 8 -> (
+    match int_of_string value with
+    | None -> Error "invalid value, expected 8-bit bitv"
+    | Some n -> Ok (I8 n) )
+  | Ty_bitv 32 -> Ok (I32 (Int32.of_string value))
+  | Ty_bitv 64 -> Ok (I64 (Int64.of_string value))
+  | Ty_fp 32 -> (
+    match float_of_string value with
+    | None -> Error "invalid value, expected float"
+    | Some n -> Ok (I32 (Int32.bits_of_float n)) )
+  | Ty_fp 64 -> (
+    match float_of_string value with
+    | None -> Error "invalid value, expected float"
+    | Some n -> Ok (I64 (Int64.bits_of_float n)) )
+  | _ -> Error "invalid value, expected num"
 
-let type_of (n : t) =
-  match n with
-  | I8 _ -> Ty.(Ty_bitv 8)
-  | I32 _ -> Ty.(Ty_bitv 32)
-  | I64 _ -> Ty.(Ty_bitv 64)
-  | F32 _ -> Ty.(Ty_fp 32)
-  | F64 _ -> Ty.(Ty_fp 64)
+let to_json (n : t) : Yojson.Basic.t = `String (to_string n)

src/ast/num.mli

@@ -14,6 +14,8 @@ type printer =
   | `Hexadecimal
   ]
 
+val type_of : t -> Ty.t
+
 val compare : t -> t -> int
 
 val equal : t -> t -> bool
@@ -26,6 +28,6 @@ val pp : t Fmt.t
 
 val to_string : t -> string
 
-val to_json : t -> Yojson.Basic.t
+val of_string : Ty.t -> string -> (t, string) result
 
-val type_of : t -> Ty.t
+val to_json : t -> Yojson.Basic.t

src/ast/ty.ml

@@ -419,6 +419,35 @@ let pp fmt = function
   | Ty_none -> Fmt.string fmt "none"
   | Ty_regexp -> Fmt.string fmt "regexp"
 
+let of_string = function
+  | "int" -> Ok Ty_int
+  | "real" -> Ok Ty_real
+  | "bool" -> Ok Ty_bool
+  | "str" -> Ok Ty_str
+  | "list" -> Ok Ty_list
+  | "app" -> Ok Ty_app
+  | "unit" -> Ok Ty_unit
+  | "none" -> Ok Ty_none
+  | "regexp" -> Ok Ty_regexp
+  | s ->
+    if String.starts_with ~prefix:"i" s then begin
+      let s = String.sub s 1 (String.length s - 1) in
+      match int_of_string s with
+      | None -> Error (Fmt.str "can not parse type %s" s)
+      | Some n when n < 0 ->
+        Error (Fmt.str "size of bitvectors must be a positive integer")
+      | Some n -> Ok (Ty_bitv n)
+    end
+    else if String.starts_with ~prefix:"f" s then begin
+      let s = String.sub s 1 (String.length s - 1) in
+      match int_of_string s with
+      | None -> Error (Fmt.str "can not parse type %s" s)
+      | Some n when n < 0 ->
+        Error (Fmt.str "size of fp must be a positive integer")
+      | Some n -> Ok (Ty_fp n)
+    end
+    else Error (Fmt.str "can not parse type %s" s)
+
 let pp_logic fmt = function
   | ALL -> Fmt.string fmt "ALL"
   | AUFLIA -> Fmt.string fmt "AUFLIA"

src/ast/ty.mli

@@ -196,4 +196,6 @@ val pp_logic : logic Fmt.t
 
 val string_of_type : t -> string
 
+val of_string : string -> (t, string) Result.t
+
 val size : t -> int

src/ast/value.ml

@@ -16,6 +16,18 @@ type t =
   | App : [> `Op of string ] * t list -> t
   | Nothing
 
+let type_of (v : t) : Ty.t =
+  match v with
+  | True | False -> Ty_bool
+  | Unit -> Ty_unit
+  | Int _ -> Ty_int
+  | Real _ -> Ty_real
+  | Str _ -> Ty_str
+  | Num n -> Num.type_of n
+  | List _ -> Ty_list
+  | App _ -> Ty_app
+  | Nothing -> Ty_none
+
 let rec compare (v1 : t) (v2 : t) : int =
   match (v1, v2) with
   | True, True | False, False | Unit, Unit | Nothing, Nothing -> 0
@@ -69,6 +81,29 @@ let rec pp fmt = function
 
 let to_string (v : t) : string = Fmt.str "%a" pp v
 
+let of_string (cast : Ty.t) v =
+  let open Result in
+  match cast with
+  | Ty_bitv _ | Ty_fp _ ->
+    let+ n = Num.of_string cast v in
+    Num n
+  | Ty_bool -> (
+    match v with
+    | "true" -> Ok True
+    | "false" -> Ok False
+    | _ -> Error "invalid value, expected boolean" )
+  | Ty_int -> (
+    match int_of_string v with
+    | None -> Error "invalid value, expected integer"
+    | Some n -> Ok (Int n) )
+  | Ty_real -> (
+    match float_of_string v with
+    | None -> Error "invalid value, expected real"
+    | Some n -> Ok (Real n) )
+  | Ty_str -> Ok (Str v)
+  | Ty_app | Ty_list | Ty_none | Ty_unit | Ty_regexp ->
+    Error (Fmt.str "unsupported parsing values of type %a" Ty.pp cast)
+
 let rec to_json (v : t) : Yojson.Basic.t =
   match v with
   | True -> `Bool true
@@ -81,15 +116,3 @@ let rec to_json (v : t) : Yojson.Basic.t =
   | List l -> `List (List.map to_json l)
   | Nothing -> `Null
   | App _ -> assert false
-
-let type_of (v : t) : Ty.t =
-  match v with
-  | True | False -> Ty_bool
-  | Unit -> Ty_unit
-  | Int _ -> Ty_int
-  | Real _ -> Ty_real
-  | Str _ -> Ty_str
-  | Num n -> Num.type_of n
-  | List _ -> Ty_list
-  | App _ -> Ty_app
-  | Nothing -> Ty_none

src/ast/value.mli

@@ -14,6 +14,8 @@ type t =
   | App : [> `Op of string ] * t list -> t
   | Nothing
 
+val type_of : t -> Ty.t
+
 val compare : t -> t -> int
 
 val equal : t -> t -> bool
@@ -26,6 +28,6 @@ val pp : t Fmt.t
 
 val to_string : t -> string
 
-val to_json : t -> Yojson.Basic.t
+val of_string : Ty.t -> string -> (t, string) result
 
-val type_of : t -> Ty.t
+val to_json : t -> Yojson.Basic.t

src/dune

@@ -59,6 +59,7 @@
   ocaml_intrinsics
   patricia-tree
   rusage
+  scfg
   smtml.prelude
   yojson
   zarith

src/solvers/model.ml

@@ -48,3 +48,137 @@ let to_json (model : t) : Yojson.t =
   in
   let model :> Yojson.t = Hashtbl.fold add_assignment model (`Assoc []) in
   `Assoc [ ("model", model) ]
+
+(** {b Example}: Model in the json format:
+
+    {@json[
+      {
+        "model" : {
+          "x_0" : { "ty" : "int", "value" : 42 },
+          "x_1" : { "ty" : "bool", "value" : true },
+          "x_2" : { "ty" : "f32", "value" : 42.42 }
+        }
+      }
+    ]} *)
+let to_json_string model =
+  let model = to_json model in
+  Fmt.str "%a" Yojson.pp model
+
+let to_scfg model =
+  let open Scfg.Types in
+  let children =
+    let bindings = get_bindings model in
+    List.map
+      (fun (symbol, value) ->
+        let p0 = Symbol.to_string symbol in
+        let p1 = Symbol.type_of symbol |> Ty.string_of_type in
+        let p2 = Value.to_string value in
+        let params = [ p0; p1; p2 ] in
+        { name = "symbol"; params; children = [] } )
+      bindings
+  in
+  [ { name = "model"; params = []; children } ]
+
+(** {b Example}: Model in the scfg format:
+
+    {@scfg[
+      model {
+        symbol x_0 int 42
+        symbol x_1 bool true
+        symbol x_2 f32 42.42
+      }
+    ]} *)
+let to_scfg_string model =
+  let model = to_scfg model in
+  Fmt.str "%a" Scfg.Pp.config model
+
+let to_smtlib _model = assert false
+
+(** {b Example}: TODO *)
+let to_smtlib_string model =
+  let _model = to_smtlib model in
+  assert false
+
+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_file file =
+      let file = Fpath.to_string file in
+      Json.from_file ~fname:file file |> from_json
+  end
+
+  module Scfg = struct
+    open Result
+
+    let from_scfg v =
+      match Scfg.Query.get_dir "model" v with
+      | None ->
+        Error "can not find the directive `model` while parsing the scfg config"
+      | Some model ->
+        let symbols = Scfg.Query.get_dirs "symbol" model.children in
+        let tbl = Hashtbl.create 16 in
+        let* () =
+          Result.list_iter
+            (fun symbol ->
+              let* name = Scfg.Query.get_param 0 symbol in
+              let* ty = Scfg.Query.get_param 1 symbol in
+              let* ty = Ty.of_string ty in
+              let* value = Scfg.Query.get_param 2 symbol in
+              let+ value = Value.of_string ty value in
+              let key = Symbol.make ty name in
+              Hashtbl.add tbl key value )
+            symbols
+        in
+        Ok tbl
+
+    let from_string s =
+      let* model = Scfg.Parse.from_string s in
+      from_scfg model
+
+    let from_channel chan =
+      let* model = Scfg.Parse.from_channel chan in
+      from_scfg model
+
+    let from_file file =
+      let* model = Scfg.Parse.from_file (Fpath.to_string file) in
+      from_scfg model
+  end
+
+  module Smtlib = struct
+    let from_string _s = assert false
+
+    let from_channel _chan = assert false
+
+    let from_file _file = assert false
+  end
+end

src/solvers/model.mli

@@ -15,6 +15,47 @@ val evaluate : t -> Symbol.t -> Value.t option
 
 val pp : ?no_values:bool -> t Fmt.t
 
+(* TODO: do we want to keep it or only leave the following three to_*_string ? *)
 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_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