Rework property language and restructure code.

config.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of Caisar.                                          *)
+(*                                                                        *)
+(**************************************************************************)
+
+open Base
+
+module Format = Caml.Format
+module Sys = Caml.Sys
+module Filename = Caml.Filename
+
+type version =
+  | Unknown
+  | Version of string
+[@@deriving show { with_path = false }, yojson]
+
+type t = {
+  name: string;
+  exe: string;
+  version: version;
+}
+[@@deriving yojson, show]
+
+type full_config = t list [@@deriving yojson, show]
+
+let exe_path_of_solver solver =
+  let module S = (val solver: Solver.S) in
+  (* We want the complete path of [exe] in $PATH: we use `command -v [exe]'
+     and retrieve the result, if any. *)
+  let tmp = Filename.temp_file "caisar" "command" in
+  let _retcode =
+    Sys.command
+      (Filename.quote_command
+         ~stdout:tmp ~stderr:tmp
+         "command" ["-v"; S.exe_name])
+  in
+  let in_channel = Stdlib.open_in tmp in
+  let found, exe =
+    try true, Stdlib.input_line in_channel
+    with End_of_file -> false, S.exe_name
+  in
+  Stdlib.close_in in_channel;
+  Sys.remove tmp;
+  if found
+  then Ok exe
+  else begin
+    match Sys.getenv_opt "DIR" with
+    | None ->
+      Error (Format.asprintf "Cannot find the executable of `%s'." S.name)
+    | Some dir ->
+      (* The env variable should already provide the path to the executable: we
+         first check that the path exists, refers to a directory and it is
+         absolute, then we concatenate the [exe] name to it. *)
+      if not (Sys.file_exists dir && Sys.is_directory dir)
+      then
+        Error (Format.sprintf "`%s' not exist or is not a directory." dir)
+      else
+      if Filename.is_relative dir
+      then
+        Error
+          (Format.sprintf
+             "`%s' is a relative path. An absolute path is required for DIR."
+             dir)
+      else
+        let exe =
+          if Filename.check_suffix dir Filename.dir_sep
+          then dir ^ exe
+          else Format.sprintf "%s%s%s" dir Filename.dir_sep exe
+        in
+        Ok exe
+  end
+
+let version_of_solver solver s =
+  let module S = (val solver: Solver.S) in
+  try
+    (* We suppose that the first occurrence that matches [re_version] is indeed
+       the version of the concercend [solver]. *)
+    ignore (Str.search_forward S.re_version s 0);
+    Version (Str.matched_string s)
+  with Stdlib.Not_found ->
+    Logs.debug (fun m -> m "No recognizable version found.");
+    Unknown
+
+let default_config_file =
+  let filename = ".caisar.conf" in
+  match Sys.getenv_opt "HOME" with
+  | None -> filename
+  | Some p -> p ^ "/.caisar.conf"
+
+let retrieve_full_config file =
+  let open Result in
+  match full_config_of_yojson (Yojson.Safe.from_file file) with
+  | Error _ | exception _ ->
+    []
+  | Ok full_config ->
+    begin
+      Logs.debug (fun m ->
+          m "Configuration in file `%s':@ %a"
+            file
+            pp_full_config full_config);
+      full_config
+    end
+
+let retrieve ~file solver =
+  let open Result in
+  let module S = (val solver: Solver.S) in
+  Logs.info (fun m ->
+      m "Reading configuration file `%s' for solver `%s'." file S.name);
+  if not (Sys.file_exists file)
+  then Error (Format.sprintf "Configuration file `%s' not exist." file)
+  else begin
+    (* Read all solver configs present in the given configuration file. *)
+    let full_config = retrieve_full_config file in
+    (* Search for a [config] with [solver]. *)
+    match List.find ~f:(fun cs -> String.equal cs.name S.name) full_config with
+    | None ->
+      Error
+        (Format.asprintf
+           "No solver `%s' found in configuration file `%s'."
+           S.name file)
+    | Some ({ name; version; _ } as config) ->
+      begin
+        Logs.info (fun m -> m "Found `%s' `%s'." name (show_version version));
+        Ok config
+      end
+  end
+
+(* All solver instances. *)
+let default_solvers =
+  [ (module Pyrat: Solver.S); (module Marabou: Solver.S) ]
+
+let detect_default_solvers () =
+  try
+    let config =
+      List.filter_map
+        ~f:(fun solver ->
+            match exe_path_of_solver solver with
+            | Error msg ->
+              Logs.info (fun m -> m "%s" msg);
+              None
+            | Ok exe ->
+              (* We detect whether solver is available in $PATH, or in the
+                 provided path via env variable, by executing `solver
+                 --version' command. *)
+              let module S = (val solver: Solver.S) in
+              let tmp = Filename.temp_file "caisar" "detect" in
+              let cmd =
+                Filename.quote_command
+                  ~stdout:tmp ~stderr:tmp
+                  exe
+                  [S.exe_default_option]
+              in
+              Logs.debug (fun m ->
+                  m "Executing command `%s' to detect `%s'."
+                    cmd S.name);
+              let retcode = Sys.command cmd in
+              let cmd_output =
+                let in_channel = Stdlib.open_in tmp in
+                let buf = Buffer.create 512 in
+                try
+                  while true do
+                    Stdlib.Buffer.add_channel buf in_channel 512;
+                  done;
+                  assert false
+                with End_of_file ->
+                  Stdlib.close_in in_channel;
+                  Buffer.contents buf
+              in
+              Sys.remove tmp;
+              if retcode <> 0
+              then begin
+                Logs.info (fun m -> m "No solver `%s' found." S.name);
+                None
+              end
+              else begin
+                (* If available, we save a [config] for solver. *)
+                let version = version_of_solver solver cmd_output in
+                let config = { name = S.name; exe; version; } in
+                Logs.app (fun m ->
+                    m "Found solver `%s' `%a' (%s)."
+                      S.name
+                      pp_version version
+                      exe);
+                Some config
+              end)
+        default_solvers
+    in
+    Ok config
+  with _ ->
+    Error "Unexpected failure."
+
+let detect ~file =
+  let open Result in
+  (* Detect default supported solvers in $PATH or $DIR. *)
+  detect_default_solvers () >>= fun default_full_config ->
+  (* Retrieve the current configuration from [file]. *)
+  let current_full_config = retrieve_full_config file in
+  (* Create new configuration file. *)
+  Logs.debug (fun m -> m "Creating new configuration file `%s'." file);
+  let out_channel = Stdlib.open_out file in
+  (* Build [full_config] by first appending [default_full_config] to
+     [current_full_config], and then deduping the result. *)
+  let full_config =
+    (* TODO: This comparison is not optimal but sufficient as long as we register
+       solver as simply as done in [detect_default_solvers]. *)
+    let compare cs1 cs2 = String.compare cs1.name cs2.name in
+    List.dedup_and_sort
+      ~compare
+      (List.append current_full_config default_full_config)
+  in
+  (* We write all solver configs in the configuration file, as JSON data. *)
+  let full_config_json = full_config_to_yojson full_config in
+  Yojson.Safe.pretty_to_channel out_channel full_config_json;
+  Stdlib.close_out out_channel;
+  Ok ()

config.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of Caisar.                                          *)
+(*                                                                        *)
+(**************************************************************************)
+
+type version =
+  | Unknown
+  | Version of string
+
+type t = private {
+  name: string;
+  exe: string;
+  version: version;
+}
+
+(** Path to default configuration file. *)
+val default_config_file: string
+
+(** The list of supported solvers by default. *)
+val default_solvers: Solver.instance list
+
+(** [detect ~file] searches for solvers in $PATH, or in the path provided in env
+    variable $DIR, and save the configurations in [file]. *)
+val detect: file:string -> (unit, string) Result.t
+
+(** @return the [solver] configuration, if any, from the given [file]. *)
+val retrieve: file:string -> Solver.instance -> (t, string) Result.t

dune

@@ -2,11 +2,12 @@
   (modules property_lexer))
 
 (menhir
-  (modules property_parser))
+  (modules property_parser)
+  (flags --table))
 
 (executable
   (name main)
   (public_name caisar)
-  (modules_without_implementation property_syntax)
-  (libraries yojson cmdliner logs logs.cli logs.fmt fmt.tty base unix str ppx_deriving_yojson.runtime)
+  (modules_without_implementation property_types)
+  (libraries menhirLib yojson cmdliner logs logs.cli logs.fmt fmt.tty base unix str ppx_deriving_yojson.runtime)
   (preprocess (pps ppx_deriving_yojson ppx_deriving.show ppx_deriving.ord ppx_deriving.eq)))

