[config] Use %{config} also for driver locations in detection config file.

config/caisar-detection-data.conf

@@ -50,7 +50,7 @@ version_switch = "--version"
 version_regexp = "\\([0-9.+]+\\)"
 version_ok  = "1.0.+"
 command = "%e %{nnet-onnx} %f --timeout %t --snc --initial-divides=4 --num-online-divides=4 --initial-timeout=0"
-driver = "caisar_drivers/marabou.drv"
+driver = "%{config}/drivers/marabou.drv"
 use_at_auto_level = 1
 
 [ATP pyrat]
@@ -61,7 +61,7 @@ version_switch = "--version"
 version_regexp = "PyRAT \\([0-9.]+\\)"
 version_ok  = "1.1"
 command = "%e -mp %{nnet-onnx} -pp %f --timeout %t"
-driver = "caisar_drivers/pyrat.drv"
+driver = "%{config}/drivers/pyrat.drv"
 use_at_auto_level = 1
 
 [ATP pyrat-vnnlib]
@@ -73,7 +73,7 @@ version_switch = "--version"
 version_regexp = "PyRAT \\([0-9.]+\\)"
 version_ok  = "1.1"
 command = "%e -mp %{nnet-onnx} -pp %f --timeout %t --domain zono poly --split"
-driver = "caisar_drivers/pyrat_vnnlib.drv"
+driver = "%{config}/drivers/pyrat_vnnlib.drv"
 use_at_auto_level = 1
 
 [ATP pyrat-acas]
@@ -85,7 +85,7 @@ version_switch = "--version"
 version_regexp = "PyRAT \\([0-9.]+\\)"
 version_ok  = "1.1"
 command = "%e -mp %{nnet-onnx} -pp %f --timeout %t --domain zono --split --scorer coef"
-driver = "caisar_drivers/pyrat.drv"
+driver = "%{config}/drivers/pyrat.drv"
 use_at_auto_level = 1
 
 [ATP nnenum]
@@ -95,7 +95,7 @@ version_switch = "--version"
 version_regexp = "\\(dummy-version\\)"
 version_ok  = "dummy-version"
 command = "%e %{nnet-onnx} %f"
-driver = "caisar_drivers/nnenum.drv"
+driver = "%{config}/drivers/nnenum.drv"
 use_at_auto_level = 1
 
 [ATP abcrown]
@@ -105,7 +105,7 @@ version_switch = "--version"
 version_regexp = "\\(dummy-version\\)"
 version_ok  = "dummy-version"
 command = "%e --device cpu --onnx_path %{nnet-onnx} --vnnlib_path %f --timeout %t"
-driver = "caisar_drivers/abcrown.drv"
+driver = "%{config}/drivers/abcrown.drv"
 use_at_auto_level = 1
 
 [ATP abcrown]
@@ -116,7 +116,7 @@ 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"
+driver = "%{config}/drivers/abcrown.drv"
 use_at_auto_level = 1
 
 [ATP saver]
@@ -126,7 +126,7 @@ version_switch = "--version 2>&1 | head -n1 && (which saver > /dev/null 2>&1)"
 version_regexp = "\\(v[0-9.]+\\)"
 version_ok = "v1.0"
 command = "%e %{svm} %{dataset} %{abstraction} %{distance} %{epsilon}"
-driver = "caisar_drivers/saver.drv"
+driver = "%{config}/drivers/saver.drv"
 use_at_auto_level = 1
 
 [ATP aimos]
@@ -136,5 +136,5 @@ version_switch = "--version"
 version_regexp = "AIMOS \\([0-9.]+\\)"
 version_ok  = "1.0"
 command = "%e --config %{aimos_file} --no-verbose"
-driver = "caisar_drivers/aimos.drv"
+driver = "%{config}/drivers/aimos.drv"
 use_at_auto_level = 1

src/verification.ml

@@ -341,15 +341,13 @@ let verify ?(debug = false) ?format ~loadpath ?memlimit ?timelimit ?dataset
            altern)
   in
   let driver =
-    match String.chop_prefix ~prefix:"caisar_drivers/" config_prover.driver with
-    | None -> Driver.load_driver_for_prover main env config_prover
-    | Some file ->
-      let file =
-        Filename.concat
-          (Filename.concat (List.hd_exn Dirs.Sites.config) "drivers")
-          file
-      in
-      Driver.load_driver_file_and_extras main env file
+    Re__Core.replace_string re_config ~by:config_site config_prover.driver
+  in
+  let driver =
+    if String.equal driver config_prover.driver
+    then Driver.load_driver_for_prover main env config_prover
+    else
+      Driver.load_driver_file_and_extras main env driver
         config_prover.extra_drivers
   in
   let cwd, mstr_theory = open_file ?format env file in