[SAVer] Test for SVM parser.

lib/ovo/ovo.ml

@@ -44,11 +44,10 @@ let skip_ovo_header filename in_channel =
   | End_of_file ->
     Error (Format.sprintf "OVO model not found in file `%s'." filename)
 
-(* Retrieve number of layers, inputs, outputs and maximum layer size. *)
+(* Retrieve inputs and outputs size. *)
 let handle_ovo_basic_info in_channel =
   match handle_ovo_line ~f:Int.of_string in_channel with
-  | [ n_layers; n_inputs; n_outputs; max_layer_size ] ->
-    Ok (n_layers, n_inputs, n_outputs, max_layer_size)
+  | [ dim ] -> Ok dim
   | _ -> ovo_format_error "second"
   | exception End_of_file -> ovo_format_error "second"
 
@@ -67,8 +66,9 @@ let parse_in_channel filename in_channel =
   try
     skip_ovo_header filename in_channel >>= fun () ->
     let in_channel = Csv.of_channel in_channel in
-    handle_ovo_basic_info in_channel >>= fun (_, n_is, n_os, _) ->
     handle_ovo_unused_flag in_channel >>= fun () ->
+    handle_ovo_basic_info in_channel >>= fun (n_is) ->
+    handle_ovo_basic_info in_channel >>= fun (n_os) ->
     Csv.close_in in_channel;
     Ok { n_inputs = n_is; n_outputs = n_os }
   with

tests/TestSVM.ovo

-// Generated using the base example shown at https://scikit-learn.org/stable/modules/generated/sklearn.svm.SVC.html
-ovo 2 2
+ovo
+3
+2
 rbf auto
 2 2
 1 2
--0.6592196433465484 -0.47786540839731506 0.6612929735049311 0.4757920782389323
--0.6324555320336759 -1.0
--1.2649110640673518 -1.0
-0.6324555320336759 1.0
-1.2649110640673518 1.0
--2.866041953212284e-05
+-0.619789656282082 -0.47452400048273524 0.6201752226538415 0.4741384341109759
+-0.6324555320336759 -1.0 -1.0
+-1.2649110640673518 -1.0 -1.0
+0.6324555320336759 1.0 1.0
+1.2649110640673518 1.0 1.0
+-3.135855377809087e-06

tests/dune

@@ -3,6 +3,7 @@
   (package caisar)
    TestNetwork.nnet
    TestNetworkONNX.onnx
+   TestSVM.ovo
    bin/pyrat.py
    bin/Marabou
    bin/saver

tests/simple_ovo.t

+Test verify
+  $ cat - > bin/alt-ergo << EOF
+  > #!/bin/sh
+  > echo "2.4.0"
+  > EOF
+
+  $ chmod u+x bin/alt-ergo bin/pyrat.py bin/Marabou bin/saver
+
+  $ bin/alt-ergo
+  2.4.0
+
+  $ bin/pyrat.py --version
+  PyRAT 1.1
+
+  $ bin/Marabou --version
+  1.0.+
+
+  $ bin/saver --version
+  v1.0
+
+  $ PATH=$(pwd)/bin:$PATH
+
+  $ caisar verify -L . --format whyml --prover=PyRAT - 2>&1 <<EOF | sed 's/\/tmp\/[a-z0-9./]*/$TMPFILE/'
+  > theory T
+  >     use TestSVM.AsArray
+  >     use ieee_float.Float64
+  >     use caisar.IOShape
+  > 
+  >     goal G: forall x1 x2 x3.
+  >        (0.0:t) .< x1 .< (0.5:t) ->
+  >        let (y1,_) = svm_apply x1 x2 x3 in
+  >        (0.0:t) .< y1 .< (0.5:t)
+  > end
+  > EOF
+  <autodetect>0 prover(s) added
+  <autodetect>Generating strategies:
+  <autodetect>Run: (Marabou --version) > $TMPFILE 2>&1
+  <autodetect>Run: (alt-ergo --version) > $TMPFILE 2>&1
+  <autodetect>Run: (pyrat.py --version) > $TMPFILE 2>&1
+  <autodetect>Run: (saver --version 2>&1 | cat) > $TMPFILE 2>&1
+  <autodetect>Found prover Alt-Ergo version 2.4.0, OK.
+  <autodetect>Found prover Marabou version 1.0.+, OK.
+  <autodetect>Found prover PyRAT version 1.1, OK.
+  <autodetect>Found prover SAVer version v1.0, OK.
+  <autodetect>4 prover(s) added
+  Goal G: Unknown
+  ()