Commit bbf948a7 authored by Aymeric Varasse's avatar Aymeric Varasse
Browse files

Added constraints on inputs for linearized ReLUs

parent 7be2e0bf
......@@ -429,14 +429,17 @@ let pp_relu_linear tname n env t g =
let idx_1 = Base.List.nth_exn idx 3 in
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
let tl = Base.Hashtbl.to_alist table in
let tl_f = fun (k,v) -> (match k with "b" -> ("b", v) | _ -> "actual_input_0_0_0_"^(Base.List.nth_exn (Base.String.split ~on:'x' k) 1) , v) in
(* let table_list = Base.List.map ~f:(fun t -> (match (Base.fst t) with "b" -> ("b", (Base.snd t)) | _ -> "actual_input_0_0_0_"^(Base.List.nth_exn (Base.String.split ~on:'x' (Base.fst t)) 1) , (Base.snd t)) (Base.Hashtbl.to_alist table) in *)
let table_list = Base.List.map ~f:(tl_f) tl in
Base.List.fold table_list ~init:"" ~f:(fun acc (k, v) -> 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 "^constraint_string
| 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))\n (> 0 "^constraint_string
| Float_Theory -> "(assert (= |CELL_"^tname^idx_str^"| (_ +zero 11 53)))"
| 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)))^\n(> (_ +zero 11 53) "^constraint_string^")"
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