Merge branch 'absolutive_nnet_path' into 'master'

Absolutize the path of nnet given to provers

See merge request laiser/caisar!11

caisar.opam

@@ -42,5 +42,5 @@ build: [
   ["dune" "install" "-p" name "--create-install-files" name]
 ]
 pin-depends: [
-  [ "why3.1.4.0" "git+https://gitlab.inria.fr/why3/why3.git#4e3d0bc71f153fe5625a4a7c92d4dd6cd5e8cf75" ]
+  [ "why3.1.4.0" "git+https://gitlab.inria.fr/why3/why3.git#047c34a8" ]
 ]

caisar.opam.template

 pin-depends: [
-  [ "why3.1.4.0" "git+https://gitlab.inria.fr/why3/why3.git#4e3d0bc71f153fe5625a4a7c92d4dd6cd5e8cf75" ]
+  [ "why3.1.4.0" "git+https://gitlab.inria.fr/why3/why3.git#047c34a8" ]
 ]

src/autodetection.ml

@@ -25,5 +25,5 @@ let autodetect ?(debug = false) () =
   let data = Autodetection.Prover_autodetection_data.from_file caisar_conf in
   let config = Whyconf.init_config (Some null) in
   let binaries = Autodetection.request_binaries_version config data in
-  let provers = Autodetection.compute_builtin_prover binaries data in
+  let provers = Autodetection.compute_builtin_prover binaries config data in
   Whyconf.set_provers config provers

src/transformations/native_nn_prover.ml

@@ -95,6 +95,7 @@ let simplify_goal env input_variables =
                       compute_defs = false;
                       compute_builtin = true;
                       compute_def_set = Term.Sls.empty;
+                      compute_max_quantifier_domain = 0;
                     }
                     env known
                 in

src/verification.ml

@@ -37,7 +37,8 @@ let combine_prover_answers answers =
     | Call_provers.Valid, r | r, Call_provers.Valid -> r
     | _ -> acc)
 
-let call_prover ~limit (prover : Why3.Whyconf.config_prover) driver task =
+let call_prover ~limit config (prover : Why3.Whyconf.config_prover) driver task
+    =
   let open Why3 in
   let task_prepared = Driver.prepare_task driver task in
   let tasks =
@@ -53,10 +54,12 @@ let call_prover ~limit (prover : Why3.Whyconf.config_prover) driver task =
     | Some _ -> assert false (* By construction of the meta. *)
     | None -> invalid_arg (Fmt.str "No neural network model found in task")
   in
+  let nn_file = Filename.concat (Caml.Sys.getcwd ()) nn_file in
   let command = Re.replace_string nnet_or_onnx ~by:nn_file command in
   let call_prover_on_task task_prepared =
     let prover_call =
-      Driver.prove_task_prepared ~command ~limit driver task_prepared
+      Driver.prove_task_prepared ~libdir:(Whyconf.libdir config)
+        ~datadir:(Whyconf.datadir config) ~command ~limit driver task_prepared
     in
     let prover_result = Call_provers.wait_on_call prover_call in
     prover_result.pr_answer
@@ -109,5 +112,7 @@ let verify ?(debug = false) format loadpath ?memlimit ~prover file =
           in
           Driver.load_driver_absolute env file prover.extra_drivers
       in
-      List.iter ~f:(call_prover ~limit prover driver) tasks)
+      List.iter
+        ~f:(call_prover ~limit (Whyconf.get_main config) prover driver)
+        tasks)
     mstr_theory

tests/bin/Marabou

-#!/bin/sh
+#!/bin/sh -e
 
 
 case $1 in
@@ -6,7 +6,9 @@ case $1 in
         echo "1.0.+"
         ;;
     *)
+        echo "PWD: $(pwd)"
         echo "NN: $1"
+        test -e $1 || (echo "Cannot find the NN file" && exit 1)
         echo "Goal:"
         cat $2
         echo "Unknown"

tests/bin/pyrat.py

-#!/bin/sh
+#!/bin/sh -e
 
 
 case $1 in
@@ -6,7 +6,9 @@ case $1 in
         echo "PyRAT 1.1"
         ;;
     *)
+        echo "PWD: $(pwd)"
         echo "NN: $2"
+        test -e $2 || (echo "Cannot find the NN file" && exit 1)
         echo "Goal:"
         cat $4
         echo "Result = Unknown"