-(* module Ptset : sig
+(* module Ptset : sig
include Set.S with type elt = int
val from_list : elt list -> t
end
-*)
+ *)
type state = int
val mk_state : unit -> state
| True
| Or of formula * formula
| And of formula * formula
- | Atom of ([ `Left | `Right ] * bool * state)
-and formula = { fid : int; pos : formula_expr; neg : formula; st : Ptset.t*Ptset.t; size: int;}
+ | Atom of ([ `Left | `Right | `LLeft | `RRight ] * bool * state)
+and formula = { fid : int; fkey : int; pos : formula_expr; neg : formula; st : (Ptset.t*Ptset.t)*(Ptset.t*Ptset.t); size: int;}
val true_ : formula
val false_ : formula
-val atom_ : [`Left | `Right ] -> bool -> state -> formula
+val atom_ : [`Left | `Right | `LLeft | `RRight ] -> bool -> state -> formula
val and_ : formula -> formula -> formula
val or_ : formula -> formula -> formula
val not_ : formula -> formula
-val equal_form : formula -> formula -> bool
+(*val equal_form : formula -> formula -> bool *)
val pr_frm : Format.formatter -> formula -> unit
val ( >=> ) : state*(TagSet.t*bool*predicate) -> formula -> t
val ( +| ) : formula -> formula -> formula
val ( *& ) : formula -> formula -> formula
-val ( ** ) : [`Left | `Right ] -> state -> formula
+val ( ** ) : [`Left | `Right | `LLeft | `RRight ] -> state -> formula
end
type transition = Transitions.t
-val equal_trans : transition -> transition -> bool
+val equal_trans : transition -> transition -> bool
module TS : sig
type t
val to_list_rev : t -> Tree.Binary.t list
val length : t -> int
val iter : (Tree.Binary.t -> unit) -> t -> unit
+ val rev_iter : (Tree.Binary.t -> unit) -> t -> unit
+ val find : (Tree.Binary.t -> bool) -> t -> Tree.Binary.t
end
-module BottomUpNew :
-sig
+(*module BottomUpJumpNew :
+sig *)
val run : t -> Tree.Binary.t -> TS.t
-end
+ val run_count : t -> Tree.Binary.t -> int
+ val run_time : t -> Tree.Binary.t -> TS.t
+(*end *)
+