engine.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of Caisar.                                          *)
+(*                                                                        *)
+(**************************************************************************)
+
+open Base
+open Property_types
+
+module Format = Caml.Format
+module Sys = Caml.Sys
+module Filename = Caml.Filename
+
+(* Verification task submitted to a solver. *)
+type task = {
+  (* Identifier. *)
+  id: string;
+  (* Original goal name. *)
+  goalname: string;
+  (* Subgoal identifier.
+     Typically a goal is translated to multiple subgoals by a solver. *)
+  subgoal: int;
+  (* The formula to verify. *)
+  formula: string;
+  (* Verification result.
+     [None] means no verification yet. *)
+  result: (Solver.Result.t, string) Result.t option;
+}
+
+let check_availability solver config =
+  let module S = (val solver: Solver.S) in
+  Logs.debug (fun m -> m "Checking actual availability of `%s'." S.name);
+  try
+    (* Execute command `solver --version' to check actual availability. *)
+    let tmp = Filename.temp_file "caisar" "avail" in
+    let cmd =
+      Filename.quote_command
+        ~stdout:tmp ~stderr:tmp
+        config.Config.exe
+        [S.exe_default_option]
+    in
+    Logs.debug (fun m ->
+        m "Executing command `%s' to check `%s' availability." cmd S.name);
+    let retcode = Sys.command cmd in
+    let in_channel = Stdlib.open_in tmp in
+    Stdlib.close_in in_channel;
+    Sys.remove tmp;
+    if retcode = 0
+    then
+      Ok ()
+    else
+      Error
+        (Format.sprintf
+           "Command `%s' failed. \
+            Try to launch the configuration process again."
+           cmd)
+  with Stdlib.Not_found | End_of_file | Failure _ | Sys_error _ ->
+    Error "Unexpected failure."
+
+let check_compatibility solver model =
+  let module S = (val solver: Solver.S) in
+  if S.is_model_format_supported model.Model.format
+  then Ok ()
+  else
+    Error
+      (Format.asprintf
+         "No support yet for `%s' and model format `%s'."
+         S.name
+         (Model.show_format model.format))
+
+let tasks_of_property solver { hypothesis; goals } =
+  let module S = (val solver: Solver.S) in
+  let table = Hashtbl.create (module String) in
+  List.iter
+    goals
+    ~f:(fun { name; formula; } ->
+        let elts = S.(repr (translate ~hypothesis ~goal:formula)) in
+        let tasks =
+          List.mapi
+            elts
+            ~f:(fun idx elt ->
+                { id = Format.sprintf "%s.%d" name idx;
+                  goalname = name;
+                  subgoal = idx;
+                  formula = Format.asprintf "%a" S.pretty elt;
+                  result = None; })
+        in
+        Hashtbl.set table ~key:name ~data:tasks);
+  table
+
+let build_command ~raw_options solver config model task =
+  let open Result in
+  let module S = (val solver: Solver.S) in
+  (* Write property to temporary file. *)
+  begin
+    try
+      let tmp = Filename.temp_file "prop" S.name in
+      let out_channel = Stdlib.open_out tmp in
+      let fmt = Format.formatter_of_out_channel out_channel in
+      Format.fprintf fmt "%s@?" task.formula;
+      Stdlib.close_out out_channel;
+      Ok tmp
+    with Sys_error e ->
+      Error (Format.sprintf "Unexpected failure:@ %s." e)
+  end >>= fun property ->
+  (* Build actual command-line. *)
+  try
+    let log = Filename.temp_file "log" S.name in
+    let output = Filename.temp_file "output" S.name in
+    let options = S.options ~model:model.Model.filename ~property ~output in
+    let command =
+      let args = options @ raw_options in
+      Filename.quote_command ~stdout:log ~stderr:log config.Config.exe args
+    in
+    Ok (command, property, log, output)
+  with Failure e ->
+    Error (Format.sprintf "Unexpected failure:@ %s." e)
+
+let extract_result solver ~log ~output =
+  let module S = (val solver: Solver.S) in
+  Logs.info (fun m -> m "Extracting result of verification.");
+  let output =
+    let content file =
+      let in_channel = Stdlib.open_in file in
+      let buf = Buffer.create 512 in
+      try
+        while true do
+          Stdlib.Buffer.add_channel buf in_channel 512;
+        done;
+        assert false
+      with End_of_file ->
+        Stdlib.close_in in_channel;
+        buf
+    in
+    let output = content output in
+    if Buffer.length output > 0
+    then output
+    else content log
+  in
+  let output = Buffer.contents output in
+  let results = [ Solver.Result.Valid; Invalid; Timeout; Unknown ] in
+  List.fold
+    results
+    ~init:Solver.Result.Failure
+    ~f:(fun acc result ->
+        let regexp = S.re_of_result result in
+        let found =
+          try Str.search_forward regexp output 0 >= 0
+          with Stdlib.Not_found -> false
+        in
+        if found
+        then result
+        else acc)
+
+let exec_tasks ~raw_options solver config model tasks_htbl =
+  let module S = (val solver: Solver.S) in
+  let open Result in
+  Logs.app (fun m -> m "Launching verification with `%s'." S.name);
+  (* Run one task at a time and modify its status. *)
+  Hashtbl.map_inplace
+    tasks_htbl
+    ~f:(fun tasks ->
+        List.map
+          tasks
+          ~f:(fun task ->
+              Logs.app (fun m ->
+                  m "Verifying goal `%s', subgoal %d (%s)."
+                    task.goalname task.subgoal task.id);
+              let res_exec_task =
+                (* Build the required command-line. *)
+                build_command ~raw_options solver config model task
+                >>= fun (cmd, prop, log, output) ->
+                (* Execute the command. *)
+                Logs.info (fun m -> m "Executing command `%s'." cmd);
+                try
+                  let retcode = Sys.command cmd in
+                  Sys.remove prop;
+                  if retcode <> 0
+                  then Error (Format.sprintf "Command `%s' has failed." cmd)
+                  else begin
+                    (* Extract and pretty-print verification result. *)
+                    let result = extract_result solver ~log ~output in
+                    Logs.app (fun m -> m "Result %s: %a."
+                                 task.id Solver.Result.pretty result);
+                    Sys.remove output;
+                    if Solver.Result.equal result Solver.Result.Failure
+                    then
+                      Logs.app (fun m ->
+                          m "See error messages in `%s' for more information."
+                            log)
+                    else
+                      Sys.remove log;
+                    Ok result
+                  end
+                with _ ->
+                  Error "Unexpected failure."
+              in
+              { task with result = Some res_exec_task; }));
+  tasks_htbl
+
+let consolidate_task_results solver tasks_htbl =
+  let module S = (val solver: Solver.S) in
+  Hashtbl.map
+    tasks_htbl
+    ~f:(fun tasks ->
+        let consolidated_result =
+          List.fold tasks ~init:None
+            ~f:(fun accum { result; _ } ->
+                let result =
+                  match result with
+                  | None -> None
+                  | Some Ok result -> Some result
+                  | Some Error _ -> Some Failure
+                in
+                match accum, result with
+                | _, None -> accum
+                | None, result -> result
+                | Some r1, Some r2 -> Some (S.consolidate r1 r2))
+        in
+        consolidated_result, tasks)
+
+let pretty_summary tasks_htbl =
+  let pretty_task_status fmt { id; result; _ } =
+    let result = Option.value_exn result in
+    let result_string =
+      match result with
+      | Ok r -> Format.asprintf "%a" Solver.Result.pretty r
+      | Error msg -> msg
+    in
+    Format.fprintf fmt "@[-- %s: @[<hov>%s@]@]" id result_string
+  in
+  let pretty_goal_tasks fmt (goalname, (consolidated_result, tasks)) =
+    Format.fprintf fmt "@[- %s: @[<v>%a@ %a@]@]"
+      goalname
+      Solver.Result.pretty (Option.value_exn consolidated_result)
+      (Format.pp_print_list ~pp_sep:Format.pp_print_space pretty_task_status)
+      tasks
+  in
+  Logs.app (fun m ->
+      m "@[<v 2>Summary:@ %a@]"
+        (Format.pp_print_list ~pp_sep:Format.pp_print_space pretty_goal_tasks)
+        (Hashtbl.to_alist tasks_htbl))
+
+let exec ~raw_options solver config model property =
+  let open Result in
+  let module S = (val solver: Solver.S) in
+  (* Check solver availability. *)
+  check_availability solver config >>= fun () ->
+  (* Check solver and model compatibility. *)
+  check_compatibility solver model >>= fun () ->
+  (* Translate property into tasks. *)
+  tasks_of_property solver property |>
+  (* Run verification process. *)
+  exec_tasks ~raw_options solver config model |>
+  (* Consolidate task results for every goal. *)
+  consolidate_task_results solver |>
+  (* Pretty print a summary on results. *)
+  pretty_summary |> fun () ->
+  Ok ()

engine.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of Caisar.                                          *)
+(*                                                                        *)
+(**************************************************************************)
+
+(** [exec ~raw_options config model property] runs a solver wrt the given
+    [config] on [property] for [model] with the provided [raw_options]. *)
+val exec:
+  raw_options:string list ->
+  Solver.instance -> Config.t -> Model.t -> Property.t -> (unit, string) Result.t

