Merge branch 'nn_theory_name_change' into 'master'

Nn theory name change

See merge request laiser/caisar!19

.gitlab-ci.yml

@@ -11,6 +11,7 @@ tests:
   script:
   - if [ ! -d _opam ]; then echo "no local switch in the CI cache, we setup a new switch"; opam switch create --yes --no-install . ocaml-base-compiler.4.13.1; fi
   - eval $(opam env)
+  - opam switch
   - sudo apt-get update
   - sudo apt install -y protobuf-compiler
   - opam repository add remote https://opam.ocaml.org

src/language.ml

@@ -9,7 +9,7 @@ open Base
 
 (* -- Support for the NNet and ONNX neural network formats. *)
 
-type ioshape = {
+type nnshape = {
   nb_inputs : int;
   nb_outputs : int;
   ty_data : Ty.ty;
@@ -19,12 +19,12 @@ type ioshape = {
 let loaded_nets = Term.Hls.create 10
 let lookup_loaded_nets = Term.Hls.find_opt loaded_nets
 
-let register_astuple nb_inputs nb_outputs filename env =
-  let net = Pmodule.read_module env [ "caisar" ] "IOShape" in
+let register_nn_as_tuple nb_inputs nb_outputs filename env =
+  let net = Pmodule.read_module env [ "caisar" ] "NN" in
   let ioshape_input_type =
     Ty.ty_app Theory.(ns_find_ts net.mod_theory.th_export [ "input_type" ]) []
   in
-  let id_as_tuple = Ident.id_fresh "AsTuple" in
+  let id_as_tuple = Ident.id_fresh "NNasTuple" in
   let th_uc = Pmodule.create_module env id_as_tuple in
   let th_uc = Pmodule.use_export th_uc net in
   let ls_net_apply =
@@ -40,19 +40,19 @@ let register_astuple nb_inputs nb_outputs filename env =
     Pmodule.add_pdecl ~vc:false th_uc
       (Pdecl.create_pure_decl (Decl.create_param_decl ls_net_apply))
   in
-  Wstdlib.Mstr.singleton "AsTuple" (Pmodule.close_module th_uc)
+  Wstdlib.Mstr.singleton "NNasTuple" (Pmodule.close_module th_uc)
 
 let nnet_parser env _ filename _ =
   let model = Nnet.parse filename in
   match model with
   | Error s -> Loc.errorm "%s" s
-  | Ok model -> register_astuple model.n_inputs model.n_outputs filename env
+  | Ok model -> register_nn_as_tuple model.n_inputs model.n_outputs filename env
 
 let onnx_parser env _ filename _ =
   let model = Onnx.parse filename in
   match model with
   | Error s -> Loc.errorm "%s" s
-  | Ok model -> register_astuple model.n_inputs model.n_outputs filename env
+  | Ok model -> register_nn_as_tuple model.n_inputs model.n_outputs filename env
 
 let register_nnet_support () =
   Env.register_format ~desc:"NNet format (ReLU only)" Pmodule.mlw_language

src/language.mli

@@ -6,14 +6,14 @@
 
 open Why3
 
-type ioshape = {
+type nnshape = {
   nb_inputs : int;
   nb_outputs : int;
   ty_data : Ty.ty;
   filename : string;
 }
 
-val lookup_loaded_nets : Term.lsymbol -> ioshape option
+val lookup_loaded_nets : Term.lsymbol -> nnshape option
 (** @return the filename of a nnet Why3 representation. *)
 
 val register_nnet_support : unit -> unit

stdlib/caisar.mlw

-theory IOShape
+theory NN
   use ieee_float.Float64
   type input_type = t
 end

tests/marabou.t

@@ -19,9 +19,9 @@ Test verify
 
   $ caisar verify -L . --format whyml --prover=Marabou - 2>&1 <<EOF | sed 's/\/tmp\/[a-z0-9_./]*/$TMPFILE/'
   > theory T
-  >   use TestNetwork.AsTuple
+  >   use TestNetwork.NNasTuple
   >   use ieee_float.Float64
-  >   use caisar.IOShape
+  >   use caisar.NN
   > 
   >   goal G: forall x1 x2 x3 x4 x5.
   >      (0.0:t) .< x1 .< (0.5:t) ->

tests/simple.t

@@ -19,9 +19,9 @@ Test verify
 
   $ caisar verify -L . --format whyml --prover=PyRAT - 2>&1 <<EOF | sed 's/\/tmp\/[a-z0-9_./]*/$TMPFILE/'
   > theory T
-  >   use TestNetwork.AsTuple
+  >   use TestNetwork.NNasTuple
   >   use ieee_float.Float64
-  >   use caisar.IOShape
+  >   use caisar.NN
   > 
   >   goal G: forall x1 x2 x3 x4 x5.
   >      (0.0:t) .< x1 .< (0.5:t) ->

tests/simple_onnx.t

@@ -19,9 +19,9 @@ Test verify
 
   $ caisar verify -L . --format whyml --prover=PyRAT - 2>&1 <<EOF | sed 's/\/tmp\/[a-z0-9_./]*/$TMPFILE/'
   > theory T
-  >   use TestNetworkONNX.AsTuple
+  >   use TestNetworkONNX.NNasTuple
   >   use ieee_float.Float64
-  >   use caisar.IOShape
+  >   use caisar.NN
   > 
   >   goal G: forall x1 x2 x3.
   >      (0.0:t) .< x1 .< (0.5:t) ->