From 1ca32b1cb66b97113f5bf01aad45042a02496ee0 Mon Sep 17 00:00:00 2001
From: Julien Girard <julien.girard2@cea.fr>
Date: Thu, 14 Apr 2022 11:30:15 +0200
Subject: [PATCH] Renamed IOShape as NN, taking into account different models
support by CAISAR.
---
src/language.ml | 2 +-
stdlib/caisar.mlw | 2 +-
tests/marabou.t | 2 +-
tests/simple.t | 2 +-
tests/simple_onnx.t | 2 +-
5 files changed, 5 insertions(+), 5 deletions(-)
diff --git a/src/language.ml b/src/language.ml
index bd67d917..9039b1b3 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 9166a2a9..5de155d8 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 ffc8f76f..2d48b03f 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 ed3d8805..bb8c30b8 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 5c6442dc..1ad6f018 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) ->
--
GitLab