From 118fbbaed8022f6acc27eb3c3421b77c02e4a131 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Fri, 24 May 2024 15:43:08 +0200
Subject: [PATCH] [prover] Complete the integration of maraboupy.
Add also a test for it (copy the one for Marabou).
---
bin/runMarabou.py | 2 +-
config/caisar-detection-data.conf | 2 +-
src/prover.ml | 3 +-
src/prover.mli | 2 +-
src/verification.ml | 7 ++--
tests/autodetect.t | 2 +-
tests/bin/runMarabou.py | 10 ++---
tests/marabou.t | 66 ++++++++++++++++++++++++++++++-
8 files changed, 80 insertions(+), 14 deletions(-)
diff --git a/bin/runMarabou.py b/bin/runMarabou.py
index 3495bc9..9e5ae83 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 b5676f3..0b1fcad 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 9aaebd4..15e12f4 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 c2eb3d4..fa27d38 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 30ef4fe..7f636a5 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 e7993d0..c60ff35 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 4ba5fbd..26bfcef 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 877caab..b20b67c 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
--
GitLab