Add colibri2 support

bin/main.ml

@@ -1,8 +1,4 @@
 open Encoding
-open Cmdliner
-module Z3_batch = Solver.Batch (Z3_mappings)
-module Z3_incremental = Solver.Incremental (Z3_mappings)
-module Interpret = Interpret.Make (Z3_batch)
 
 let get_contents = function
   | "-" -> In_channel.input_all In_channel.stdin
@@ -14,27 +10,72 @@ let get_contents = function
 
 let parse_file file = get_contents file |> Parse.from_string
 
-let main files =
-  match files with
-  | [] ->
-    let ast = parse_file "-" in
-    ignore @@ Interpret.start ast
-  | _ ->
-    ignore
-    @@ List.fold_left
-         (fun state file ->
-           let ast = Parse.from_file ~filename:file in
-           Some (Interpret.start ?state ast) )
-         None files
+type prover =
+  | Z3_prover
+  | Colibri2_prover
 
-let files =
-  let doc = "source files" in
-  Arg.(value & pos_all non_dir_file [] & info [] ~doc)
+let prover_conv =
+  Cmdliner.Arg.conv
+    ( (fun str ->
+        try
+          Ok
+            ( match str with
+            | "Z3" | "z3" -> Z3_prover
+            | "Colibri2" | "colibri2" -> Colibri2_prover
+            | _ ->
+              failwith (Fmt.str "Unsupported prover %s, try Z3 or Colibri2" str)
+            )
+        with Failure s -> Error (`Msg s) )
+    , fun fmt -> function
+        | Z3_prover -> Fmt.pf fmt "Z3"
+        | Colibri2_prover -> Fmt.pf fmt "Colibri2" )
 
-let cli =
-  let info = Cmd.info "smtml" ~version:"%%VERSION%%" in
-  Cmd.v info Term.(const main $ files)
+let parse_cmdline =
+  let aux files prover incremental debug =
+    let module Mappings =
+      ( val match prover with
+            | Z3_prover -> (module Z3_mappings)
+            | Colibri2_prover -> (module Colibri2_mappings)
+          : Mappings_intf.S )
+    in
+    Mappings.set_debug debug;
+    let module Interpret =
+      ( val if incremental then
+              (module Interpret.Make (Solver.Incremental (Mappings)))
+            else (module Interpret.Make (Solver.Batch (Mappings)))
+          : Interpret_intf.S )
+    in
+    match files with
+    | [] ->
+      let ast = parse_file "-" in
+      ignore @@ Interpret.start ast
+    | _ ->
+      ignore
+      @@ List.fold_left
+           (fun state file ->
+             let ast = Parse.from_file ~filename:file in
+             Some (Interpret.start ?state ast) )
+           None files
+  in
+  let open Cmdliner in
+  let files =
+    Arg.(value & pos_all string [] & info [] ~docv:"files" ~doc:"files to read")
+  and prover =
+    Arg.(
+      value & opt prover_conv Z3_prover
+      & info [ "p"; "prover" ] ~doc:"SMT solver to use" )
+  and incremental =
+    Arg.(
+      value & flag
+      & info [ "incremental" ] ~doc:"Use the SMT solver in the incremental mode" )
+  and debug =
+    Arg.(value & flag & info [ "debug" ] ~doc:"Print debugging messages")
+  in
+  Cmd.v
+    (Cmd.info "smtml" ~version:"%%VERSION%%")
+    Term.(const aux $ files $ prover $ incremental $ debug)
 
 let () =
-  Printexc.record_backtrace true;
-  exit @@ Cmd.eval cli
+  match Cmdliner.Cmd.eval_value parse_cmdline with
+  | Error (`Parse | `Term | `Exn) -> exit 2
+  | Ok (`Ok () | `Version | `Help) -> ()

dune-project

@@ -25,6 +25,7 @@
    (ocaml (>= "4.14.0"))
    ocaml_intrinsics
    (z3 (and (>= "4.12.2") (< "4.13")))
+   colibri2
    (menhir
     (and
     :build

encoding.opam

@@ -13,6 +13,7 @@ depends: [
   "ocaml" {>= "4.14.0"}
   "ocaml_intrinsics"
   "z3" {>= "4.12.2" & < "4.13"}
+  "colibri2"
   "menhir" {build & >= "20220210"}
   "cmdliner" {>= "1.2.0"}
   "zarith" {>= "1.5"}
@@ -36,3 +37,7 @@ build: [
 ]
 dev-repo: "git+https://github.com/formalsec/encoding.git"
 available: (arch = "x86_64" | arch = "arm64") & os != "win32" & arch != "x86_32"
+pin-depends: [
+  [ "colibri2.0.4.0" "git+https://git.frama-c.com/pub/colibrics.git#5.1.0"]
+  [ "colibrilib.0.4.0" "git+https://git.frama-c.com/pub/colibrics.git#5.1.0"]
+]

encoding.opam.template

@@ -1 +1,5 @@
 available: (arch = "x86_64" | arch = "arm64") & os != "win32" & arch != "x86_32"
+pin-depends: [
+  [ "colibri2.0.4.0" "git+https://git.frama-c.com/pub/colibrics.git#5.1.0"]
+  [ "colibrilib.0.4.0" "git+https://git.frama-c.com/pub/colibrics.git#5.1.0"]
+]