src/Bdd.ml

-Original file line number
+Diff line change
@@ -0,0 +1,100 @@
+    (** Implementation of BDDs with hashconsing *)
+    type t = {id: int; l: t; r: t; value: int}
+    (* type tree = One | Zero | Tree of tree * tree * int *)
+    (* and t = int * tree *)
+    let rec null = {id = -1; l = null; r = null; value = -1}
+    let one = {id = 0; l = null; r = null; value = -1}
+    let zero = {id = 1; l = null; r = null; value = -1}
+    type bdd = t
+    module S = struct
+      type t = bdd
+      let equal b1 b2 =
+        b1.l == b2.l && b1.r == b2.r
+      let hash b =
+* (b.l.id + (29 * b.r.id))
+    end
+    module HashedBdd = S
+    module HBdd = Hashtbl.Make(S)
+    let create =
+      let htbl = HBdd.create 53 in
+      let id = ref 2 in
+      fun v l r ->
+        let i = !id in
+        let b = {id = i; l; r; value = v} in
+        try
+          HBdd.find htbl b
+        with
+          Not_found ->
+            HBdd.add htbl b b;
+            incr id;
+            b
+    module HPair = Hashtbl.Make(
+      struct
+        type t = bdd * bdd
+        let equal (b1, b2) (b1', b2') =
+          S.equal b1 b1' && S.equal b2 b2'
+        let hash (b1, b2) =
+          S.hash b1 + 29 * S.hash b2
+      end)
+    let is_leaf b = b == one || b == zero
+    let boolean_equiv b =
+      (* if b <> from one and zero, assert false will be evaluated *)
+      b == one || (b <> zero && assert false)
+    let apply op =
+      let htbl = HPair.create 53 in
+      let apply_op op b1 b2 =
+        let b1 = boolean_equiv b1 in
+        let b2 = boolean_equiv b2 in
+        let res = op b1 b2 in
+        if res then one else zero
+      in
+      let rec apply b1 b2 =
+        try HPair.find htbl (b1, b2)
+        with Not_found ->
+          let res =
+            if is_leaf b1 && is_leaf b2 then
+              apply_op op b1 b2
+            else if b1.value = b2.value then
+              create b1.value (apply b1.l b2.l) (apply b1.r b2.r)
+            else if b1.value < b2.value then
+              create b1.value (apply b1.l b2) (apply b1.r b2)
+            else create b2.value (apply b1 b2.l) (apply b1 b2.r)
+          in
+          HPair.add htbl (b1, b2) res; res
+      in
+      apply
+    let rec restrict bool value b =
+      if is_leaf b then b
+      else
+        if b.value < value then
+          let l = restrict bool value b.l in
+          let r = restrict bool value b.r in
+          create b.value l r
+        else if b.value = value then
+          if bool then b.r else b.l
+        else b
+    let exists value b =
+      let l = restrict false value b in
+      let r = restrict true value b in
+      apply ( or ) l r

Mu-Calculus : result #2

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open

picdc wants to merge 27 commits into fredokun:mu-calculus from Thriim:master

-Original file line number
+Diff line change
@@ -0,0 +1,100 @@
+    (** Implementation of BDDs with hashconsing *)
+    type t = {id: int; l: t; r: t; value: int}
+    (* type tree = One | Zero | Tree of tree * tree * int *)
+    (* and t = int * tree *)
+    let rec null = {id = -1; l = null; r = null; value = -1}
+    let one = {id = 0; l = null; r = null; value = -1}
+    let zero = {id = 1; l = null; r = null; value = -1}
+    type bdd = t
+    module S = struct
+      type t = bdd
+      let equal b1 b2 =
+        b1.l == b2.l && b1.r == b2.r
+      let hash b =
+* (b.l.id + (29 * b.r.id))
+    end
+    module HashedBdd = S
+    module HBdd = Hashtbl.Make(S)
+    let create =
+      let htbl = HBdd.create 53 in
+      let id = ref 2 in
+      fun v l r ->
+        let i = !id in
+        let b = {id = i; l; r; value = v} in
+        try
+          HBdd.find htbl b
+        with
+          Not_found ->
+            HBdd.add htbl b b;
+            incr id;
+            b
+    module HPair = Hashtbl.Make(
+      struct
+        type t = bdd * bdd
+        let equal (b1, b2) (b1', b2') =
+          S.equal b1 b1' && S.equal b2 b2'
+        let hash (b1, b2) =
+          S.hash b1 + 29 * S.hash b2
+      end)
+    let is_leaf b = b == one || b == zero
+    let boolean_equiv b =
+      (* if b <> from one and zero, assert false will be evaluated *)
+      b == one || (b <> zero && assert false)
+    let apply op =
+      let htbl = HPair.create 53 in
+      let apply_op op b1 b2 =
+        let b1 = boolean_equiv b1 in
+        let b2 = boolean_equiv b2 in
+        let res = op b1 b2 in
+        if res then one else zero
+      in
+      let rec apply b1 b2 =
+        try HPair.find htbl (b1, b2)
+        with Not_found ->
+          let res =
+            if is_leaf b1 && is_leaf b2 then
+              apply_op op b1 b2
+            else if b1.value = b2.value then
+              create b1.value (apply b1.l b2.l) (apply b1.r b2.r)
+            else if b1.value < b2.value then
+              create b1.value (apply b1.l b2) (apply b1.r b2)
+            else create b2.value (apply b1 b2.l) (apply b1 b2.r)
+          in
+          HPair.add htbl (b1, b2) res; res
+      in
+      apply
+    let rec restrict bool value b =
+      if is_leaf b then b
+      else
+        if b.value < value then
+          let l = restrict bool value b.l in
+          let r = restrict bool value b.r in
+          create b.value l r
+        else if b.value = value then
+          if bool then b.r else b.l
+        else b
+    let exists value b =
+      let l = restrict false value b in
+      let r = restrict true value b in
+      apply ( or ) l r

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Mu-Calculus : result #2

Uh oh!

Diff view

Diff view

There are no files selected for viewing

Uh oh!

Mu-Calculus : result #2

Are you sure you want to change the base?

Uh oh!

Mu-Calculus : result #2

Uh oh!

Uh oh!

Diff view

Diff view

There are no files selected for viewing

Uh oh!