From: Kim Nguyễn Date: Wed, 17 Jul 2013 15:59:01 +0000 (+0200) Subject: Sanitize the representation of formula X-Git-Tag: v0.1~73 X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=commitdiff_plain;h=90ce5857f6cad2ebc753fdbc8e37882a1ff47415 Sanitize the representation of formula - rename the toplevel Formula module to Boolean - rename Ata.SFormula to Formula - move the flag saying whether an atom is positive or negative to Boolean - distinguish predicates that are moves from generic predicates. --- diff --git a/src/ata.ml b/src/ata.ml index df43392..3fa2698 100644 --- a/src/ata.ml +++ b/src/ata.ml @@ -15,32 +15,27 @@ INCLUDE "utils.ml" open Format +type move = [ `First_child + | `Next_sibling + | `Parent + | `Previous_sibling + | `Stay ] -type predicate = | First_child - | Next_sibling - | Parent - | Previous_sibling - | Stay +type predicate = Move of move * State.t | Is_first_child | Is_next_sibling - | Is of (Tree.NodeKind.t) + | Is of Tree.NodeKind.t | Has_first_child | Has_next_sibling -let is_move p = match p with -| First_child | Next_sibling -| Parent | Previous_sibling | Stay -> true -| _ -> false +let is_move = function Move _ -> true | _ -> false - -type atom = predicate * bool * State.t - -module Atom : (Formula.ATOM with type data = atom) = +module Atom : (Boolean.ATOM with type data = predicate) = struct module Node = struct - type t = atom + type t = predicate let equal n1 n2 = n1 = n2 let hash n = Hashtbl.hash n end @@ -48,85 +43,74 @@ struct include Hcons.Make(Node) let print ppf a = - let p, b, q = a.node in - if not b then fprintf ppf "%s" Pretty.lnot; - match p with - | First_child -> fprintf ppf "FC(%a)" State.print q - | Next_sibling -> fprintf ppf "NS(%a)" State.print q - | Parent -> fprintf ppf "FC%s(%a)" Pretty.inverse State.print q - | Previous_sibling -> fprintf ppf "NS%s(%a)" Pretty.inverse State.print q - | Stay -> fprintf ppf "%s(%a)" Pretty.epsilon State.print q - | Is_first_child -> fprintf ppf "FC%s?" Pretty.inverse - | Is_next_sibling -> fprintf ppf "NS%s?" Pretty.inverse + match a.node with + | Move (m, q) -> begin + match m with + `First_child -> fprintf ppf "%s" Pretty.down_arrow + | `Next_sibling -> fprintf ppf "%s" Pretty.right_arrow + | `Parent -> fprintf ppf "%s" Pretty.up_arrow + | `Previous_sibling -> fprintf ppf "%s" Pretty.left_arrow + | `Stay -> fprintf ppf "%s" Pretty.bullet + end; + fprintf ppf "%a" State.print q + | Is_first_child -> fprintf ppf "%s?" Pretty.up_arrow + | Is_next_sibling -> fprintf ppf "%s?" Pretty.left_arrow | Is k -> fprintf ppf "is-%a?" Tree.NodeKind.print k - | Has_first_child -> fprintf ppf "FC?" - | Has_next_sibling -> fprintf ppf "NS?" - - let neg a = - let p, b, q = a.node in - make (p, not b, q) - + | Has_first_child -> fprintf ppf "%s?" Pretty.down_arrow + | Has_next_sibling -> fprintf ppf "%s?" Pretty.right_arrow end -module SFormula = +module Formula = struct - include Formula.Make(Atom) + include Boolean.Make(Atom) open Tree.NodeKind - let mk_atom a b c = atom_ (Atom.make (a,b,c)) - let mk_kind k = mk_atom (Is k) true State.dummy - let has_first_child = - (mk_atom Has_first_child true State.dummy) + let mk_atom a = atom_ (Atom.make a) + let mk_kind k = mk_atom (Is k) + + let has_first_child = mk_atom Has_first_child - let has_next_sibling = - (mk_atom Has_next_sibling true State.dummy) + let has_next_sibling = mk_atom Has_next_sibling - let is_first_child = - (mk_atom Is_first_child true State.dummy) + let is_first_child = mk_atom Is_first_child - let is_next_sibling = - (mk_atom Is_next_sibling true State.dummy) + let is_next_sibling = mk_atom Is_next_sibling - let is_attribute = - (mk_atom (Is Attribute) true State.dummy) + let is_attribute = mk_atom (Is Attribute) - let is_element = - (mk_atom (Is Element) true State.dummy) + let is_element = mk_atom (Is Element) - let is_processing_instruction = - (mk_atom (Is ProcessingInstruction) true State.dummy) + let is_processing_instruction = mk_atom (Is ProcessingInstruction) - let is_comment = - (mk_atom (Is Comment) true State.dummy) + let is_comment = mk_atom (Is Comment) + let mk_move m q = mk_atom (Move(m,q)) let first_child q = - and_ - (mk_atom First_child true q) - has_first_child + and_ + (mk_move `First_child q) + has_first_child let next_sibling q = and_ - (mk_atom Next_sibling true q) + (mk_move `Next_sibling q) has_next_sibling let parent q = and_ - (mk_atom Parent true q) + (mk_move `Parent q) is_first_child let previous_sibling q = and_ - (mk_atom Previous_sibling true q) + (mk_move `Previous_sibling q) is_next_sibling - let stay q = - (mk_atom Stay true q) + let stay q = mk_move `Stay q let get_states phi = fold (fun phi acc -> match expr phi with - | Formula.Atom a -> let _, _, q = Atom.node a in - if q != State.dummy then StateSet.add q acc else acc + | Boolean.Atom ({ Atom.node = Move(_,q) ; _ }, _) -> StateSet.add q acc | _ -> acc ) phi StateSet.empty @@ -134,11 +118,11 @@ end module Transition = Hcons.Make (struct - type t = State.t * QNameSet.t * SFormula.t + type t = State.t * QNameSet.t * Formula.t let equal (a, b, c) (d, e, f) = a == d && b == e && c == f let hash (a, b, c) = - HASHINT4 (PRIME1, a, ((QNameSet.uid b) :> int), ((SFormula.uid c) :> int)) + HASHINT4 (PRIME1, a, ((QNameSet.uid b) :> int), ((Formula.uid c) :> int)) end) @@ -151,7 +135,7 @@ end = let print ppf ?(sep="\n") l = iter (fun t -> let q, lab, f = Transition.node t in - fprintf ppf "%a, %a -> %a%s" State.print q QNameSet.print lab SFormula.print f sep) l + fprintf ppf "%a, %a -> %a%s" State.print q QNameSet.print lab Formula.print f sep) l end @@ -218,7 +202,7 @@ type t = { id : Uid.t; mutable states : StateSet.t; mutable selection_states: StateSet.t; - transitions: (State.t, (QNameSet.t*SFormula.t) list) Hashtbl.t; + transitions: (State.t, (QNameSet.t*Formula.t) list) Hashtbl.t; mutable cache2 : TransList.t Cache.N2.t; mutable cache4 : Config.t Cache.N4.t; } @@ -226,7 +210,7 @@ type t = { let next = Uid.make_maker () let dummy2 = TransList.cons - (Transition.make (State.dummy,QNameSet.empty, SFormula.false_)) + (Transition.make (State.dummy,QNameSet.empty, Formula.false_)) TransList.nil @@ -300,30 +284,33 @@ let get_trans a tag states = let simplify_atom atom pos q { Config.node=config; _ } = if (pos && StateSet.mem q config.sat) - || ((not pos) && StateSet.mem q config.unsat) then SFormula.true_ + || ((not pos) && StateSet.mem q config.unsat) then Formula.true_ else if (pos && StateSet.mem q config.unsat) - || ((not pos) && StateSet.mem q config.sat) then SFormula.false_ + || ((not pos) && StateSet.mem q config.sat) then Formula.false_ else atom let eval_form phi fcs nss ps ss summary = let rec loop phi = - begin match SFormula.expr phi with - Formula.True | Formula.False -> phi - | Formula.Atom a -> - let p, b, q = Atom.node a in begin - match p with - | First_child -> simplify_atom phi b q fcs - | Next_sibling -> simplify_atom phi b q nss - | Parent | Previous_sibling -> simplify_atom phi b q ps - | Stay -> simplify_atom phi b q ss - | Is_first_child -> SFormula.of_bool (b == (is_left summary)) - | Is_next_sibling -> SFormula.of_bool (b == (is_right summary)) - | Is k -> SFormula.of_bool (b == (k == (kind summary))) - | Has_first_child -> SFormula.of_bool (b == (has_left summary)) - | Has_next_sibling -> SFormula.of_bool (b == (has_right summary)) + begin match Formula.expr phi with + Boolean.True | Boolean.False -> phi + | Boolean.Atom (a, b) -> + begin + match a.Atom.node with + | Move (m, q) -> + let states = match m with + `First_child -> fcs + | `Next_sibling -> nss + | `Parent | `Previous_sibling -> ps + | `Stay -> ss + in simplify_atom phi b q states + | Is_first_child -> Formula.of_bool (b == (is_left summary)) + | Is_next_sibling -> Formula.of_bool (b == (is_right summary)) + | Is k -> Formula.of_bool (b == (k == (kind summary))) + | Has_first_child -> Formula.of_bool (b == (has_left summary)) + | Has_next_sibling -> Formula.of_bool (b == (has_right summary)) end - | Formula.And(phi1, phi2) -> SFormula.and_ (loop phi1) (loop phi2) - | Formula.Or (phi1, phi2) -> SFormula.or_ (loop phi1) (loop phi2) + | Boolean.And(phi1, phi2) -> Formula.and_ (loop phi1) (loop phi2) + | Boolean.Or (phi1, phi2) -> Formula.or_ (loop phi1) (loop phi2) end in loop phi @@ -354,9 +341,9 @@ let eval_trans auto fcs nss ps ss = let new_phi = eval_form phi fcs nss ps old_config old_summary in - if SFormula.is_true new_phi then + if Formula.is_true new_phi then StateSet.add q a_sat, a_unsat, StateSet.add q a_rem, a_kept, a_todo - else if SFormula.is_false new_phi then + else if Formula.is_false new_phi then a_sat, StateSet.add q a_unsat, StateSet.add q a_rem, a_kept, a_todo else let new_tr = Transition.make (q, lab, new_phi) in @@ -389,11 +376,11 @@ let add_trans a q s f = let lab2 = QNameSet.diff labs s in let tr1 = if QNameSet.is_empty lab1 then [] - else [ (lab1, SFormula.or_ phi f) ] + else [ (lab1, Formula.or_ phi f) ] in let tr2 = if QNameSet.is_empty lab2 then [] - else [ (lab2, SFormula.or_ phi f) ] + else [ (lab2, Formula.or_ phi f) ] in (QNameSet.union acup labs, tr1@ tr2 @ atrs) ) (QNameSet.empty, []) trs @@ -433,7 +420,7 @@ let print fmt a = let strs_strings, max_pre, max_all = List.fold_left (fun (accl, accp, acca) (q, s, f) -> let s1 = State.print _str_fmt q; _flush_str_fmt () in let s2 = QNameSet.print _str_fmt s; _flush_str_fmt () in - let s3 = SFormula.print _str_fmt f; _flush_str_fmt () in + let s3 = Formula.print _str_fmt f; _flush_str_fmt () in let pre = Pretty.length s1 + Pretty.length s2 in let all = Pretty.length s3 in ( (q, s1, s2, s3) :: accl, max accp pre, max acca all) @@ -467,7 +454,7 @@ let complete_transitions a = let nqtrans = if QNameSet.is_empty rem then qtrans else - (rem, SFormula.false_) :: qtrans + (rem, Formula.false_) :: qtrans in Hashtbl.replace a.transitions q nqtrans ) a.states @@ -479,7 +466,7 @@ let cleanup_states a = memo := StateSet.add q !memo; let trs = try Hashtbl.find a.transitions q with Not_found -> [] in List.iter (fun (_, phi) -> - StateSet.iter loop (SFormula.get_states phi)) trs + StateSet.iter loop (Formula.get_states phi)) trs end in StateSet.iter loop a.selection_states; @@ -496,39 +483,39 @@ let normalize_negations auto = let memo_state = Hashtbl.create 17 in let todo = Queue.create () in let rec flip b f = - match SFormula.expr f with - Formula.True | Formula.False -> if b then f else SFormula.not_ f - | Formula.Or(f1, f2) -> (if b then SFormula.or_ else SFormula.and_)(flip b f1) (flip b f2) - | Formula.And(f1, f2) -> (if b then SFormula.and_ else SFormula.or_)(flip b f1) (flip b f2) - | Formula.Atom(a) -> begin - let l, b', q = Atom.node a in - if q == State.dummy then if b then f else SFormula.not_ f - else - if b == b' then begin - (* a appears positively, either no negation or double negation *) - if not (Hashtbl.mem memo_state (q,b)) then Queue.add (q,true) todo; - SFormula.atom_ (Atom.make (l, true, q)) - end else begin + match Formula.expr f with + Boolean.True | Boolean.False -> if b then f else Formula.not_ f + | Boolean.Or(f1, f2) -> (if b then Formula.or_ else Formula.and_)(flip b f1) (flip b f2) + | Boolean.And(f1, f2) -> (if b then Formula.and_ else Formula.or_)(flip b f1) (flip b f2) + | Boolean.Atom(a, b') -> begin + match a.Atom.node with + | Move (m, q) -> + if b == b' then begin + (* a appears positively, either no negation or double negation *) + if not (Hashtbl.mem memo_state (q,b)) then Queue.add (q,true) todo; + Formula.mk_atom (Move(m, q)) + end else begin (* need to reverse the atom either we have a positive state deep below a negation or we have a negative state in a positive formula b' = sign of the state b = sign of the enclosing formula *) - let not_q = - try + let not_q = + try (* does the inverted state of q exist ? *) - Hashtbl.find memo_state (q, false) - with - Not_found -> + Hashtbl.find memo_state (q, false) + with + Not_found -> (* create a new state and add it to the todo queue *) - let nq = State.make () in - auto.states <- StateSet.add nq auto.states; - Hashtbl.add memo_state (q, false) nq; - Queue.add (q, false) todo; nq - in - SFormula.atom_ (Atom.make (l, true, not_q)) - end + let nq = State.make () in + auto.states <- StateSet.add nq auto.states; + Hashtbl.add memo_state (q, false) nq; + Queue.add (q, false) todo; nq + in + Formula.mk_atom (Move (m,not_q)) + end + | _ -> if b then f else Formula.not_ f end in (* states that are not reachable from a selection stat are not interesting *) @@ -553,5 +540,3 @@ let normalize_negations auto = Hashtbl.replace auto.transitions q' trans'; done; cleanup_states auto - - diff --git a/src/ata.mli b/src/ata.mli index d65fabb..e4f0ffd 100644 --- a/src/ata.mli +++ b/src/ata.mli @@ -13,28 +13,27 @@ (* *) (***********************************************************************) -type predicate = - First_child - | Next_sibling - | Parent - | Previous_sibling - | Stay - | Is_first_child - | Is_next_sibling - | Is of Tree.NodeKind.t - | Has_first_child - | Has_next_sibling +type move = [ `First_child + | `Next_sibling + | `Parent + | `Previous_sibling + | `Stay ] + +type predicate = Move of move * State.t + | Is_first_child + | Is_next_sibling + | Is of Tree.NodeKind.t + | Has_first_child + | Has_next_sibling val is_move : predicate -> bool -type atom = predicate * bool * State.t +module Atom : Boolean.ATOM with type data = predicate -module Atom : Formula.ATOM with type data = atom - -module SFormula : +module Formula : sig - include module type of Formula.Make(Atom) - val mk_atom : predicate -> bool -> State.t -> t + include module type of Boolean.Make(Atom) + val mk_atom : predicate -> t val mk_kind : Tree.NodeKind.t -> t val has_first_child : t val has_next_sibling : t @@ -54,7 +53,7 @@ module SFormula : module Transition : Hcons.S with - type data = State.t * QNameSet.t * SFormula.t + type data = State.t * QNameSet.t * Formula.t module TransList : sig include Hlist.S with type elt = Transition.t @@ -79,7 +78,7 @@ type t = private { id : Uid.t; mutable states : StateSet.t; mutable selection_states: StateSet.t; - transitions: (State.t, (QNameSet.t*SFormula.t) list) Hashtbl.t; + transitions: (State.t, (QNameSet.t*Formula.t) list) Hashtbl.t; mutable cache2 : TransList.t Cache.N2.t; mutable cache4 : Config.t Cache.N4.t; } @@ -94,7 +93,7 @@ val get_trans : t -> QNameSet.elt -> StateSet.t -> TransList.t val eval_trans : t -> Config.t -> Config.t -> Config.t -> Config.t -> Config.t -val add_trans : t -> State.t -> QNameSet.t -> SFormula.t -> unit +val add_trans : t -> State.t -> QNameSet.t -> Formula.t -> unit val print : Format.formatter -> t -> unit val complete_transitions : t -> unit val cleanup_states : t -> unit diff --git a/src/boolean.ml b/src/boolean.ml new file mode 100644 index 0000000..296f7a6 --- /dev/null +++ b/src/boolean.ml @@ -0,0 +1,161 @@ +(***********************************************************************) +(* *) +(* TAToo *) +(* *) +(* Kim Nguyen, LRI UMR8623 *) +(* Université Paris-Sud & CNRS *) +(* *) +(* 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 +open Misc + +(* + +(** Implementation of hashconsed Boolean formulae *) + +*) +module type ATOM = +sig + include Hcons.S + 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 'atom * bool + +module Make (A: ATOM) = +struct + + + type 'hcons node = { + pos : ('hcons,A.t) expr; + mutable neg : 'hcons; + } + + 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 + | Atom(p1, b1), Atom(p2, b2) -> p1 == p2 && b1 == b2 + | _ -> false + + let hash f = + match f.pos with + | False -> 0 + | True -> 1 + | Or (f1, f2) -> + 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(p, b) -> HASHINT3(PRIME5, Uid.to_int (A.uid p), int_of_bool b) + 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(p,b) -> fprintf ppf "%s%a" (if b then "" else Pretty.lnot) A.print p + in + if parent then fprintf ppf ")" + +let print ppf f = print ~parent:false ppf f + +let is_true f = (expr f) == True +let is_false f = (expr f) == False + +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 true_,false_ = cons True False + +let atom_ p = + let a, _ = cons (Atom(p, true)) (Atom(p, false)) in a + +let not_ f = f.Node.node.neg + +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) *) + + if equal f1 f2 then f1 + else if equal f1 (not_ f2) then true_ + + (* simplification *) + else if is_true f1 || is_true f2 then true_ + else if is_false f1 && is_false f2 then false_ + else if is_false f1 then f2 + else if is_false f2 then f1 + + (* commutativity of | *) + else + let f1, f2 = order f1 f2 in + fst (cons (Or(f1,f2)) (And(not_ f1, not_ f2))) + + +let and_ f1 f2 = + not_ (or_ (not_ f1) (not_ 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 diff --git a/src/boolean.mli b/src/boolean.mli new file mode 100644 index 0000000..73af3c1 --- /dev/null +++ b/src/boolean.mli @@ -0,0 +1,83 @@ +(***********************************************************************) +(* *) +(* TAToo *) +(* *) +(* Kim Nguyen, LRI UMR8623 *) +(* Université Paris-Sud & CNRS *) +(* *) +(* Copyright 2010-2012 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. *) +(* *) +(***********************************************************************) + +module type ATOM = +sig + include Hcons.S + 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 'atom * bool + +(** View of the internal representation of a formula, + used for pattern matching *) + +module Make(A : ATOM) : +sig + type t + + (** Abstract type representing hashconsed formulae *) + + val hash : t -> int + (** Hash function for formulae *) + + val uid : t -> Uid.t + (** Returns a unique ID for formulae *) + + val equal : t -> t -> bool + (** Equality over formulae *) + + val expr : t -> (t,A.t) expr + (** Return a view of the formulae *) + + val compare : t -> t -> int + (** Comparison of formulae *) + + val print : Format.formatter -> t -> unit + (** Pretty printer *) + + val is_true : t -> bool + (** [is_true f] tests whether the formula is the atom True *) + + val is_false : t -> bool + (** [is_false f] tests whether the formula is the atom False *) + + val true_ : t + (** Atom True *) + + val false_ : t + (** Atom False *) + + val atom_ : A.t -> t + (** [atom_ a] creates a new formula consisting of the atome a. + *) + + 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 fold : (t -> 'a -> 'a) -> t -> 'a -> 'a + (** [fold f phi acc] folds [f] over the formula structure *) + +end diff --git a/src/formula.ml b/src/formula.ml deleted file mode 100644 index 1e440bc..0000000 --- a/src/formula.ml +++ /dev/null @@ -1,177 +0,0 @@ -(***********************************************************************) -(* *) -(* TAToo *) -(* *) -(* Kim Nguyen, LRI UMR8623 *) -(* Université Paris-Sud & CNRS *) -(* *) -(* 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 - -(* - -(** 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 'atom - -module Make (P: ATOM) = -struct - - - type 'hcons node = { - pos : ('hcons,P.t) expr; - mutable neg : 'hcons; - } - - 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 - | Atom(p1), Atom(p2) -> p1 == p2 - | _ -> false - - let hash f = - match f.pos with - | False -> 0 - | True -> 1 - | Or (f1, f2) -> - 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(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(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 *) - in - if parent then fprintf ppf ")" - -let print ppf f = print ~parent:false ppf f - -let is_true f = (expr f) == True -let is_false f = (expr f) == False - - -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 true_,false_ = cons True False - -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 or_ f1 f2 = - (* Tautologies: x|x, x|not(x) *) - - if equal f1 f2 then f1 - else if equal f1 (not_ f2) then true_ - - (* simplification *) - else if is_true f1 || is_true f2 then true_ - else if is_false f1 && is_false f2 then false_ - else if is_false f1 then f2 - else if is_false f2 then f1 - - (* commutativity of | *) - else - let f1, f2 = order f1 f2 in - fst (cons (Or(f1,f2)) (And(not_ f1, not_ f2))) - - -let and_ f1 f2 = - not_ (or_ (not_ f1) (not_ 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 diff --git a/src/formula.mli b/src/formula.mli deleted file mode 100644 index f69a40d..0000000 --- a/src/formula.mli +++ /dev/null @@ -1,86 +0,0 @@ -(***********************************************************************) -(* *) -(* TAToo *) -(* *) -(* Kim Nguyen, LRI UMR8623 *) -(* Université Paris-Sud & CNRS *) -(* *) -(* Copyright 2010-2012 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. *) -(* *) -(***********************************************************************) - -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 'atom - -(** View of the internal representation of a formula, - used for pattern matching *) - -module Make(P : ATOM) : -sig - type t - - (** Abstract type representing hashconsed formulae *) - - val hash : t -> int - (** Hash function for formulae *) - - val uid : t -> Uid.t - (** Returns a unique ID for formulae *) - - val equal : t -> t -> bool - (** Equality over formulae *) - - val expr : t -> (t,P.t) expr - (** Return a view of the formulae *) - - val compare : t -> t -> int - (** Comparison of formulae *) - - val print : Format.formatter -> t -> unit - (** Pretty printer *) - - val is_true : t -> bool - (** [is_true f] tests whether the formula is the atom True *) - - val is_false : t -> bool - (** [is_false f] tests whether the formula is the atom False *) - - val true_ : t - (** Atom True *) - - val false_ : t - (** Atom False *) - - 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 fold : (t -> 'a -> 'a) -> t -> 'a -> 'a - (** [fold f phi acc] folds [f] over the formula structure *) - -end diff --git a/src/xpath/compile.ml b/src/xpath/compile.ml index c52c720..8ab26fb 100644 --- a/src/xpath/compile.ml +++ b/src/xpath/compile.ml @@ -17,11 +17,11 @@ open Ast let ( => ) a b = (a, b) -let ( ++ ) a b = Ata.SFormula.or_ a b -let ( %% ) a b = Ata.SFormula.and_ a b +let ( ++ ) a b = Ata.Formula.or_ a b +let ( %% ) a b = Ata.Formula.and_ a b let ( @: ) a b = StateSet.add a b -module F = Ata.SFormula +module F = Ata.Formula let node_set = QNameSet.remove QName.document QNameSet.any @@ -121,7 +121,7 @@ let rec compile_expr e trans states = states2 | Fun_call (f, [ e0 ]) when (QName.to_string f) = "not" -> let phi, trans0, states0 = compile_expr e0 trans states in - (Ata.SFormula.not_ phi), + (F.not_ phi), trans0, states0 | Path p -> compile_path p trans states @@ -130,9 +130,9 @@ let rec compile_expr e trans states = and compile_path paths trans states = List.fold_left (fun (aphi, atrans, astates) p -> let phi, ntrans, nstates = compile_single_path p atrans astates in - (Ata.SFormula.or_ phi aphi), + (F.or_ phi aphi), ntrans, - nstates) (Ata.SFormula.false_,trans,states) paths + nstates) (F.false_,trans,states) paths and compile_single_path p trans states = let steps = @@ -147,7 +147,7 @@ and compile_single_path p trans states = and compile_step_list l trans states = match l with - | [] -> Ata.SFormula.true_, trans, states + | [] -> F.true_, trans, states | (axis, test, elist) :: ll -> let phi0, trans0, states0 = compile_step_list ll trans states in let phi1, trans1, states1 = @@ -182,7 +182,7 @@ let compile_top_level_step_list l trans states = is attribute *) let phi0 = if axis != Attribute then - phi0 %% (Ata.SFormula.not_ Ata.SFormula.is_attribute) + phi0 %% (F.not_ F.is_attribute) else phi0 in match ll with @@ -214,7 +214,7 @@ let compile_top_level_step_list l trans states = compile_axis_test Self (QNameSet.singleton QName.document, Tree.NodeKind.Node) - Ata.SFormula.true_ + F.true_ trans states in