Use dolmen

dune-project

@@ -38,6 +38,7 @@
  )
  (depends
   dune
+  dolmen
   (ocaml
    (>= "4.14.0"))
   (prelude

smtml.opam

@@ -10,6 +10,7 @@ doc: "https://formalsec.github.io/smtml/smtml/index.html"
 bug-reports: "https://github.com/formalsec/smtml/issues"
 depends: [
   "dune" {>= "3.10"}
+  "dolmen"
   "ocaml" {>= "4.14.0"}
   "prelude" {>= "0.3"}
   "ocaml_intrinsics"

src/dune

@@ -30,6 +30,7 @@
   solver
   solver_intf
   solver_dispatcher
+  smtlib
   symbol
   statistics
   ty
@@ -40,6 +41,7 @@
  (flags
   (:standard -open Prelude))
  (libraries
+  dolmen
   hc
   menhirLib
   ocaml_intrinsics

src/parser/smtlib.ml

@@ -0,0 +1,98 @@
+module Loc = Dolmen.Std.Loc
+module Id = Dolmen.Std.Id
+
+module Term = struct
+  type t = Expr.t
+
+  let const ?loc:_ (_id : Id.t) : t = assert false
+
+  let str ?loc:_ (x : string) = Expr.value (Str x)
+
+  let int ?loc:_ (_ : string) = assert false
+
+  let real ?loc:_ (_ : string) = assert false
+
+  let hexa ?loc:_ (_ : string) = assert false
+
+  let binary ?loc:_ (_ : string) = assert false
+
+  let colon ?loc:_ (_ : t) (_ : t) : t = assert false
+
+  let apply ?loc:_ (_ : t) (_ : t list) : t = assert false
+
+  let letand ?loc:_ = assert false
+
+  let forall ?loc:_ = assert false
+
+  let exists ?loc:_ = assert false
+
+  let match_ ?loc:_ = assert false
+
+  let sexpr ?loc:_ = assert false
+
+  let annot ?loc:_ = assert false
+end
+
+module Statement = struct
+  type t = Ast.t
+
+  let reset ?loc:_ () = assert false
+
+  let set_logic ?loc:_ _logic =
+    (* Ast.Set_logic (Ty.logic_of_string logic) *)
+    assert false
+
+  let set_option ?loc:_ _ = assert false
+
+  let exit ?loc:_ () = assert false
+
+  let push ?loc:_ _n = Ast.Push
+
+  let pop ?loc:_ n = Ast.Pop n
+
+  let reset_assertions ?loc:_ () = assert false
+
+  let type_decl ?loc:_ = assert false
+
+  let type_def ?loc:_ = assert false
+
+  let datatypes ?loc:_ = assert false
+
+  let fun_decl ?loc:_ = assert false
+
+  let fun_def ?loc:_ = assert false
+
+  let funs_def_rec ?loc:_ _ = assert false
+
+  let assert_ ?loc:_ term = Ast.Assert term
+
+  let get_assertions ?loc:_ () = assert false
+
+  let check_sat ?loc:_ _terms = Ast.Check_sat
+
+  let get_model ?loc:_ () = Ast.Get_model
+
+  let get_value ?loc:_ _terms = assert false
+
+  let get_assignment ?loc:_ = assert false
+
+  let get_proof ?loc:_ () = assert false
+
+  let get_unsat_core ?loc:_ () = assert false
+
+  let get_unsat_assumptions ?loc:_ () = assert false
+
+  let get_info ?loc:_ _ = assert false
+
+  let get_option ?loc:_ _opt = assert false
+
+  let echo ?loc:_ _x = assert false
+
+  let set_info ?loc:_ = assert false
+end
+
+module Parser = Dolmen.Smtlib2.Script.Latest.Make (Loc) (Id) (Term) (Statement)
+
+let from_file filename =
+  let _, stmts = Parser.parse_file (Fpath.to_string filename) in
+  stmts