Commit 2a949e57 authored by Aymeric Varasse's avatar Aymeric Varasse
Browse files

Adapt pp_relu_linear to CAMUS network

parent 0ca0cec2
......@@ -426,10 +426,11 @@ let pp_relu_linear tname n env t g =
let idx_1 = Base.List.nth_exn idx 1 in
(* let idx_2 = Base.List.nth_exn idx 2 in
let idx_3 = Base.List.nth_exn idx 3 in *)
match Base.List.nth_exn to_activate (idx_1 * (Base.Int.of_float(Base.Float.sqrt (Base.Float.of_int(List.length n_op))))
(* match Base.List.nth_exn to_activate (idx_1 * (Base.Int.of_float(Base.Float.sqrt (Base.Float.of_int(List.length n_op))))
+ idx_0 * (Base.Int.of_float(Base.Float.sqrt (Base.Float.of_int(List.length n_op))))
(* + idx_0 * 3 *)
) with
) with *)
match false with
| true -> "(assert (= |CELL_"^tname^idx_str^"| |CELL_"^pname^idx_str^"|))"
| false -> begin match t with
| Linear_Real_Theory | Real_Theory -> "(assert (= |CELL_"^tname^idx_str^"| 0))"
......@@ -437,11 +438,6 @@ let pp_relu_linear tname n env t g =
end
in
(* let lin_relu t = match t with
| Real_Theory | Linear_Real_Theory -> "reluR"
| Float_Theory -> "reluFP"
in *)
(* get_unary_op (lin_relu t) pname tname (List.map ~f:relu_cell_to_smt (get_flat_indices_cfg size)) *)
List.map relu_cell_to_smt (all_coords size)
(* Apparently Keras puts an identity layer at the end
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment