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

Fixed issue with unexpected sat facets

parent bbf948a7
......@@ -427,19 +427,22 @@ let pp_relu_linear tname n env t g =
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
(* let idx_0 = Base.List.nth_exn idx 1 in
let idx_1 = Base.List.nth_exn idx 0 in *)
let constraint_string =
let table = Base.List.nth_exn tbl idx_1 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 tl_f = fun (k,v) -> (match k with "b" -> ("b", v) | _ -> (Base.List.nth_exn (Base.String.split ~on:'x' k) 1), v) 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
Base.List.fold table_list ~init:"" ~f:(fun acc (k, v) -> match k with
| "b" -> acc^(float_of_string_accurate v t)
| _ -> acc^" (* "^"|CELL_actual_input_0_0_0_"^k^"| "^(float_of_string_accurate v t)) 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)))^\n(> (_ +zero 11 53) "^constraint_string^")"
| Linear_Real_Theory | Real_Theory -> "(assert (= |CELL_"^tname^idx_str^"| 0))\n(assert (> 0 (+"^constraint_string^"))"
| Float_Theory -> "(assert (= |CELL_"^tname^idx_str^"| (_ +zero 11 53)))^\n(assert (> (_ +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