Commit c1336b43 authored by Kim Nguyễn's avatar Kim Nguyễn

Expose the empty constructor for BDDs outside of the Bool.Make functor.

parent 63256102
...@@ -2,6 +2,13 @@ let (<) : int -> int -> bool = (<) ...@@ -2,6 +2,13 @@ let (<) : int -> int -> bool = (<)
let (>) : int -> int -> bool = (>) let (>) : int -> int -> bool = (>)
let (=) : int -> int -> bool = (=) let (=) : int -> int -> bool = (=)
type 'a bdd =
False
| True
| Split of int * 'a * 'a bdd * 'a bdd * 'a bdd
let empty = False
module type S = module type S =
sig sig
type elem type elem
...@@ -32,10 +39,7 @@ end ...@@ -32,10 +39,7 @@ end
module Make(X : Custom.T) = module Make(X : Custom.T) =
struct struct
type elem = X.t type elem = X.t
type t = type t = elem bdd
| True
| False
| Split of int * elem * t * t * t
let rec equal a b = let rec equal a b =
(a == b) || (a == b) ||
...@@ -175,7 +179,7 @@ struct ...@@ -175,7 +179,7 @@ struct
let split0 x pos ign neg = let split0 x pos ign neg =
Split (compute_hash x pos ign neg, x, pos, ign, neg) Split (compute_hash x pos ign neg, x, pos, ign, neg)
let empty = False let empty = empty
let full = True let full = True
(* Invariants: (* Invariants:
...@@ -339,6 +343,7 @@ sig ...@@ -339,6 +343,7 @@ sig
module Atom : S module Atom : S
include S with type elem = Atom.t Var.var_or_atom include S with type elem = Atom.t Var.var_or_atom
and type t = Atom.t Var.var_or_atom bdd
val var : Var.t -> t val var : Var.t -> t
......
type 'a bdd
val empty : 'a bdd
module type S = module type S =
sig sig
include Custom.T
type elem type elem
include Custom.T
val get: t -> (elem list * elem list) list val get: t -> (elem list * elem list) list
...@@ -29,6 +33,7 @@ sig ...@@ -29,6 +33,7 @@ sig
module Atom : S module Atom : S
include S with type elem = Atom.t Var.var_or_atom include S with type elem = Atom.t Var.var_or_atom
and type t = Atom.t Var.var_or_atom bdd
val var : Var.t -> t val var : Var.t -> t
......
...@@ -1571,9 +1571,9 @@ module Iter = ...@@ -1571,9 +1571,9 @@ module Iter =
let simplify = let simplify =
let memo = DescrHash.create 17 in let memo = DescrHash.create 17 in
let aux (type bdd) (type atom) let aux (type atom)
inj inj
(module BV : Bool.V with type t = bdd and type Atom.t = atom ) b (module BV : Bool.V with type Atom.t = atom ) b
= =
let clean b = let clean b =
if is_empty (inj b) then BV.empty else b if is_empty (inj b) then BV.empty else b
...@@ -1657,10 +1657,10 @@ module Iter = ...@@ -1657,10 +1657,10 @@ module Iter =
| l1, l2 -> cap (l1 @ List.map neg l2) :: acc | l1, l2 -> cap (l1 @ List.map neg l2) :: acc
) acc (B.get bv) ) acc (B.get bv)
in in
let cplx_bdd (type bdd) (type atom) (type atom2) let cplx_bdd (type atom) (type atom2)
any any
do_atom do_atom
(module BV : Bool.V with type t = bdd and type Atom.t = atom and type Atom.elem = atom2) (module BV : Bool.V with type Atom.t = atom and type Atom.elem = atom2)
acc acc
bdd bdd
= =
...@@ -2143,8 +2143,8 @@ module Print = struct ...@@ -2143,8 +2143,8 @@ module Print = struct
| `Var x -> (Var.Set.add x acc_v, acc_a) | `Var x -> (Var.Set.add x acc_v, acc_a)
) (Var.Set.empty, init) l ) (Var.Set.empty, init) l
in in
let fill_line (type s) let fill_line (type atom) (module BV : Bool.V with type Atom.t = atom)
(module BV : Bool.V with type t = s) table get set t = table get set t =
List.iter (fun (p, n) -> List.iter (fun (p, n) ->
let v1, a1 = split_var_atom (fun a b -> BV.(cap (atom a) b)) BV.full p in let v1, a1 = split_var_atom (fun a b -> BV.(cap (atom a) b)) BV.full p in
let v2, a2 = split_var_atom (fun a b -> BV.(cup (atom a) b)) BV.empty n in let v2, a2 = split_var_atom (fun a b -> BV.(cup (atom a) b)) BV.empty n in
...@@ -2167,7 +2167,9 @@ module Print = struct ...@@ -2167,7 +2167,9 @@ module Print = struct
let h = let h =
try try
let no_var = VarTable.find h Key.empty in let no_var = VarTable.find h Key.empty in
let update_field (type s) (module BV : Bool.V with type t = s) get set d1 d2 = let update_field
(type atom) (module BV : Bool.V with type Atom.t = atom)
get set d1 d2 =
let bdd = get d1 in let bdd = get d1 in
if BV.(is_empty (diff full bdd)) then set d2 bdd else d2 if BV.(is_empty (diff full bdd)) then set d2 bdd else d2
in in
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment