From d9c0e4863807eaf472e875a4bad35cfefe985c95 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Kim=20Nguy=E1=BB=85n?= Date: Wed, 6 Feb 2013 14:30:45 +0100 Subject: [PATCH] Implement formulae parametrized by atomic predicates. --- src/ata.ml | 72 +++++++++++++++++++++++-- src/formula.ml | 138 +++++++++++++++++++++++++++++------------------- src/formula.mli | 100 ++++++++++++++++++----------------- src/hcons.ml | 5 +- src/sigs.ml | 6 ++- 5 files changed, 212 insertions(+), 109 deletions(-) diff --git a/src/ata.ml b/src/ata.ml index cad28e1..6ec859c 100644 --- a/src/ata.ml +++ b/src/ata.ml @@ -14,20 +14,84 @@ (***********************************************************************) (* - Time-stamp: + Time-stamp: *) 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 (); @@ -47,7 +111,7 @@ let add_trans a q s f = (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 @@ -84,7 +148,7 @@ let print fmt a = 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)) diff --git a/src/formula.ml b/src/formula.ml index 7bd8ca6..ad774ea 100644 --- a/src/formula.ml +++ b/src/formula.ml @@ -14,7 +14,7 @@ (***********************************************************************) (* - Time-stamp: + Time-stamp: *) INCLUDE "utils.ml" @@ -22,33 +22,54 @@ 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 = @@ -56,44 +77,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) - - | 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 @@ -105,7 +125,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 +136,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 +144,12 @@ let cons pos neg = 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) *) @@ -156,3 +175,12 @@ let and_ f1 f2 = 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 diff --git a/src/formula.mli b/src/formula.mli index 9a0b066..e83bca1 100644 --- a/src/formula.mli +++ b/src/formula.mli @@ -14,72 +14,78 @@ (***********************************************************************) (* - Time-stamp: + Time-stamp: *) -(** 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 diff --git a/src/hcons.ml b/src/hcons.ml index 6a40b06..1fc059c 100644 --- a/src/hcons.ml +++ b/src/hcons.ml @@ -14,7 +14,7 @@ (***********************************************************************) (* - Time-stamp: + Time-stamp: *) include Sigs.HCONS @@ -48,6 +48,7 @@ struct 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 @@ -76,7 +77,7 @@ struct let hash v = v let uid v = Uid.of_int v - + let dummy _ = ~-1 let equal x y = x == y let init () = () diff --git a/src/sigs.ml b/src/sigs.ml index a3cf635..1022404 100644 --- a/src/sigs.ml +++ b/src/sigs.ml @@ -14,7 +14,7 @@ (***********************************************************************) (* - Time-stamp: + Time-stamp: *) (** This module contains all the signatures of the project, to avoid @@ -158,6 +158,10 @@ struct (** 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 -- 2.17.1