diff --git a/bin/runMarabou.py b/bin/runMarabou.py index b1168276dd3945a056364157e4f8f57f06e3ca9c..99e526cca2c8a5c59ef2e7c950416e57a64c2d66 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 0b1fcad74e4f4a43cc3f4777875a7b966756fe89..b46330fd9bba706431dd50344ff226420da4298e 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 15e12f4d615d6c6a671dc981b100247c29e0cd79..ae5a1df29df5fafad197258a63c10e572d6663f9 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 fa27d381d32402c9e14b050cfac6882d609aebc0..35f47727044c83f1a837e76d68abcc5308bd4907 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 c60ff35906d28ede20aa5e37b32c79307fb1e134..b146b2ec5ce2ef331b5800a67c9c38fcc6b77cc8 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 26bfcef80cfb24c2223e52560a5702828cfc1795..c17b176196afa5c7be2e5b2c0cc22ea07b16b815 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 b20b67cec5281594706c90d9dd397635d83c80bd..e693ada48541a39650d591382de2c99e0c068d91 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