From c61e51dd0b7eb05ef3d173a90aed7c6e969dbef1 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Fri, 17 Mar 2023 17:23:45 +0100
Subject: [PATCH] [interpretation] c'est l'heure de gouter.
---
src/interpretation.ml | 86 ++--
tests/interpretation_dataset.t | 811 +++++++++++++++++++++++++++++----
2 files changed, 777 insertions(+), 120 deletions(-)
diff --git a/src/interpretation.ml b/src/interpretation.ml
index a4d0337..5db1a81 100644
--- a/src/interpretation.ml
+++ b/src/interpretation.ml
@@ -29,12 +29,13 @@ type dataset = DS_csv of Csv.t [@printer fun fmt _ -> Fmt.pf fmt "<csv>"]
type classifier = string [@@deriving show]
type data = D_csv of string list [@@deriving show]
+type index = I_csv of int [@@deriving show]
type caisar_op =
| Classifier of classifier
| Dataset of dataset
| Data of data
- | Index of int
+ | Index of index
| Tensor of int
[@@deriving show]
@@ -44,13 +45,13 @@ type caisar_env = {
cwd : string;
}
-let ls_of_caisar_op engine op ty =
+let ls_of_caisar_op engine op ty_args ty =
let caisar_env = CRE.user_env engine in
Fmt.pr "ls_of_caisar_op: %a@." pp_caisar_op op;
Option.iter ty ~f:(Fmt.pr "ty: %a@." Pretty.print_ty);
Hashtbl.find_or_add caisar_env.ls_of_caisar_op op ~default:(fun () ->
let id = Ident.id_fresh "caisar_op" in
- let ls = Term.create_lsymbol id [] ty in
+ let ls = Term.create_lsymbol id ty_args ty in
Fmt.pr "ls: %a@." Pretty.print_ls ls;
Hashtbl.Poly.add_exn caisar_env.ls_of_caisar_op ~key:op ~data:ls;
Term.Hls.add caisar_env.caisar_op_of_ls ls op;
@@ -60,8 +61,9 @@ let caisar_op_of_ls engine ls =
let caisar_env = CRE.user_env engine in
Term.Hls.find caisar_env.caisar_op_of_ls ls
-let term_of_caisar_op engine op ty =
- Term.t_app_infer (ls_of_caisar_op engine op ty) []
+let term_of_caisar_op ?(args = []) engine op ty =
+ let t_args, ty_args = List.unzip args in
+ Term.t_app_infer (ls_of_caisar_op engine op ty_args ty) t_args
let caisar_env _env cwd =
{
@@ -108,7 +110,7 @@ let builtin_caisar : caisar_env CRE.built_in_theories list =
Term.t_int_const (BigInt.of_int (Int.of_string label)) )
in
Term (Term.t_tuple [ t_features; t_label ])
- | Data _ | Classifier _ | Var _ | Index _ -> assert false)
+ | Data _ | Classifier _ | Tensor _ | Index _ -> assert false)
| [
Term ({ t_node = Tapp _; _ } as t1); Term ({ t_node = Tvar _; _ } as t2);
] ->
@@ -125,7 +127,30 @@ let builtin_caisar : caisar_env CRE.built_in_theories list =
| [ Term { t_node = Tapp (ls, []); _ } ] -> (
match caisar_op_of_ls engine ls with
| Dataset (DS_csv csv) -> Int (BigInt.of_int (Csv.lines csv))
- | Data _ | Classifier _ | Var _ | Index _ -> assert false)
+ | Data _ | Classifier _ | Tensor _ | Index _ -> assert false)
+ | _ -> invalid_arg (error_message ls)
+ in
+
+ (* Tensor *)
+ let tget : _ CRE.builtin =
+ fun engine ls vl ty ->
+ Fmt.pr "--@.hash_get: ls:%a , ty:%a@." Pretty.print_ls ls
+ Fmt.(option ~none:nop Pretty.print_ty)
+ ty;
+ match vl with
+ | [
+ Term ({ t_node = Tapp (lsapp1, lsapp1_args); _ } as t1);
+ Term ({ t_node = Tapp (lsapp2, _); _ } as t2);
+ ] -> (
+ Fmt.pr "Terms: %a , %a@." Pretty.print_term t1 Pretty.print_term t2;
+ match (caisar_op_of_ls engine lsapp1, caisar_op_of_ls engine lsapp2) with
+ | Tensor n1, Index (I_csv i1) ->
+ assert (i1 <= n1);
+ Term (List.nth_exn lsapp1_args i1)
+ | _ -> assert false)
+ | [ Term t1; Term t2 ] ->
+ Fmt.pr "Terms: %a , %a@." Pretty.print_term t1 Pretty.print_term t2;
+ Term (Term.t_app_infer ls [ t1; t2 ])
| _ -> invalid_arg (error_message ls)
in
@@ -188,6 +213,7 @@ let builtin_caisar : caisar_env CRE.built_in_theories list =
"Vector",
[],
[ (Ident.op_get "" (* ([]) *), None, vget); ("length", None, length) ] );
+ ([ "interpretation" ], "Tensor", [], [ (Ident.op_infix "#", None, tget) ]);
( [ "interpretation" ],
"Classifier",
[],
@@ -212,24 +238,24 @@ let bounded_quant engine vs ~cond : CRE.bounded_quant_result option =
if not (Term.vs_equal vs vs2)
then None
else
+ let n =
+ match caisar_op_of_ls engine ls with
+ | Data (D_csv d) -> List.length d
+ | _ -> assert false
+ in
+ let ty =
+ match vs.vs_ty with
+ | { ty_node = Tyapp (_, ty :: _); _ } -> ty
+ | _ -> assert false
+ in
let new_quant =
- let n =
- match caisar_op_of_ls engine ls with
- | Data (D_csv d) -> List.length d
- | _ -> assert false
- in
- let ty =
- match vs.vs_ty with
- | { ty_node = Tyapp (_, ty :: _); _ } -> ty
- | _ -> assert false
- in
- (* Fmt.pr "TY: %a@." Pretty.print_ty ty; *)
- List.init n ~f:(fun i ->
- let preid = Ident.id_fresh (Fmt.str "caisar_es%i" i) in
+ List.init n ~f:(fun _ ->
+ let preid = Ident.id_fresh "caisar_es" in
Term.create_vsymbol preid ty)
in
+ let args = List.map new_quant ~f:(fun vs -> (Term.t_var vs, ty)) in
let substitutions =
- [ term_of_caisar_op engine (Tensor new_quant) (Some vs.vs_ty) ]
+ [ term_of_caisar_op ~args engine (Tensor n) (Some vs.vs_ty) ]
in
Some { new_quant; substitutions }
| Tapp
@@ -243,26 +269,14 @@ let bounded_quant engine vs ~cond : CRE.bounded_quant_result option =
else
let n =
match caisar_op_of_ls engine ls with
- | Var d -> List.length d
+ | Tensor d -> d
| _ -> assert false
| exception _ -> 5
in
- let new_quant =
- []
- (* let ty = *)
- (* match vs.vs_ty with *)
- (* | { ty_node = Tyapp (_, ty :: _); _ } -> ty *)
- (* | _ -> assert false *)
- (* in *)
- (* (\* Fmt.pr "TY: %a@." Pretty.print_ty ty; *\) *)
- (* List.init n ~f:(fun i -> *)
- (* let preid = Ident.id_fresh (Fmt.str "caisar_vi%i" i) in *)
- (* Term.create_vsymbol preid ty) *)
- in
- (* let substitutions = List.map new_quant ~f:Term.t_var in *)
+ let new_quant = [] in
let substitutions =
List.init n ~f:(fun i ->
- term_of_caisar_op engine (Index i) (Some vs.vs_ty))
+ term_of_caisar_op engine (Index (I_csv i)) (Some vs.vs_ty))
in
Some { new_quant; substitutions }
| _ -> None
diff --git a/tests/interpretation_dataset.t b/tests/interpretation_dataset.t
index 4bcaabe..4b0ea58 100644
--- a/tests/interpretation_dataset.t
+++ b/tests/interpretation_dataset.t
@@ -65,6 +65,64 @@ Test interpret on dataset
int)
ls: caisar_op1
--
+ hash_get: ls:(#) , ty:t
+ Terms: perturbed_image , v
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: perturbed_image , v
+ --
+ valid_index: perturbed_image - y2 v1
+ ls_of_caisar_op: (Interpretation.Index (Interpretation.I_csv 4))
+ ty: vector
+ int
+ ls: caisar_op2
+ ls_of_caisar_op: (Interpretation.Index (Interpretation.I_csv 3))
+ ty: vector
+ int
+ ls: caisar_op3
+ ls_of_caisar_op: (Interpretation.Index (Interpretation.I_csv 2))
+ ty: vector
+ int
+ ls: caisar_op4
+ ls_of_caisar_op: (Interpretation.Index (Interpretation.I_csv 1))
+ ty: vector
+ int
+ ls: caisar_op5
+ ls_of_caisar_op: (Interpretation.Index (Interpretation.I_csv 0))
+ ty: vector
+ int
+ ls: caisar_op6
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: perturbed_image - y2 , caisar_op2
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: perturbed_image - y2 , caisar_op2
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: perturbed_image - y2 , caisar_op3
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: perturbed_image - y2 , caisar_op3
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: perturbed_image - y2 , caisar_op4
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: perturbed_image - y2 , caisar_op4
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: perturbed_image - y2 , caisar_op5
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: perturbed_image - y2 , caisar_op5
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: perturbed_image - y2 , caisar_op6
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: perturbed_image - y2 , caisar_op6
+ --
apply_classifier: ls:(@@) , ty:vector
t
Terms: y0 , perturbed_image
@@ -107,6 +165,42 @@ Test interpret on dataset
vget: ls:([]) , ty:t
Terms: y0 @@ perturbed_image , 2
--
+ hash_get: ls:(#) , ty:t
+ Terms: perturbed_image1 , v2
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: perturbed_image1 , v2
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: perturbed_image1 - y21 , caisar_op2
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: perturbed_image1 - y21 , caisar_op2
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: perturbed_image1 - y21 , caisar_op3
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: perturbed_image1 - y21 , caisar_op3
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: perturbed_image1 - y21 , caisar_op4
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: perturbed_image1 - y21 , caisar_op4
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: perturbed_image1 - y21 , caisar_op5
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: perturbed_image1 - y21 , caisar_op5
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: perturbed_image1 - y21 , caisar_op6
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: perturbed_image1 - y21 , caisar_op6
+ --
apply_classifier: ls:(@@) , ty:vector
t
Terms: caisar_op , perturbed_image1
@@ -149,6 +243,42 @@ Test interpret on dataset
vget: ls:([]) , ty:t
Terms: caisar_op @@ perturbed_image1 , y31
--
+ hash_get: ls:(#) , ty:t
+ Terms: perturbed_image2 , v3
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: perturbed_image2 , v3
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: perturbed_image2 - y22 , caisar_op2
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: perturbed_image2 - y22 , caisar_op2
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: perturbed_image2 - y22 , caisar_op3
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: perturbed_image2 - y22 , caisar_op3
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: perturbed_image2 - y22 , caisar_op4
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: perturbed_image2 - y22 , caisar_op4
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: perturbed_image2 - y22 , caisar_op5
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: perturbed_image2 - y22 , caisar_op5
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: perturbed_image2 - y22 , caisar_op6
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: perturbed_image2 - y22 , caisar_op6
+ --
apply_classifier: ls:(@@) , ty:vector
t
Terms: caisar_op , perturbed_image2
@@ -203,10 +333,46 @@ Test interpret on dataset
"0.776470588"]))
ty: tensor
t
- ls: caisar_op2
- reduce_match@(caisar_op2,
+ ls: caisar_op7
+ reduce_match@(caisar_op7,
1)
--
+ hash_get: ls:(#) , ty:t
+ Terms: perturbed_image3 , v4
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: perturbed_image3 , v4
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: perturbed_image3 - y23 , caisar_op2
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: perturbed_image3 - y23 , caisar_op2
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: perturbed_image3 - y23 , caisar_op3
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: perturbed_image3 - y23 , caisar_op3
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: perturbed_image3 - y23 , caisar_op4
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: perturbed_image3 - y23 , caisar_op4
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: perturbed_image3 - y23 , caisar_op5
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: perturbed_image3 - y23 , caisar_op5
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: perturbed_image3 - y23 , caisar_op6
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: perturbed_image3 - y23 , caisar_op6
+ --
apply_classifier: ls:(@@) , ty:vector
t
Terms: caisar_op , perturbed_image3
@@ -249,95 +415,246 @@ Test interpret on dataset
vget: ls:([]) , ty:t
Terms: caisar_op @@ perturbed_image3 , y33
--
- equal_shape: caisar_op2 perturbed_image4
- ls_of_caisar_op: <var>
+ equal_shape: caisar_op7 perturbed_image4
+ ls_of_caisar_op: (Interpretation.Tensor 5)
ty: tensor
t
- ls: caisar_op3
+ ls: caisar_op8
+ --
+ valid_index: caisar_op8 caisar_es caisar_es1 caisar_es2 caisar_es3 caisar_es4 v5
+ ls_of_caisar_op: (Interpretation.Index (Interpretation.I_csv 4))
+ ty: vector
+ int
+ ls_of_caisar_op: (Interpretation.Index (Interpretation.I_csv 3))
+ ty: vector
+ int
+ ls_of_caisar_op: (Interpretation.Index (Interpretation.I_csv 2))
+ ty: vector
+ int
+ ls_of_caisar_op: (Interpretation.Index (Interpretation.I_csv 1))
+ ty: vector
+ int
+ ls_of_caisar_op: (Interpretation.Index (Interpretation.I_csv 0))
+ ty: vector
+ int
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: caisar_op8 caisar_es caisar_es1 caisar_es2 caisar_es3 caisar_es4 , caisar_op2
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: caisar_op8 caisar_es caisar_es1 caisar_es2 caisar_es3 caisar_es4 , caisar_op2
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: caisar_op8 caisar_es caisar_es1 caisar_es2 caisar_es3 caisar_es4 , caisar_op3
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: caisar_op8 caisar_es caisar_es1 caisar_es2 caisar_es3 caisar_es4 , caisar_op3
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: caisar_op8 caisar_es caisar_es1 caisar_es2 caisar_es3 caisar_es4 , caisar_op4
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: caisar_op8 caisar_es caisar_es1 caisar_es2 caisar_es3 caisar_es4 , caisar_op4
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: caisar_op8 caisar_es caisar_es1 caisar_es2 caisar_es3 caisar_es4 , caisar_op5
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: caisar_op8 caisar_es caisar_es1 caisar_es2 caisar_es3 caisar_es4 , caisar_op5
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: caisar_op8 caisar_es caisar_es1 caisar_es2 caisar_es3 caisar_es4 , caisar_op6
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: caisar_op8 caisar_es caisar_es1 caisar_es2 caisar_es3 caisar_es4 , caisar_op6
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: caisar_op8 caisar_es caisar_es1 caisar_es2 caisar_es3 caisar_es4
+ - caisar_op7 , caisar_op2
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: caisar_op8 caisar_es caisar_es1 caisar_es2 caisar_es3 caisar_es4
+ - caisar_op7 , caisar_op2
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: caisar_op8 caisar_es caisar_es1 caisar_es2 caisar_es3 caisar_es4
+ - caisar_op7 , caisar_op3
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: caisar_op8 caisar_es caisar_es1 caisar_es2 caisar_es3 caisar_es4
+ - caisar_op7 , caisar_op3
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: caisar_op8 caisar_es caisar_es1 caisar_es2 caisar_es3 caisar_es4
+ - caisar_op7 , caisar_op4
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: caisar_op8 caisar_es caisar_es1 caisar_es2 caisar_es3 caisar_es4
+ - caisar_op7 , caisar_op4
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: caisar_op8 caisar_es caisar_es1 caisar_es2 caisar_es3 caisar_es4
+ - caisar_op7 , caisar_op5
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: caisar_op8 caisar_es caisar_es1 caisar_es2 caisar_es3 caisar_es4
+ - caisar_op7 , caisar_op5
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: caisar_op8 caisar_es caisar_es1 caisar_es2 caisar_es3 caisar_es4
+ - caisar_op7 , caisar_op6
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: caisar_op8 caisar_es caisar_es1 caisar_es2 caisar_es3 caisar_es4
+ - caisar_op7 , caisar_op6
--
apply_classifier: ls:(@@) , ty:vector
t
- Terms: caisar_op , caisar_op3
+ Terms: caisar_op , caisar_op8 caisar_es caisar_es1 caisar_es2 caisar_es3
+ caisar_es4
--
vget: ls:([]) , ty:t
- Terms: caisar_op @@ caisar_op3 , 0
+ Terms: caisar_op
+ @@ caisar_op8 caisar_es caisar_es1 caisar_es2 caisar_es3 caisar_es4 , 0
--
apply_classifier: ls:(@@) , ty:vector
t
- Terms: caisar_op , caisar_op3
+ Terms: caisar_op , caisar_op8 caisar_es caisar_es1 caisar_es2 caisar_es3
+ caisar_es4
--
vget: ls:([]) , ty:t
- Terms: caisar_op @@ caisar_op3 , y34
+ Terms: caisar_op
+ @@ caisar_op8 caisar_es caisar_es1 caisar_es2 caisar_es3 caisar_es4 , y34
--
apply_classifier: ls:(@@) , ty:vector
t
- Terms: caisar_op , caisar_op3
+ Terms: caisar_op , caisar_op8 caisar_es caisar_es1 caisar_es2 caisar_es3
+ caisar_es4
--
vget: ls:([]) , ty:t
- Terms: caisar_op @@ caisar_op3 , 1
+ Terms: caisar_op
+ @@ caisar_op8 caisar_es caisar_es1 caisar_es2 caisar_es3 caisar_es4 , 1
--
apply_classifier: ls:(@@) , ty:vector
t
- Terms: caisar_op , caisar_op3
+ Terms: caisar_op , caisar_op8 caisar_es caisar_es1 caisar_es2 caisar_es3
+ caisar_es4
--
vget: ls:([]) , ty:t
- Terms: caisar_op @@ caisar_op3 , y34
+ Terms: caisar_op
+ @@ caisar_op8 caisar_es caisar_es1 caisar_es2 caisar_es3 caisar_es4 , y34
--
apply_classifier: ls:(@@) , ty:vector
t
- Terms: caisar_op , caisar_op3
+ Terms: caisar_op , caisar_op8 caisar_es caisar_es1 caisar_es2 caisar_es3
+ caisar_es4
--
vget: ls:([]) , ty:t
- Terms: caisar_op @@ caisar_op3 , 2
+ Terms: caisar_op
+ @@ caisar_op8 caisar_es caisar_es1 caisar_es2 caisar_es3 caisar_es4 , 2
--
apply_classifier: ls:(@@) , ty:vector
t
- Terms: caisar_op , caisar_op3
+ Terms: caisar_op , caisar_op8 caisar_es caisar_es1 caisar_es2 caisar_es3
+ caisar_es4
--
vget: ls:([]) , ty:t
- Terms: caisar_op @@ caisar_op3 , y34
+ Terms: caisar_op
+ @@ caisar_op8 caisar_es caisar_es1 caisar_es2 caisar_es3 caisar_es4 , y34
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: caisar_op8 caisar_es5 caisar_es6 caisar_es7 caisar_es8 caisar_es9
+ - caisar_op7 , caisar_op2
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: caisar_op8 caisar_es5 caisar_es6 caisar_es7 caisar_es8 caisar_es9
+ - caisar_op7 , caisar_op2
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: caisar_op8 caisar_es5 caisar_es6 caisar_es7 caisar_es8 caisar_es9
+ - caisar_op7 , caisar_op3
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: caisar_op8 caisar_es5 caisar_es6 caisar_es7 caisar_es8 caisar_es9
+ - caisar_op7 , caisar_op3
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: caisar_op8 caisar_es5 caisar_es6 caisar_es7 caisar_es8 caisar_es9
+ - caisar_op7 , caisar_op4
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: caisar_op8 caisar_es5 caisar_es6 caisar_es7 caisar_es8 caisar_es9
+ - caisar_op7 , caisar_op4
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: caisar_op8 caisar_es5 caisar_es6 caisar_es7 caisar_es8 caisar_es9
+ - caisar_op7 , caisar_op5
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: caisar_op8 caisar_es5 caisar_es6 caisar_es7 caisar_es8 caisar_es9
+ - caisar_op7 , caisar_op5
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: caisar_op8 caisar_es5 caisar_es6 caisar_es7 caisar_es8 caisar_es9
+ - caisar_op7 , caisar_op6
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: caisar_op8 caisar_es5 caisar_es6 caisar_es7 caisar_es8 caisar_es9
+ - caisar_op7 , caisar_op6
--
apply_classifier: ls:(@@) , ty:vector
t
- Terms: caisar_op , caisar_op3
+ Terms: caisar_op , caisar_op8 caisar_es5 caisar_es6 caisar_es7 caisar_es8
+ caisar_es9
--
vget: ls:([]) , ty:t
- Terms: caisar_op @@ caisar_op3 , 0
+ Terms: caisar_op
+ @@ caisar_op8 caisar_es5 caisar_es6 caisar_es7 caisar_es8 caisar_es9 , 0
--
apply_classifier: ls:(@@) , ty:vector
t
- Terms: caisar_op , caisar_op3
+ Terms: caisar_op , caisar_op8 caisar_es5 caisar_es6 caisar_es7 caisar_es8
+ caisar_es9
--
vget: ls:([]) , ty:t
- Terms: caisar_op @@ caisar_op3 , 1
+ Terms: caisar_op
+ @@ caisar_op8 caisar_es5 caisar_es6 caisar_es7 caisar_es8 caisar_es9 , 1
--
apply_classifier: ls:(@@) , ty:vector
t
- Terms: caisar_op , caisar_op3
+ Terms: caisar_op , caisar_op8 caisar_es5 caisar_es6 caisar_es7 caisar_es8
+ caisar_es9
--
vget: ls:([]) , ty:t
- Terms: caisar_op @@ caisar_op3 , 1
+ Terms: caisar_op
+ @@ caisar_op8 caisar_es5 caisar_es6 caisar_es7 caisar_es8 caisar_es9 , 1
--
apply_classifier: ls:(@@) , ty:vector
t
- Terms: caisar_op , caisar_op3
+ Terms: caisar_op , caisar_op8 caisar_es5 caisar_es6 caisar_es7 caisar_es8
+ caisar_es9
--
vget: ls:([]) , ty:t
- Terms: caisar_op @@ caisar_op3 , 1
+ Terms: caisar_op
+ @@ caisar_op8 caisar_es5 caisar_es6 caisar_es7 caisar_es8 caisar_es9 , 1
--
apply_classifier: ls:(@@) , ty:vector
t
- Terms: caisar_op , caisar_op3
+ Terms: caisar_op , caisar_op8 caisar_es5 caisar_es6 caisar_es7 caisar_es8
+ caisar_es9
--
vget: ls:([]) , ty:t
- Terms: caisar_op @@ caisar_op3 , 2
+ Terms: caisar_op
+ @@ caisar_op8 caisar_es5 caisar_es6 caisar_es7 caisar_es8 caisar_es9 , 2
--
apply_classifier: ls:(@@) , ty:vector
t
- Terms: caisar_op , caisar_op3
+ Terms: caisar_op , caisar_op8 caisar_es5 caisar_es6 caisar_es7 caisar_es8
+ caisar_es9
--
vget: ls:([]) , ty:t
- Terms: caisar_op @@ caisar_op3 , 1
+ Terms: caisar_op
+ @@ caisar_op8 caisar_es5 caisar_es6 caisar_es7 caisar_es8 caisar_es9 , 1
--
vget: ls:([]) , ty:(tensor t,
int)
@@ -348,10 +665,46 @@ Test interpret on dataset
"0.784313725"]))
ty: tensor
t
- ls: caisar_op4
- reduce_match@(caisar_op4,
+ ls: caisar_op9
+ reduce_match@(caisar_op9,
0)
--
+ hash_get: ls:(#) , ty:t
+ Terms: perturbed_image5 , v6
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: perturbed_image5 , v6
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: perturbed_image5 - y24 , caisar_op2
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: perturbed_image5 - y24 , caisar_op2
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: perturbed_image5 - y24 , caisar_op3
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: perturbed_image5 - y24 , caisar_op3
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: perturbed_image5 - y24 , caisar_op4
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: perturbed_image5 - y24 , caisar_op4
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: perturbed_image5 - y24 , caisar_op5
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: perturbed_image5 - y24 , caisar_op5
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: perturbed_image5 - y24 , caisar_op6
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: perturbed_image5 - y24 , caisar_op6
+ --
apply_classifier: ls:(@@) , ty:vector
t
Terms: caisar_op , perturbed_image5
@@ -394,124 +747,414 @@ Test interpret on dataset
vget: ls:([]) , ty:t
Terms: caisar_op @@ perturbed_image5 , y35
--
- equal_shape: caisar_op4 perturbed_image6
- ls_of_caisar_op: <var>
+ equal_shape: caisar_op9 perturbed_image6
+ ls_of_caisar_op: (Interpretation.Tensor 5)
ty: tensor
t
- ls: caisar_op5
+ --
+ valid_index: caisar_op8 caisar_es10 caisar_es11 caisar_es12 caisar_es13
+ caisar_es14 v7
+ ls_of_caisar_op: (Interpretation.Index (Interpretation.I_csv 4))
+ ty: vector
+ int
+ ls_of_caisar_op: (Interpretation.Index (Interpretation.I_csv 3))
+ ty: vector
+ int
+ ls_of_caisar_op: (Interpretation.Index (Interpretation.I_csv 2))
+ ty: vector
+ int
+ ls_of_caisar_op: (Interpretation.Index (Interpretation.I_csv 1))
+ ty: vector
+ int
+ ls_of_caisar_op: (Interpretation.Index (Interpretation.I_csv 0))
+ ty: vector
+ int
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: caisar_op8 caisar_es10 caisar_es11 caisar_es12 caisar_es13 caisar_es14 , caisar_op2
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: caisar_op8 caisar_es10 caisar_es11 caisar_es12 caisar_es13 caisar_es14 , caisar_op2
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: caisar_op8 caisar_es10 caisar_es11 caisar_es12 caisar_es13 caisar_es14 , caisar_op3
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: caisar_op8 caisar_es10 caisar_es11 caisar_es12 caisar_es13 caisar_es14 , caisar_op3
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: caisar_op8 caisar_es10 caisar_es11 caisar_es12 caisar_es13 caisar_es14 , caisar_op4
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: caisar_op8 caisar_es10 caisar_es11 caisar_es12 caisar_es13 caisar_es14 , caisar_op4
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: caisar_op8 caisar_es10 caisar_es11 caisar_es12 caisar_es13 caisar_es14 , caisar_op5
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: caisar_op8 caisar_es10 caisar_es11 caisar_es12 caisar_es13 caisar_es14 , caisar_op5
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: caisar_op8 caisar_es10 caisar_es11 caisar_es12 caisar_es13 caisar_es14 , caisar_op6
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: caisar_op8 caisar_es10 caisar_es11 caisar_es12 caisar_es13 caisar_es14 , caisar_op6
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: caisar_op8 caisar_es10 caisar_es11 caisar_es12 caisar_es13 caisar_es14
+ - caisar_op9 , caisar_op2
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: caisar_op8 caisar_es10 caisar_es11 caisar_es12 caisar_es13 caisar_es14
+ - caisar_op9 , caisar_op2
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: caisar_op8 caisar_es10 caisar_es11 caisar_es12 caisar_es13 caisar_es14
+ - caisar_op9 , caisar_op3
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: caisar_op8 caisar_es10 caisar_es11 caisar_es12 caisar_es13 caisar_es14
+ - caisar_op9 , caisar_op3
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: caisar_op8 caisar_es10 caisar_es11 caisar_es12 caisar_es13 caisar_es14
+ - caisar_op9 , caisar_op4
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: caisar_op8 caisar_es10 caisar_es11 caisar_es12 caisar_es13 caisar_es14
+ - caisar_op9 , caisar_op4
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: caisar_op8 caisar_es10 caisar_es11 caisar_es12 caisar_es13 caisar_es14
+ - caisar_op9 , caisar_op5
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: caisar_op8 caisar_es10 caisar_es11 caisar_es12 caisar_es13 caisar_es14
+ - caisar_op9 , caisar_op5
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: caisar_op8 caisar_es10 caisar_es11 caisar_es12 caisar_es13 caisar_es14
+ - caisar_op9 , caisar_op6
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: caisar_op8 caisar_es10 caisar_es11 caisar_es12 caisar_es13 caisar_es14
+ - caisar_op9 , caisar_op6
--
apply_classifier: ls:(@@) , ty:vector
t
- Terms: caisar_op , caisar_op5
+ Terms: caisar_op , caisar_op8 caisar_es10 caisar_es11 caisar_es12 caisar_es13
+ caisar_es14
--
vget: ls:([]) , ty:t
- Terms: caisar_op @@ caisar_op5 , 0
+ Terms: caisar_op
+ @@ caisar_op8 caisar_es10 caisar_es11 caisar_es12 caisar_es13
+ caisar_es14 , 0
--
apply_classifier: ls:(@@) , ty:vector
t
- Terms: caisar_op , caisar_op5
+ Terms: caisar_op , caisar_op8 caisar_es10 caisar_es11 caisar_es12 caisar_es13
+ caisar_es14
--
vget: ls:([]) , ty:t
- Terms: caisar_op @@ caisar_op5 , y36
+ Terms: caisar_op
+ @@ caisar_op8 caisar_es10 caisar_es11 caisar_es12 caisar_es13
+ caisar_es14 , y36
--
apply_classifier: ls:(@@) , ty:vector
t
- Terms: caisar_op , caisar_op5
+ Terms: caisar_op , caisar_op8 caisar_es10 caisar_es11 caisar_es12 caisar_es13
+ caisar_es14
--
vget: ls:([]) , ty:t
- Terms: caisar_op @@ caisar_op5 , 1
+ Terms: caisar_op
+ @@ caisar_op8 caisar_es10 caisar_es11 caisar_es12 caisar_es13
+ caisar_es14 , 1
--
apply_classifier: ls:(@@) , ty:vector
t
- Terms: caisar_op , caisar_op5
+ Terms: caisar_op , caisar_op8 caisar_es10 caisar_es11 caisar_es12 caisar_es13
+ caisar_es14
--
vget: ls:([]) , ty:t
- Terms: caisar_op @@ caisar_op5 , y36
+ Terms: caisar_op
+ @@ caisar_op8 caisar_es10 caisar_es11 caisar_es12 caisar_es13
+ caisar_es14 , y36
--
apply_classifier: ls:(@@) , ty:vector
t
- Terms: caisar_op , caisar_op5
+ Terms: caisar_op , caisar_op8 caisar_es10 caisar_es11 caisar_es12 caisar_es13
+ caisar_es14
--
vget: ls:([]) , ty:t
- Terms: caisar_op @@ caisar_op5 , 2
+ Terms: caisar_op
+ @@ caisar_op8 caisar_es10 caisar_es11 caisar_es12 caisar_es13
+ caisar_es14 , 2
--
apply_classifier: ls:(@@) , ty:vector
t
- Terms: caisar_op , caisar_op5
+ Terms: caisar_op , caisar_op8 caisar_es10 caisar_es11 caisar_es12 caisar_es13
+ caisar_es14
--
vget: ls:([]) , ty:t
- Terms: caisar_op @@ caisar_op5 , y36
+ Terms: caisar_op
+ @@ caisar_op8 caisar_es10 caisar_es11 caisar_es12 caisar_es13
+ caisar_es14 , y36
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: caisar_op8 caisar_es15 caisar_es16 caisar_es17 caisar_es18 caisar_es19
+ - caisar_op9 , caisar_op2
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: caisar_op8 caisar_es15 caisar_es16 caisar_es17 caisar_es18 caisar_es19
+ - caisar_op9 , caisar_op2
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: caisar_op8 caisar_es15 caisar_es16 caisar_es17 caisar_es18 caisar_es19
+ - caisar_op9 , caisar_op3
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: caisar_op8 caisar_es15 caisar_es16 caisar_es17 caisar_es18 caisar_es19
+ - caisar_op9 , caisar_op3
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: caisar_op8 caisar_es15 caisar_es16 caisar_es17 caisar_es18 caisar_es19
+ - caisar_op9 , caisar_op4
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: caisar_op8 caisar_es15 caisar_es16 caisar_es17 caisar_es18 caisar_es19
+ - caisar_op9 , caisar_op4
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: caisar_op8 caisar_es15 caisar_es16 caisar_es17 caisar_es18 caisar_es19
+ - caisar_op9 , caisar_op5
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: caisar_op8 caisar_es15 caisar_es16 caisar_es17 caisar_es18 caisar_es19
+ - caisar_op9 , caisar_op5
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: caisar_op8 caisar_es15 caisar_es16 caisar_es17 caisar_es18 caisar_es19
+ - caisar_op9 , caisar_op6
+ --
+ hash_get: ls:(#) , ty:t
+ Terms: caisar_op8 caisar_es15 caisar_es16 caisar_es17 caisar_es18 caisar_es19
+ - caisar_op9 , caisar_op6
--
apply_classifier: ls:(@@) , ty:vector
t
- Terms: caisar_op , caisar_op5
+ Terms: caisar_op , caisar_op8 caisar_es15 caisar_es16 caisar_es17 caisar_es18
+ caisar_es19
--
vget: ls:([]) , ty:t
- Terms: caisar_op @@ caisar_op5 , 0
+ Terms: caisar_op
+ @@ caisar_op8 caisar_es15 caisar_es16 caisar_es17 caisar_es18
+ caisar_es19 , 0
--
apply_classifier: ls:(@@) , ty:vector
t
- Terms: caisar_op , caisar_op5
+ Terms: caisar_op , caisar_op8 caisar_es15 caisar_es16 caisar_es17 caisar_es18
+ caisar_es19
--
vget: ls:([]) , ty:t
- Terms: caisar_op @@ caisar_op5 , 0
+ Terms: caisar_op
+ @@ caisar_op8 caisar_es15 caisar_es16 caisar_es17 caisar_es18
+ caisar_es19 , 0
--
apply_classifier: ls:(@@) , ty:vector
t
- Terms: caisar_op , caisar_op5
+ Terms: caisar_op , caisar_op8 caisar_es15 caisar_es16 caisar_es17 caisar_es18
+ caisar_es19
--
vget: ls:([]) , ty:t
- Terms: caisar_op @@ caisar_op5 , 1
+ Terms: caisar_op
+ @@ caisar_op8 caisar_es15 caisar_es16 caisar_es17 caisar_es18
+ caisar_es19 , 1
--
apply_classifier: ls:(@@) , ty:vector
t
- Terms: caisar_op , caisar_op5
+ Terms: caisar_op , caisar_op8 caisar_es15 caisar_es16 caisar_es17 caisar_es18
+ caisar_es19
--
vget: ls:([]) , ty:t
- Terms: caisar_op @@ caisar_op5 , 0
+ Terms: caisar_op
+ @@ caisar_op8 caisar_es15 caisar_es16 caisar_es17 caisar_es18
+ caisar_es19 , 0
--
apply_classifier: ls:(@@) , ty:vector
t
- Terms: caisar_op , caisar_op5
+ Terms: caisar_op , caisar_op8 caisar_es15 caisar_es16 caisar_es17 caisar_es18
+ caisar_es19
--
vget: ls:([]) , ty:t
- Terms: caisar_op @@ caisar_op5 , 2
+ Terms: caisar_op
+ @@ caisar_op8 caisar_es15 caisar_es16 caisar_es17 caisar_es18
+ caisar_es19 , 2
--
apply_classifier: ls:(@@) , ty:vector
t
- Terms: caisar_op , caisar_op5
+ Terms: caisar_op , caisar_op8 caisar_es15 caisar_es16 caisar_es17 caisar_es18
+ caisar_es19
--
vget: ls:([]) , ty:t
- Terms: caisar_op @@ caisar_op5 , 0
- G : ((forall v:vector int.
- valid_index caisar_op3 v ->
- le (0.0:t) (caisar_op3 # v) /\ le (caisar_op3 # v) (1.0:t)) ->
- (forall v:vector int.
- valid_index (caisar_op3 - caisar_op2) v ->
- le (neg (0.375:t)) ((caisar_op3 - caisar_op2) # v) /\
- le ((caisar_op3 - caisar_op2) # v) (0.375:t)) ->
- lt (caisar_op @@ caisar_op3)[0] (caisar_op @@ caisar_op3)[1] /\
- lt (caisar_op @@ caisar_op3)[2] (caisar_op @@ caisar_op3)[1]) /\
- ((forall v:vector int.
- valid_index caisar_op5 v ->
- le (0.0:t) (caisar_op5 # v) /\ le (caisar_op5 # v) (1.0:t)) ->
- (forall v:vector int.
- valid_index (caisar_op5 - caisar_op4) v ->
- le (neg (0.375:t)) ((caisar_op5 - caisar_op4) # v) /\
- le ((caisar_op5 - caisar_op4) # v) (0.375:t)) ->
- lt (caisar_op @@ caisar_op5)[1] (caisar_op @@ caisar_op5)[0] /\
- lt (caisar_op @@ caisar_op5)[2] (caisar_op @@ caisar_op5)[0])
+ Terms: caisar_op
+ @@ caisar_op8 caisar_es15 caisar_es16 caisar_es17 caisar_es18
+ caisar_es19 , 0
+ G : (forall caisar_es20:t, caisar_es21:t, caisar_es22:t, caisar_es23:t,
+ caisar_es24:t.
+ ((((le (0.0:t) caisar_es24 /\ le caisar_es24 (1.0:t)) /\
+ le (0.0:t) caisar_es23 /\ le caisar_es23 (1.0:t)) /\
+ le (0.0:t) caisar_es22 /\ le caisar_es22 (1.0:t)) /\
+ le (0.0:t) caisar_es21 /\ le caisar_es21 (1.0:t)) /\
+ le (0.0:t) caisar_es20 /\ le caisar_es20 (1.0:t) ->
+ ((((le (neg (0.375:t))
+ ((caisar_op8 caisar_es20 caisar_es21 caisar_es22 caisar_es23
+ caisar_es24 - caisar_op7)
+ # caisar_op2) /\
+ le
+ ((caisar_op8 caisar_es20 caisar_es21 caisar_es22 caisar_es23
+ caisar_es24 - caisar_op7)
+ # caisar_op2)
+ (0.375:t)) /\
+ le (neg (0.375:t))
+ ((caisar_op8 caisar_es20 caisar_es21 caisar_es22 caisar_es23
+ caisar_es24 - caisar_op7)
+ # caisar_op3) /\
+ le
+ ((caisar_op8 caisar_es20 caisar_es21 caisar_es22 caisar_es23
+ caisar_es24 - caisar_op7)
+ # caisar_op3)
+ (0.375:t)) /\
+ le (neg (0.375:t))
+ ((caisar_op8 caisar_es20 caisar_es21 caisar_es22 caisar_es23
+ caisar_es24 - caisar_op7)
+ # caisar_op4) /\
+ le
+ ((caisar_op8 caisar_es20 caisar_es21 caisar_es22 caisar_es23
+ caisar_es24 - caisar_op7)
+ # caisar_op4)
+ (0.375:t)) /\
+ le (neg (0.375:t))
+ ((caisar_op8 caisar_es20 caisar_es21 caisar_es22 caisar_es23
+ caisar_es24 - caisar_op7)
+ # caisar_op5) /\
+ le
+ ((caisar_op8 caisar_es20 caisar_es21 caisar_es22 caisar_es23
+ caisar_es24 - caisar_op7)
+ # caisar_op5)
+ (0.375:t)) /\
+ le (neg (0.375:t))
+ ((caisar_op8 caisar_es20 caisar_es21 caisar_es22 caisar_es23
+ caisar_es24 - caisar_op7)
+ # caisar_op6) /\
+ le
+ ((caisar_op8 caisar_es20 caisar_es21 caisar_es22 caisar_es23
+ caisar_es24 - caisar_op7)
+ # caisar_op6)
+ (0.375:t) ->
+ lt
+ (caisar_op
+ @@ caisar_op8 caisar_es20 caisar_es21 caisar_es22 caisar_es23
+ caisar_es24)
+ [0]
+ (caisar_op
+ @@ caisar_op8 caisar_es20 caisar_es21 caisar_es22 caisar_es23
+ caisar_es24)
+ [1] /\
+ lt
+ (caisar_op
+ @@ caisar_op8 caisar_es20 caisar_es21 caisar_es22 caisar_es23
+ caisar_es24)
+ [2]
+ (caisar_op
+ @@ caisar_op8 caisar_es20 caisar_es21 caisar_es22 caisar_es23
+ caisar_es24)
+ [1]) /\
+ (forall caisar_es20:t, caisar_es21:t, caisar_es22:t, caisar_es23:t,
+ caisar_es24:t.
+ ((((le (0.0:t) caisar_es24 /\ le caisar_es24 (1.0:t)) /\
+ le (0.0:t) caisar_es23 /\ le caisar_es23 (1.0:t)) /\
+ le (0.0:t) caisar_es22 /\ le caisar_es22 (1.0:t)) /\
+ le (0.0:t) caisar_es21 /\ le caisar_es21 (1.0:t)) /\
+ le (0.0:t) caisar_es20 /\ le caisar_es20 (1.0:t) ->
+ ((((le (neg (0.375:t))
+ ((caisar_op8 caisar_es20 caisar_es21 caisar_es22 caisar_es23
+ caisar_es24 - caisar_op9)
+ # caisar_op2) /\
+ le
+ ((caisar_op8 caisar_es20 caisar_es21 caisar_es22 caisar_es23
+ caisar_es24 - caisar_op9)
+ # caisar_op2)
+ (0.375:t)) /\
+ le (neg (0.375:t))
+ ((caisar_op8 caisar_es20 caisar_es21 caisar_es22 caisar_es23
+ caisar_es24 - caisar_op9)
+ # caisar_op3) /\
+ le
+ ((caisar_op8 caisar_es20 caisar_es21 caisar_es22 caisar_es23
+ caisar_es24 - caisar_op9)
+ # caisar_op3)
+ (0.375:t)) /\
+ le (neg (0.375:t))
+ ((caisar_op8 caisar_es20 caisar_es21 caisar_es22 caisar_es23
+ caisar_es24 - caisar_op9)
+ # caisar_op4) /\
+ le
+ ((caisar_op8 caisar_es20 caisar_es21 caisar_es22 caisar_es23
+ caisar_es24 - caisar_op9)
+ # caisar_op4)
+ (0.375:t)) /\
+ le (neg (0.375:t))
+ ((caisar_op8 caisar_es20 caisar_es21 caisar_es22 caisar_es23
+ caisar_es24 - caisar_op9)
+ # caisar_op5) /\
+ le
+ ((caisar_op8 caisar_es20 caisar_es21 caisar_es22 caisar_es23
+ caisar_es24 - caisar_op9)
+ # caisar_op5)
+ (0.375:t)) /\
+ le (neg (0.375:t))
+ ((caisar_op8 caisar_es20 caisar_es21 caisar_es22 caisar_es23
+ caisar_es24 - caisar_op9)
+ # caisar_op6) /\
+ le
+ ((caisar_op8 caisar_es20 caisar_es21 caisar_es22 caisar_es23
+ caisar_es24 - caisar_op9)
+ # caisar_op6)
+ (0.375:t) ->
+ lt
+ (caisar_op
+ @@ caisar_op8 caisar_es20 caisar_es21 caisar_es22 caisar_es23
+ caisar_es24)
+ [1]
+ (caisar_op
+ @@ caisar_op8 caisar_es20 caisar_es21 caisar_es22 caisar_es23
+ caisar_es24)
+ [0] /\
+ lt
+ (caisar_op
+ @@ caisar_op8 caisar_es20 caisar_es21 caisar_es22 caisar_es23
+ caisar_es24)
+ [2]
+ (caisar_op
+ @@ caisar_op8 caisar_es20 caisar_es21 caisar_es22 caisar_es23
+ caisar_es24)
+ [0])
+ caisar_op7,
+ (Interpretation.Data
+ (Interpretation.D_csv
+ ["0.0"; "1.0"; "0.784313725"; "0.019607843"; "0.776470588"]))
caisar_op,
(Interpretation.Classifier
"$TESTCASE_ROOT/TestNetwork.nnet")
- caisar_op5, <var>
- caisar_op3, <var>
- caisar_op1, (Interpretation.Dataset <csv>)
- caisar_op4,
+ caisar_op9,
(Interpretation.Data
(Interpretation.D_csv
["1.0"; "0.0"; "0.019607843"; "0.776470588"; "0.784313725"]))
- caisar_op2,
- (Interpretation.Data
- (Interpretation.D_csv
- ["0.0"; "1.0"; "0.784313725"; "0.019607843"; "0.776470588"]))
+ caisar_op1, (Interpretation.Dataset <csv>)
+ caisar_op8, (Interpretation.Tensor 5)
+ caisar_op2, (Interpretation.Index (Interpretation.I_csv 4))
+ caisar_op3, (Interpretation.Index (Interpretation.I_csv 3))
+ caisar_op4, (Interpretation.Index (Interpretation.I_csv 2))
+ caisar_op5, (Interpretation.Index (Interpretation.I_csv 1))
+ caisar_op6,
+ (Interpretation.Index (Interpretation.I_csv 0))
--
GitLab