(***********************************************************************)
(*
- Time-stamp: <Last modified on 2013-01-30 19:09:27 CET by Kim Nguyen>
+ Time-stamp: <Last modified on 2013-02-06 14:24:24 CET by Kim Nguyen>
*)
open Format
+type move = [ `Left | `Right | `Up1 | `Up2 | `Epsilon ]
+type state_ctx = { left : StateSet.t;
+ right : StateSet.t;
+ up1 : StateSet.t;
+ up2 : StateSet.t;
+ epsilon : StateSet.t}
+type ctx_ = { mutable positive : state_ctx;
+ mutable negative : state_ctx }
+type pred_ = move * bool * State.t
+module Move : (Formula.PREDICATE with type data = pred_ and type ctx = ctx_ ) =
+struct
+
+ module Node =
+ struct
+ type t = move * bool * State.t
+ let equal n1 n2 = n1 = n2
+ let hash n = Hashtbl.hash n
+ end
+
+ type ctx = ctx_
+ let make_ctx a b c d e =
+ { left = a; right = b; up1 = c; up2 = d; epsilon = e }
+
+ include Hcons.Make(Node)
+
+ let print ppf a =
+ let _ = flush_str_formatter() in
+ let fmt = str_formatter in
+
+ let m, b, s = a.node in
+ let dir,num =
+ match m with
+ | `Left -> Pretty.down_arrow, Pretty.subscript 1
+ | `Right -> Pretty.down_arrow, Pretty.subscript 2
+ | `Epsilon -> Pretty.epsilon, ""
+ | `Up1 -> Pretty.up_arrow, Pretty.subscript 1
+ | `Up2 -> Pretty.up_arrow, Pretty.subscript 2
+ in
+ fprintf fmt "%s%s" dir num;
+ State.print fmt s;
+ let str = flush_str_formatter() in
+ if b then fprintf ppf "%s" str
+ else Pretty.pp_overline ppf str
+
+ let neg p =
+ let l, b, s = p.node in
+ make (l, not b, s)
+
+ let eval ctx p =
+ let l, b, s = p.node in
+ let nctx = if b then ctx.positive else ctx.negative in
+ StateSet.mem s begin
+ match l with
+ `Left -> nctx.left
+ | `Right -> nctx.right
+ | `Up1 -> nctx.up1
+ | `Up2 -> nctx.up2
+ | `Epsilon -> nctx.epsilon
+ end
+end
+
+module SFormula = Formula.Make(Move)
type t = {
id : Uid.t;
mutable states : StateSet.t;
mutable top_states : StateSet.t;
mutable bottom_states: StateSet.t;
mutable selection_states: StateSet.t;
- transitions: (State.t, (QNameSet.t*Formula.t) list) Hashtbl.t;
+ transitions: (State.t, (QNameSet.t*SFormula.t) list) Hashtbl.t;
}
+
+
let next = Uid.make_maker ()
let create () = { id = next ();
(rem, tr :: atrs)
else
let nrem = QNameSet.diff rem labs in
- nrem, (nlabs, Formula.or_ phi f)::atrs
+ nrem, (nlabs, SFormula.or_ phi f)::atrs
) (s, []) trs
in
let ntrs = if QNameSet.is_empty rem then ntrs
let strs_strings, maxs = List.fold_left (fun (accl, accm) (q, s, f) ->
let s1 = State.print sfmt q; flush_str_formatter () in
let s2 = QNameSet.print sfmt s; flush_str_formatter () in
- let s3 = Formula.print sfmt f; flush_str_formatter () in
+ let s3 = SFormula.print sfmt f; flush_str_formatter () in
( (s1, s2, s3) :: accl,
max
accm (2 + String.length s1 + String.length s2))
(***********************************************************************)
(*
- Time-stamp: <Last modified on 2013-02-04 16:03:28 CET by Kim Nguyễn>
+ Time-stamp: <Last modified on 2013-02-06 14:30:27 CET by Kim Nguyen>
*)
INCLUDE "utils.ml"
open Format
+(*
+
+(** Implementation of hashconsed Boolean formulae *)
+
type move = [ `Left | `Right | `Epsilon | `Up1 | `Up2 ]
-type 'formula expr =
+
+(** Direction for automata predicates *)
+*)
+module type PREDICATE =
+sig
+ type t
+ type ctx
+ val eval : ctx -> t -> bool
+ val neg : t -> t
+ include Hcons.Abstract with type t := t
+ include Sigs.AUX.Printable with type t := t
+end
+
+type ('formula,'pred) expr =
| False
| True
| Or of 'formula * 'formula
| And of 'formula * 'formula
- | Atom of move * bool * State.t
+ | Atom of 'pred
+
+module Make (P: PREDICATE) =
+struct
-type 'hcons node = {
- pos : 'hcons expr;
- mutable neg : 'hcons;
-}
-external hash_const_variant : [> ] -> int = "%identity"
-external vb : bool -> int = "%identity"
+ type 'hcons node = {
+ pos : ('hcons,P.t) expr;
+ mutable neg : 'hcons;
+ }
-module rec Node : Hcons.S
- with type data = Data.t = Hcons.Make (Data)
- and Data : Hashtbl.HashedType with type t = Node.t node =
+ external hash_const_variant : [> ] -> int = "%identity"
+ external vb : bool -> int = "%identity"
+
+ module rec Node : Hcons.S
+ with type data = Data.t = Hcons.Make (Data)
+ and Data : Hashtbl.HashedType with type t = Node.t node =
struct
type t = Node.t node
let equal x y =
match x.pos, y.pos with
| a,b when a == b -> true
| Or(xf1, xf2), Or(yf1, yf2)
- | And(xf1, xf2), And(yf1,yf2) -> (xf1 == yf1) && (xf2 == yf2)
- | Atom(d1, p1, s1), Atom(d2 ,p2 ,s2) -> d1 == d2 && p1 == p2 && s1 == s2
+ | And(xf1, xf2), And(yf1,yf2) -> xf1 == yf1 && xf2 == yf2
+ | Atom(p1), Atom(p2) -> p1 == p2
| _ -> false
let hash f =
| False -> 0
| True -> 1
| Or (f1, f2) ->
- HASHINT3 (PRIME1, Uid.to_int f1.Node.id, Uid.to_int f2.Node.id)
+ HASHINT3 (PRIME1, Uid.to_int f1.Node.id, Uid.to_int f2.Node.id)
| And (f1, f2) ->
- HASHINT3(PRIME3, Uid.to_int f1.Node.id, Uid.to_int f2.Node.id)
-
- | Atom(d, p, s) -> HASHINT4(PRIME5, hash_const_variant d,vb p,s)
+ HASHINT3(PRIME3, Uid.to_int f1.Node.id, Uid.to_int f2.Node.id)
+ | Atom(p) -> HASHINT2(PRIME5, Uid.to_int (P.uid p))
end
-type t = Node.t
-let hash x = x.Node.hash
-let uid x = x.Node.id
-let equal = Node.equal
-let expr f = f.Node.node.pos
-
-let compare f1 f2 = compare f1.Node.id f2.Node.id
-let prio f =
- match expr f with
- | True | False -> 10
- | Atom _ -> 8
- | And _ -> 6
- | Or _ -> 1
-
-let rec print ?(parent=false) ppf f =
- if parent then fprintf ppf "(";
- let _ = match expr f with
- | True -> fprintf ppf "%s" Pretty.top
- | False -> fprintf ppf "%s" Pretty.bottom
- | And(f1,f2) ->
- print ~parent:(prio f > prio f1) ppf f1;
- fprintf ppf " %s " Pretty.wedge;
- print ~parent:(prio f > prio f2) ppf f2;
- | Or(f1,f2) ->
- (print ppf f1);
- fprintf ppf " %s " Pretty.vee;
- (print ppf f2);
- | Atom(dir, b, s) ->
- let _ = flush_str_formatter() in
- let fmt = str_formatter in
- let a_str, d_str =
+ type t = Node.t
+ let hash x = x.Node.hash
+ let uid x = x.Node.id
+ let equal = Node.equal
+ let expr f = f.Node.node.pos
+
+ let compare f1 f2 = compare f1.Node.id f2.Node.id
+ let prio f =
+ match expr f with
+ | True | False -> 10
+ | Atom _ -> 8
+ | And _ -> 6
+ | Or _ -> 1
+
+ let rec print ?(parent=false) ppf f =
+ if parent then fprintf ppf "(";
+ let _ = match expr f with
+ | True -> fprintf ppf "%s" Pretty.top
+ | False -> fprintf ppf "%s" Pretty.bottom
+ | And(f1,f2) ->
+ print ~parent:(prio f > prio f1) ppf f1;
+ fprintf ppf " %s " Pretty.wedge;
+ print ~parent:(prio f > prio f2) ppf f2;
+ | Or(f1,f2) ->
+ (print ppf f1);
+ fprintf ppf " %s " Pretty.vee;
+ (print ppf f2);
+ | Atom(p) -> fprintf ppf "%a" P.print p
+(* let _ = flush_str_formatter() in
+ let fmt = str_formatter in
+ let a_str, d_str =
match dir with
| `Left -> Pretty.down_arrow, Pretty.subscript 1
| `Right -> Pretty.down_arrow, Pretty.subscript 2
State.print fmt s;
let str = flush_str_formatter() in
if b then fprintf ppf "%s" str
- else Pretty.pp_overline ppf str
+ else Pretty.pp_overline ppf str *)
in
if parent then fprintf ppf ")"
let cons pos neg =
- let nnode = Node.make { pos = neg; neg = (Obj.magic 0); } in
+ let nnode = Node.make { pos = neg; neg = Obj.magic 0 } in
let pnode = Node.make { pos = pos; neg = nnode } in
(Node.node nnode).neg <- pnode; (* works because the neg field isn't taken into
account for hashing ! *)
let true_,false_ = cons True False
-let atom_ d p s =
- fst (cons (Atom(d,p,s)) (Atom(d,not p,s)))
-let not_ f = f.Node.node.neg
+let atom_ p = fst (cons (Atom(p)) (Atom(P.neg p)))
+let not_ f = f.Node.node.neg
-let order f1 f2 = if uid f1 < uid f2 then f2,f1 else f1,f2
+let order f1 f2 = if uid f1 < uid f2 then f2,f1 else f1,f2
let or_ f1 f2 =
(* Tautologies: x|x, x|not(x) *)
let of_bool = function true -> true_ | false -> false_
+let rec eval ctx f =
+ match f.Node.node.pos with
+ True -> true
+ | False -> false
+ | Atom p -> P.eval ctx p
+ | And(f1, f2) -> eval ctx f1 && eval ctx f2
+ | Or(f1, f2) -> eval ctx f1 || eval ctx f2
+
+end
(***********************************************************************)
(*
- Time-stamp: <Last modified on 2013-02-04 16:04:03 CET by Kim Nguyễn>
+ Time-stamp: <Last modified on 2013-02-05 16:11:43 CET by Kim Nguyen>
*)
-(** Implementation of hashconsed Boolean formulae *)
-
-type move = [ `Left | `Right | `Epsilon | `Up1 | `Up2 ]
-
-(** Direction for automata predicates *)
-
-type 'formula expr =
+module type PREDICATE =
+sig
+ type t
+ type ctx
+ val eval : ctx -> t -> bool
+ val neg : t -> t
+ include Hcons.Abstract with type t := t
+ include Sigs.AUX.Printable with type t := t
+end
+
+type ('formula,'pred) expr =
| False
| True
| Or of 'formula * 'formula
| And of 'formula * 'formula
- | Atom of move * bool * State.t
+ | Atom of 'pred
(** View of the internal representation of a formula,
used for pattern matching *)
-type t
-
-(** Abstract type representing hashconsed formulae *)
+module Make(P : PREDICATE) :
+sig
+ type t
-val hash : t -> int
-(** Hash function for formulae *)
+ (** Abstract type representing hashconsed formulae *)
-val uid : t -> Uid.t
-(** Returns a unique ID for formulae *)
+ val hash : t -> int
+ (** Hash function for formulae *)
-val equal : t -> t -> bool
-(** Equality over formulae *)
+ val uid : t -> Uid.t
+ (** Returns a unique ID for formulae *)
-val expr : t -> t expr
-(** Equality over formulae *)
+ val equal : t -> t -> bool
+ (** Equality over formulae *)
-(*val st : t -> StateSet.t * StateSet.t
-(** states occuring left and right, positively or negatively *)
-*)
-
-val compare : t -> t -> int
-(** Comparison of formulae *)
+ val expr : t -> (t,P.t) expr
+ (** Equality over formulae *)
-val print : Format.formatter -> t -> unit
-(** Pretty printer *)
+ val compare : t -> t -> int
+ (** Comparison of formulae *)
-val is_true : t -> bool
-(** [is_true f] tests whether the formula is the atom True *)
+ val print : Format.formatter -> t -> unit
+ (** Pretty printer *)
-val is_false : t -> bool
-(** [is_false f] tests whether the formula is the atom False *)
+ val is_true : t -> bool
+ (** [is_true f] tests whether the formula is the atom True *)
-val true_ : t
-(** Atom True *)
+ val is_false : t -> bool
+ (** [is_false f] tests whether the formula is the atom False *)
-val false_ : t
-(** Atom False *)
-
-val atom_ : move -> bool -> StateSet.elt -> t
-(** [atom_ dir b q] creates a down_left or down_right atom for state
- [q]. The atom is positive if [b == true].
-*)
+ val true_ : t
+ (** Atom True *)
-val not_ : t -> t
-val or_ : t -> t -> t
-val and_ : t -> t -> t
-(** Boolean connective *)
+ val false_ : t
+ (** Atom False *)
-val of_bool : bool -> t
-(** Convert an ocaml Boolean value to a formula *)
+ val atom_ : P.t -> t
+ (** [atom_ dir b q] creates a down_left or down_right atom for state
+ [q]. The atom is positive if [b == true].
+ *)
+
+ val not_ : t -> t
+ val or_ : t -> t -> t
+ val and_ : t -> t -> t
+ (** Boolean connective *)
+
+ val of_bool : bool -> t
+ (** Convert an ocaml Boolean value to a formula *)
+
+ val eval : P.ctx -> t -> bool
+ (** Evaluate a formula given a context for atomic predicates *)
+end
(***********************************************************************)
(*
- Time-stamp: <Last modified on 2013-01-30 19:08:47 CET by Kim Nguyen>
+ Time-stamp: <Last modified on 2013-02-06 14:26:22 CET by Kim Nguyen>
*)
include Sigs.HCONS
let init () =
T.clear pool;
uid_make := Uid.make_maker ()
+ let dummy x = { id = Uid.dummy; hash = H.hash x; node = x }
let make x =
let cell = { id = Uid.dummy; hash = H.hash x; node = x } in
let hash v = v
let uid v = Uid.of_int v
-
+ let dummy _ = ~-1
let equal x y = x == y
let init () = ()
(***********************************************************************)
(*
- Time-stamp: <Last modified on 2013-01-30 19:07:19 CET by Kim Nguyen>
+ Time-stamp: <Last modified on 2013-02-05 15:58:13 CET by Kim Nguyen>
*)
(** This module contains all the signatures of the project, to avoid
(** Initializes the internal storage. Any previously hashconsed
element is discarded. *)
val init : unit -> unit
+
+ (** Create a dummy (non-hashconsed) node with a boggus identifer
+ and hash *)
+ val dummy : data -> t
end