diff --git a/config/caisar-detection-data.conf b/config/caisar-detection-data.conf index b762961a1b08cc4b4d89244ae64457b62ea329b2..c560676cb7ec899f15364d3a856d6f14f77e86e1 100644 --- a/config/caisar-detection-data.conf +++ b/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 diff --git a/src/verification.ml b/src/verification.ml index 77f6e2bcea07dd9b2b6b877b4337670617c38be8..93df264486663c0db38594686c0586074025a705 100644 --- a/src/verification.ml +++ b/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