[prover] Complete the integration of maraboupy.

Add also a test for it (copy the one for Marabou).

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

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"

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

src/prover.mli

@@ -22,7 +22,7 @@
 
 type t = private
   | Marabou
-  | Maraboupy [@name "Maraboupy"]
+  | Maraboupy
   | Pyrat [@name "PyRAT"]
   | Saver [@name "SAVer"]
   | Aimos [@name "AIMOS"]

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 ->

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

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

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