[abcrown] Add support for the prover alpha-beta-CROWN.

bin/abcrown.sh

+#!/usr/bin/env sh
+###########################################################################
+#                                                                         #
+#  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).             #
+#                                                                         #
+###########################################################################
+
+if [ "$1" = "--version" ]; then
+    DIRNAME=$( dirname -- "$0"; )
+    $DIRNAME/findmodule.py "complete_verifier.abcrown" "dummy"
+else
+    python3 -m complete_verifier.abcrown "$@"
+fi

bin/dune

@@ -3,4 +3,5 @@
  (section bin)
  (files
   (findmodule.py as findmodule.py)
-  (nnenum.sh as nnenum.sh)))
+  (nnenum.sh as nnenum.sh)
+  (abcrown.sh as abcrown.sh)))

config/caisar-detection-data.conf

@@ -98,6 +98,16 @@ command = "%e %{nnet-onnx} %f"
 driver = "caisar_drivers/nnenum.drv"
 use_at_auto_level = 1
 
+[ATP abcrown]
+name = "alpha-beta-CROWN"
+exec = "abcrown.sh"
+version_switch = "--version"
+version_regexp = "\\(dummy\\)"
+version_ok  = "dummy"
+command = "%e --device cpu --onnx_path %{nnet-onnx} --vnnlib_path %f --timeout %t"
+driver = "caisar_drivers/abcrown.drv"
+use_at_auto_level = 1
+
 [ATP saver]
 name = "SAVer"
 exec = "saver"

config/drivers/abcrown.drv

+(**************************************************************************)
+(*                                                                        *)
+(*  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).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* Why3 driver for alpha-beta-CROWN *)
+
+prelude ";;; produced by alpha-beta-CROWN driver"
+
+import "vnnlib.gen"
+
+valid "^Result: safe"
+invalid "^Result: unsafe"
+timeout "^Time out!!!!!!!!"
+unknown "^Result: unknown" ""

config/dune

@@ -11,5 +11,6 @@
   (drivers/aimos.drv as drivers/aimos.drv)
   (drivers/vnnlib.gen as drivers/vnnlib.gen)
   (drivers/pyrat_vnnlib.drv as drivers/pyrat_vnnlib.drv)
-  (drivers/nnenum.drv as drivers/nnenum.drv))
+  (drivers/nnenum.drv as drivers/nnenum.drv)
+  (drivers/abcrown.drv as drivers/abcrown.drv))
  (package caisar))

src/prover.ml

@@ -27,9 +27,10 @@ type t =
   | Aimos [@name "AIMOS"]
   | CVC5 [@name "cvc5"]
   | Nnenum [@name "nnenum"]
+  | ABCrown [@name "alpha-beta-CROWN"]
 [@@deriving yojson, show]
 
-let list_available () = [ Marabou; Pyrat; Saver; Aimos; CVC5; Nnenum ]
+let list_available () = [ Marabou; Pyrat; Saver; Aimos; CVC5; Nnenum; ABCrown ]
 
 let of_string prover =
   let prover = String.lowercase_ascii prover in
@@ -40,6 +41,7 @@ let of_string prover =
   | "aimos" -> Some Aimos
   | "cvc5" -> Some CVC5
   | "nnenum" -> Some Nnenum
+  | "abcrown" -> Some ABCrown
   | _ -> None
 
 let to_string = function
@@ -49,7 +51,8 @@ let to_string = function
   | Aimos -> "AIMOS"
   | CVC5 -> "CVC5"
   | Nnenum -> "nnenum"
+  | ABCrown -> "alpha-beta-CROWN"
 
 let has_vnnlib_support = function
   | Pyrat -> true
-  | Marabou | Saver | Aimos | CVC5 | Nnenum -> false
+  | Marabou | Saver | Aimos | CVC5 | Nnenum | ABCrown -> false

src/prover.mli

@@ -27,6 +27,7 @@ type t = private
   | Aimos [@name "AIMOS"]
   | CVC5 [@name "cvc5"]
   | Nnenum [@name "nnenum"]
+  | ABCrown [@name "alpha-beta-CROWN"]
 [@@deriving yojson, show]
 
 val list_available : unit -> t list

src/verification.ml

@@ -262,7 +262,7 @@ let call_prover ~cwd ~limit config env prover config_prover driver ?dataset task
     | (Marabou | Pyrat | Nnenum) when Option.is_some dataset ->
       let dataset = Unix.realpath (Option.value_exn dataset) in
       answer_dataset limit config env prover config_prover driver dataset task
-    | Marabou | Pyrat | Nnenum ->
+    | Marabou | Pyrat | Nnenum | ABCrown ->
       let task = Interpretation.interpret_task ~cwd env task in
       let proof_strategy = Proof_strategy.apply_native_nn_prover in
       answer_generic limit config env prover config_prover driver