A tentative first empty schema.

main.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of Caisar.                                          *)
+(*                                                                        *)
+(**************************************************************************)
+
+let () =
+  (* Parse command-line using the Arg standard library module.
+     A typical command-line is the following:
+     ./caisar -onnx [filename] -solver [solvername] -prop [filename]
+  *)
+  (* Build a [Solver.t] and a [Solver.model]. *)
+  (* Build a [Property.t]. *)
+  (* Call [Solver.solve]. *)
+  Format.printf "Please do something useful.@."

property.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of Caisar.                                          *)
+(*                                                                        *)
+(**************************************************************************)
+
+type var =
+  | Input of string
+  | Output of string
+
+type t =
+  | Ge of var * float
+  | Le of float * var
+  | And of t * t
+  | Or of t * t
+
+let property_of_string s =
+  ignore s;
+  None
+
+let pretty fmt t =
+  ignore (fmt, t)

property.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of Caisar.                                          *)
+(*                                                                        *)
+(**************************************************************************)
+
+(** A property. *)
+type t
+
+(** [property_of_string s] builds a property out of [s], if possible. *)
+val property_of_string: string -> t option
+
+(** [pretty property] pretty prints [property]. *)
+val pretty: Format.formatter -> t -> unit

solver.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of Caisar.                                          *)
+(*                                                                        *)
+(**************************************************************************)
+
+type t =
+  | Pyrat
+  | Marabou
+
+type model =
+  | Onnx of string
+  | Nnet of string
+
+let solve solver model property =
+  (* Build the required command-line. *)
+  (* Execute the command-line just built. *)
+  ignore (solver, model, property)

solver.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of Caisar.                                          *)
+(*                                                                        *)
+(**************************************************************************)
+
+(** Supported solvers. *)
+type t =
+  | Pyrat
+  | Marabou
+
+(** Supported model format. *)
+type model =
+  | Onnx of string
+  | Nnet of string
+
+(** [solve solver model property] runs [solver] on [property] for [model]. *)
+val solve: t -> model -> Property.t -> unit