implement set, test, star, subseteq, and add README. add tests for star (#6)

Author: etw33

README.md

@@ -0,0 +1,17 @@
+# Overview
+This package implements hash-consed binary decision diagrams (BDDs) and identity-suppressed decision diagrams (IDDs).
+
+An IDD, like a BBD, can be seen as representing a transition relation R on a state space of boolean vectors. I.e. boolean vector pair (v1, v2) belongs to R if and only if evaluating the IDD-representation of R in the environment given by (v1, v2) yields true.
+
+The main motivation for IDDs is that they represent the identity relation in a constant amount of space instead of in an amount of space that is linear in the size of the boolean vectors.
+
+# Provided operations
+## BDDs
+* Constructors: true, false, if-then-else
+* Operations: equality, negation, disjunction, conjunction
+
+## IDDs
+* Constructors: identity relation, empty relation, test, set, branch
+* Operations: equality, subset test, apply algorithm, union, sequential composition, transitive-reflexive closure
+
+

src/idd.ml

@@ -22,6 +22,14 @@ let manager () : manager = {
   seq_cache = Hashtbl.create (module Pair);
 }
 
+let test mgr i b =
+  Dd.branch mgr.dd (Var.inp i) (if b then Dd.ctrue else Dd.cfalse)
+    (if b then Dd.cfalse else Dd.ctrue)
+
+let set mgr i b =
+  Dd.branch mgr.dd (Var.out i) (if b then Dd.ctrue else Dd.cfalse)
+    (if b then Dd.cfalse else Dd.ctrue)
+
 let rec eval' expl (tree:t) (env:Var.t -> bool) (n:int) =
   match tree with
   | False ->
@@ -87,7 +95,6 @@ let branch (mgr : manager) (x : Var.t) (hi : t) (lo : t) : t =
     end
   (* ) *)
 
-
 let extract (d:t) (side:bool) : t =
   match d with
   | False | True -> d
@@ -173,6 +180,16 @@ let rec seq mgr (d0:t) (d1:t) =
           (union mgr (seq mgr d0_01 d1_10) (seq mgr d0_00 d1_00)))
     )
 
+let star mgr (d0:t) =
+  let rec loop curr prev =
+    if equal curr prev then prev else
+      loop (seq mgr curr curr) curr
+  in
+  loop (union mgr ident d0) ident
+
+let subseteq mgr (d0:t) (d1:t) =
+  equal (union mgr d0 d1) d1
+
 (* relational operations *)
 module Rel = struct
 

src/idd.mli

@@ -21,16 +21,16 @@ val empty : t
 (** For i < n,
   eval (test i b) env n =
     env (Var.inp i) = b && eval ident env n
-  rel n (test i b) = { (x,x) | x \in B^n, x_i = b }
+  rel n (test i b) = \{ (x,x) | x \in B^n, x_i = b \}
      *)
-val test : int -> bool -> t
+val test : manager -> int -> bool -> t
 
 (** For i < n,
   eval (set i b) env n = eval ident env' n, where
     env' x = if x = Var.inp i then b else env x
-  rel n (set i b) = { (x,x[i:=b]) | x \in B^n }
+  rel n (set i b) = \{ (x,x[i:=b]) | x \in B^n \}
   *)
-val set : int -> bool -> t
+val set : manager -> int -> bool -> t
 
 (** [branch mgr var hi lo] is the diagram that behaves like [hi] when
     [var = true], and like [lo] when [var = false]. *)
@@ -47,7 +47,7 @@ val seq : manager -> t -> t -> t
 val union : manager -> t -> t -> t
 
 (** (Relational) transitive-reflexive closure  *)
-val star : t -> t
+val star : manager -> t -> t
 
 (** {2 Boolean operations} *)
 
@@ -58,7 +58,7 @@ val star : t -> t
 val equal : t -> t -> bool
 
 (** relational containment *)
-val subseteq : t -> t -> bool
+val subseteq : manager -> t -> t -> bool
 
 (** {2 Semantics} *)
 

test/idd_test.ml

@@ -151,4 +151,49 @@ module Basic = struct
        )
      )
 
+  (* Star tests *)
+
+  let is_transitive d0 max_idx =
+    Idd.(
+      let alllsts = all_lsts max_idx in
+      List.cartesian_product alllsts alllsts |>
+      List.cartesian_product alllsts |>
+      List.for_all ~f:(fun (lst1, (lst2, lst3)) ->
+          if eval d0 (env_from_lsts lst1 lst2) max_idx &&
+             eval d0 (env_from_lsts lst2 lst3) max_idx then
+            eval d0 (env_from_lsts lst1 lst3) max_idx
+          else true
+        )
+    )
+
+  let%test "[star d0] contains d0 and is reflexive and transitive" =
+    List.for_all trees ~f:(fun d0 ->
+        Idd.(
+          let starred = star mgr d0 in
+          let max1, max2 = index d0 + 1, index starred + 1 in
+          let max_idx = max max1 max2 in
+          (* contains d0 check *)
+          subseteq mgr d0 starred &&
+          (* reflexive check *)
+          subseteq mgr ident starred &&
+          (* transitive check *)
+          is_transitive starred max_idx
+        )
+      )
+
+  let%test "[star d0] is the smallest" =
+    List.for_all small_trees ~f:(fun d0 ->
+        Idd.(
+          let starred = star mgr d0 in
+          let max1 = index d0 + 1 in
+          List.for_all small_trees ~f:(fun d1 ->
+            let max2 = index d1 + 1 in
+            let max_idx = max max1 max2 in
+            if subseteq mgr ident d1 && subseteq mgr d0 d1 &&
+               is_transitive d1 max_idx
+            then subseteq mgr starred d1 else true
+          )
+        )
+    )
+
 end