Commit 7be2e0bf authored by Aymeric Varasse's avatar Aymeric Varasse
Browse files

Fix pp_relu_linear to set linear regions to inputs

parent 97a5dc1c
......@@ -415,24 +415,27 @@ let pp_relu_linear tname n env t g =
let n_op = match n.operator_parameters with
| Some p -> (match p with
| IR.Vertex.RW_Linearized_ReLu_params x -> Base.fst x
| IR.Vertex.RW_Linearized_ReLu_params x -> x
| _ -> failwith "Something is odd with the type of the operator_parameters")
| None -> failwith "Something is odd with the operator_parameters"
in
let tbl = Base.fst (Base.snd n_op) in
let is_positive x = if (x >= 0.) then true else false in
let is_positive_tuple (x0, x1, x2) = [is_positive x0; is_positive x1; is_positive x2] in
let to_activate = Base.List.map ~f:is_positive_tuple n_op in
let to_activate = Base.List.map ~f:is_positive_tuple (Base.fst n_op) in
let relu_cell_to_smt idx =
let idx_str = stringify_int idx in
let idx_0 = Base.List.nth_exn idx 2 in
let idx_1 = Base.List.nth_exn idx 3 in
match Base.List.nth_exn
(* (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) *)
(Base.List.nth_exn to_activate idx_1) idx_0
let constraint_string =
let table = Base.List.nth_exn tbl idx_1 in
Base.Hashtbl.fold table ~init:"" ~f:(fun ~key:k ~data:v acc -> acc^"( *"^" "^k^" "^ (Float.to_string v))
in
match Base.List.nth_exn (Base.List.nth_exn to_activate idx_1) idx_0
with
| true -> "(assert (= |CELL_"^tname^idx_str^"| |CELL_"^pname^idx_str^"|))\n (assert (> 0"
| true -> "(assert (= |CELL_"^tname^idx_str^"| |CELL_"^pname^idx_str^"|))\n (assert (< 0 "^constraint_string
| false -> begin match t with
| Linear_Real_Theory | Real_Theory -> "(assert (= |CELL_"^tname^idx_str^"| 0))"
| Linear_Real_Theory | Real_Theory -> "(assert (= |CELL_"^tname^idx_str^"| 0))\n (> 0 "^constraint_string
| Float_Theory -> "(assert (= |CELL_"^tname^idx_str^"| (_ +zero 11 53)))"
end
in
......
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