Implement formulae parametrized by atomic predicates.

diff --git a/src/ata.ml b/src/ata.ml
index cad28e1..6ec859c 100644 (file)
--- a/src/ata.ml
+++ b/src/ata.ml
@@ -14,20 +14,84 @@
 (***********************************************************************)
 
 (*
 (***********************************************************************)
 
 (*

-  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
 *)
 
 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;
 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 ();
 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
         (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
     ) (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 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))
     ( (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 (file)
--- a/src/formula.ml
+++ b/src/formula.ml
@@ -14,7 +14,7 @@
 (***********************************************************************)
 
 (*
 (***********************************************************************)
 
 (*

-  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"
 *)
 
 INCLUDE "utils.ml"


@@ -22,33 +22,54 @@ INCLUDE "utils.ml"
 open Format
 
 
 open Format
 
 

+(*
+
+(** Implementation of hashconsed Boolean formulae *)
+

 type move = [ `Left | `Right | `Epsilon | `Up1 | `Up2 ]
 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
   | 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)
   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
 
     let hash f =


@@ -56,44 +77,43 @@ module rec Node : Hcons.S
       | False -> 0
       | True -> 1
       | Or (f1, f2) ->
       | 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) ->
       | 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
 
   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
           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
         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 ")"
 
   in
     if parent then fprintf ppf ")"
 


@@ -116,7 +136,7 @@ let is_false f = (expr f) == False
 
 
 let cons pos neg =
 
 
 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 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 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 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 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 (file)
--- a/src/formula.mli
+++ b/src/formula.mli
@@ -14,72 +14,78 @@
 (***********************************************************************)
 
 (*
 (***********************************************************************)
 
 (*

-  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
   | 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 *)
 
 
 (** 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 (file)
--- a/src/hcons.ml
+++ b/src/hcons.ml
@@ -14,7 +14,7 @@
 (***********************************************************************)
 
 (*
 (***********************************************************************)
 
 (*

-  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
 *)
 
 include Sigs.HCONS


@@ -48,6 +48,7 @@ struct
   let init () =
     T.clear pool;
     uid_make := Uid.make_maker ()
   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 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 hash v = v
 
   let uid v = Uid.of_int v

-
+  let dummy _ = ~-1

   let equal x y = x == y
 
   let init () = ()
   let equal x y = x == y
 
   let init () = ()

diff --git a/src/sigs.ml b/src/sigs.ml
index a3cf635..1022404 100644 (file)
--- a/src/sigs.ml
+++ b/src/sigs.ml
@@ -14,7 +14,7 @@
 (***********************************************************************)
 
 (*
 (***********************************************************************)
 
 (*

-  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
 *)
 
 (** 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
     (** 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
 
 
   end