main.ml

@@ -6,6 +6,7 @@
 
 open Base
 open Cmdliner
+
 module Format = Caml.Format
 
 let caisar = "caisar"
@@ -50,23 +51,24 @@ let config cmd detect file () =
     (fun m -> m "Command `%s' with configuration file `%s'." cmd file);
   if detect
   then begin
-    match Solver.detect ~file with
+    match Config.detect ~file with
     | Ok () -> Logs.app (fun m -> m "Configuration saved in `%s'." file)
     | Error e -> Logs.err (fun m -> m "%s" e)
   end
 
 let verify cmd raw_options config_file model property solver () =
+  let module S = (val solver: Solver.S) in
   Logs.debug
     (fun m ->
        m "Command `%s' with@ model `%s',@ property `%s' and@ solver `%s' \
           (using configuration file `%s')."
-         cmd model property (Solver.show_solver solver) config_file);
+         cmd model property S.name config_file);
   let do_verify () =
     let open Result in
     Model.build ~filename:model >>= fun model ->
     Property.build ~filename:property >>= fun property ->
-    Solver.get_config solver ~file:config_file >>= fun config ->
-    Solver.exec ~raw_options config model property
+    Config.retrieve ~file:config_file solver >>= fun config ->
+    Engine.exec ~raw_options solver config model property
   in
   match do_verify () with
   | Ok () -> Logs.app (fun m -> m "Done.")
@@ -95,7 +97,7 @@ let config_cmd =
     let doc =
       Format.sprintf "$(b,FILE) to write the %s configuration to." caisar
     in
-    Arg.(value & pos 0 string Solver.default_config_file
+    Arg.(value & pos 0 string Config.default_config_file
          & info [] ~docv:docv_filename ~doc)
   in
   let doc = Format.sprintf "%s configuration." caisar in
@@ -120,7 +122,11 @@ let verify_cmd =
   let docv_solver = "SOLVER" in
   let solver =
     let solver_names =
-      List.map ~f:(fun s -> String.lowercase (Solver.show s)) Solver.defaults
+      List.map
+        Config.default_solvers
+        ~f:(fun solver ->
+            let module S = (val solver: Solver.S) in
+            String.lowercase S.name)
     in
     let doc =
       Format.asprintf
@@ -134,11 +140,13 @@ let verify_cmd =
     let solvers =
       Arg.enum
         (List.map
-           ~f:(fun s -> String.lowercase (Solver.show_solver s), s)
-           Solver.defaults)
+           Config.default_solvers
+           ~f:(fun solver ->
+               let module S = (val solver: Solver.S) in
+               String.lowercase S.name, solver))
     in
     Arg.(required
-         & pos 2 (some solvers) (Some Solver.Pyrat)
+         & pos 2 (some solvers) (Some (module Pyrat: Solver.S))
          & info [] ~docv:docv_solver ~doc)
   in
   let docv_model = "MODEL" in
@@ -158,7 +166,7 @@ let verify_cmd =
   in
   let config_filename =
     let doc = "$(b,FILE) to read the configuration from." in
-    Arg.(value & opt file Solver.default_config_file
+    Arg.(value & opt file Config.default_config_file
          & info ["c"; "config"] ~doc)
   in
   let doc = "Property verification of neural networks." in

marabou.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of Caisar.                                          *)
+(*                                                                        *)
+(**************************************************************************)
+
+open Property_types
+
+type t = Property.disjunct Property.nform
+
+let name = "Marabou"
+let exe_name = "Marabou"
+let exe_default_option = "--version"
+let re_version = Str.regexp "[0-9]\\(\\.[0-9]\\)*\\(\\.?[A-Za-z-+]\\)*"
+
+let re_of_result result =
+  Str.regexp
+    (match result with
+     | Solver.Result.Valid -> "\\(s\\|S\\)at\\|SAT"
+     | Invalid -> "\\(u\\|U\\)nsat\\|UNSAT"
+     | Timeout -> "\\(t\\|T\\)imeout\\|TIMEOUT"
+     | Unknown -> "\\(u\\|U\\)nknown\\|UNKNOWN"
+     | Failure -> assert false)
+
+let is_model_format_supported = function
+  | Model.Nnet _ -> true
+  | Onnx -> false
+
+let options ~model ~property ~output =
+  let verbosity_level =
+    match Logs.level () with
+    | None | Some (App | Error | Warning) -> 0
+    | Some Info -> 1
+    | Some Debug -> 2
+  in
+  [ "--property";  property;
+    "--input"; model;
+    "--verbosity"; Int.to_string verbosity_level;
+    "--summary-file"; output ]
+
+let consolidate r1 r2=
+  match r1, r2 with
+  | _, Solver.Result.Valid | Solver.Result.Valid, _ -> Solver.Result.Valid
+  | Invalid, result | result, Invalid -> result
+  | Failure, _ | _, Failure -> Failure
+  | Timeout, _ | _, Timeout -> Timeout
+  | Unknown, Unknown -> Unknown
+
+(* Transform [k_y_0 + ky_1 + ... + ky_n cop ky_n+1] into [ky_n+1 + k_y_0 +
+   ky_1 + ... + ky_n cop 0], taking care of the sign. *)
+let rec constant_rhs formula =
+  match formula with
+  | Constraint (terms, cop, General (sign_opt, cst_opt, var)) ->
+    let terms =
+      match sign_opt, cst_opt with
+      | _, Some Int i when i = 0 -> terms
+      | _, Some Float f when Base.Float.(=) f 0. -> terms
+      | (None | Some Plus), None ->
+        General (Some Minus, None, var) :: terms
+      | (None | Some Plus), Some cst ->
+        let negcst =
+          match cst with
+          | Int i -> Int (~- i)
+          | Float f -> Float (~-. f)
+        in
+        General (Some Plus, Some negcst, var) :: terms
+      | Some Minus, _ ->
+        General (Some Plus, cst_opt, var) :: terms
+    in
+    Constraint (terms, cop, Constant (Int 0))
+  | Constraint (_, _, Constant _) ->
+    formula
+  | And (p1, p2) ->
+    And (constant_rhs p1, constant_rhs p2)
+  | Or (p1, p2) ->
+    Or (constant_rhs p1, constant_rhs p2)
+
+let translate ~hypothesis ~goal =
+  let goal = constant_rhs goal in
+  Property.dnf_of_formula (And (hypothesis, goal))
+
+let repr = Property.get_disjuncts
+
+let pretty fmt t =
+  let pp_terms fmt terms =
+    match terms with
+    | [] ->
+      assert false (* Terms are non-empty lists by construction. *)
+    | [ t ] ->
+      Property.pretty_term fmt t
+    | t :: tt ->
+      let pp_term = Property.pretty_term ~pp_sign:true in
+      Format.fprintf fmt "@[%a %a@]"
+        pp_term t
+        (Format.pp_print_list
+           ~pp_sep:(fun fmt () -> Format.pp_print_char fmt ' ')
+           pp_term) tt
+  in
+  let rec pp_formula fmt formula =
+    match formula with
+    | Constraint (terms, cop, term) ->
+      Format.fprintf fmt "%a %a %a"
+        pp_terms terms
+        Property.pretty_cop cop
+        (Property.pretty_term ~pp_sign:true) term
+    | And (p1, p2) ->
+      Format.fprintf fmt "%a@\n%a" pp_formula p1 pp_formula p2
+    | Or _ ->
+      (* Marabou does not handle Or connectives directly. Anyway, it should
+         not happen as in [translate] we convert the original goal into a
+         dnf-like form where we retrieve only the final conjuncts. *)
+      assert false
+  in
+  Format.fprintf fmt "@[%a@]" pp_formula t

