X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=blobdiff_plain;f=src%2Fformula.ml;h=1e440bc23f9778bd7c4c68bed85a93ea026d1136;hp=1dd0f14f0d2d2ac422c451ecc1946409cedc943b;hb=41dd1fed04cabad212f10fce3484545f6e9d9444;hpb=f5d90fb688bc1a9b29815fc33c369856e6c51a67 diff --git a/src/formula.ml b/src/formula.ml index 1dd0f14..1e440bc 100644 --- a/src/formula.ml +++ b/src/formula.ml @@ -5,45 +5,61 @@ (* Kim Nguyen, LRI UMR8623 *) (* Université Paris-Sud & CNRS *) (* *) -(* Copyright 2010-2012 Université Paris-Sud and Centre National de la *) +(* Copyright 2010-2013 Université Paris-Sud and Centre National de la *) (* Recherche Scientifique. All rights reserved. This file is *) (* distributed under the terms of the GNU Lesser General Public *) (* License, with the special exception on linking described in file *) (* ../LICENSE. *) (* *) (***********************************************************************) + 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 - | Move of (move * bool * State.t) - | Label of QNameSet.t + | Atom of 'atom + +module Make (P: ATOM) = +struct + -type 'hcons node = { - pos : 'hcons expr; - mutable neg : 'hcons; -} + type 'hcons node = { + pos : ('hcons,P.t) expr; + mutable neg : 'hcons; + } -external hash_const_variant : [> ] -> int = "%identity" -external vb : bool -> int = "%identity" + 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 = + 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 = (*x.size == y.size &&*) + 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 - | Label s1, Label s2 -> s1 == s2 + | And(xf1, xf2), And(yf1,yf2) -> xf1 == yf1 && xf2 == yf2 + | Atom(p1), Atom(p2) -> p1 == p2 | _ -> false let hash f = @@ -51,57 +67,55 @@ 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) - | Label s -> HASHINT2(PRIME7, Uid.to_int s.QNameSet.id) + 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.key -let uid x = x.Node.id -let equal = Node.equal -let expr f = f.Node.node.pos -(*let st f = f.Node.node.st*) -(*let size f = f.Node.node.size*) -let compare f1 f2 = compare f1.Node.id f2.Node.id -let prio f = - match expr f with - | True | False -> 10 - | Move _ -> 8 - | Label _ -> 7 - | 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); - | Label s -> fprintf ppf "%a" QNameSet.print s - | 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 + | `Epsilon -> Pretty.epsilon, "" + | `Up1 -> Pretty.up_arrow, Pretty.subscript 1 + | `Up2 -> Pretty.up_arrow, Pretty.subscript 2 in fprintf fmt "%s%s" a_str d_str; 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 ")" @@ -111,38 +125,21 @@ let is_true f = (expr f) == True let is_false f = (expr f) == False -let cons pos neg s1 s2 size1 size2 = - let nnode = Node.make { pos = neg; neg = (Obj.magic 0); st = s2; size = size2 } in - let pnode = Node.make { pos = pos; neg = nnode ; st = s1; size = size1 } in +let cons pos neg = + 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 ! *) pnode,nnode -let empty_pair = StateSet.empty, StateSet.empty -let true_,false_ = cons True False empty_pair empty_pair 0 0 -let atom_ d p s = - let si = StateSet.singleton s in - let ss = match d with - | `Left -> si, StateSet.empty - | `Right -> StateSet.empty, si - in fst (cons (Atom(d,p,s)) (Atom(d,not p,s)) ss ss 1 1) - -let not_ f = f.Node.node.neg +let true_,false_ = cons True False -let union_pair (l1,r1) (l2, r2) = - StateSet.union l1 l2, - StateSet.union r1 r2 +let atom_ p = fst (cons (Atom(p)) (Atom(P.neg p))) -let merge_states f1 f2 = - let sp = - union_pair (st f1) (st f2) - and sn = - union_pair (st (not_ f1)) (st (not_ f2)) - in - sp,sn +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) *) @@ -159,10 +156,7 @@ let or_ f1 f2 = (* commutativity of | *) else let f1, f2 = order f1 f2 in - let psize = (size f1) + (size f2) in - let nsize = (size (not_ f1)) + (size (not_ f2)) in - let sp, sn = merge_states f1 f2 in - fst (cons (Or(f1,f2)) (And(not_ f1, not_ f2)) sp sn psize nsize) + fst (cons (Or(f1,f2)) (And(not_ f1, not_ f2))) let and_ f1 f2 = @@ -171,12 +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 -module Infix = struct - let ( +| ) f1 f2 = or_ f1 f2 - - let ( *& ) f1 f2 = and_ f1 f2 - - let ( *+ ) d s = atom_ d true s - let ( *- ) d s = atom_ d false s end