From 7dc9e16b9b8a3cbce11b90272e80bba291750a67 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Wed, 29 May 2024 17:19:05 +0200
Subject: [PATCH] [prover] Prefer using maraboupy as the official name of the
 package.

---
 bin/runMarabou.py                 | 2 +-
 config/caisar-detection-data.conf | 4 ++--
 src/prover.ml                     | 4 ++--
 src/prover.mli                    | 2 +-
 tests/autodetect.t                | 4 ++--
 tests/bin/runMarabou.py           | 2 +-
 tests/marabou.t                   | 2 +-
 7 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/bin/runMarabou.py b/bin/runMarabou.py
index b116827..99e526c 100755
--- a/bin/runMarabou.py
+++ b/bin/runMarabou.py
@@ -56,7 +56,7 @@ def maraboupy_version(marabou_binary: str):
     maraboupy_version = version("maraboupy")
     output = result.stdout.strip()
     if maraboupy_version in output:
-        return f"Maraboupy {maraboupy_version}"
+        return f"maraboupy {maraboupy_version}"
 
     return sys.exit(1)
 
diff --git a/config/caisar-detection-data.conf b/config/caisar-detection-data.conf
index 0b1fcad..b46330f 100644
--- a/config/caisar-detection-data.conf
+++ b/config/caisar-detection-data.conf
@@ -54,10 +54,10 @@ driver = "%{config}/drivers/marabou.drv"
 use_at_auto_level = 1
 
 [ATP maraboupy]
-name = "Maraboupy"
+name = "maraboupy"
 exec = "runMarabou.py"
 version_switch = "--version"
-version_regexp = "Maraboupy \\([0-9.]+\\)"
+version_regexp = "maraboupy \\([0-9.]+\\)"
 version_ok  = "2.0.0"
 command = "%e %{nnet-onnx} %f --timeout %t"
 driver = "%{config}/drivers/marabou.drv"
diff --git a/src/prover.ml b/src/prover.ml
index 15e12f4..ae5a1df 100644
--- a/src/prover.ml
+++ b/src/prover.ml
@@ -22,7 +22,7 @@
 
 type t =
   | Marabou
-  | Maraboupy
+  | Maraboupy [@name "maraboupy"]
   | Pyrat [@name "PyRAT"]
   | Saver [@name "SAVer"]
   | Aimos [@name "AIMOS"]
@@ -49,7 +49,7 @@ let of_string prover =
 
 let to_string = function
   | Marabou -> "Marabou"
-  | Maraboupy -> "Maraboupy"
+  | Maraboupy -> "maraboupy"
   | Pyrat -> "PyRAT"
   | Saver -> "SAVer"
   | Aimos -> "AIMOS"
diff --git a/src/prover.mli b/src/prover.mli
index fa27d38..35f4772 100644
--- a/src/prover.mli
+++ b/src/prover.mli
@@ -22,7 +22,7 @@
 
 type t = private
   | Marabou
-  | Maraboupy
+  | Maraboupy [@name "maraboupy"]
   | Pyrat [@name "PyRAT"]
   | Saver [@name "SAVer"]
   | Aimos [@name "AIMOS"]
diff --git a/tests/autodetect.t b/tests/autodetect.t
index c60ff35..b146b2e 100644
--- a/tests/autodetect.t
+++ b/tests/autodetect.t
@@ -31,14 +31,13 @@ Test autodetect
   dummy-version
 
   $ bin/runMarabou.py --version
-  Maraboupy 2.0.0
+  maraboupy 2.0.0
 
   $ caisar config -d
   AIMOS 1.0
   Alt-Ergo 2.4.0
   CVC5 1.0.2
   Marabou 1.0.+
-  Maraboupy 2.0.0
   PyRAT 1.1
   PyRAT 1.1 (ACAS)
   PyRAT 1.1 (ACASd)
@@ -47,4 +46,5 @@ Test autodetect
   SAVer v1.0
   alpha-beta-CROWN dummy-version
   alpha-beta-CROWN dummy-version (ACAS)
+  maraboupy 2.0.0
   nnenum dummy-version
diff --git a/tests/bin/runMarabou.py b/tests/bin/runMarabou.py
index 26bfcef..c17b176 100755
--- a/tests/bin/runMarabou.py
+++ b/tests/bin/runMarabou.py
@@ -2,7 +2,7 @@
 
 case $1 in
     --version)
-        echo "Maraboupy 2.0.0"
+        echo "maraboupy 2.0.0"
         ;;
     *)
         echo "PWD: $(pwd)"
diff --git a/tests/marabou.t b/tests/marabou.t
index b20b67c..e693ada 100644
--- a/tests/marabou.t
+++ b/tests/marabou.t
@@ -101,7 +101,7 @@ Test verify
   Goal I: Unknown ()
   Goal J: Unknown ()
 
-  $ caisar verify --prover=Maraboupy --ltag=ProverSpec file.mlw
+  $ caisar verify --prover=maraboupy --ltag=ProverSpec file.mlw
   [DEBUG]{ProverSpec} Prover-tailored specification:
   x0 >= 0.0
   x0 <= 0.5
-- 
GitLab