From c02ea958bdcc17697d04220c748045438ef77110 Mon Sep 17 00:00:00 2001
From: Jean-Christophe Filliatre <Jean-Christophe.Filliatre@lri.fr>
Date: Mon, 28 Feb 2022 10:58:04 +0100
Subject: [PATCH] restored implementation comments

---
 lib/bdd.ml | 27 +++++++++++++--------------
 1 file changed, 13 insertions(+), 14 deletions(-)

diff --git a/lib/bdd.ml b/lib/bdd.ml
index 2d78a8b..ef9cf11 100644
--- a/lib/bdd.ml
+++ b/lib/bdd.ml
@@ -97,6 +97,11 @@ let get_max_var () = max_var
 type bdd = { tag: int; node : view }
 and view = Zero | One | Node of variable * bdd (*low*) * bdd (*high*)
 
+(* Notes:
+   - Variables are ordered as integers, i.e. variable indices increase
+     as we descend in the BDD.
+   - A node is created using function `mk` below. *)
+
 type t = bdd (* export *)
 
 let view b = b.node
@@ -282,6 +287,10 @@ let high b = match b.node with
   | Zero | One -> invalid_arg "Bdd.low"
   | Node (_, _, h) -> h
 
+(* Note: `mk` ensures that BDDs are reduced and maximally shared.
+   But it *does not* ensure that BDDs are ordered. This is ensured by
+   the various functions below. See for instance the code of `gapply`
+   and the way it compares variables before proceeding recursively. *)
 let mk v ~low ~high =
   if low == high then low else hashcons_node v low high
 
@@ -415,7 +424,6 @@ let mk_imp = gapply Op_imp
 let mk_iff = gapply (Op_any (fun b1 b2 -> b1 == b2))
 
 
-
 (** {2 quantifier elimination} *)
 
 let rec quantifier_elim cache op filter b =
@@ -451,18 +459,16 @@ let rec extract_known_values cache b =
   with Not_found ->
     let res = match b.node with
       | Zero | One -> BddVarMap.empty
-      | Node(v,{node=Zero;_},h) ->
+      | Node(v, {node=Zero;_}, h) ->
          (* if v then h else 0 --> v /\ h *)
          BddVarMap.add v true (extract_known_values cache h)
-      | Node(v,l,{node=Zero;_}) ->
+      | Node(v, l, {node=Zero;_}) ->
          (* if v then 0 else l --> !v /\ l *)
          BddVarMap.add v false (extract_known_values cache l)
-      | Node(_,l,h) ->
+      | Node(_, l, h) ->
          let m1 = extract_known_values cache l in
          let m2 = extract_known_values cache h in
-         let merge_bool _ b1 b2 =
-           if b1=b2 then Some b1 else None
-         in
+         let merge_bool _ b1 b2 = if b1 = b2 then Some b1 else None in
          BddVarMap.union merge_bool m1 m2
     in
     H1.add cache b res;
@@ -472,13 +478,6 @@ let extract_known_values b =
   let cache = H1.create cache_default_size in
   extract_known_values cache b
 
-
-
-
-
-
-
-
 let apply f = gapply (Op_any f)
 
 let constrain b1 b2 =