property_syntax.mli → marabou.mli

@@ -4,17 +4,4 @@
 (*                                                                        *)
 (**************************************************************************)
 
-type var =
-  | Input of string
-  | Output of string
-
-type cop = Eq | Ge | Le | Gt | Lt
-
-type cst =
-  | Int of int
-  | Float of float
-
-type t =
-  | Atomic_cst of var * cop * cst
-  | Atomic_var of var * cop * var
-  | And of t * t
+include Solver.S

model.ml

@@ -5,6 +5,7 @@
 (**************************************************************************)
 
 open Base
+
 module Format = Caml.Format
 module Sys = Caml.Sys
 module Filename = Caml.Filename

property.ml

@@ -5,66 +5,64 @@
 (**************************************************************************)
 
 open Base
+open Property_types
+
 module Format = Caml.Format
 module Sys = Caml.Sys
+module Lexer = Property_lexer
+module Parser = Property_parser
+module MI = Parser.MenhirInterpreter
+module ER = MenhirLib.ErrorReports
+module LU = MenhirLib.LexerUtil
 
-type t = Property_syntax.t
-
-let do_build ~property line =
-  let linebuf = Lexing.from_string line in
-  try
-    let p = Property_parser.main Property_lexer.token linebuf in
-    let property =
-      Option.value_map
-        property
-        ~default:p
-        ~f:(fun p' -> Property_syntax.And (p', p))
-    in
-    Ok property
+type t = Property_types.t
+type 'a printer = Caml.Format.formatter -> 'a -> unit
+
+(* [show text (pos1, pos2)] displays a range of the input text [text]
+   delimited by the positions [pos1] and [pos2]. *)
+let show text positions =
+  ER.extract text positions
+  |> ER.sanitize
+  |> ER.compress
+  |> ER.shorten 20 (* max width 43 *)
+
+(* The parser has succeeded and produced a property. *)
+let succeed (property: t) =
+  Ok property
+
+(* The parser has encountered a syntax error. *)
+let fail text buffer (_ : t MI.checkpoint) =
+  (* Indicate where in the input file the error occurred. *)
+  let location = LU.range (ER.last buffer) in
+  (* Show the tokens just before and just after the error. *)
+  let indication =
+    Format.sprintf "Syntax error %s." (ER.show (show text) buffer)
+  in
+  (* Show these three components. *)
+  Error (Format.sprintf "%s%s" location indication)
+
+let build ~filename =
+  (* Read the file; allocate and initialize a lexing buffer. *)
+  let text, lexbuf = LU.read filename in
+  (* Wrap the lexer and lexbuf together into a supplier, that is, a
+     function of type [unit -> token * position * position]. *)
+  let supplier = MI.lexer_lexbuf_to_supplier Lexer.token lexbuf in
+  (* Equip the supplier with a two-place buffer that records the positions
+     of the last two tokens. This is useful when a syntax error occurs, as
+     these are the token just before and just after the error. *)
+  let buffer, supplier = ER.wrap_supplier supplier in
+  (* Fetch the parser's initial checkpoint. *)
+  let checkpoint = Parser.Incremental.main lexbuf.lex_curr_p in
+  (* Run the parser. *)
+  try MI.loop_handle succeed (fail text buffer) supplier checkpoint
   with
   | Property_lexer.Error msg ->
     Error (Format.sprintf "%s" msg)
-  | Property_parser.Error ->
-    Error
-      (Format.sprintf
-         "Property syntax error at offset %d."
-         (Lexing.lexeme_start linebuf))
 
-let build ~filename =
-  if Sys.file_exists filename
-  then
-    let in_channel = Stdlib.open_in filename in
-    let rec read_one_line ~property channel =
-      let line_opt, continue = Property_lexer.line channel in
-      if not continue
-      then begin
-        Stdlib.close_in in_channel;
-        Result.of_option
-          property
-          ~error:(Format.sprintf "No property found in `%s'." filename)
-      end
-      else begin
-        let property_or_error =
-          (* Since [continue] is true, there is a line by lexer construction. *)
-          let line = Option.value_exn line_opt in
-          do_build ~property line
-        in
-        Result.join
-          (Result.map
-             property_or_error
-             ~f:(fun p -> read_one_line ~property:(Some p) channel))
-      end
-    in
-    read_one_line ~property:None (Lexing.from_channel in_channel)
-  else
-    Error (Format.sprintf "No such file `%s'." filename)
-
-let rec repr t =
-  let open Property_syntax in
-  let string_of_var = function
-    | Input s -> Format.sprintf "Input %s" s
-    | Output s -> Format.sprintf "Output %s" s
-  in
+
+(* Printing. *)
+
+let pretty_cop fmt cop =
   let string_of_cop = function
     | Eq -> "="
     | Ge -> ">="
@@ -72,23 +70,134 @@ let rec repr t =
     | Gt -> ">"
     | Lt -> "<"
   in
-  let string_of_cst = function
-    | Int i -> Format.sprintf "int %d" i
-    | Float f -> Format.sprintf "float %f" f
-  in
-  match t with
-  | Atomic_cst (var, cop, cst) ->
-    let var_s = string_of_var var in
-    let cop_s = string_of_cop cop in
-    let cst_s = string_of_cst cst in
-    Format.sprintf "%s %s %s" var_s cop_s cst_s
-  | Atomic_var (var1, cop, var2) ->
-    let var1_s = string_of_var var1 in
-    let cop_s = string_of_cop cop in
-    let var2_s = string_of_var var2 in
-    Format.sprintf "%s %s %s" var1_s cop_s var2_s
+  Format.pp_print_string fmt (string_of_cop cop)
+
+let pretty_var fmt = function
+  | Input s | Output s -> Format.pp_print_string fmt s
+
+let pretty_cst fmt = function
+  | Int i -> Format.fprintf fmt "%d" i
+  | Float f -> Format.fprintf fmt "%f" f
+
+let pretty_term ?(pp_sign=false) fmt = function
+  | Constant cst ->
+    pretty_cst fmt cst
+  | General (sign_opt, cst_opt, var) ->
+    begin match sign_opt, cst_opt with
+      | _, Some Int i when i = 0 -> ()
+      | _, Some Float f when Float.(=) f 0. -> ()
+      | (None | Some Plus), None ->
+        Format.fprintf fmt "@[%s%a@]"
+          (if not pp_sign then "" else "+")
+          pretty_var var
+      | (None | Some Plus), Some cst ->
+        let is_cst_negative =
+          match cst with
+          | Int i -> Int.is_negative i
+          | Float f -> Float.is_negative f
+        in
+        Format.fprintf fmt "@[%s%a%a@]"
+          (if not pp_sign || is_cst_negative then "" else "+")
+          pretty_cst cst
+          pretty_var var
+      | Some Minus, None ->
+        Format.fprintf fmt "@[-%a@]" pretty_var var
+      | Some Minus, Some cst ->
+        let negcst, is_negcst_negative =
+          match cst with
+          | Int i -> Int (~- i), i > 0
+          | Float f -> Float (~-. f), Float.(>) f 0.
+        in
+        Format.fprintf fmt "@[%s%a%a@]"
+          (if not pp_sign || is_negcst_negative then "" else "+")
+          pretty_cst negcst
+          pretty_var var
+    end
+
+let pretty_terms pp_term fmt terms =
+  match terms with
+  | [] ->
+    assert false (* Terms are non-empty lists by construction. *)
+  | [ t ] ->
+    pp_term fmt t
+  | t :: tt ->
+    Format.fprintf fmt "@[%a %a@]"
+      pp_term t
+      (Format.pp_print_list
+         ~pp_sep:(fun fmt () -> Format.pp_print_char fmt ' ')
+         pp_term) tt
+
+let rec pretty_formula fmt formula =
+  match formula with
+  | Constraint ([], _, _) ->
+    (* Non-empty list by construction. *)
+    assert false
+  | Constraint (terms, cop, term) ->
+    Format.fprintf fmt "@[%a %a %a@]"
+      (pretty_terms pretty_term) terms
+      pretty_cop cop
+      (pretty_term ~pp_sign:false) term
   | And (p1, p2) ->
-    Format.sprintf "And (%s, %s)" (repr p1) (repr p2)
+    Format.fprintf fmt "@[%a@ &&@ %a@]" pretty_formula p1 pretty_formula p2
+  | Or (p1, p2) ->
+    Format.fprintf fmt "@[%a@ ||@ %a@]" pretty_formula p1 pretty_formula p2
+
+let pretty_goal fmt goal =
+  Format.fprintf fmt "@[<v 2>goal %s:@ @[<hov>%a@]@]"
+    goal.name
+    pretty_formula goal.formula
 
 let pretty fmt t =
-  ignore (fmt, t)
+  Format.fprintf fmt "@[%a@]@\n@[<v>%a@]"
+    pretty_formula t.hypothesis
+    (Format.pp_print_list pretty_goal) t.goals
+
+
+(* Normal forms. *)
+
+type conjunct = formula
+type disjunct = formula
+type 'a nform = formula list
+
+let combine ~f f1 f2 =
+  if List.is_empty f1 || List.is_empty f2
+  then assert false
+  else begin
+    let rec loop (l1: formula list) l2 acc =
+      match l1 with
+      | [] ->
+        acc
+      | t :: tt ->
+        loop tt l2 List.(rev_append (map ~f:(fun x -> f t x) l2) acc)
+    in
+    List.rev (loop f1 f2 [])
+  end
+
+let rec convert_to_nf ~and_ ~or_ formula =
+  match formula with
+  | Constraint _ ->
+    [ formula ]
+  | And (p1, p2) ->
+    and_ (convert_to_nf ~and_ ~or_ p1) (convert_to_nf ~and_ ~or_ p2)
+  | Or (p1, p2) ->
+    or_ (convert_to_nf ~and_ ~or_ p1) (convert_to_nf ~and_ ~or_ p2)
+
+let cnf_of_formula (formula: formula) =
+  let and_ = function
+    | [] -> assert false
+    | [ _ ] as f -> f
+    | t :: tt -> [ List.fold tt ~init:t ~f:(fun acc f -> And (acc, f)) ]
+  in
+  convert_to_nf
+    ~and_:(fun l1 l2 -> and_ (List.append l1 l2))
+    ~or_:(combine ~f:(fun x y -> Or (x, y)))
+    formula
+
+let dnf_of_formula (formula: formula) =
+  convert_to_nf
+    ~and_:(combine ~f:(fun x y -> And (x, y)))
+    ~or_:List.append
+    formula
+
+let get_conjuncts = Fn.id
+let get_disjuncts = Fn.id

property.mli

@@ -5,15 +5,47 @@
 (**************************************************************************)
 
 open Base
+open Property_types
 
-(** A property. *)
-type t = Property_syntax.t
+type t = Property_types.t
 
 (** Builds a property out of the content of the given [filename], if possible. *)
 val build: filename:string -> (t, string) Result.t
 
-(** Provides the raw representation of the given property. *)
-val repr: t -> string
+(** {2 Pretty printing.} *)
+
+type 'a printer = Caml.Format.formatter -> 'a -> unit
+
+(** Comparison operator pretty printer. *)
+val pretty_cop: cop printer
+
+(** Variable pretty printer. *)
+val pretty_var: var printer
+
+(** Constant pretty printer. *)
+val pretty_cst: constant printer
+
+(** Term pretty printer.
+    @param pp_sign determines whether the printer should print the sign also
+    for monomial terms.
+*)
+val pretty_term: ?pp_sign:bool -> term printer
+
+(** Term list pretty printer given one for a term. *)
+val pretty_terms: term printer -> term list printer
 
 (** [pretty property] pretty prints [property]. *)
 val pretty: Caml.Format.formatter -> t -> unit
+
+
+(** {2 Normal forms.} *)
+
+type conjunct
+type disjunct
+type 'a nform
+
+val cnf_of_formula: formula -> conjunct nform
+val dnf_of_formula: formula -> disjunct nform
+
+val get_conjuncts: conjunct nform -> formula list
+val get_disjuncts: disjunct nform -> formula list

property_lexer.mll

@@ -11,35 +11,49 @@
 let input = 'x'['0'-'9']+
 let output = 'y'['0'-'9']+
 
-(* This rule looks for a single line, terminated with '\n' or eof. It returns a
-   pair of an optional string, the line that was found, and a Boolean flag,
-   false if eof was reached. *)
-
-rule line = parse
-| ([^'\n']* '\n') as line
-    (* Normal case: one line, no eof. *)
-    { Some line, true }
-| eof
-    (* Normal case: no data, eof. *)
-    { None, false }
-| ([^'\n']+ as line) eof
-    (* Special case: some data but missing '\n', then eof.
-       Consider this as the last line, and add the missing '\n'. *)
-    { Some (line ^ "\n"), false }
+(* Keywords. *)
+
+let goal = "goal"
+
+(* Macros. *)
+
+let space = [' ' '\t' '\r']
+
+let dec     = ['0'-'9']
+let dec_sep = ['0'-'9' '_']
+
+let lalpha = ['a'-'z']
+let ualpha = ['A'-'Z']
+let alpha  = (lalpha | ualpha)
 
-(* This rule analyzes a single line and turns it into a stream of tokens. *)
+let suffix = (alpha | dec_sep)*
+let ident = alpha suffix
 
-and token = parse
+
+(* This rule analyzes multiple lines until eof and turns them into a stream of
+   tokens. *)
+
+rule token = parse
 | [' ' '\t' '\r']
     { token lexbuf }
+| '\n'
+    { MenhirLib.LexerUtil.newline lexbuf; token lexbuf }
 | input as i
     { INPUT i }
 | output as o
     { OUTPUT o }
-| '-'?['0'-'9']+'.'['0'-'9']+ as f
+| goal
+    { GOAL }
+| (ident as gid) space* ":"
+    { GOALID gid }
+| ('-'|'+')?['0'-'9']+'.'['0'-'9']+ as f
     { FLOAT (float_of_string f) }
-| '-'?['0'-'9']+ as i
+| ('-'|'+')?['0'-'9']+ as i
     { INT (int_of_string i) }
+| "+"
+    { PLUS }
+| "-"
+    { MINUS }
 | "="
     { EQ }
 | ">"
@@ -50,7 +64,15 @@ and token = parse
     { GE }
 | "<="
     { LE }
-| '\n'
-    { EOL }
+| "&&"
+    { AND }
+| "||"
+    { OR }
+| '('
+    { LPAREN }
+| ')'
+    { RPAREN }
+| eof
+    { EOF }
 | _
-    { raise (Error (Printf.sprintf "Property lexer at offset %d: unexpected character.\n" (Lexing.lexeme_start lexbuf))) }
+    { raise (Error (Format.sprintf "Property lexer at offset %d: unexpected character." (Lexing.lexeme_start lexbuf))) }

property_parser.mly

@@ -8,49 +8,103 @@
 
 %token <int> INT
 %token <float> FLOAT
-%token <string> INPUT OUTPUT
+%token <string> INPUT OUTPUT GOALID
 %token EQ GT LT GE LE
-%token EOL
+%token PLUS MINUS
+%token AND OR
+%token LPAREN RPAREN
+%token GOAL
+%token EOF
 
 (* Starting rule. *)
 
-%start <Property_syntax.t> main
-%{ open Property_syntax %}
+%start <Property_types.t> main
+%{ open Property_types %}
 
 %%
 
-(* Rules. *)
-
-main:
-| p = property EOL
-    { p }
-
-property:
-| var cop cst
-    { Atomic_cst ($1, $2, $3) }
-| var cop var
-    { Atomic_var ($1, $2, $3) }
-
-var:
-| i = INPUT
-    { Input i }
-| o = OUTPUT
-    { Output o }
-
-cst:
-| i = INT
-    { Int i }
-| f = FLOAT
-    { Float f }
-
-cop:
-| EQ
-   { Eq }
-| GE
-   { Ge }
-| LE
-   { Le }
-| GT
-   { Gt }
-| LT
-   { Lt }
+(* -------------------------------------------------------------------------- *)
+
+(* We parse a property given by
+   a hypothesis
+   a non-empty list of goals
+   followed by an end-of-file. *)
+
+let main :=
+  ~ = hypothesis; goals = nonempty_list(goal); EOF; { { hypothesis; goals; } }
+
+(* A hypothesis is a conjunctive formula over constraints. *)
+
+let hypothesis ==
+  and_formula(constraint_)
+
+(* A goal has a name and a formula. *)
+
+let goal :=
+  GOAL; name = GOALID; ~ = formula; { { name; formula; } }
+
+(* A formula is given by disjunctions of conjuctions of (delimited) formulae. *)
+
+let formula ==
+  or_formula(and_formula(delimited_formula))
+
+(* A disjunctive formula is a left-associative list of formulae, separated by OR
+   (i.e. ||) connective. *)
+
+let or_formula(elem) :=
+  | elem
+  | ors = or_formula(elem); OR; ~ = elem; { Or (ors, elem) }
+
+(* A conjunctive formula is a left-associative list of formulae, separated by
+   AND (i.e. &&) connective. *)
+
+let and_formula(elem) :=
+  | elem
+  | ands = and_formula(elem); AND; ~ = elem; { And (ands, elem) }
+
+(* A delimited formula is
+   either a constraint
+   or a parenthesized formula. *)
+
+let delimited_formula :=
+  | constraint_
+  | delimited(LPAREN, formula, RPAREN)
+
+(* A constraint is the application of a comparison operator to a non-empty list
+   of terms and a constant or a term. *)
+
+let constraint_ :=
+  | terms = nonempty_list(term); ~ = cop; ~ = constant; { Constraint (terms, cop, Constant constant) }
+  | terms = nonempty_list(term); ~ = cop; ~ = term; { Constraint (terms, cop, term) }
+
+(* A term is a constant coupled with a variable, possibly with a sign. *)
+
+let term :=
+  s = ioption(sign); c = ioption(constant); ~ = variable; { General (s, c, variable) }
+
+(* A constant is an integer or float value. *)
+
+let constant :=
+  | ~ = INT; <Int>
+  | ~ = FLOAT; <Float>
+
+(* A variable is either input or output. *)
+
+let variable :=
+  | ~ = INPUT; <Input>
+  | ~ = OUTPUT; <Output>
+
+(* Signs. *)
+
+let sign ==
+  | PLUS;  { Plus }
+  | MINUS; { Minus }
+
+(* Comparison operators. *)
+
+let cop ==
+  | EQ; { Eq }
+  | GE; { Ge }
+  | LE; { Le }
+  | GT; { Gt }
+  | LT; { Lt }

property_types.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of Caisar.                                          *)
+(*                                                                        *)
+(**************************************************************************)
+
+type cop = Eq | Ge | Le | Gt | Lt
+type sign = Plus | Minus
+
+type constant =
+  | Int of int
+  | Float of float
+
+type var =
+  | Input of string
+  | Output of string
+
+type term =
+  | Constant of constant
+  | General of sign option * constant option * var
+
+type formula =
+  | Constraint of term list * cop * term
+  | And of formula * formula
+  | Or of formula * formula
+
+type goal = {
+  name: string;
+  formula: formula;
+}
+
+type t = {
+  hypothesis: formula;
+  goals: goal list;
+}

