diff --git a/config/caisar-detection-data.conf b/config/caisar-detection-data.conf index 054b3d8ac73ff597af4afb95a406b080b65fb986..78e3f18272d8aedfe7910c5998b4d110d6bfece7 100644 --- a/config/caisar-detection-data.conf +++ b/config/caisar-detection-data.conf @@ -74,6 +74,17 @@ command = "%e -mp %{nnet-onnx} -pp %f --timeout %t --domain zono poly --split" driver = "caisar_drivers/pyrat_vnnlib.drv" use_at_auto_level = 1 +[ATP pyrat-acas] +name = "PyRAT" +alternative = "ACAS" +exec = "pyrat.py" +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" +use_at_auto_level = 1 + [ATP nnenum] name = "nnenum" exec = "nnenum.sh" diff --git a/tests/autodetect.t b/tests/autodetect.t index dc9de889d81ac056b9673c29290a6a351f7dfdcc..36d66f12046ac5df419dc6a0e4444422522eeb9c 100644 --- a/tests/autodetect.t +++ b/tests/autodetect.t @@ -42,13 +42,15 @@ Test autodetect <autodetect>Found prover Marabou version 1.0.+, OK. <autodetect>Found prover PyRAT version 1.1, OK. <autodetect>Found prover PyRAT version 1.1 (alternative: VNNLIB) + <autodetect>Found prover PyRAT version 1.1 (alternative: ACAS) <autodetect>Found prover nnenum version dummy, OK. <autodetect>Found prover SAVer version v1.0, OK. - <autodetect>7 prover(s) added + <autodetect>8 prover(s) added [caisar] Alt-Ergo 2.4.0 CVC5 1.0.2 Marabou 1.0.+ PyRAT 1.1 + PyRAT 1.1 (ACAS) PyRAT 1.1 (VNNLIB) SAVer v1.0 nnenum dummy