Fix a embarassing bug when counting bdd solution number.

source/common/bddd.ml

@@ -39,14 +39,7 @@ let snt_build = ref false
 
 let (sol_number_snt : snt -> Bdd.t -> sol_nb * sol_nb) =
   fun snt bdd ->
-    try 
-      Hashtbl.find snt bdd 
-    with Not_found ->  
-      let bdd_not = (Bdd.dnot bdd) in 
-      let (st, se) = Hashtbl.find snt bdd_not in 
-	Hashtbl.add snt bdd (se, st); 
-	(se, st) 
-
+    Hashtbl.find snt bdd 
 
 let (sol_number : Bdd.t -> sol_nb * sol_nb) =
   (sol_number_snt !snt_ref) 
@@ -60,7 +53,7 @@ let (init_snt : unit -> unit) =
   fun _ -> 
     let bdd_true = Bdd.dtrue !Formula_to_bdd.bdd_manager in
     let bdd_false = Bdd.dfalse !Formula_to_bdd.bdd_manager in
-      (Hashtbl. add !snt_ref (bdd_true) (one_sol, zero_sol));
+      (Hashtbl.add !snt_ref (bdd_true) (one_sol, zero_sol));
       (Hashtbl.add !snt_ref (bdd_false) (zero_sol, one_sol))
 
 let (clear_snt: unit -> unit) =
@@ -77,54 +70,44 @@ let (clear_snt: unit -> unit) =
 
 let (sol_number_exists : Bdd.t -> snt -> bool) =
   fun bdd snt -> 
-      Hashtbl.mem snt bdd || Hashtbl.mem snt (Bdd.dnot bdd)
+      Hashtbl.mem snt bdd
 
 
 let rec (build_sol_nb_table_rec: Bdd.t -> Bdd.t -> snt -> sol_nb) =
   fun bdd comb snt -> 
     (** Returns the relative (to which bbd points to it) number of
-      solutions of [bdd]. Also udpates the solution number table 
-      for [bdd], and recursively for all its sub-bdds.
-
-      [comb] is a positive cube that ougth to contain the indexes of
-      boolean vars that are still to be generated, and the numerical
-      indexes that appears in [bdd].  
-
-      Note that this sol number make abstraction of the volume of
-      polyhedron which dimension is greater than 2. It is very bad as
-      far as the fairness of the draw is concerned, but really,
-      computing it would be far too expensive for our purpose
-      (real-time!). Cf fair_bddd.ml for a more fair version.
+        solutions of [bdd]. Also udpates the solution number table 
+        for [bdd], and recursively for all its sub-bdds.
+
+        [comb] is a positive cube that ougth to contain the indexes of
+        boolean vars that are still to be generated, and the numerical
+        indexes that appears in [bdd].  
+
+        Note that this sol number make abstraction of the volume of
+        polyhedron which dimension is greater than 2. It is very bad as
+        far as the fairness of the draw is concerned, but really,
+        computing it would be far too expensive for our purpose
+        (real-time!). Cf fair_bddd.ml for a more fair version.
     *)
     let _ = assert (
       not (Bdd.is_cst bdd) && (Bdd.topvar comb) = (Bdd.topvar bdd) )
     in
     let sol_nb =
       try
-	(* either it has already been computed ... *)
-	let (nt, ne) = sol_number_snt snt bdd in
-	  (* solutions numbers in the table are absolute *)
-	  (add_sol_nb nt ne)
+	     (* either it has already been computed ... *)
+	     let (nt, ne) = sol_number_snt snt bdd in
+	       (add_sol_nb nt ne)
 
       with Not_found ->
-	(* ... or not. *)
-	let nt = compute_absolute_sol_nb (Bdd.dthen bdd) comb snt in
-	let ne = compute_absolute_sol_nb (Bdd.delse bdd) comb snt in
-	  Hashtbl.replace snt bdd (nt, ne);
-	  (add_sol_nb nt ne)
+	     (* ... or not. *)
+	     let nt = compute_absolute_sol_nb (Bdd.dthen bdd) comb snt in
+	     let ne = compute_absolute_sol_nb (Bdd.delse bdd) comb snt in
+	       Hashtbl.replace snt bdd (nt, ne);
+	       (add_sol_nb nt ne)
     in
