solver.ml 17.6 KB
 Erwan Jahier committed Mar 17, 2010 1 ``````(*----------------------------------------------------------------------- `````` Erwan Jahier committed Mar 17, 2010 2 ``````** Copyright (C) 2001, 2002 - Verimag. `````` Erwan Jahier committed Mar 17, 2010 3 4 5 6 7 8 9 10 ``````** This file may only be copied under the terms of the GNU Library General ** Public License **----------------------------------------------------------------------- ** ** File: solver.ml ** Main author: jahier@imag.fr *) `````` Erwan Jahier committed Mar 17, 2010 11 ``````open List `````` Erwan Jahier committed Mar 17, 2010 12 ``````open Formula `````` Erwan Jahier committed Mar 17, 2010 13 ``````open Env_state `````` Erwan Jahier committed Mar 17, 2010 14 ``````open Util `````` Erwan Jahier committed Mar 17, 2010 15 ``````open Hashtbl `````` Erwan Jahier committed Mar 17, 2010 16 `````` `````` Erwan Jahier committed Mar 17, 2010 17 18 19 ``````(****************************************************************************) let (formula_list_to_conj: formula list -> formula) = `````` Erwan Jahier committed Mar 17, 2010 20 `````` fun fl -> `````` Erwan Jahier committed Mar 17, 2010 21 22 23 24 25 26 27 28 29 `````` (** Transform a (non-empty) list of formula to the conjunction made of those formula. *) match fl with [] -> assert false | f::[] -> f | f1::f2::tail -> List.fold_left (fun x y -> And(x, y)) (And(f1, f2)) tail `````` Erwan Jahier committed Mar 17, 2010 30 `````` `````` Erwan Jahier committed Mar 17, 2010 31 32 33 ``````let rec (formula_to_bdd : formula -> Bdd.t) = fun f -> (** Transform the formula [f] into a bdd. Also tabulates the `````` Erwan Jahier committed Mar 17, 2010 34 35 `````` result in the [bdd_tbl] field of [env_state] because this translation is expensive. `````` Erwan Jahier committed Mar 17, 2010 36 `````` *) `````` Erwan Jahier committed Mar 17, 2010 37 38 `````` try Hashtbl.find env_state.bdd_tbl f with Not_found -> `````` Erwan Jahier committed Mar 17, 2010 39 40 `````` let bdd = match f with `````` Erwan Jahier committed Mar 17, 2010 41 42 `````` Not(f1) -> Bdd.dnot (formula_to_bdd f1) | Or(f1, f2) -> Bdd.dor (formula_to_bdd f1) (formula_to_bdd f2) `````` Erwan Jahier committed Mar 17, 2010 43 44 45 46 `````` | And(f1, f2) -> Bdd.dand (formula_to_bdd f1) (formula_to_bdd f2) | True -> Bdd.dtrue () | False -> Bdd.dfalse () `````` Erwan Jahier committed Mar 17, 2010 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 `````` | Bvar(vn) -> Bdd.var (Env_state.atomic_formula_to_index f) | Eq(e1, e2) -> (* We transform [e1 = e2] into [e1 <= e2 ^ e1 >= e2] as the numeric solver can not handle disequalities *) ( Bdd.dand (Bdd.var (Env_state.atomic_formula_to_index (SupEq(e1, e2)))) (Bdd.var (Env_state.atomic_formula_to_index (InfEq(e1, e2)))) ) | Neq(e1, e2) -> (* We transform [e1 <> e2] into [e1 < e2 ^ e1 > e2] as the numeric solver can not handle disequalities *) ( Bdd.dand (Bdd.var (Env_state.atomic_formula_to_index (Sup(e1, e2)))) (Bdd.var (Env_state.atomic_formula_to_index (Inf(e1, e2)))) ) | SupEq(e1, e2) -> Bdd.var (Env_state.atomic_formula_to_index f) | Sup(e1, e2) -> Bdd.var (Env_state.atomic_formula_to_index f) | InfEq(e1, e2) -> Bdd.var (Env_state.atomic_formula_to_index f) | Inf(e1, e2) -> Bdd.var (Env_state.atomic_formula_to_index f) `````` Erwan Jahier committed Mar 17, 2010 65 66 `````` in let _ = match f with `````` Erwan Jahier committed Mar 17, 2010 67 `````` Not(nf) -> () `````` Erwan Jahier committed Mar 17, 2010 68 69 `````` | _ -> Hashtbl.add env_state.bdd_tbl (Not(f)) (Bdd.dnot bdd) in `````` Erwan Jahier committed Mar 17, 2010 70 71 72 `````` (* print_string ("\$\$\$ building the bdd of " ^ (formula_to_string f) ^ "\n") ; *) (* flush stdout ; *) `````` Erwan Jahier committed Mar 17, 2010 73 74 `````` Hashtbl.add env_state.bdd_tbl f bdd; bdd `````` Erwan Jahier committed Mar 17, 2010 75 76 `````` `````` Erwan Jahier committed Mar 17, 2010 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 ``````(****************************************************************************) (****************************************************************************) (* Exported *) let rec (is_satisfiable: formula list -> bool) = fun fl -> let f = formula_list_to_conj fl in let bdd = formula_to_bdd (formula_list_to_conj fl) in not (Bdd.is_false bdd) && ( try let (n, m) = find env_state.snt bdd in not ((zero_sol, zero_sol) = (n, m)) with Not_found -> true ) (****************************************************************************) `````` Erwan Jahier committed Mar 17, 2010 97 98 99 100 101 102 103 104 105 106 ``````(****************************************************************************) type var = int (** In the following, we call a comb the bdd of a conjunction of litterals (var). They provide the ordering in which litterals appear in the bdds we manipulate. *) `````` Erwan Jahier committed Mar 17, 2010 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 ``````(* XXX To remove when mldd is fixed *) let check_sol_nb_build bdd bdd_not comb ne nt not_ne not_nt = (**) let card_sol_t = (**) (Bdd.cardinal (**) (List.length (**) (Bdd.int_of_support (Bdd.dthen comb))) (Bdd.dthen bdd)) in (**) let card_sol_e = (**) (Bdd.cardinal (**) (List.length (**) (Bdd.int_of_support (Bdd.dthen comb))) (Bdd.delse bdd)) in (**) let nt_float = float_of_sol_nb nt in (**) let ne_float = float_of_sol_nb ne in (**) (**) let card_sol_t_not = (**) (Bdd.cardinal (**) (List.length (**) (Bdd.int_of_support (Bdd.dthen comb))) (**) (Bdd.dthen bdd_not)) in (**) let card_sol_e_not = (**) (Bdd.cardinal (**) (List.length (**) (Bdd.int_of_support (Bdd.dthen comb))) (**) (Bdd.delse bdd_not)) in (**) let nt_float_not = float_of_sol_nb not_nt in (**) let ne_float_not = float_of_sol_nb not_ne in (**) if (**) (card_sol_t <> nt_float) || (**) (card_sol_e <> ne_float) || (**) (card_sol_t_not <> nt_float_not) || (**) (card_sol_e_not <> ne_float_not) (**) then (**) begin (**) print_string "Lurette computes: "; (**) print_string (string_of_sol_nb (add_sol_nb nt ne)); (**) print_string " = "; (**) print_string (string_of_sol_nb nt); (**) print_string " + ";print_string (string_of_sol_nb ne); (**) print_string "\nBdd.cardinal computes: "; (**) print_float (Bdd.cardinal (**) (List.length (Bdd.int_of_support comb)) (**) bdd); (**) print_string " = "; print_float card_sol_t; (**) print_string " + "; print_float card_sol_e ; (**) print_string "\n\n"; flush stdout ; (**) Print.bdd_with_dot (**) bdd (**) (fun index -> (**) Formula.formula_to_string (**) (Env_state.index_to_atomic_formula index)) (**) "bdd" ; (**) (**) print_string "(Not) Lurette computes: "; (**) print_string (string_of_sol_nb (add_sol_nb not_nt not_ne)); (**) print_string " = ";print_string (string_of_sol_nb not_nt); (**) print_string " + ";print_string (string_of_sol_nb not_ne); (**) print_string "\nBdd.cardinal computes: "; (**) print_float (Bdd.cardinal (**) (List.length (Bdd.int_of_support comb)) (**) bdd_not); (**) print_string " = "; print_float card_sol_t_not; (**) print_string " + "; print_float card_sol_e_not ; (**) print_string "\n\n"; flush stdout ; (**) Print.bdd_with_dot (**) bdd_not (**) (fun index -> (**) Formula.formula_to_string (**) (Env_state.index_to_atomic_formula index)) (**) "bdd_not" ; (**) (**) Util.gv "bdd.ps"; (**) Util.gv "bdd_not.ps"; (**) false (**) end (**) else (**) true `````` Erwan Jahier committed Mar 17, 2010 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 ``````let rec (count_missing_vars: Bdd.t -> var -> int -> Bdd.t * int) = fun comb var cpt -> (* Returns [cpt] + the number of variables occurring in [comb] before reaching [var] ([var] excluded). Also returns the comb which topvar is [var]. *) let _ = assert (not (Bdd.is_cst comb)) in let combvar = Bdd.topvar comb in if var = combvar then (comb, cpt) else count_missing_vars (Bdd.dthen comb) var (cpt+1) let rec (build_sol_nb_table: Bdd.t -> Bdd.t -> sol_nb * sol_nb) = fun bdd comb -> (** Returns the relative (to which bbd points to it) number of solutions of [bdd] and the one of its negation. Also udpates the solution number table [env_state.snt] for [bdd] and its negation, and recursively for all its sub-bdds. *) let bdd_not = (Bdd.dnot bdd) in let (sol_nb, sol_nb_not) = try let (nt, ne) = Hashtbl.find env_state.snt bdd and (not_nt, not_ne) = Hashtbl.find env_state.snt bdd_not in (* solutions numbers in the table are absolute *) ((add_sol_nb nt ne), (add_sol_nb not_nt not_ne)) with Not_found -> let _ = assert (not (Bdd.is_cst bdd)) in let _ = assert ((Bdd.topvar bdd) = (Bdd.topvar comb)) in let (nt, not_nt) = compute_absolute_sol_nb (Bdd.dthen bdd) comb in let (ne, not_ne) = compute_absolute_sol_nb (Bdd.delse bdd) comb in `````` Erwan Jahier committed Mar 17, 2010 217 218 `````` let _ = assert ( (* XXX Debugging stuff *) check_sol_nb_build bdd bdd_not comb ne nt not_ne not_nt) `````` Erwan Jahier committed Mar 17, 2010 219 220 221 222 223 224 225 226 227 228 229 230 231 232 `````` in Hashtbl.add env_state.snt bdd (nt, ne) ; Hashtbl.add env_state.snt bdd_not (not_nt, not_ne) ; ((add_sol_nb nt ne), (add_sol_nb not_nt not_ne)) in (sol_nb, sol_nb_not) and (compute_absolute_sol_nb: Bdd.t -> Bdd.t -> sol_nb * sol_nb) = fun sub_bdd comb -> (* returns the absolute number of solutions of [sub_bdd] (and its negation) w.r.t. [comb], where [comb] is the comb of the father of [sub_bdd]. *) if Bdd.is_cst sub_bdd then `````` Erwan Jahier committed Mar 17, 2010 233 234 235 `````` let sol_nb = (two_power_of (List.length (Bdd.int_of_support (Bdd.dthen comb)))) in `````` Erwan Jahier committed Mar 17, 2010 236 237 238 239 240 241 242 243 244 245 246 247 `````` if Bdd.is_true sub_bdd then (sol_nb, zero_sol) else (zero_sol, sol_nb) else let topvar = Bdd.topvar sub_bdd in let (sub_comb, missing_vars_nb) = count_missing_vars (Bdd.dthen comb) topvar 0 in let (n0, not_n0) = build_sol_nb_table sub_bdd sub_comb in let factor = (two_power_of missing_vars_nb) in (mult_sol_nb n0 factor, mult_sol_nb not_n0 factor) `````` Erwan Jahier committed Mar 17, 2010 248 249 250 251 `````` (****************************************************************************) (****************************************************************************) `````` Erwan Jahier committed Mar 17, 2010 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 ``````(*XXX Debugging stuff (to remove when the ML in mldd is fixed) *) let check_sol_nb comb bdd n m t = (*XXX*) let card_sol_t = (*XXX*) (Bdd.cardinal (List.length (*XXX*) (Bdd.int_of_support (Bdd.dthen comb))) (Bdd.dthen bdd)) (*XXX*) and card_sol_e = (*XXX*) (Bdd.cardinal (List.length (*XXX*) (Bdd.int_of_support (Bdd.dthen comb))) (Bdd.delse bdd)) (*XXX*) and n_float = float_of_sol_nb n (*XXX*) and m_float = float_of_sol_nb m (*XXX*) in (*XXX*) if (*XXX*) ( (card_sol_t <> n_float) || (card_sol_e <> m_float) ) (*XXX*) && (card_sol_t < 10. ** 12.) (*XXX*) (* Bdd.cardinal ougth to do rounding errors after 10^12 *) (*XXX*) && (card_sol_e < 10. ** 12.) (*XXX*) then (*XXX*) begin (*XXX*) print_string "Lurette computes: "; print_string (string_of_sol_nb t); (*XXX*) print_string " = ";print_string (string_of_sol_nb n); (*XXX*) print_string " + ";print_string (string_of_sol_nb m); (*XXX*) print_string "\nBdd.cardinal computes: "; (*XXX*) print_float (Bdd.cardinal (List.length (Bdd.int_of_support comb)) bdd); (*XXX*) print_string " = "; print_float card_sol_t; (*XXX*) print_string " + "; print_float card_sol_e ; (*XXX*) print_string "\n\n"; flush stdout ; (*XXX*) Print.bdd_with_dot (*XXX*) bdd (*XXX*) (fun index -> Formula.formula_to_string (Env_state.index_to_atomic_formula index)) (*XXX*) "bbd" ; (*XXX*) Util.gv "bdd.ps"; (*XXX*) false (*XXX*) end (*XXX*) else (*XXX*) true (*XXX*) let (toss_up_one_var: var -> subst) = `````` Erwan Jahier committed Mar 17, 2010 296 `````` fun var -> `````` Erwan Jahier committed Mar 17, 2010 297 298 299 300 301 302 303 304 305 306 307 `````` (* [var] is a index that ougth to correspond to a boolean variable. This fonction performs a toss and returns a substitution for the corresponding boolean variable. *) let af = Env_state.index_to_atomic_formula var in let vn = ( match af with Bvar(vn0) -> vn0 | _ -> (* Only bool index ougth to appear in the comb. *) assert false ) in `````` Erwan Jahier committed Mar 17, 2010 308 `````` let ran = Random.float 1. in `````` Erwan Jahier committed Mar 17, 2010 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 `````` if (ran < 0.5) then (vn, Formula.Bool(true)) else (vn, Formula.Bool(false)) let is_a_numeric_constraint af = match af with Bvar(_) -> false | _ -> true (* exported *) exception No_numeric_solution let (formula_to_nc : formula -> Rnumsolver.nc) = fun f -> match f with Sup(e1, e2) -> Rnumsolver.Sup(e1, e2) | SupEq(e1, e2) -> Rnumsolver.SupEq(e1, e2) | Inf(e1, e2) -> Rnumsolver.Inf(e1, e2) | InfEq(e1, e2) -> Rnumsolver.InfEq(e1, e2) | _ -> assert false `````` Erwan Jahier committed Mar 17, 2010 332 `````` `````` Erwan Jahier committed Mar 17, 2010 333 334 335 336 337 338 339 340 ``````let rec (draw_in_bdd: subst list * Rnumsolver.store -> Bdd.t -> Bdd.t -> subst list * Rnumsolver.store) = fun (sl, store) bdd comb -> (** Returns [sl] appended to a draw of all the boolean variables bigger than the topvar of [bdd] according to the ordering induced by the comb [comb]. Also returns the (non empty) store obtained by adding to [store] all the numeric constraints that were encountered during this draw. `````` Erwan Jahier committed Mar 17, 2010 341 `````` `````` Erwan Jahier committed Mar 17, 2010 342 343 344 `````` Raises the [No_numeric_solution] exception whenever no valid path in [bdd] leads to a satisfiable set of numeric constraints. `````` Erwan Jahier committed Mar 17, 2010 345 346 `````` *) let _ = assert (not (Bdd.is_cst bdd)) in `````` Erwan Jahier committed Mar 17, 2010 347 348 `````` let _ = assert (Hashtbl.mem env_state.snt bdd) in let bddvar = Bdd.topvar bdd in `````` Erwan Jahier committed Mar 17, 2010 349 `````` let combvar = Bdd.topvar comb in `````` Erwan Jahier committed Mar 17, 2010 350 351 `````` let af = (Env_state.index_to_atomic_formula bddvar) in let top_var_is_numeric = is_a_numeric_constraint af in `````` Erwan Jahier committed Mar 17, 2010 352 `````` if `````` Erwan Jahier committed Mar 17, 2010 353 354 `````` bddvar <> combvar && not top_var_is_numeric `````` Erwan Jahier committed Mar 17, 2010 355 `````` then `````` Erwan Jahier committed Mar 17, 2010 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 `````` let new_sl = (toss_up_one_var combvar)::sl in draw_in_bdd (new_sl, store) bdd (Bdd.dthen comb) else (* bddvar = bddvar xor top_var_is_numeric *) (* nb: I handle those two cases alltogether to avoid code duplication (i.e., retrieving sol numbers, performing the toss, the recursive call, handling the base case where a dtrue bdd is reached, etc). It makes the code a little bit more obscur, but ... *) let (n, m) = Hashtbl.find env_state.snt bdd in let _ = if ((eq_sol_nb n zero_sol) && (eq_sol_nb m zero_sol)) then raise No_numeric_solution ; (* XXX Debug stuff (to remove when the mem leak in mldd is fixed) *) assert (check_sol_nb comb bdd n m (add_sol_nb n m)) `````` Erwan Jahier committed Mar 17, 2010 371 `````` in `````` Erwan Jahier committed Mar 17, 2010 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 `````` let (store_plus_af, store_plus_not_af) = (* A first trick to avoid code dup (cf nb above) *) if top_var_is_numeric then Rnumsolver.split store (formula_to_nc af) else (store, store) in let (swap, store1, bdd1, bool1, sol_nb1, store2, bdd2, bool2, sol_nb2) = (* Depending on the result of a toss (based on the number of solution in each branch), we try the [else] or the [then] branch first. [swap] indicates whether or not the [else] part is put before the [then] one. *) let ran = Random.float 1. in if ran < ((float_of_sol_nb n) /. (float_of_sol_nb (add_sol_nb n m))) `````` Erwan Jahier committed Mar 17, 2010 387 `````` then `````` Erwan Jahier committed Mar 17, 2010 388 389 390 391 392 `````` (false, store_plus_af, (Bdd.dthen bdd), true, n, store_plus_not_af, (Bdd.delse bdd), false, m ) else (true, store_plus_not_af, (Bdd.delse bdd), false, m, store_plus_af, (Bdd.dthen bdd), true, n ) `````` Erwan Jahier committed Mar 17, 2010 393 `````` in `````` Erwan Jahier committed Mar 17, 2010 394 395 396 397 398 399 400 401 402 403 404 `````` let (sl1, sl2, new_comb) = ( (* A second trick to avoid code dup (cf nb above) *) match af with Bvar(vn) -> (((vn, Formula.Bool(bool1))::sl), ((vn, Formula.Bool(bool2))::sl), (Bdd.dthen comb) ) | _ -> (* top_var_is_numeric *) (sl, sl, comb) ) `````` Erwan Jahier committed Mar 17, 2010 405 `````` in `````` Erwan Jahier committed Mar 17, 2010 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 `````` let res_opt = (* A solution will be found in this branch iff there exists at least one path in the bdd that leads to a satisfiable set of numeric constraints. If it is not the case, [res_opt] is bound to [None]. *) if not (Rnumsolver.is_empty store1) then try let tail_draw1 = if Bdd.is_true bdd1 then (* Toss the remaining bool vars. *) ( (List.append sl1 (map toss_up_one_var (Bdd.int_of_support new_comb))), store1 ) else draw_in_bdd (sl1, store1) bdd1 new_comb in Some(tail_draw1) with No_numeric_solution -> None `````` Erwan Jahier committed Mar 17, 2010 429 `````` else `````` Erwan Jahier committed Mar 17, 2010 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 `````` ( (* Update the table of sol nbs *) if swap then Hashtbl.replace env_state.snt bdd (n, zero_sol) else Hashtbl.replace env_state.snt bdd (zero_sol, m); None ) in match res_opt with Some(res) -> res | None -> (* The second branch is now tried because no path in the first bdd leaded to a satisfiable set of numeric constraints. *) if not (eq_sol_nb sol_nb2 zero_sol) then if not (Rnumsolver.is_empty store2) then if Bdd.is_true bdd2 then ( (List.append sl2 (List.map toss_up_one_var (Bdd.int_of_support new_comb))), store2 ) else draw_in_bdd (sl2, store2) bdd2 new_comb else ( (* Update the table of sol nbs *) if swap then Hashtbl.replace env_state.snt bdd (0, m) else Hashtbl.replace env_state.snt bdd (n, 0); raise No_numeric_solution ) else raise No_numeric_solution `````` Erwan Jahier committed Mar 17, 2010 470 471 `````` `````` Erwan Jahier committed Mar 17, 2010 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 ``````let (draw : vn list -> vnt list -> Bdd.t -> Bdd.t -> subst list * subst list) = fun bool_vars_to_gen num_vnt_to_gen comb bdd -> (** Draw the output and local vars to be generated by the environnent. *) let (bool_subst_l, store) = draw_in_bdd ([], (Rnumsolver.new_store num_vnt_to_gen)) bdd comb in let num_subst_l = Rnumsolver.draw_inside store in let subst_l = append bool_subst_l num_subst_l in let (out_vars, _) = List.split (env_state.output_var_names) in assert ( (* Checks that we generated all variables. *) let (gen_vars, _) = split subst_l in let (num_vars_to_gen, _) = split num_vnt_to_gen in let vars_to_gen = append bool_vars_to_gen num_vars_to_gen in (sort (compare) gen_vars) = (sort (compare) vars_to_gen) ); (* Splits output and local vars. *) List.partition (fun (vn, _) -> List.mem vn out_vars) subst_l `````` Erwan Jahier committed Mar 17, 2010 493 `````` `````` Erwan Jahier committed Mar 17, 2010 494 `````` `````` Erwan Jahier committed Mar 17, 2010 495 `````` `````` Erwan Jahier committed Mar 17, 2010 496 ``````(* Exported *) `````` Erwan Jahier committed Mar 17, 2010 497 498 499 ``````let (solve_formula: int -> formula list -> vn list -> vnt list -> (subst list * subst list) list) = fun p fl bool_vars_to_gen num_vars_to_gen -> `````` Erwan Jahier committed Mar 17, 2010 500 501 `````` let f = formula_list_to_conj fl in let bdd = Hashtbl.find env_state.bdd_tbl f in `````` Erwan Jahier committed Mar 17, 2010 502 `````` let bool_vars_to_gen_f = `````` Erwan Jahier committed Mar 17, 2010 503 504 505 `````` List.fold_left (fun acc vn -> (And(Bvar(vn), acc))) True `````` Erwan Jahier committed Mar 17, 2010 506 `````` bool_vars_to_gen `````` Erwan Jahier committed Mar 17, 2010 507 `````` in `````` Erwan Jahier committed Mar 17, 2010 508 `````` let comb = formula_to_bdd bool_vars_to_gen_f in `````` Erwan Jahier committed Mar 17, 2010 509 `````` `````` Erwan Jahier committed Mar 17, 2010 510 511 512 513 514 515 516 517 518 519 ``````(**) let _ = (**) (* XXX Recompute the solution number everytime as long as mldd sucks *) (**) begin (**) Hashtbl.clear env_state.snt ; (**) Hashtbl.add env_state.snt (**) (Bdd.dtrue ()) (one_sol, zero_sol); (**) Hashtbl.add env_state.snt (**) (Bdd.dfalse ()) (zero_sol, one_sol) (**) end (**) in `````` Erwan Jahier committed Mar 17, 2010 520 521 522 `````` let _ = if not (Hashtbl.mem env_state.snt bdd) then `````` Erwan Jahier committed Mar 17, 2010 523 `````` let rec skip_var comb v = `````` Erwan Jahier committed Mar 17, 2010 524 525 `````` let topvar = (Bdd.topvar comb) in if v = topvar then comb else skip_var (Bdd.dthen comb) v `````` Erwan Jahier committed Mar 17, 2010 526 527 528 529 530 531 `````` in let comb2 = skip_var comb (Bdd.topvar bdd) in build_sol_nb_table bdd comb2 else (zero_sol, zero_sol) in `````` Erwan Jahier committed Mar 17, 2010 532 533 534 535 `````` try Util.unfold (draw bool_vars_to_gen num_vars_to_gen comb) bdd p with No_numeric_solution -> (* XXX I should rather redraw with an another formula *) []``````