From e0bf308db2695db4e8432c48ea632e5bc8320753 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Thu, 1 Oct 2020 17:54:49 +0200
Subject: [PATCH] A tentative first empty schema.

---
 main.ml      | 15 +++++++++++++++
 property.ml  | 22 ++++++++++++++++++++++
 property.mli | 14 ++++++++++++++
 solver.ml    | 18 ++++++++++++++++++
 solver.mli   | 18 ++++++++++++++++++
 5 files changed, 87 insertions(+)
 create mode 100644 main.ml
 create mode 100644 property.ml
 create mode 100644 property.mli
 create mode 100644 solver.ml
 create mode 100644 solver.mli

diff --git a/main.ml b/main.ml
new file mode 100644
index 0000000..c767fdf
--- /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 0000000..43dc0af
--- /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 0000000..b3a480b
--- /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 0000000..0656c47
--- /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 0000000..ffb1d9c
--- /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
-- 
GitLab