diff --git a/bin/runMarabou.py b/bin/runMarabou.py
index 3495bc9d3d75415bcd29a09b956f6b76e6b2a6ba..9e5ae83efd46b2d63b46e281ce1bbed28503076d 100755
--- a/bin/runMarabou.py
+++ b/bin/runMarabou.py
@@ -92,7 +92,7 @@ def main():
)
else:
if args.version:
- print(f"Maraboupy version {version('maraboupy')}")
+ print(f"Maraboupy {version('maraboupy')}")
else:
assert args.network != None
assert args.prop != None
diff --git a/config/caisar-detection-data.conf b/config/caisar-detection-data.conf
index b5676f310d6942359f4122b22772f749721e82fc..0b1fcad74e4f4a43cc3f4777875a7b966756fe89 100644
--- a/config/caisar-detection-data.conf
+++ b/config/caisar-detection-data.conf
@@ -57,7 +57,7 @@ use_at_auto_level = 1
name = "Maraboupy"
exec = "runMarabou.py"
version_switch = "--version"
-version_regexp = "Maraboupy version \\([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 9aaebd4105fe584a14b2f2140f8fe74eb9e75ff5..15e12f4d615d6c6a671dc981b100247c29e0cd79 100644
--- a/src/prover.ml
+++ b/src/prover.ml
@@ -22,7 +22,7 @@
type t =
| Marabou
- | Maraboupy [@name "Maraboupy"]
+ | Maraboupy
| Pyrat [@name "PyRAT"]
| Saver [@name "SAVer"]
| Aimos [@name "AIMOS"]
@@ -38,6 +38,7 @@ let of_string prover =
let prover = String.lowercase_ascii prover in
match prover with
| "marabou" -> Some Marabou
+ | "maraboupy" -> Some Maraboupy
| "pyrat" -> Some Pyrat
| "saver" -> Some Saver
| "aimos" -> Some Aimos
diff --git a/src/prover.mli b/src/prover.mli
index c2eb3d4b9dd795ac92571b36b2f97a0fc293777d..fa27d381d32402c9e14b050cfac6882d609aebc0 100644
--- a/src/prover.mli
+++ b/src/prover.mli
@@ -22,7 +22,7 @@
type t = private
| Marabou
- | Maraboupy [@name "Maraboupy"]
+ | Maraboupy
| Pyrat [@name "PyRAT"]
| Saver [@name "SAVer"]
| Aimos [@name "AIMOS"]
diff --git a/src/verification.ml b/src/verification.ml
index 30ef4fe66f24201b9225439a23fc714709982c13..7f636a5e88bcdea9e59977d9a7f61d8a7badd0ab 100644
--- a/src/verification.ml
+++ b/src/verification.ml
@@ -237,7 +237,7 @@ let answer_dataset limit config env prover config_prover driver dataset task =
in
let dataset_answers =
match prover with
- | Prover.Marabou ->
+ | Prover.Marabou | Maraboupy ->
(* We turn each task in [dataset_tasks] into a list (ie, conjunction) of
disjunctions of tasks. *)
let tasks = List.map ~f:(Trans.apply Split.split_all) dataset_tasks in
@@ -345,7 +345,7 @@ let answer_generic limit config prover config_prover driver ~proof_strategy task
(* Turn [task] into a list (ie, conjunction) of disjunctions of
tasks. *)
match prover with
- | Prover.Marabou -> Trans.apply Split.split_all task
+ | Prover.Marabou | Maraboupy -> Trans.apply Split.split_all task
| Pyrat | Nnenum | ABCrown -> Trans.apply Split.split_premises task
| _ -> [ task ]
in
@@ -368,7 +368,8 @@ let call_prover ~cwd ~limit config env prover config_prover driver ?dataset
let proof_strategy = Proof_strategy.apply_svm_prover_strategy in
answer_saver limit config env config_prover ~proof_strategy task
| Aimos -> answer_aimos limit config env config_prover dataset task
- | (Marabou | Pyrat | Nnenum | ABCrown) when Option.is_some dataset ->
+ | (Marabou | Maraboupy | Pyrat | Nnenum | ABCrown)
+ when Option.is_some dataset ->
let dataset = Unix.realpath (Option.value_exn dataset) in
answer_dataset limit config env prover config_prover driver dataset task
| Marabou | Maraboupy | Pyrat | Nnenum | ABCrown ->
diff --git a/tests/autodetect.t b/tests/autodetect.t
index e7993d0288b360ca3e8d0d7f5d7d41ef02191f41..c60ff35906d28ede20aa5e37b32c79307fb1e134 100644
--- a/tests/autodetect.t
+++ b/tests/autodetect.t
@@ -31,7 +31,7 @@ Test autodetect
dummy-version
$ bin/runMarabou.py --version
- Maraboupy version 2.0.0
+ Maraboupy 2.0.0
$ caisar config -d
AIMOS 1.0
diff --git a/tests/bin/runMarabou.py b/tests/bin/runMarabou.py
index 4ba5fbd8125758a81063b086bcdde7bf2f5c3bac..26bfcef80cfb24c2223e52560a5702828cfc1795 100755
--- a/tests/bin/runMarabou.py
+++ b/tests/bin/runMarabou.py
@@ -2,13 +2,13 @@
case $1 in
--version)
- echo "Maraboupy version 2.0.0"
+ echo "Maraboupy 2.0.0"
;;
*)
echo "PWD: $(pwd)"
- echo "NN: $2"
- test -e $2 || (echo "Cannot find the NN file" && exit 1)
+ echo "NN: $1"
+ test -e $1 || (echo "Cannot find the NN file" && exit 1)
echo "Goal:"
- cat $4
- echo "Result = Unknown"
+ cat $2
+ echo "Unknown"
esac
diff --git a/tests/marabou.t b/tests/marabou.t
index 877caabd60842bcca9082a97e8c29b9667c87b66..b20b67cec5281594706c90d9dd397635d83c80bd 100644
--- a/tests/marabou.t
+++ b/tests/marabou.t
@@ -4,7 +4,7 @@ Test verify
$ bin/Marabou --version
1.0.+
- $ caisar verify --format whyml --prover=Marabou --ltag=ProverSpec - <<EOF
+ $ cat > file.mlw <<EOF
> theory T
> use ieee_float.Float64
> use caisar.types.Vector
@@ -38,6 +38,70 @@ Test verify
> (nn @@ i)[1] .< (nn @@ i)[0] \/ (nn @@ i)[0] .< (nn @@ i)[1]
> end
> EOF
+
+ $ caisar verify --prover=Marabou --ltag=ProverSpec file.mlw
+ [DEBUG]{ProverSpec} Prover-tailored specification:
+ x0 >= 0.0
+ x0 <= 0.5
+ y0 <= 0.0
+
+ [DEBUG]{ProverSpec} Prover-tailored specification:
+ x0 >= 0.0
+ x0 <= 0.5
+ y0 >= 0.5
+
+ [DEBUG]{ProverSpec} Prover-tailored specification:
+ x0 >= 0.0
+ x0 <= 0.5
+ x1 >= 0.5
+ x1 <= 1.0
+ y0 <= 0.0
+ y0 <= 0.5
+
+ [DEBUG]{ProverSpec} Prover-tailored specification:
+ x0 >= 0.0
+ x0 <= 0.5
+ x1 >= 0.5
+ x1 <= 1.0
+ y1 <= 0.0
+
+ [DEBUG]{ProverSpec} Prover-tailored specification:
+ x0 >= 0.0
+ x0 <= 0.5
+ x1 >= 0.5
+ x1 <= 1.0
+ y1 >= 0.5
+
+ [DEBUG]{ProverSpec} Prover-tailored specification:
+ x0 >= 0.0
+ x0 <= 0.5
+ x1 >= 0.5
+ x1 <= 1.0
+ +y1 -y0 >= 0
+ +y0 -y1 >= 0
+
+ [DEBUG]{ProverSpec} Prover-tailored specification:
+ x0 >= 0.0
+ x0 <= 0.5
+ x1 >= 0.5
+ x1 <= 1.0
+ +y1 -y0 >= 0
+ +y0 -y1 >= 0
+
+ [DEBUG]{ProverSpec} Prover-tailored specification:
+ x0 >= 0.75
+ x0 <= 1.0
+ x1 >= 0.5
+ x1 <= 1.0
+ +y1 -y0 >= 0
+ +y0 -y1 >= 0
+
+ Goal G: Unknown ()
+ Goal H: Unknown ()
+ Goal I: Unknown ()
+ Goal J: Unknown ()
+
+ $ caisar verify --prover=Maraboupy --ltag=ProverSpec file.mlw
[DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.0
x0 <= 0.5