(* 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 ]
-type 'hcons expr =
- | False | True
- | Or of 'hcons * 'hcons
- | And of 'hcons * 'hcons
- | Atom of (move * bool * State.t)
-
-type 'hcons node = {
- pos : 'hcons expr;
- mutable neg : 'hcons;
- st : StateSet.t * StateSet.t;
- size: int; (* Todo check if this is needed *)
-}
-
-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 =
+
+(*
+
+(** 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 = 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)
- | 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.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
- | 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
+ | `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 ")"
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 true_,false_ = cons True False
-let not_ f = f.Node.node.neg
+let atom_ p = fst (cons (Atom(p)) (Atom(P.neg p)))
-let union_pair (l1,r1) (l2, r2) =
- StateSet.union l1 l2,
- StateSet.union r1 r2
-
-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) *)
(* 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 =
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
projects / tatoo.git / blobdiff