pyrat.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of Caisar.                                          *)
+(*                                                                        *)
+(**************************************************************************)
+
+open Property_types
+
+type t = Property.conjunct Property.nform
+
+let name = "PyRAT"
+let exe_name = "pyrat.py"
+let exe_default_option = "-v"
+let re_version = Str.regexp "[0-9]\\(\\.[0-9]\\)*\\(\\.?[A-Za-z-+]\\)*"
+
+let re_of_result result =
+  Str.regexp
+    (match result with
+     | Solver.Result.Valid -> "True"
+     | Invalid -> "False"
+     | Timeout -> "Timeout"
+     | Unknown -> "Unknown"
+     | Failure -> assert false)
+
+let is_model_format_supported = function
+  | Model.Nnet _ -> true
+  | Onnx -> false
+
+let options ~model ~property ~output:_ =
+  model :: property ::
+  match Logs.level () with
+  | None | Some (App | Error | Warning) -> []
+  | Some (Info | Debug) -> [ "--verbose" ]
+
+let consolidate _r1 _r2 = assert false
+
+let translate ~hypothesis ~goal =
+  Property.cnf_of_formula (And (hypothesis, goal))
+
+let repr = Property.get_conjuncts
+
+let pretty fmt t =
+  let rec pp_formula fmt formula =
+    match formula with
+    | Constraint (terms, cop, term) ->
+      Format.fprintf fmt "%a %a %a"
+        Property.(pretty_terms (pretty_term ~pp_sign:false)) terms
+        Property.pretty_cop cop
+        (Property.pretty_term ~pp_sign:false) term
+    | And (p1, p2) ->
+      Format.fprintf fmt "%a@\n%a" pp_formula p1 pp_formula p2
+    | Or (p1, p2) ->
+      Format.fprintf fmt "%a or %a" pp_formula p1 pp_formula p2
+  in
+  Format.fprintf fmt "@[%a@]" pp_formula t