-(*     let sol_nb' = ((Bdd.nbminterms (Bdd.size comb) bdd) /. 2.0) in   *)
-(*       if sol_nb <> sol_nb' then   *)
-(* 	(   *)
-(* 	  print_string (" @@@ " ^ (string_of_float sol_nb) ^ " "    *)
-(* 			^ (string_of_float sol_nb') ^ " \n");   *)
-(* 	  flush stdout;   *)
-(* 	  exit 1   *)
-(* 	)   *)
-(*       else   *)
-	sol_nb
+	     sol_nb
 and 
-  (compute_absolute_sol_nb: Bdd.t  -> Bdd.t -> snt -> sol_nb) =
+    (compute_absolute_sol_nb: Bdd.t  -> Bdd.t -> snt -> sol_nb) =
   fun sub_bdd comb snt -> 
     (*
       Returns the absolute number of solutions of [sub_bdd]  w.r.t. [comb], 
@@ -146,36 +129,36 @@ and
       Bdd.is_true sub_bdd 
     then
       let sol_nb = 
-	if 
-	  Bdd.is_true comb
-	then
-	  one_sol
-	else
-	  two_power_of (Bdd.supportsize (Bdd.dthen comb)) 
+	     if 
+	       Bdd.is_true comb
+	     then
+	       one_sol
+	     else
+	       two_power_of (Bdd.supportsize (Bdd.dthen comb)) 
       in
-	sol_nb
+	     sol_nb
     else 
       let topvar = Bdd.topvar sub_bdd in
       let rec
-	(count_missing_vars: Bdd.t -> var_idx -> int -> Bdd.t * int) =
-	fun comb var_idx cpt -> 
-	  (* Returns [cpt] + the number of variables occurring in [comb]
-	     before reaching [var_idx] ([var_idx] excluded). Also returns the comb
-	     which topvar is [var_idx]. *)
-
-	  let _ = assert (not (Bdd.is_cst comb)) in
-	  let combvar = Bdd.topvar comb in
-	    if var_idx = combvar
-	    then (comb, cpt)
-	    else count_missing_vars (Bdd.dthen comb) var_idx (cpt+1)
+	       (count_missing_vars: Bdd.t -> var_idx -> int -> Bdd.t * int) =
+	     fun comb var_idx cpt -> 
+	       (* Returns [cpt] + the number of variables occurring in [comb]
+	          before reaching [var_idx] ([var_idx] excluded). Also returns the comb
+	          which topvar is [var_idx]. *)
+
+	       let _ = assert (not (Bdd.is_cst comb)) in
+	       let combvar = Bdd.topvar comb in
+	         if var_idx = combvar
+	         then (comb, cpt)
+	         else count_missing_vars (Bdd.dthen comb) var_idx (cpt+1)
       in
       let (sub_comb, missing_vars_nb) = 
-	count_missing_vars (Bdd.dthen comb) topvar 0
+	     count_missing_vars (Bdd.dthen comb) topvar 0
       in
       let n0 = build_sol_nb_table_rec sub_bdd sub_comb snt in
       let factor = (two_power_of missing_vars_nb) in
       let res = mult_sol_nb n0 factor in
-	res
+	     res
 
 
 
@@ -388,11 +371,17 @@ and (draw_in_bdd_rec_bool: Var.env_in -> Var.env -> int -> string -> var ->
 	          [res_opt] is bound to [None]. 
 	       *)
 	       try 
-	         draw_in_bdd_rec input memory vl ctx_msg (sl1, store) bdd1 new_comb
+            if not (eq_sol_nb sol_nb1 zero_sol)
+	         then (
+              assert (not (Bdd.is_false bdd1)) ;
+              draw_in_bdd_rec input memory vl ctx_msg (sl1, store) bdd1 new_comb)
+            else raise No_numeric_solution
 	       with
 	           No_numeric_solution ->
 		          if not (eq_sol_nb sol_nb2 zero_sol)
-		          then draw_in_bdd_rec input memory vl ctx_msg (sl2, store) bdd2 new_comb
+		          then (
+                  assert (not (Bdd.is_false bdd1)) ;
+                  draw_in_bdd_rec input memory vl ctx_msg (sl2, store) bdd2 new_comb)
 		            (* 
 		               The second branch is now tried because no path in
 		               the first bdd leaded to a satisfiable set of
@@ -436,7 +425,6 @@ and (draw_in_bdd_rec_ineq: Var.env_in -> Var.env -> int -> string -> Constraint.
 	     raise No_numeric_solution 
       )
     in 
-
     let ran = Random.float 1. in
     let cstr_neg = Constraint.neg_ineq cstr in
     let (cstr1, bdd1, sol_nb1, cstr2, bdd2, sol_nb2) =
@@ -450,6 +438,7 @@ and (draw_in_bdd_rec_ineq: Var.env_in -> Var.env -> int -> string -> Constraint.
       (*     let bddi = try Hashtbl.find bdd_to_int bdd with _ -> -1 *)
       (*     and bdd1i = try Hashtbl.find bdd_to_int bdd1 with _ -> -1 *)
       (*     and bdd2i = try Hashtbl.find bdd_to_int bdd2 with _ -> -1 in *)
+
     let store1 = add_constraint store (Ineq cstr1) in
       (* A solution will be found in this branch iff there exists
 	      at least one path in the bdd that leads to a satisfiable