| Ref (k, i) -> "-" ^ J.string_of_mark k ^ "-" ^ string_of_int i
| Unk -> "-" ^ J.string_of_mark k
+(* Note: remove assigned variables *)
let pp_table st =
- let map k n =
+ let map k n =
warn (Printf.sprintf "%s: v %s (s:%b b:%b)"
(J.string_of_mark k) (string_of_value k n.v) n.s n.b
)
let rec generated st h i =
let default = dynamic h i in
let k = J.new_mark () in
- match resolve_key_with_default st default k with
- | k, n when n = default -> if !G.trace >= level then pp_table st; n
- | _, n when n.s = true -> generated st h i
- | _ -> assert false
+ let k, n = resolve_key_with_default st default k in
+ if n.s then generated st h i else begin
+ if n <> default then H.replace st k default;
+ if !G.trace >= level then pp_table st; default
+ end
let assert_finite st n j =
if !G.trace >= level then warn (Printf.sprintf "ASSERT FINITE %u" j);
if !G.trace >= level then warn "UNKNOWN";
let default = empty () in
let k = J.new_mark () in
- match resolve_key_with_default st default k with
- | k, n when n = default -> if !G.trace >= level then pp_table st; cell true (Ref (k, 0))
- | _, n when n.s = true -> n
- | _ -> unknown st
-
+ let k, n = resolve_key_with_default st default k in
+ if n.s then match n.v with
+ | Inf
+ | Fin _ -> n
+ | Unk -> if !G.trace >= level then pp_table st; cell true (Ref (k, 0))
+ | Ref _ -> assert false
+ else unknown st
+
let minus st n j =
if !G.trace >= level then warn (Printf.sprintf "MINUS %u" j);
let rec aux k n j = match n.v with
let is_not_zero st n =
let _, n = resolve_layer st n in n.v <> zero
+