[aimos] Add AIMOS as a prover and basic answer_aimos.

src/AIMOS.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of CAISAR.                                          *)
+(*                                                                        *)
+(*  Copyright (C) 2022                                                    *)
+(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
+(*         alternatives)                                                  *)
+(*                                                                        *)
+(*  You can redistribute it and/or modify it under the terms of the GNU   *)
+(*  Lesser General Public License as published by the Free Software       *)
+(*  Foundation, version 2.1.                                              *)
+(*                                                                        *)
+(*  It is distributed in the hope that it will be useful,                 *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the          *)
+(*  GNU Lesser General Public License for more details.                   *)
+(*                                                                        *)
+(*  See the GNU Lesser General Public License version 2.1                 *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+open Why3
+open Base
+
+let aimos_file = Re__Core.(compile (str "%{aimos_file}"))
+
+let build_command config_prover aimos_filename =
+  let command = Whyconf.get_complete_command ~with_steps:false config_prover in
+  Re__Core.replace_string aimos_file ~by:aimos_filename command
+
+let re_aimos_output = Re__Pcre.regexp "((,\\s)(\\d+\\.\\d+))"
+
+let build_answer predicate_kind prover_result =
+  let threshold =
+    match predicate_kind with
+    | Dataset.MetaRobust f -> Float.of_string (Dataset.string_of_eps f)
+    | _ -> failwith "Unsupported property"
+  in
+  match prover_result.Call_provers.pr_answer with
+  | Call_provers.HighFailure -> (
+    let pr_output = prover_result.pr_output in
+    match Re__Core.exec_opt re_aimos_output pr_output with
+    | Some re_group ->
+      (* The regex matches the only group (the 3rd one) that contains
+         dot-separated numerical values that follow a comma and a space. This is
+         not ideal as there might be edge cases where the regex matches other
+         parts of the output that are not supposed to be matched. This will be
+         fixed later on, but for now is good enough. *)
+      let res_aimos = Float.of_string (Re__Core.Group.get re_group 3) in
+      let prover_answer =
+        if Float.( >= ) res_aimos threshold
+        then Call_provers.Valid
+        else Call_provers.Invalid
+      in
+      prover_answer
+    | None -> failwith "Cannot interpret the output provided by AIMOS")
+  | _ ->
+    (* Any other answer than HighFailure should never happen as we do not define
+       anything in AIMOS's driver. *)
+    assert false
+
+let call_prover limit config config_prover
+  (predicate : (Language.nn_shape, string) Dataset.predicate) aimos_config =
+  let command = build_command config_prover aimos_config in
+  let prover_call =
+    let res_parser =
+      {
+        Call_provers.prp_regexps =
+          [ ("NeverMatch", Call_provers.Failure "Should not happen in CAISAR") ];
+        prp_timeregexps = [];
+        prp_stepregexps = [];
+        prp_exitcodes = [];
+        prp_model_parser = Model_parser.lookup_model_parser "no_model";
+      }
+    in
+    Call_provers.call_on_buffer ~libdir:(Whyconf.libdir config)
+      ~datadir:(Whyconf.datadir config) ~command ~limit ~res_parser
+      ~filename:" " ~get_counterexmp:false ~gen_new_file:false
+      ~printing_info:Printer.default_printing_info (Buffer.create 10)
+  in
+  let prover_result = Call_provers.wait_on_call prover_call in
+  build_answer predicate.property prover_result

src/AIMOS.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of CAISAR.                                          *)
+(*                                                                        *)
+(*  Copyright (C) 2022                                                    *)
+(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
+(*         alternatives)                                                  *)
+(*                                                                        *)
+(*  You can redistribute it and/or modify it under the terms of the GNU   *)
+(*  Lesser General Public License as published by the Free Software       *)
+(*  Foundation, version 2.1.                                              *)
+(*                                                                        *)
+(*  It is distributed in the hope that it will be useful,                 *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the          *)
+(*  GNU Lesser General Public License for more details.                   *)
+(*                                                                        *)
+(*  See the GNU Lesser General Public License version 2.1                 *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+open Why3
+
+val call_prover :
+  Call_provers.resource_limit ->
+  Whyconf.main ->
+  Whyconf.config_prover ->
+  (Language.nn_shape, string) Dataset.predicate ->
+  string ->
+  Call_provers.prover_answer

src/prover.ml

@@ -24,11 +24,12 @@ type t =
   | Marabou
   | Pyrat [@name "PyRAT"]
   | Saver [@name "SAVer"]
+  | Aimos [@name "AIMOS"]
   | CVC5 [@name "cvc5"]
   | Nnenum [@name "nnenum"]
 [@@deriving yojson, show]
 
-let list_available () = [ Marabou; Pyrat; Saver; CVC5; Nnenum ]
+let list_available () = [ Marabou; Pyrat; Saver; Aimos; CVC5; Nnenum ]
 
 let of_string prover =
   let prover = String.lowercase_ascii prover in
@@ -36,6 +37,7 @@ let of_string prover =
   | "marabou" -> Some Marabou
   | "pyrat" -> Some Pyrat
   | "saver" -> Some Saver
+  | "aimos" -> Some Aimos
   | "cvc5" -> Some CVC5
   | "nnenum" -> Some Nnenum
   | _ -> None
@@ -44,9 +46,10 @@ let to_string = function
   | Marabou -> "Marabou"
   | Pyrat -> "PyRAT"
   | Saver -> "SAVer"
+  | Aimos -> "AIMOS"
   | CVC5 -> "CVC5"
   | Nnenum -> "nnenum"
 
 let has_vnnlib_support = function
   | Pyrat -> true
-  | Marabou | Saver | CVC5 | Nnenum -> false
+  | Marabou | Saver | Aimos | CVC5 | Nnenum -> false

src/prover.mli

@@ -24,6 +24,7 @@ type t = private
   | Marabou
   | Pyrat [@name "PyRAT"]
   | Saver [@name "SAVer"]
+  | Aimos [@name "AIMOS"]
   | CVC5 [@name "cvc5"]
   | Nnenum [@name "nnenum"]
 [@@deriving yojson, show]

src/verification.ml

@@ -203,6 +203,37 @@ let answer_dataset limit config env prover config_prover driver dataset task =
   in
   (prover_answer, additional_info)
 
+let answer_aimos limit config env config_prover dataset task aimos_config =
+  let predicate =
+    let on_model ls =
+      let message = Fmt.str "No NN model found as %a" Pretty.print_ls ls in
+      Option.value_exn ~message (Language.lookup_loaded_nets ls)
+    in
+    let on_dataset _ls =
+      match dataset with
+      | None -> invalid_arg "No dataset provided"
+      | Some filename ->
+        if String.is_suffix filename ~suffix:".csv"
+        then filename
+        else
+          invalid_arg
+            (Fmt.str "File '%s' has an unsupported  extension" filename)
+    in
+    Dataset.interpret_predicate env ~on_model ~on_dataset task
+  in
+  let aimos_filename =
+    match aimos_config with
+    (* WARNING: change this path if you're not me, and make sure to have an
+       absolute path *)
+    | None -> "/home/aymeric/caisar/aimos_config.yml"
+    | Some s -> s
+  in
+  let answer =
+    AIMOS.call_prover limit config config_prover predicate aimos_filename
+  in
+  let additional_info = Some "" in
+  (answer, additional_info)
+
 let answer_generic limit config env prover config_prover driver task =
   let task = Proof_strategy.apply_native_nn_prover env task in
   let task = Driver.prepare_task driver task in
@@ -235,6 +266,12 @@ let call_prover ?dataset ~limit config env prover config_prover driver task =
         answer_saver limit config env config_prover dataset task
       in
       (prover_answer, Generic additional_info)
+    | Aimos ->
+      let prover_answer, additional_info =
+        (* TODO: add real config file *)
+        answer_aimos limit config env config_prover dataset task None
+      in
+      (prover_answer, Generic additional_info)
     | (Marabou | Pyrat | Nnenum) when Option.is_some dataset ->
       let dataset = Unix.realpath (Option.value_exn dataset) in
       let prover_answer, additional_info =