[config] Add first support for abcrown config files.

config/abcrown/acasxu.yaml

+# Configuration file for running the ACASXu benchmark (all properties).
+general:
+  enable_incomplete_verification: False
+  loss_reduction_func: max
+data:
+  num_outputs: 5
+solver:
+  batch_size: 1000  # Number of parallel domains to compute on GPU.
+  bound_prop_method: crown
+  beta-crown:
+    iteration: 10  # Iterations for computing intermediate layer bounds.
+  alpha-crown:
+    iteration: 10
+    share_slopes: True  # This produces slightly looser bounds, but faster.
+bab:
+  branching:
+    method: naive  # Split on input space.
+    candidates: 3
+    sb_coeff_thresh: 0.01
+    input_split:
+      enable: True
+      enhanced_bound_prop_method: alpha-crown
+      enhanced_bound_patience: 20
+      enhanced_branching_method: sb
+      attack_patience: 80
+attack:
+  pgd_order: after

config/caisar-detection-data.conf

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

config/dune

@@ -3,8 +3,9 @@
   (site
    (caisar config)))
  (files
-  custom_transformations.py
   caisar-detection-data.conf
+  custom_transformations.py
+  (abcrown/acasxu.yaml as abcrown/acasxu.yaml)
   (drivers/pyrat.drv as drivers/pyrat.drv)
   (drivers/marabou.drv as drivers/marabou.drv)
   (drivers/saver.drv as drivers/saver.drv)

src/verification.ml

@@ -150,6 +150,8 @@ let answer_aimos limit config env config_prover dataset task =
   (answer, additional_info)
 
 let nnet_or_onnx = Re__Core.(compile (str "%{nnet-onnx}"))
+let config_re = Re__Core.(compile (str "%{config}"))
+let config_site = List.hd_exn Dirs.Sites.config
 
 let call_prover_on_task limit config command driver task =
   let prover_call =
@@ -247,6 +249,7 @@ let answer_generic limit config prover config_prover driver ~proof_strategy task
         Whyconf.get_complete_command ~with_steps:false config_prover
       in
       let command = Re__Core.replace_string nnet_or_onnx ~by:nn_file command in
+      let command = Re__Core.replace_string config_re ~by:config_site command in
       List.map tasks ~f:(call_prover_on_task limit config command driver))
   in
   let prover_answer = combine_prover_answers answers in

tests/autodetect.t

@@ -53,9 +53,10 @@ Test autodetect
   <autodetect>Found prover PyRAT version 1.1 (alternative: ACAS)
   <autodetect>Found prover nnenum version dummy-version, OK.
   <autodetect>Found prover alpha-beta-CROWN version dummy-version, OK.
+  <autodetect>Found prover alpha-beta-CROWN version dummy-version (alternative: ACAS)
   <autodetect>Found prover SAVer version v1.0, OK.
   <autodetect>Found prover AIMOS version 1.0, OK.
-  <autodetect>10 prover(s) added
+  <autodetect>11 prover(s) added
   [caisar] AIMOS 1.0
            Alt-Ergo 2.4.0
            CVC5 1.0.2
@@ -65,4 +66,5 @@ Test autodetect
            PyRAT 1.1 (VNNLIB)
            SAVer v1.0
            alpha-beta-CROWN dummy-version
+           alpha-beta-CROWN dummy-version (ACAS)
            nnenum dummy-version