- (* Pack into an integer the result of the is_* and has_ predicates
- for a given node *)
- type t = int
- let dummy = -1
- (*
- ...44443210
- ...4444 -> kind
- 3 -> has_right
- 2 -> has_left
- 1 -> is_right
- 0 -> is_left
- *)
- let is_left (s : t) : bool =
- s land 1 != 0
-
- let is_right (s : t) : bool =
- s land 0b10 != 0
-
- let has_left (s : t) : bool =
- s land 0b100 != 0
-
- let has_right (s : t) : bool =
- s land 0b1000 != 0
-
- let kind (s : t) : Tree.NodeKind.t =
- Obj.magic (s lsr 4)
-
- let make is_left is_right has_left has_right kind =
- (int_of_bool is_left) lor
- ((int_of_bool is_right) lsl 1) lor
- ((int_of_bool has_left) lsl 2) lor
- ((int_of_bool has_right) lsl 3) lor
- ((Obj.magic kind) lsl 4)
-end
-
-let dummy_set = StateSet.singleton State.dummy
-
-
-
- IFDEF HTMLTRACE
- THEN
-type sat_array = StateSet.t array list
- DEFINE IFHTML(a,b) = (a)
- ELSE
-type sat_array = StateSet.t array
- DEFINE IFHTML(a,b) = (b)
- END
-
-let unsafe_get a i =
- if i < 0 then StateSet.empty else
- Array.unsafe_get (IFHTML(List.hd a, a)) i
-
-let unsafe_set a i v old_v =
- if v != old_v then
- Array.unsafe_set (IFHTML(List.hd a, a)) i v
-
-type 'a run = {
- tree : 'a ;
- (* The argument of the run *)
- auto : Ata.t;
- (* The automaton to be run *)
- mutable sat: sat_array;
- (* A mapping from node preorders to states satisfied at that node *)
- mutable pass : int;
- (* Number of run we have performed *)
- mutable fetch_trans_cache : Ata.Formula.t Cache.N2.t;
- (* A cache from states * label to list of transitions *)
- mutable td_cache : StateSet.t Cache.N6.t;
- mutable bu_cache : StateSet.t Cache.N6.t;
- (* Two 6-way caches used during the top-down and bottom-up phase
- label * self-set * fc-set * ns-set * parent-set * node-shape -> self-set
- *)
- node_summaries: (int, int16_unsigned_elt, c_layout) Array1.t;
- stats : stats;
-}