X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=blobdiff_plain;f=src%2Fformula.ml;h=1e440bc23f9778bd7c4c68bed85a93ea026d1136;hp=f4022f91e6346bdf3c43412c186a8e4dada91fb5;hb=41dd1fed04cabad212f10fce3484545f6e9d9444;hpb=6b66008811639324be623a42037b60e02056772c diff --git a/src/formula.ml b/src/formula.ml index f4022f9..1e440bc 100644 --- a/src/formula.ml +++ b/src/formula.ml @@ -13,42 +13,53 @@ (* *) (***********************************************************************) -(* - Time-stamp: -*) - INCLUDE "utils.ml" open Format +(* -type move = [ `Left | `Right | `Epsilon | `Up1 | `Up2 ] -type 'formula expr = +(** Implementation of hashconsed Boolean formulae *) + +*) +module type ATOM = +sig + type t + val neg : t -> t + include Hcons.Abstract with type t := t + include Common_sig.Printable with type t := t +end + +type ('formula,'atom) expr = | False | True | Or of 'formula * 'formula | And of 'formula * 'formula - | Atom of move * bool * State.t + | Atom of 'atom + +module Make (P: ATOM) = +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 : Common_sig.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) - | Move(d1, p1, s1), Move(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 = @@ -56,44 +67,43 @@ module rec Node : Hcons.S | 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) - - | Move(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 - | Move _ -> 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); - | Move(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 @@ -105,7 +115,7 @@ let rec print ?(parent=false) ppf f = 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 ")" @@ -116,7 +126,7 @@ let is_false f = (expr f) == False 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 ! *) @@ -124,13 +134,12 @@ let cons pos neg = let true_,false_ = cons True False -let atom_ d p s = - fst (cons (Move(d,p,s)) (Move(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) *) @@ -156,3 +165,13 @@ let and_ f1 f2 = let of_bool = function true -> true_ | false -> false_ +let fold f phi acc = + let rec loop phi acc = + match expr phi with + | And (phi1, phi2) | Or(phi1, phi2) -> + loop phi2 (loop phi1 (f phi acc)) + | _ -> f phi acc + in + loop phi acc + +end