From 06fe846795c3aecdaf7ef655667b835e4081c24f Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Fri, 30 Jul 2021 18:31:46 +0200
Subject: [PATCH] Add Marabou data for autodetection.

---
 config/caisar-detection-data.conf | 10 ++++++++++
 config/drivers/marabou.drv        |  1 +
 tests/autodetect.t                |  3 ++-
 tests/simple.t                    |  8 +++++---
 4 files changed, 18 insertions(+), 4 deletions(-)
 create mode 100644 config/drivers/marabou.drv

diff --git a/config/caisar-detection-data.conf b/config/caisar-detection-data.conf
index 688a4de8..95f48470 100644
--- a/config/caisar-detection-data.conf
+++ b/config/caisar-detection-data.conf
@@ -10,3 +10,13 @@ command_steps = "%e --steps-bound %S %f"
 driver = "alt_ergo"
 editor = "altgr-ergo"
 use_at_auto_level = 1
+
+[ATP marabou]
+name = "Marabou"
+exec = "Marabou"
+version_switch = "--version"
+version_regexp = "\\([0-9.+]+\\)"
+version_ok  = "1.0.+"
+command = "%e --timeout %t %f"
+driver = "drivers/marabou"
+use_at_auto_level = 1
diff --git a/config/drivers/marabou.drv b/config/drivers/marabou.drv
new file mode 100644
index 00000000..8a2487dd
--- /dev/null
+++ b/config/drivers/marabou.drv
@@ -0,0 +1 @@
+(* Why3 drivers for Marabou *)
diff --git a/tests/autodetect.t b/tests/autodetect.t
index c391f46e..b99f1264 100644
--- a/tests/autodetect.t
+++ b/tests/autodetect.t
@@ -1,3 +1,4 @@
-Test verify
+Test autodetect
   $ caisar config -d
   [caisar] Alt-Ergo 2.4.0
+           Marabou 1.0.+
diff --git a/tests/simple.t b/tests/simple.t
index 567c187e..d4a317de 100644
--- a/tests/simple.t
+++ b/tests/simple.t
@@ -13,13 +13,15 @@ Test verify
   > EOF
   <autodetect>0 prover(s) added
   <autodetect>Generating strategies:
-  <autodetect>Run: (alt-ergo --version) > /tmp/build71161f.dune/out615f55 2>&1
-  <autodetect>Run: (alt-ergo-2.4.0 --version) > /tmp/build71161f.dune/outd1f15f 2>&1
+  <autodetect>Run: (Marabou --version) > /tmp/buildb7d8c3.dune/oute22a8d 2>&1
+  <autodetect>Run: (alt-ergo --version) > /tmp/buildb7d8c3.dune/outf61830 2>&1
+  <autodetect>Run: (alt-ergo-2.4.0 --version) > /tmp/buildb7d8c3.dune/out36e3db 2>&1
   <autodetect>command 'alt-ergo-2.4.0 --version' failed. Output:
   sh: 1: alt-ergo-2.4.0: not found
   
   <autodetect>Found prover Alt-Ergo version 2.4.0, OK.
-  <autodetect>1 prover(s) added
+  <autodetect>Found prover Marabou version 1.0.+, OK.
+  <autodetect>2 prover(s) added
   (* this is the prelude for Alt-Ergo, version >= 2.4.0 *)
   (* this is a prelude for Alt-Ergo integer arithmetic *)
   (* this is a prelude for Alt-Ergo real arithmetic *)
-- 
GitLab