(***********************************************************************)
(*
- 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"
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 =
| 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
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 ")"
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 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 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
projects / tatoo.git / blobdiff