pyrat.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of Caisar.                                          *)
+(*                                                                        *)
+(**************************************************************************)
+
+include Solver.S

solver.ml

@@ -5,480 +5,38 @@
 (**************************************************************************)
 
 open Base
-module Format = Caml.Format
-module Sys = Caml.Sys
-module Filename = Caml.Filename
-
-(* Supported solvers. *)
-type solver =
-  | Pyrat
-  | Marabou
- [@@deriving show { with_path = false }, ord, eq, yojson]
-
-
-(* Utilities. *)
-
-let defaults = [ Pyrat; Marabou ]
-
-let rec pp_property_marabou property =
-  let open Property_syntax in
-  let string_of_cop = function
-    | Eq -> "="
-    | Ge -> ">="
-    | Le -> "<="
-    | Gt -> ">"
-    | Lt -> "<"
-  in
-  let string_of_cst = function
-    | Int i -> Stdlib.string_of_int i
-    | Float f -> Stdlib.string_of_float f
-  in
-  match property with
-  | Atomic_cst ((Input v | Output v), cop, cst) ->
-    Format.sprintf "%s %s %s" v (string_of_cop cop) (string_of_cst cst)
-  | Atomic_var ((Input v1 | Output v1), cop, (Input v2 | Output v2)) ->
-    Format.sprintf "%s %s %s" v1 (string_of_cop cop) v2
-  | And (p1, p2) ->
-    let s1 = pp_property_marabou p1 in
-    let s2 = pp_property_marabou p2 in
-    Format.sprintf "%s\n%s" s1 s2
-
-let pp_property_pyrat = pp_property_marabou
-
-let pp_property solver property =
-  match solver with
-  | Pyrat ->
-    Ok (pp_property_pyrat property)
-  | Marabou ->
-    Ok (pp_property_marabou property)
-
-let default_exe_name_of_solver = function
-  | Pyrat -> "pyrat.py"
-  | Marabou -> "Marabou"
-
-let default_option_of_solver = function
-  | Pyrat -> "-v"
-  | Marabou -> "--version"
-
-let exe_path_of_solver solver =
-  let exe = default_exe_name_of_solver solver in
-  (* We want the complete path of [exe] in $PATH: we use `command -v [exe]'
-     and retrieve the result, if any. *)
-  let tmp = Filename.temp_file "caisar" "command" in
-  let _retcode =
-    Sys.command
-      (Filename.quote_command
-         ~stdout:tmp ~stderr:tmp
-         "command" ["-v"; exe])
-  in
-  let in_channel = Stdlib.open_in tmp in
-  let found, exe =
-    try true, Stdlib.input_line in_channel
-    with End_of_file -> false, exe
-  in
-  Stdlib.close_in in_channel;
-  Sys.remove tmp;
-  if found
-  then Ok exe
-  else begin
-    match Sys.getenv_opt "DIR" with
-    | None ->
-      Error
-        (Format.asprintf "Cannot find the executable of `%a'." pp_solver solver)
-    | Some dir ->
-      (* The env variable should already provide the path to the executable: we
-         first check that the path exists, refers to a directory and it is
-         absolute, then we concatenate the [exe] name to it. *)
-      if not (Sys.file_exists dir && Sys.is_directory dir)
-      then
-        Error (Format.sprintf "`%s' not exist or is not a directory." dir)
-      else
-      if Filename.is_relative dir
-      then
-        Error
-          (Format.sprintf
-             "`%s' is a relative path. An absolute path is required for DIR."
-             dir)
-      else
-        let exe =
-          if Filename.check_suffix dir Filename.dir_sep
-          then dir ^ exe
-          else Format.sprintf "%s%s%s" dir Filename.dir_sep exe
-        in
-        Ok exe
-  end
-
-let string_valid_of_solver = function
-  | Pyrat -> "True"
-  | Marabou -> "\\(s\\|S\\)at\\|SAT"
-
-let string_invalid_of_solver = function
-  | Pyrat -> "False"
-  | Marabou -> "\\(u\\|U\\)nsat\\|UNSAT"
-
-let string_timeout_of_solver = function
-  | Pyrat -> "Timeout"
-  | Marabou -> "\\(t\\|T\\)imeout\\|TIMEOUT"
-
-let string_unknown_of_solver = function
-  | Pyrat -> "Unknown"
-  | Marabou -> "\\(u\\|U\\)nknown\\|UNKNOWN"
-
-
-(* Configuration. *)
-
-type version =
-  | Unknown
-  | Version of string
-[@@deriving show { with_path = false }, yojson]
+open Property_types
 
-type config = {
-  solver: solver;
-  exe: string;
-  version: version;
-} [@@deriving yojson, show]
-
-type full_config = config list [@@deriving yojson, show]
-
-let version_of_solver solver s =
-  let regexp_string =
-    (* We use same pattern to extract solver version numbers for the moment. *)
-    match solver with
-    | Pyrat | Marabou ->
-      (* We want to match for version string of the form '0.0.1alpha+'. *)
-      "[0-9]\\(\\.[0-9]\\)*\\(\\.?[A-Za-z-+]\\)*"
-  in
-  let regexp_version = Str.regexp regexp_string in
-  try
-    (* We suppose that the first occurrence that matches [regexp_string] is
-       indeed the version of the concercend [solver]. *)
-    ignore (Str.search_forward regexp_version s 0);
-    Version (Str.matched_string s)
-  with Stdlib.Not_found ->
-    Logs.debug (fun m -> m "No recognizable version found.");
-    Unknown
-
-let default_config_file =
-  let filename = ".caisar.conf" in
-  match Sys.getenv_opt "HOME" with
-  | None -> filename
-  | Some p -> p ^ "/.caisar.conf"
-
-let get_full_config filename =
-  let open Result in
-  match full_config_of_yojson (Yojson.Safe.from_file filename) with
-  | Error _ | exception _ ->
-    []
-  | Ok full_config ->
-    begin
-      Logs.debug
-        (fun m -> m "Configuration in file `%s':@ %s"
-            filename (show_full_config full_config));
-      full_config
-    end
-
-let get_config ~file solver =
-  let open Result in
-  Logs.info
-    (fun m -> m "Reading configuration file `%s' for solver `%a'."
-        file
-        pp_solver solver);
-  if not (Sys.file_exists file)
-  then Error (Format.sprintf "Configuration file `%s' not exist." file)
-  else begin
-    (* Read all solver configs present in the given configuration file. *)
-    let full_config = get_full_config file in
-    (* Search for a [config] with [solver]. *)
-    match List.find ~f:(fun cs -> equal_solver cs.solver solver) full_config with
-    | None ->
-      Error
-        (Format.asprintf
-           "No solver `%a' found in configuration file `%s'."
-           pp_solver solver
-           file)
-    | Some config ->
-      begin
-        Logs.info
-          (fun m -> m "Found `%a' `%s'."
-              pp_solver config.solver
-              (show_version config.version));
-        Ok config
-      end
-  end
-
-let create_config_file file =
-  Logs.debug (fun m -> m "Creating new configuration file `%s'." file);
-  Stdlib.open_out file
-
-let detect_default_solvers () =
-  try
-    let config =
-      List.filter_map
-        ~f:(fun solver ->
-            match exe_path_of_solver solver with
-            | Error msg ->
-              Logs.info (fun m -> m "%s" msg);
-              None
-            | Ok exe ->
-              (* We detect whether solver is available in $PATH, or in the
-                 provided path via env variable, by executing `solver
-                 --version' command. *)
-              let tmp = Filename.temp_file "caisar" "detect" in
-              let cmd =
-                Filename.quote_command
-                  ~stdout:tmp ~stderr:tmp
-                  exe
-                  [default_option_of_solver solver]
-              in
-              Logs.debug
-                (fun m -> m "Executing command `%s' to detect `%a'."
-                    cmd pp_solver solver);
-              let retcode = Sys.command cmd in
-              let cmd_output =
-                let in_channel = Stdlib.open_in tmp in
-                let buf = Buffer.create 512 in
-                try
-                  while true do
-                    Stdlib.Buffer.add_channel buf in_channel 512;
-                  done;
-                  assert false
-                with End_of_file ->
-                  Stdlib.close_in in_channel;
-                  Buffer.contents buf
-              in
-              Sys.remove tmp;
-              if retcode <> 0
-              then begin
-                Logs.info (fun m -> m "No solver `%a' found." pp_solver solver);
-                None
-              end
-              else begin
-                (* If available, we save a [config] for solver. *)
-                let version = version_of_solver solver cmd_output in
-                let config = { solver; exe; version; } in
-                Logs.app
-                  (fun m -> m "Found solver `%a' `%a' (%s)."
-                      pp_solver solver
-                      pp_version version
-                      exe);
-                Some config
-              end)
-        defaults
-    in
-    Ok config
-  with _ ->
-    Error "Unexpected failure."
-
-let detect ~file =
-  let open Result in
-  (* Detect default supported solvers in $PATH or $DIR. *)
-  detect_default_solvers () >>= fun default_full_config ->
-  (* Retrieve the current configuration from [file]. *)
-  let current_full_config = get_full_config file in
-  (* Create new configuration file. *)
-  let out_channel = create_config_file file in
-  (* Build [full_config] by first appending [default_full_config] to
-     [current_full_config], and then deduping the result. *)
-  let full_config =
-    (* TODO: This comparison is not optimal but sufficient as long as we register
-       solver as simply as done in [detect_default_solvers]. *)
-    let compare cs1 cs2 = compare_solver cs1.solver cs2.solver in
-    List.dedup_and_sort
-      ~compare
-      (List.append current_full_config default_full_config)
-  in
-  (* We write all solver configs in the configuration file, as JSON data. *)
-  let full_config_json = full_config_to_yojson full_config in
-  Yojson.Safe.pretty_to_channel out_channel full_config_json;
-  Stdlib.close_out out_channel;
-  Ok ()
-
-
-(* Verification. *)
-
-(* Verification result. *)
-type result =
-  | Valid
-  | Invalid
-  | Timeout
-  | Unknown
-  | Failure
-[@@deriving show { with_path = false }, eq]
-
-let check_availability config =
-  Logs.debug
-    (fun m -> m "Checking actual availability of `%a'."
-        pp_solver config.solver);
-  try
-    (* Execute command `solver --version' to check actual availability. *)
-    let tmp = Filename.temp_file "caisar" "avail" in
-    let cmd =
-      Filename.quote_command
-        ~stdout:tmp ~stderr:tmp
-        config.exe
-        [default_option_of_solver config.solver]
-    in
-    Logs.debug
-      (fun m -> m "Executing command `%s' to check `%a' availability."
-          cmd
-          pp_solver config.solver);
-    let retcode = Sys.command cmd in
-    let in_channel = Stdlib.open_in tmp in
-    Stdlib.close_in in_channel;
-    Sys.remove tmp;
-    if retcode = 0
-    then
-      Ok ()
-    else
-      Error
-        (Format.sprintf
-           "Command `%s' failed. Try to launch the configuration process again."
-           cmd)
-  with Stdlib.Not_found | End_of_file | Failure _ | Sys_error _ ->
-    Error "Unexpected failure."
-
-let check_compatibility config model =
-  let solver = config.solver in
-  match solver, model.Model.format with
-  | (Pyrat | Marabou), (Model.Onnx as f) ->
-    Error
-      (Format.asprintf
-         "No support yet for `%a' and model format `%s'."
-         pp_solver solver
-         (Model.show_format f))
-  | _ ->
-    Ok ()
-
-let build_command ~raw_options confg_solver property model =
-  let open Result in
-  let solver = confg_solver.solver in
-  (* Format property wrt solver. *)
-  pp_property solver property >>= fun s ->
-  (* Write property to temporary file. *)
-  begin
-    try
-      let tmp = Filename.temp_file "prop" (show_solver solver) in
-      let out_channel = Stdlib.open_out tmp in
-      let fmt = Format.formatter_of_out_channel out_channel in
-      Format.fprintf fmt "%s@?" s;
-      Stdlib.close_out out_channel;
-      Ok tmp
-    with Sys_error e ->
-      Error (Format.sprintf "Unexpected failure:@ %s." e)
-  end >>= fun prop ->
-  (* Build actual command-line. *)
-  try
-    let stdout = Filename.temp_file "output" (show_solver solver) in
-    let summary =
-      match solver with
-      | Pyrat -> None
-      | Marabou -> Some (Filename.temp_file "summary" (show_solver solver))
-    in
-    let cmd =
-      let exe = confg_solver.exe in
-      let args =
-        match solver with
-        | Pyrat ->
-          let verbose =
-            match Logs.level () with
-            | None | Some (App | Error | Warning) -> false
-            | Some (Info | Debug) -> true
-          in
-          model.Model.filename ::
-          prop ::
-          if verbose then "--verbose" :: raw_options else raw_options
-        | Marabou ->
-          let verbosity_level =
-            match Logs.level () with
-            | None | Some (App | Error | Warning) -> 0
-            | Some Info -> 1
-            | Some Debug -> 2
-          in
-          "--property" ::  prop ::
-          "--input" :: model.Model.filename ::
-          "--verbosity" :: Int.to_string verbosity_level ::
-          "--summary-file" :: Option.value_exn summary ::
-          raw_options
-      in
-      Filename.quote_command ~stdout ~stderr:stdout exe args
-    in
-    Ok (prop, cmd, (stdout, summary))
-  with Failure e ->
-    Error (Format.sprintf "Unexpected failure:@ %s." e)
-
-let extract_result config stdout summary =
-  Logs.info (fun m -> m "Extracting result of verification.");
-  let solver = config.solver in
-  let output =
-    let file =
-      match solver with
-      | Pyrat -> stdout
-      | Marabou -> Option.value_exn summary
-    in
-    let in_channel = Stdlib.open_in file in
-    let buf = Buffer.create 512 in
-    try
-      while true do
-        Stdlib.Buffer.add_channel buf in_channel 512;
-      done;
-      assert false
-    with End_of_file ->
-      Stdlib.close_in in_channel;
-      Buffer.contents buf
-  in
-  let regexps_result =
-    [ (string_valid_of_solver, Valid);
-      (string_invalid_of_solver, Invalid);
-      (string_timeout_of_solver, Timeout);
-      (string_unknown_of_solver, Unknown); ]
-  in
-  List.fold
-    regexps_result
-    ~init:Failure
-    ~f:(fun acc (f, result) ->
-        let regexp = Str.regexp (f solver) in
-        let found =
-          try Str.search_forward regexp output 0 >= 0
-          with Stdlib.Not_found -> false
-        in
-        if found
-        then result
-        else acc)
-
-let pretty_result fmt result =
-  Format.fprintf fmt "%s" (String.uppercase (show_result result))
+module Format = Caml.Format
 
-let exec ~raw_options config model property =
-  let open Result in
-  (* Check solver availability. *)
-  check_availability config >>= fun () ->
-  (* Check solver and model compatibility. *)
-  check_compatibility config model >>= fun () ->
-  (* Build the required command-line. *)
-  build_command ~raw_options config property model
-  >>= fun (prop, cmd, (stdout, summary)) ->
-  (* Execute the command. *)
-  begin
-    Logs.app (fun m ->
-        m "Launching verification with `%a'." pp_solver config.solver);
-    try
-      Logs.info (fun m -> m "Executing command `%s'." cmd);
-      let retcode = Sys.command cmd in
-      Sys.remove prop;
-      if retcode <> 0
-      then
-        Error (Format.sprintf "Command `%s' failed." cmd)
-      else begin
-        (* Extract and pretty-print verification result. *)
-        let result = extract_result config stdout summary in
-        Logs.app (fun m -> m "Result: %a." pretty_result result);
-        if equal_result result Failure
-        then Logs.app (fun m ->
-            m "See error messages in `%s' for more information." stdout)
-        else Sys.remove stdout;
-        Option.value_map summary ~default:() ~f:Sys.remove;
-        Ok ()
-      end
-    with _ ->
-      Error "Unexpected failure."
-  end
+module Result = struct
+  type t =
+    | Valid
+    | Invalid
+    | Timeout
+    | Unknown
+    | Failure
+  [@@deriving show { with_path = false }, eq]
+
+  let pretty fmt t =
+    Format.fprintf fmt "%s" (String.uppercase (show t))
+end
+
+(* Solver instances. *)
+
+module type S = sig
+  type t
+  val name: string
+  val exe_name: string
+  val exe_default_option: string
+  val re_version: Str.regexp
+  val re_of_result: Result.t -> Str.regexp
+  val is_model_format_supported: Model.format -> bool
+  val options: model:string -> property:string -> output:string -> string list
+  val consolidate: Result.t -> Result.t -> Result.t
+  val translate: hypothesis:formula -> goal:formula -> t
+  val repr: t -> formula list
+  val pretty: Caml.Format.formatter -> formula -> unit
+end
+
+type instance = (module S)

solver.mli

@@ -4,28 +4,60 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(** Supported solvers. *)
-type solver = Pyrat | Marabou [@@deriving show]
+open Property_types
 
-(** The list of supported solvers by default. *)
-val defaults: solver list
+(** Solver possible results. *)
+module Result: sig
+  type t =
+    | Valid
+    | Invalid
+    | Timeout
+    | Unknown
+    | Failure
+  [@@deriving show, eq]
 
-val default_config_file: string
+  val pretty: Caml.Format.formatter -> t -> unit
+end
 
-(** [detect ~file] searches for solvers in $PATH, or in the path provided in env
-    variable $DIR, and save the configurations in [file]. *)
-val detect: file:string -> (unit, string) Result.t
+(** Solvers common interface. *)
+module type S = sig
+  type t
 
-(** Solver configuration. *)
-type config
+  (** The name of the solver. *)
+  val name: string
 
-(** [get_config ~file solver] retrieves the [solver] configuration, if any, from
-    the given [file]. *)
-val get_config: file:string -> solver -> (config, string) Result.t
+  (** The executable name. *)
+  val exe_name: string
 
-(** [exec ~raw_options config model property] runs a solver wrt the given
-    [config] on [property] for [model] with the provided [raw_options], if any.
-*)
-val exec:
-  raw_options:string list ->
-  config -> Model.t -> Property.t -> (unit, string) Result.t
+  (** The default option of the executable. Typically, `--version'. *)
+  val exe_default_option: string
+
+  (** Regexp for extracting the solver version when running the solver on the
+      default option. *)
+  val re_version: Str.regexp
+
+  (** @return regexp for extracting the given result from the solver output. *)
+  val re_of_result: Result.t -> Str.regexp
+
+  (** @return whether the given model format is supported by the solver. *)
+  val is_model_format_supported: Model.format -> bool
+
+  (** @return solver options to execute the solver on the given [model] and
+      [property] files, while using [output] as file to store the result. *)
+  val options: model:string -> property:string -> output:string -> string list
+
+  (** @return consolidated result of the given ones. *)
+  val consolidate: Result.t -> Result.t -> Result.t
+
+  (** Encodes the given formulae into the solver internal representation. *)
+  val translate: hypothesis:formula -> goal:formula -> t
+
+  (** Decodes the internal representation into formulae. *)
+  val repr: t -> formula list
+
+  (** Solver pretty-printing of formulae. *)
+  val pretty: Caml.Format.formatter -> formula -> unit
+end
+
+(** An actual instance of solver interface [S]. *)
+type instance = (module S)