(* 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 | `Epsilon | `Up1 | `Up2 ]
-type 'formula expr =
+
+(*
+
+(** 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
- | Move of move * bool * State.t
+ | Atom of 'atom
+
+module Make (P: ATOM) =
+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 : 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)
- | Move(d1, p1, s1), Move(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)
-
- | Move(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
- | Move _ -> 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);
- | Move(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 (Move(d,p,s)) (Move(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 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
projects / tatoo.git / blobdiff