diff --git a/src/interpretation.ml b/src/interpretation.ml
index fbd18c2daa78dbd365c5f735659d533554d12c18..a4d03376eb0c3126acbdce2c6d3535e03853fd70 100644
--- a/src/interpretation.ml
+++ b/src/interpretation.ml
@@ -24,31 +24,18 @@ module CRE = Reduction_engine (* Caisar Reduction Engine *)
open Why3
open Base
-type dataset = CSV of Csv.t [@printer fun fmt _ -> Fmt.pf fmt "<csv>"]
+type dataset = DS_csv of Csv.t [@printer fun fmt _ -> Fmt.pf fmt "<csv>"]
[@@deriving show]
type classifier = string [@@deriving show]
+type data = D_csv of string list [@@deriving show]
type caisar_op =
- | Dataset of dataset
- | Data of string list
| Classifier of classifier
- | ClassifierApp of Term.term * Term.term
- [@printer
- fun fmt (t1, t2) ->
- Fmt.pf fmt "%a@@%a" Pretty.print_term t1 Pretty.print_term t2]
- | VGet of Term.term * Term.term
- [@printer
- fun fmt (t1, t2) ->
- Fmt.pf fmt "%a[%a]" Pretty.print_term t1 Pretty.print_term t2]
- | EqualShape of Term.term * Term.term
- [@printer
- fun fmt (t1, t2) ->
- Fmt.pf fmt "EqShape %a %a" Pretty.print_term t1 Pretty.print_term t2]
- | ValidIndex of Term.term * Term.term
- [@printer
- fun fmt (t1, t2) ->
- Fmt.pf fmt "ValidIdx %a %a" Pretty.print_term t1 Pretty.print_term t2]
+ | Dataset of dataset
+ | Data of data
+ | Index of int
+ | Tensor of int
[@@deriving show]
type caisar_env = {
@@ -104,7 +91,7 @@ let builtin_caisar : caisar_env CRE.built_in_theories list =
] -> (
Fmt.pr "Terms: %a , %a@." Pretty.print_term t1 Pretty.print_term t2;
match caisar_op_of_ls engine lsapp with
- | Dataset (CSV csv) ->
+ | Dataset (DS_csv csv) ->
let row = List.nth_exn csv (Number.to_small_integer i) in
let label, features =
match row with
@@ -117,23 +104,16 @@ let builtin_caisar : caisar_env CRE.built_in_theories list =
| _ -> assert false
in
let t_features, t_label =
- ( term_of_caisar_op engine (Data features) ty_features,
+ ( term_of_caisar_op engine (Data (D_csv features)) ty_features,
Term.t_int_const (BigInt.of_int (Int.of_string label)) )
in
Term (Term.t_tuple [ t_features; t_label ])
- | ClassifierApp (_, _) -> Term (Term.t_app_infer ls [ t1; t2 ])
- | Data _ | Classifier _ | VGet (_, _) | EqualShape _ | ValidIndex _ ->
- assert false)
+ | Data _ | Classifier _ | Var _ | Index _ -> assert false)
| [
- Term ({ t_node = Tapp (lsapp, _); _ } as t1);
- Term ({ t_node = Tvar _; _ } as t2);
- ] -> (
+ Term ({ t_node = Tapp _; _ } as t1); Term ({ t_node = Tvar _; _ } as t2);
+ ] ->
Fmt.pr "Terms: %a , %a@." Pretty.print_term t1 Pretty.print_term t2;
- match caisar_op_of_ls engine lsapp with
- | Dataset _ -> assert false
- | ClassifierApp (_, _) -> Term (Term.t_app_infer ls [ t1; t2 ])
- | Data _ | Classifier _ | VGet (_, _) | EqualShape _ | ValidIndex _ ->
- assert false)
+ Term (Term.t_app_infer ls [ t1; t2 ])
| _ -> invalid_arg (error_message ls)
in
let length : _ CRE.builtin =
@@ -144,47 +124,8 @@ let builtin_caisar : caisar_env CRE.built_in_theories list =
match vl with
| [ Term { t_node = Tapp (ls, []); _ } ] -> (
match caisar_op_of_ls engine ls with
- | Dataset (CSV csv) -> Int (BigInt.of_int (Csv.lines csv))
- | Data _ | Classifier _ | ClassifierApp _ | VGet _ | EqualShape _
- | ValidIndex _ ->
- assert false)
- | [ Term t1; Term ({ t_node = Tvar _; _ } as t2) ] ->
- Fmt.pr "Terms: %a , %a@." Pretty.print_term t1 Pretty.print_term t2;
- Term (term_of_caisar_op engine (VGet (t1, t2)) ty)
- | _ -> invalid_arg (error_message ls)
- in
-
- (* Tensor *)
- let _valid_index : _ CRE.builtin =
- fun engine ls vl ty ->
- Fmt.pr "--@.valid_index: ls:%a , ty:%a@." Pretty.print_ls ls
- Fmt.(option ~none:nop Pretty.print_ty)
- ty;
- match vl with
- | [
- Term ({ t_node = Tvar _; _ } as t1); Term ({ t_node = Tvar _; _ } as t2);
- ]
- | [ Term t1; Term ({ t_node = Tvar _; _ } as t2) ] ->
- Fmt.pr "Terms: %a , %a@." Pretty.print_term t1 Pretty.print_term t2;
- Term (term_of_caisar_op engine (ValidIndex (t1, t2)) ty)
- (* Term Term.t_true *)
- | _ -> invalid_arg (error_message ls)
- in
- let _equal_shape : _ CRE.builtin =
- fun engine ls vl ty ->
- Fmt.pr "--@.equal_shape: ls:%a , ty:%a@." Pretty.print_ls ls
- Fmt.(option ~none:nop Pretty.print_ty)
- ty;
- match vl with
- | [
- Term ({ t_node = Tvar _; _ } as t1); Term ({ t_node = Tvar _; _ } as t2);
- ] ->
- Fmt.pr "Terms: %a , %a@." Pretty.print_term t1 Pretty.print_term t2;
- Term (Term.t_app_infer ls [ t1; t2 ])
- | [ Term t1; Term t2 ] ->
- Fmt.pr "Terms: %a , %a@." Pretty.print_term t1 Pretty.print_term t2;
- Term (term_of_caisar_op engine (EqualShape (t1, t2)) ty)
- (* Term Term.t_true *)
+ | Dataset (DS_csv csv) -> Int (BigInt.of_int (Csv.lines csv))
+ | Data _ | Classifier _ | Var _ | Index _ -> assert false)
| _ -> invalid_arg (error_message ls)
in
@@ -208,7 +149,7 @@ let builtin_caisar : caisar_env CRE.built_in_theories list =
| _ -> invalid_arg (error_message ls)
in
let apply_classifier : _ CRE.builtin =
- fun engine ls vl ty ->
+ fun _engine ls vl ty ->
Fmt.pr "--@.apply_classifier: ls:%a , ty:%a@." Pretty.print_ls ls
Fmt.(option ~none:nop Pretty.print_ty)
ty;
@@ -219,9 +160,6 @@ let builtin_caisar : caisar_env CRE.built_in_theories list =
| [ Term ({ t_node = Tapp (_lsapp, _); _ } as t1); Term t2 ] ->
Fmt.pr "Terms: %a , %a@." Pretty.print_term t1 Pretty.print_term t2;
Term (Term.t_app_infer ls [ t1; t2 ])
- | [ Term t1; Term t2 ] ->
- Fmt.pr "Terms: %a , %a@." Pretty.print_term t1 Pretty.print_term t2;
- Term (term_of_caisar_op engine (ClassifierApp (t1, t2)) ty)
| _ -> invalid_arg (error_message ls)
in
@@ -239,7 +177,7 @@ let builtin_caisar : caisar_env CRE.built_in_theories list =
let { cwd; _ } = CRE.user_env engine in
let caisar_op =
let filename = Caml.Filename.concat cwd dataset in
- let dataset = CSV (Csv.load filename) in
+ let dataset = DS_csv (Csv.load filename) in
Dataset dataset
in
Term (term_of_caisar_op engine caisar_op ty)
@@ -250,11 +188,6 @@ let builtin_caisar : caisar_env CRE.built_in_theories list =
"Vector",
[],
[ (Ident.op_get "" (* ([]) *), None, vget); ("length", None, length) ] );
- ( [ "interpretation" ],
- "Tensor",
- [],
- [ (* ("valid_index", None, valid_index); *)
- (* ("equal_shape", None, equal_shape); *) ] );
( [ "interpretation" ],
"Classifier",
[],
@@ -268,6 +201,72 @@ let builtin_caisar : caisar_env CRE.built_in_theories list =
[ ("read_dataset", None, read_dataset) ] );
]
+let bounded_quant engine vs ~cond : CRE.bounded_quant_result option =
+ match cond.Term.t_node with
+ | Tapp
+ ( { ls_name = { id_string = "equal_shape"; _ }; _ },
+ [
+ ({ t_node = Tapp (ls, _); _ } as t1); ({ t_node = Tvar vs2; _ } as t2);
+ ] ) ->
+ Fmt.pr "--@.equal_shape: %a %a@." Pretty.print_term t1 Pretty.print_term t2;
+ if not (Term.vs_equal vs vs2)
+ then None
+ else
+ 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
+ Term.create_vsymbol preid ty)
+ in
+ let substitutions =
+ [ term_of_caisar_op engine (Tensor new_quant) (Some vs.vs_ty) ]
+ in
+ Some { new_quant; substitutions }
+ | Tapp
+ ( { ls_name = { id_string = "valid_index"; _ }; _ },
+ [
+ ({ t_node = Tapp (ls, _); _ } as t1); ({ t_node = Tvar vs2; _ } as t2);
+ ] ) ->
+ Fmt.pr "--@.valid_index: %a %a@." Pretty.print_term t1 Pretty.print_term t2;
+ if not (Term.vs_equal vs vs2)
+ then None
+ else
+ let n =
+ match caisar_op_of_ls engine ls with
+ | Var d -> List.length 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 substitutions =
+ List.init n ~f:(fun i ->
+ term_of_caisar_op engine (Index i) (Some vs.vs_ty))
+ in
+ Some { new_quant; substitutions }
+ | _ -> None
+
let interpret_task ~cwd env task =
let known_map = Task.task_known task in
let caisar_env = caisar_env env cwd in
@@ -279,10 +278,12 @@ let interpret_task ~cwd env task =
compute_max_quantifier_domain = Int.max_value;
}
in
- let engine = CRE.create params env known_map caisar_env builtin_caisar in
+ let engine =
+ CRE.create ~bounded_quant params env known_map caisar_env builtin_caisar
+ in
let f = Task.task_goal_fmla task in
Fmt.pr "TERM: %a@." Pretty.print_term f;
- let f = CRE.normalize ~limit:1000 engine Term.Mvs.empty f in
+ let f = CRE.normalize ~limit:Int.max_value engine Term.Mvs.empty f in
Fmt.pr "%a : %a@.%a@." Pretty.print_pr (Task.task_goal task) Pretty.print_term
f print_caisar_op caisar_env
diff --git a/src/reduction_engine.mli b/src/reduction_engine.mli
index 695db72ba9833cdae09498d6dd82ea212c3d0fec..bcb1c4863f6441089c3fb45ad0744a5fc6c82ca5 100644
--- a/src/reduction_engine.mli
+++ b/src/reduction_engine.mli
@@ -99,14 +99,14 @@ type 'a built_in_theories =
* (string * (Ty.tysymbol -> unit)) list
* (string * Why3.Term.lsymbol ref option * 'a builtin) list
- type bounded_quant_result = {
- new_quant: Term.vsymbol list;
- substitutions : Term.term list;
- }
-
-type 'a bounded_quant = 'a engine -> Term.vsymbol -> cond:Term.term ->
- bounded_quant_result option
-
+type bounded_quant_result = {
+ new_quant : Term.vsymbol list;
+ substitutions : Term.term list;
+}
+
+type 'a bounded_quant =
+ 'a engine -> Term.vsymbol -> cond:Term.term -> bounded_quant_result option
+
val create :
?bounded_quant:'a bounded_quant ->
params ->
diff --git a/tests/interpretation_dataset.t b/tests/interpretation_dataset.t
index ca4ded6ccec1b837b797fbc59c755396032c4ae3..4bcaabea3065c710e7b79908a8674b97149bfdb0 100644
--- a/tests/interpretation_dataset.t
+++ b/tests/interpretation_dataset.t
@@ -31,8 +31,8 @@ Test interpret on dataset
>
> predicate robust_around (c: classifier) (eps: t) (i: image) (l: label_) =
> forall perturbed_image: image.
- > valid_image perturbed_image ->
> equal_shape i perturbed_image ->
+ > valid_image perturbed_image ->
> let p = perturbed_image - i in
> bounded_by_epsilon p eps ->
> advises c perturbed_image l
@@ -47,57 +47,471 @@ Test interpret on dataset
> robust classifier dataset eps
> end
> EOF
- G : match caisar_op[0] with
- | a, b ->
- ((fun (y2:tensor t) (y3:int) ->
- forall perturbed_image:tensor t.
- (forall v:vector int.
- valid_index perturbed_image v ->
- le (0.0:t) (perturbed_image # v) /\
- le (perturbed_image # v) (1.0:t)) ->
- equal_shape y2 perturbed_image ->
- (forall v:vector int.
- valid_index (perturbed_image - y2) v ->
- le (neg (0.375:t)) ((perturbed_image - y2) # v) /\
- le ((perturbed_image - y2) # v) (0.375:t)) ->
- (0 < y3 \/ 0 = y3) /\ (y3 < 1 \/ y3 = 1) ->
- (forall j:int.
- ((0 < j \/ 0 = j) /\ (j < 1 \/ j = 1)) /\ not j = y3 ->
- lt
- (read_classifier ("TestNetwork.nnet":string) NNet
- @@ perturbed_image)
- [j]
- (read_classifier ("TestNetwork.nnet":string) NNet
- @@ perturbed_image)
- [y3]))
- @ a)
- @ b
- end = True /\
- match caisar_op[1] with
- | a, b ->
- ((fun (y2:tensor t) (y3:int) ->
- forall perturbed_image:tensor t.
- (forall v:vector int.
- valid_index perturbed_image v ->
- le (0.0:t) (perturbed_image # v) /\
- le (perturbed_image # v) (1.0:t)) ->
- equal_shape y2 perturbed_image ->
- (forall v:vector int.
- valid_index (perturbed_image - y2) v ->
- le (neg (0.375:t)) ((perturbed_image - y2) # v) /\
- le ((perturbed_image - y2) # v) (0.375:t)) ->
- (0 < y3 \/ 0 = y3) /\ (y3 < 1 \/ y3 = 1) ->
- (forall j:int.
- ((0 < j \/ 0 = j) /\ (j < 1 \/ j = 1)) /\ not j = y3 ->
- lt
- (read_classifier ("TestNetwork.nnet":string) NNet
- @@ perturbed_image)
- [j]
- (read_classifier ("TestNetwork.nnet":string) NNet
- @@ perturbed_image)
- [y3]))
- @ a)
- @ b
- end = True
+ TERM: let classifier = read_classifier ("TestNetwork.nnet":string) NNet in
+ let dataset =
+ (read_dataset ("dataset.csv":string) CSV: vector (tensor t, int))
+ in let eps = (0.375:t) in robust classifier dataset eps
+ --
+ read_classifier: ls:read_classifier , ty:classifier
+ ls_of_caisar_op: (Interpretation.Classifier
+ "$TESTCASE_ROOT/TestNetwork.nnet")
+ ty: classifier
+ ls: caisar_op
+ --
+ read_dataset: ls:read_dataset , ty:vector (tensor t,
+ int)
+ ls_of_caisar_op: (Interpretation.Dataset <csv>)
+ ty: vector (tensor t,
+ int)
+ ls: caisar_op1
+ --
+ apply_classifier: ls:(@@) , ty:vector
+ t
+ Terms: y0 , perturbed_image
+ --
+ vget: ls:([]) , ty:t
+ Terms: y0 @@ perturbed_image , y3
+ --
+ apply_classifier: ls:(@@) , ty:vector
+ t
+ Terms: y0 , perturbed_image
+ --
+ vget: ls:([]) , ty:t
+ Terms: y0 @@ perturbed_image , 0
+ --
+ apply_classifier: ls:(@@) , ty:vector
+ t
+ Terms: y0 , perturbed_image
+ --
+ vget: ls:([]) , ty:t
+ Terms: y0 @@ perturbed_image , y3
+ --
+ apply_classifier: ls:(@@) , ty:vector
+ t
+ Terms: y0 , perturbed_image
+ --
+ vget: ls:([]) , ty:t
+ Terms: y0 @@ perturbed_image , 1
+ --
+ apply_classifier: ls:(@@) , ty:vector
+ t
+ Terms: y0 , perturbed_image
+ --
+ vget: ls:([]) , ty:t
+ Terms: y0 @@ perturbed_image , y3
+ --
+ apply_classifier: ls:(@@) , ty:vector
+ t
+ Terms: y0 , perturbed_image
+ --
+ vget: ls:([]) , ty:t
+ Terms: y0 @@ perturbed_image , 2
+ --
+ apply_classifier: ls:(@@) , ty:vector
+ t
+ Terms: caisar_op , perturbed_image1
+ --
+ vget: ls:([]) , ty:t
+ Terms: caisar_op @@ perturbed_image1 , 0
+ --
+ apply_classifier: ls:(@@) , ty:vector
+ t
+ Terms: caisar_op , perturbed_image1
+ --
+ vget: ls:([]) , ty:t
+ Terms: caisar_op @@ perturbed_image1 , y31
+ --
+ apply_classifier: ls:(@@) , ty:vector
+ t
+ Terms: caisar_op , perturbed_image1
+ --
+ vget: ls:([]) , ty:t
+ Terms: caisar_op @@ perturbed_image1 , 1
+ --
+ apply_classifier: ls:(@@) , ty:vector
+ t
+ Terms: caisar_op , perturbed_image1
+ --
+ vget: ls:([]) , ty:t
+ Terms: caisar_op @@ perturbed_image1 , y31
+ --
+ apply_classifier: ls:(@@) , ty:vector
+ t
+ Terms: caisar_op , perturbed_image1
+ --
+ vget: ls:([]) , ty:t
+ Terms: caisar_op @@ perturbed_image1 , 2
+ --
+ apply_classifier: ls:(@@) , ty:vector
+ t
+ Terms: caisar_op , perturbed_image1
+ --
+ vget: ls:([]) , ty:t
+ Terms: caisar_op @@ perturbed_image1 , y31
+ --
+ apply_classifier: ls:(@@) , ty:vector
+ t
+ Terms: caisar_op , perturbed_image2
+ --
+ vget: ls:([]) , ty:t
+ Terms: caisar_op @@ perturbed_image2 , 0
+ --
+ apply_classifier: ls:(@@) , ty:vector
+ t
+ Terms: caisar_op , perturbed_image2
+ --
+ vget: ls:([]) , ty:t
+ Terms: caisar_op @@ perturbed_image2 , y32
+ --
+ apply_classifier: ls:(@@) , ty:vector
+ t
+ Terms: caisar_op , perturbed_image2
+ --
+ vget: ls:([]) , ty:t
+ Terms: caisar_op @@ perturbed_image2 , 1
+ --
+ apply_classifier: ls:(@@) , ty:vector
+ t
+ Terms: caisar_op , perturbed_image2
+ --
+ vget: ls:([]) , ty:t
+ Terms: caisar_op @@ perturbed_image2 , y32
+ --
+ apply_classifier: ls:(@@) , ty:vector
+ t
+ Terms: caisar_op , perturbed_image2
+ --
+ vget: ls:([]) , ty:t
+ Terms: caisar_op @@ perturbed_image2 , 2
+ --
+ apply_classifier: ls:(@@) , ty:vector
+ t
+ Terms: caisar_op , perturbed_image2
+ --
+ vget: ls:([]) , ty:t
+ Terms: caisar_op @@ perturbed_image2 , y32
+ reduce_match@e
+ --
+ length: ls:length , ty:int
+ --
+ vget: ls:([]) , ty:(tensor t,
+ int)
+ Terms: caisar_op1 , 0
+ ls_of_caisar_op: (Interpretation.Data
+ (Interpretation.D_csv
+ ["0.0"; "1.0"; "0.784313725"; "0.019607843";
+ "0.776470588"]))
+ ty: tensor
+ t
+ ls: caisar_op2
+ reduce_match@(caisar_op2,
+ 1)
+ --
+ apply_classifier: ls:(@@) , ty:vector
+ t
+ Terms: caisar_op , perturbed_image3
+ --
+ vget: ls:([]) , ty:t
+ Terms: caisar_op @@ perturbed_image3 , 0
+ --
+ apply_classifier: ls:(@@) , ty:vector
+ t
+ Terms: caisar_op , perturbed_image3
+ --
+ vget: ls:([]) , ty:t
+ Terms: caisar_op @@ perturbed_image3 , y33
+ --
+ apply_classifier: ls:(@@) , ty:vector
+ t
+ Terms: caisar_op , perturbed_image3
+ --
+ vget: ls:([]) , ty:t
+ Terms: caisar_op @@ perturbed_image3 , 1
+ --
+ apply_classifier: ls:(@@) , ty:vector
+ t
+ Terms: caisar_op , perturbed_image3
+ --
+ vget: ls:([]) , ty:t
+ Terms: caisar_op @@ perturbed_image3 , y33
+ --
+ apply_classifier: ls:(@@) , ty:vector
+ t
+ Terms: caisar_op , perturbed_image3
+ --
+ vget: ls:([]) , ty:t
+ Terms: caisar_op @@ perturbed_image3 , 2
+ --
+ apply_classifier: ls:(@@) , ty:vector
+ t
+ Terms: caisar_op , perturbed_image3
+ --
+ vget: ls:([]) , ty:t
+ Terms: caisar_op @@ perturbed_image3 , y33
+ --
+ equal_shape: caisar_op2 perturbed_image4
+ ls_of_caisar_op: <var>
+ ty: tensor
+ t
+ ls: caisar_op3
+ --
+ apply_classifier: ls:(@@) , ty:vector
+ t
+ Terms: caisar_op , caisar_op3
+ --
+ vget: ls:([]) , ty:t
+ Terms: caisar_op @@ caisar_op3 , 0
+ --
+ apply_classifier: ls:(@@) , ty:vector
+ t
+ Terms: caisar_op , caisar_op3
+ --
+ vget: ls:([]) , ty:t
+ Terms: caisar_op @@ caisar_op3 , y34
+ --
+ apply_classifier: ls:(@@) , ty:vector
+ t
+ Terms: caisar_op , caisar_op3
+ --
+ vget: ls:([]) , ty:t
+ Terms: caisar_op @@ caisar_op3 , 1
+ --
+ apply_classifier: ls:(@@) , ty:vector
+ t
+ Terms: caisar_op , caisar_op3
+ --
+ vget: ls:([]) , ty:t
+ Terms: caisar_op @@ caisar_op3 , y34
+ --
+ apply_classifier: ls:(@@) , ty:vector
+ t
+ Terms: caisar_op , caisar_op3
+ --
+ vget: ls:([]) , ty:t
+ Terms: caisar_op @@ caisar_op3 , 2
+ --
+ apply_classifier: ls:(@@) , ty:vector
+ t
+ Terms: caisar_op , caisar_op3
+ --
+ vget: ls:([]) , ty:t
+ Terms: caisar_op @@ caisar_op3 , y34
+ --
+ apply_classifier: ls:(@@) , ty:vector
+ t
+ Terms: caisar_op , caisar_op3
+ --
+ vget: ls:([]) , ty:t
+ Terms: caisar_op @@ caisar_op3 , 0
+ --
+ apply_classifier: ls:(@@) , ty:vector
+ t
+ Terms: caisar_op , caisar_op3
+ --
+ vget: ls:([]) , ty:t
+ Terms: caisar_op @@ caisar_op3 , 1
+ --
+ apply_classifier: ls:(@@) , ty:vector
+ t
+ Terms: caisar_op , caisar_op3
+ --
+ vget: ls:([]) , ty:t
+ Terms: caisar_op @@ caisar_op3 , 1
+ --
+ apply_classifier: ls:(@@) , ty:vector
+ t
+ Terms: caisar_op , caisar_op3
+ --
+ vget: ls:([]) , ty:t
+ Terms: caisar_op @@ caisar_op3 , 1
+ --
+ apply_classifier: ls:(@@) , ty:vector
+ t
+ Terms: caisar_op , caisar_op3
+ --
+ vget: ls:([]) , ty:t
+ Terms: caisar_op @@ caisar_op3 , 2
+ --
+ apply_classifier: ls:(@@) , ty:vector
+ t
+ Terms: caisar_op , caisar_op3
+ --
+ vget: ls:([]) , ty:t
+ Terms: caisar_op @@ caisar_op3 , 1
+ --
+ vget: ls:([]) , ty:(tensor t,
+ int)
+ Terms: caisar_op1 , 1
+ ls_of_caisar_op: (Interpretation.Data
+ (Interpretation.D_csv
+ ["1.0"; "0.0"; "0.019607843"; "0.776470588";
+ "0.784313725"]))
+ ty: tensor
+ t
+ ls: caisar_op4
+ reduce_match@(caisar_op4,
+ 0)
+ --
+ apply_classifier: ls:(@@) , ty:vector
+ t
+ Terms: caisar_op , perturbed_image5
+ --
+ vget: ls:([]) , ty:t
+ Terms: caisar_op @@ perturbed_image5 , 0
+ --
+ apply_classifier: ls:(@@) , ty:vector
+ t
+ Terms: caisar_op , perturbed_image5
+ --
+ vget: ls:([]) , ty:t
+ Terms: caisar_op @@ perturbed_image5 , y35
+ --
+ apply_classifier: ls:(@@) , ty:vector
+ t
+ Terms: caisar_op , perturbed_image5
+ --
+ vget: ls:([]) , ty:t
+ Terms: caisar_op @@ perturbed_image5 , 1
+ --
+ apply_classifier: ls:(@@) , ty:vector
+ t
+ Terms: caisar_op , perturbed_image5
+ --
+ vget: ls:([]) , ty:t
+ Terms: caisar_op @@ perturbed_image5 , y35
+ --
+ apply_classifier: ls:(@@) , ty:vector
+ t
+ Terms: caisar_op , perturbed_image5
+ --
+ vget: ls:([]) , ty:t
+ Terms: caisar_op @@ perturbed_image5 , 2
+ --
+ apply_classifier: ls:(@@) , ty:vector
+ t
+ Terms: caisar_op , perturbed_image5
+ --
+ vget: ls:([]) , ty:t
+ Terms: caisar_op @@ perturbed_image5 , y35
+ --
+ equal_shape: caisar_op4 perturbed_image6
+ ls_of_caisar_op: <var>
+ ty: tensor
+ t
+ ls: caisar_op5
+ --
+ apply_classifier: ls:(@@) , ty:vector
+ t
+ Terms: caisar_op , caisar_op5
+ --
+ vget: ls:([]) , ty:t
+ Terms: caisar_op @@ caisar_op5 , 0
+ --
+ apply_classifier: ls:(@@) , ty:vector
+ t
+ Terms: caisar_op , caisar_op5
+ --
+ vget: ls:([]) , ty:t
+ Terms: caisar_op @@ caisar_op5 , y36
+ --
+ apply_classifier: ls:(@@) , ty:vector
+ t
+ Terms: caisar_op , caisar_op5
+ --
+ vget: ls:([]) , ty:t
+ Terms: caisar_op @@ caisar_op5 , 1
+ --
+ apply_classifier: ls:(@@) , ty:vector
+ t
+ Terms: caisar_op , caisar_op5
+ --
+ vget: ls:([]) , ty:t
+ Terms: caisar_op @@ caisar_op5 , y36
+ --
+ apply_classifier: ls:(@@) , ty:vector
+ t
+ Terms: caisar_op , caisar_op5
+ --
+ vget: ls:([]) , ty:t
+ Terms: caisar_op @@ caisar_op5 , 2
+ --
+ apply_classifier: ls:(@@) , ty:vector
+ t
+ Terms: caisar_op , caisar_op5
+ --
+ vget: ls:([]) , ty:t
+ Terms: caisar_op @@ caisar_op5 , y36
+ --
+ apply_classifier: ls:(@@) , ty:vector
+ t
+ Terms: caisar_op , caisar_op5
+ --
+ vget: ls:([]) , ty:t
+ Terms: caisar_op @@ caisar_op5 , 0
+ --
+ apply_classifier: ls:(@@) , ty:vector
+ t
+ Terms: caisar_op , caisar_op5
+ --
+ vget: ls:([]) , ty:t
+ Terms: caisar_op @@ caisar_op5 , 0
+ --
+ apply_classifier: ls:(@@) , ty:vector
+ t
+ Terms: caisar_op , caisar_op5
+ --
+ vget: ls:([]) , ty:t
+ Terms: caisar_op @@ caisar_op5 , 1
+ --
+ apply_classifier: ls:(@@) , ty:vector
+ t
+ Terms: caisar_op , caisar_op5
+ --
+ vget: ls:([]) , ty:t
+ Terms: caisar_op @@ caisar_op5 , 0
+ --
+ apply_classifier: ls:(@@) , ty:vector
+ t
+ Terms: caisar_op , caisar_op5
+ --
+ vget: ls:([]) , ty:t
+ Terms: caisar_op @@ caisar_op5 , 2
+ --
+ apply_classifier: ls:(@@) , ty:vector
+ t
+ Terms: caisar_op , caisar_op5
+ --
+ 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])
caisar_op,
- (Interpretation.Dataset <csv>)
+ (Interpretation.Classifier
+ "$TESTCASE_ROOT/TestNetwork.nnet")
+ caisar_op5, <var>
+ caisar_op3, <var>
+ caisar_op1, (Interpretation.Dataset <csv>)
+ caisar_op4,
+ (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"]))