diff --git a/src/language.ml b/src/language.ml index bd67d917830d164cf679c11c66130f86a30808f7..9039b1b32401caaa73b3aa531a79454b762d879d 100644 --- a/src/language.ml +++ b/src/language.ml @@ -20,7 +20,7 @@ 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 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 diff --git a/stdlib/caisar.mlw b/stdlib/caisar.mlw index 9166a2a923317ff4bd192e7a27bba880dd625628..5de155d87e928dbc7e5589bdb62fcb830450f016 100644 --- a/stdlib/caisar.mlw +++ b/stdlib/caisar.mlw @@ -1,4 +1,4 @@ -theory IOShape +theory NN use ieee_float.Float64 type input_type = t end diff --git a/tests/marabou.t b/tests/marabou.t index ffc8f76fa172b42c341cb485ddfbbc84117d2dbd..2d48b03f87e2836145fbcfffc4f49d6b68cf0e2e 100644 --- a/tests/marabou.t +++ b/tests/marabou.t @@ -21,7 +21,7 @@ Test verify > theory T > use TestNetwork.AsTuple > 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) -> diff --git a/tests/simple.t b/tests/simple.t index ed3d8805237a465f83a0201fb3e3ac2c55b76002..bb8c30b88f879a8b76db1ff7bc9cefbf2ed516be 100644 --- a/tests/simple.t +++ b/tests/simple.t @@ -21,7 +21,7 @@ Test verify > theory T > use TestNetwork.AsTuple > 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) -> diff --git a/tests/simple_onnx.t b/tests/simple_onnx.t index 5c6442dcde26cb32ec666d1c052e275b0831013d..1ad6f0184af8e2cbbb2fb1b5c103f32def648f0b 100644 --- a/tests/simple_onnx.t +++ b/tests/simple_onnx.t @@ -21,7 +21,7 @@ Test verify > theory T > use TestNetworkONNX.AsTuple > use ieee_float.Float64 - > use caisar.IOShape + > use caisar.NN > > goal G: forall x1 x2 x3. > (0.0:t) .< x1 .< (0.5:t) ->