aboutsummaryrefslogtreecommitdiffstats
path: root/kvx/abstractbb/Impure/ocaml/ImpHConsOracles.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kvx/abstractbb/Impure/ocaml/ImpHConsOracles.ml')
-rw-r--r--kvx/abstractbb/Impure/ocaml/ImpHConsOracles.ml66
1 files changed, 0 insertions, 66 deletions
diff --git a/kvx/abstractbb/Impure/ocaml/ImpHConsOracles.ml b/kvx/abstractbb/Impure/ocaml/ImpHConsOracles.ml
deleted file mode 100644
index 2b66899b..00000000
--- a/kvx/abstractbb/Impure/ocaml/ImpHConsOracles.ml
+++ /dev/null
@@ -1,66 +0,0 @@
-open ImpPrelude
-open HConsingDefs
-
-let make_dict (type key) (p: key Dict.hash_params) =
- let module MyHashedType = struct
- type t = key
- let equal = p.Dict.test_eq
- let hash = p.Dict.hashing
- end in
- let module MyHashtbl = Hashtbl.Make(MyHashedType) in
- let dict = MyHashtbl.create 1000 in
- {
- Dict.set = (fun (k,d) -> MyHashtbl.replace dict k d);
- Dict.get = (fun k -> MyHashtbl.find_opt dict k)
- }
-
-
-exception Stop;;
-
-let xhCons (type a) (hp:a hashP) =
- (* We use a hash-table, but a hash-set would be sufficient ! *)
- (* Thus, we could use a weak hash-set, but prefer avoid it for easier debugging *)
- (* Ideally, a parameter would allow to select between the weak or full version *)
- let module MyHashedType = struct
- type t = a hashinfo
- let equal x y = hp.hash_eq x.hdata y.hdata
- let hash x = Hashtbl.hash x.hcodes
- end in
- let module MyHashtbl = Hashtbl.Make(MyHashedType) in
- let pick t =
- let res = ref None in
- try
- MyHashtbl.iter (fun k d -> res:=Some (k,d); raise Stop) t;
- None
- with
- | Stop -> !res
- in
- let t = MyHashtbl.create 1000 in
- let logs = ref [] in
- {
- hC = (fun (k:a hashinfo) ->
- match MyHashtbl.find_opt t k with
- | Some d -> d
- | None -> (*print_string "+";*)
- let d = hp.set_hid k.hdata (MyHashtbl.length t) in
- MyHashtbl.add t {k with hdata = d } d; d);
- next_log = (fun info -> logs := (MyHashtbl.length t, info)::(!logs));
- next_hid = (fun () -> MyHashtbl.length t);
- remove = (fun (x:a hashinfo) -> MyHashtbl.remove t x);
- export = fun () ->
- match pick t with
- | None -> { get_info = (fun _ -> raise Not_found); iterall = (fun _ -> ()) }
- | Some (k,_) ->
- (* the state is fully copied at export ! *)
- let logs = ref (List.rev_append (!logs) []) in
- let rec step_log i =
- match !logs with
- | (j, info)::l' when i>=j -> logs:=l'; info::(step_log i)
- | _ -> []
- in let a = Array.make (MyHashtbl.length t) k in
- MyHashtbl.iter (fun k d -> a.(hp.get_hid d) <- k) t;
- {
- get_info = (fun i -> a.(i));
- iterall = (fun iter_node -> Array.iteri (fun i k -> iter_node (step_log i) i k) a)
- }
- }