diff --git a/main.ml b/main.ml
new file mode 100644
index 0000000000000000000000000000000000000000..c767fdf3711b77093d2b0835c8b69e2153e64032
--- /dev/null
+++ b/main.ml
@@ -0,0 +1,15 @@
+(**************************************************************************)
+(*                                                                        *)
+(*  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.@."
diff --git a/property.ml b/property.ml
new file mode 100644
index 0000000000000000000000000000000000000000..43dc0af5bbf049dbcaade5910254388f6317380b
--- /dev/null
+++ b/property.ml
@@ -0,0 +1,22 @@
+(**************************************************************************)
+(*                                                                        *)
+(*  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)
diff --git a/property.mli b/property.mli
new file mode 100644
index 0000000000000000000000000000000000000000..b3a480bda9fa0a081a03b480c0456e683fbbe2fc
--- /dev/null
+++ b/property.mli
@@ -0,0 +1,14 @@
+(**************************************************************************)
+(*                                                                        *)
+(*  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
diff --git a/solver.ml b/solver.ml
new file mode 100644
index 0000000000000000000000000000000000000000..0656c474bfa26bc6c5e4f95bd4f3e273c30710c6
--- /dev/null
+++ b/solver.ml
@@ -0,0 +1,18 @@
+(**************************************************************************)
+(*                                                                        *)
+(*  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)
diff --git a/solver.mli b/solver.mli
new file mode 100644
index 0000000000000000000000000000000000000000..ffb1d9cb2049ae15df8e058b32e20dcb6a54a58c
--- /dev/null
+++ b/solver.mli
@@ -0,0 +1,18 @@
+(**************************************************************************)
+(*                                                                        *)
+(*  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