From cf3939659babe7fd2119b6b35c04849ac169debb Mon Sep 17 00:00:00 2001
From: Julien Girard <julien.girard2@cea.fr>
Date: Mon, 21 Nov 2022 16:55:50 +0100
Subject: [PATCH] [config] Added a PyRAT config for solving ACAS problems.
---
config/caisar-detection-data.conf | 11 +++++++++++
tests/autodetect.t | 4 +++-
2 files changed, 14 insertions(+), 1 deletion(-)
diff --git a/config/caisar-detection-data.conf b/config/caisar-detection-data.conf
index 054b3d8..78e3f18 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 dc9de88..36d66f1 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
--
GitLab