solver.ml 13.4 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 `````` Not(f1) -> Bdd.dnot (formula_to_bdd f1) `````` Erwan Jahier committed Mar 17, 2010 42 `````` | Or(f1, f2) -> Bdd.dor (formula_to_bdd f1) (formula_to_bdd f2) `````` Erwan Jahier committed Mar 17, 2010 43 44 `````` | And(f1, f2) -> Bdd.dand (formula_to_bdd f1) (formula_to_bdd f2) `````` Erwan Jahier committed Mar 17, 2010 45 46 47 `````` | True -> Bdd.dtrue env_state.bdd_manager | False -> Bdd.dfalse env_state.bdd_manager | Bvar(vn) -> Bdd.ithvar env_state.bdd_manager (Env_state.atomic_formula_to_index f) `````` Erwan Jahier committed Mar 17, 2010 48 49 50 51 52 `````` | Eq(e1, e2) -> (* We transform [e1 = e2] into [e1 <= e2 ^ e1 >= e2] as the numeric solver can not handle disequalities *) ( Bdd.dand `````` Erwan Jahier committed Mar 17, 2010 53 54 `````` (Bdd.ithvar env_state.bdd_manager (Env_state.atomic_formula_to_index (SupEq(e1, e2)))) (Bdd.ithvar env_state.bdd_manager (Env_state.atomic_formula_to_index (InfEq(e1, e2)))) ) `````` Erwan Jahier committed Mar 17, 2010 55 56 57 58 `````` | Neq(e1, e2) -> (* We transform [e1 <> e2] into [e1 < e2 ^ e1 > e2] as the numeric solver can not handle disequalities *) ( Bdd.dand `````` Erwan Jahier committed Mar 17, 2010 59 60 61 62 63 64 `````` (Bdd.ithvar env_state.bdd_manager (Env_state.atomic_formula_to_index (Sup(e1, e2)))) (Bdd.ithvar env_state.bdd_manager (Env_state.atomic_formula_to_index (Inf(e1, e2)))) ) | SupEq(e1, e2) -> Bdd.ithvar env_state.bdd_manager (Env_state.atomic_formula_to_index f) | Sup(e1, e2) -> Bdd.ithvar env_state.bdd_manager (Env_state.atomic_formula_to_index f) | InfEq(e1, e2) -> Bdd.ithvar env_state.bdd_manager (Env_state.atomic_formula_to_index f) | Inf(e1, e2) -> Bdd.ithvar env_state.bdd_manager (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 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 ``````(****************************************************************************) 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. *) 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 (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 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 149 `````` let sol_nb = `````` Erwan Jahier committed Mar 17, 2010 150 151 `````` if Bdd.is_true comb (* iff no bool are to be gen *) then one_sol `````` Erwan Jahier committed Mar 17, 2010 152 `````` else (two_power_of (List.length (Bdd.list_of_support (Bdd.dthen comb)))) `````` Erwan Jahier committed Mar 17, 2010 153 `````` in `````` Erwan Jahier committed Mar 17, 2010 154 155 156 157 158 159 `````` 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) = `````` Erwan Jahier committed Mar 17, 2010 160 161 162 `````` if Bdd.is_true comb (* iff no bool are to be gen *) then (comb, 0) else count_missing_vars (Bdd.dthen comb) topvar 0 `````` Erwan Jahier committed Mar 17, 2010 163 164 165 166 167 `````` 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 168 169 170 171 `````` (****************************************************************************) (****************************************************************************) `````` Erwan Jahier committed Mar 17, 2010 172 173 `````` let (toss_up_one_var: var -> subst) = `````` Erwan Jahier committed Mar 17, 2010 174 `````` fun var -> `````` Erwan Jahier committed Mar 17, 2010 175 176 177 178 179 180 181 182 183 184 185 `````` (* [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 186 `````` let ran = Random.float 1. in `````` Erwan Jahier committed Mar 17, 2010 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 `````` 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 210 `````` `````` Erwan Jahier committed Mar 17, 2010 211 212 213 214 215 216 217 218 ``````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 219 `````` `````` Erwan Jahier committed Mar 17, 2010 220 221 222 `````` 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 223 224 `````` *) let _ = assert (not (Bdd.is_cst bdd)) in `````` Erwan Jahier committed Mar 17, 2010 225 226 227 228 `````` let _ = assert (Hashtbl.mem env_state.snt bdd) in let bddvar = Bdd.topvar bdd in 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 229 `````` if `````` Erwan Jahier committed Mar 17, 2010 230 231 `````` not(Bdd.is_true comb) && (* iff no bool are to be gen *) bddvar <> (Bdd.topvar comb) && `````` Erwan Jahier committed Mar 17, 2010 232 `````` not top_var_is_numeric `````` Erwan Jahier committed Mar 17, 2010 233 `````` then `````` Erwan Jahier committed Mar 17, 2010 234 `````` let new_sl = (toss_up_one_var (Bdd.topvar comb))::sl in `````` Erwan Jahier committed Mar 17, 2010 235 236 `````` draw_in_bdd (new_sl, store) bdd (Bdd.dthen comb) else `````` Erwan Jahier committed Mar 17, 2010 237 `````` (* bddvar = combvar xor top_var_is_numeric *) `````` Erwan Jahier committed Mar 17, 2010 238 239 240 241 242 243 244 245 246 `````` (* 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 ; `````` Erwan Jahier committed Mar 17, 2010 247 `````` in `````` Erwan Jahier committed Mar 17, 2010 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 `````` 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 263 `````` then `````` Erwan Jahier committed Mar 17, 2010 264 265 266 267 268 `````` (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 269 `````` in `````` Erwan Jahier committed Mar 17, 2010 270 271 272 273 274 275 `````` 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), `````` Erwan Jahier committed Mar 17, 2010 276 `````` (if Bdd.is_true comb then comb else Bdd.dthen comb) ) `````` Erwan Jahier committed Mar 17, 2010 277 278 279 280 `````` | _ -> (* top_var_is_numeric *) (sl, sl, comb) ) `````` Erwan Jahier committed Mar 17, 2010 281 `````` in `````` Erwan Jahier committed Mar 17, 2010 282 283 284 285 286 287 288 289 290 291 292 293 294 295 `````` 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 `````` Erwan Jahier committed Mar 17, 2010 296 `````` (map toss_up_one_var (Bdd.list_of_support new_comb))), `````` Erwan Jahier committed Mar 17, 2010 297 298 299 300 301 302 303 304 `````` 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 305 `````` else `````` Erwan Jahier committed Mar 17, 2010 306 `````` None `````` Erwan Jahier committed Mar 17, 2010 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 `````` 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 `````` Erwan Jahier committed Mar 17, 2010 323 `````` (Bdd.list_of_support new_comb))), `````` Erwan Jahier committed Mar 17, 2010 324 325 326 327 328 `````` store2 ) else draw_in_bdd (sl2, store2) bdd2 new_comb else `````` Erwan Jahier committed Mar 17, 2010 329 `````` raise No_numeric_solution `````` Erwan Jahier committed Mar 17, 2010 330 331 `````` else raise No_numeric_solution `````` Erwan Jahier committed Mar 17, 2010 332 `````` `````` Erwan Jahier committed Mar 17, 2010 333 `````` `````` Erwan Jahier committed Mar 17, 2010 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 ``````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 355 `````` `````` Erwan Jahier committed Mar 17, 2010 356 `````` `````` Erwan Jahier committed Mar 17, 2010 357 `````` `````` Erwan Jahier committed Mar 17, 2010 358 ``````(* Exported *) `````` Erwan Jahier committed Mar 17, 2010 359 360 361 ``````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 362 363 `````` let f = formula_list_to_conj fl in let bdd = Hashtbl.find env_state.bdd_tbl f in `````` Erwan Jahier committed Mar 17, 2010 364 `````` let bool_vars_to_gen_f = `````` Erwan Jahier committed Mar 17, 2010 365 366 367 `````` List.fold_left (fun acc vn -> (And(Bvar(vn), acc))) True `````` Erwan Jahier committed Mar 17, 2010 368 `````` bool_vars_to_gen `````` Erwan Jahier committed Mar 17, 2010 369 `````` in `````` Erwan Jahier committed Mar 17, 2010 370 `````` let comb = formula_to_bdd bool_vars_to_gen_f in `````` Erwan Jahier committed Mar 17, 2010 371 `````` `````` Erwan Jahier committed Mar 17, 2010 372 373 374 375 376 377 378 379 380 381 ``````(* (**) 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 env_state.bdd_manager) (one_sol, zero_sol); *) (* (**) Hashtbl.add env_state.snt *) (* (**) (Bdd.dfalse env_state.bdd_manager) (zero_sol, one_sol) *) (* (**) end *) (* (**) in *) `````` Erwan Jahier committed Mar 17, 2010 382 383 384 `````` let _ = if not (Hashtbl.mem env_state.snt bdd) then `````` Erwan Jahier committed Mar 17, 2010 385 `````` let rec skip_var comb v = `````` Erwan Jahier committed Mar 17, 2010 386 387 388 389 390 `````` if Bdd.is_true comb (* iff no bool are to be gen *) then comb else let topvar = (Bdd.topvar comb) in if v = topvar then comb else skip_var (Bdd.dthen comb) v `````` Erwan Jahier committed Mar 17, 2010 391 392 393 394 395 396 `````` 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 397 398 `````` try Util.unfold (draw bool_vars_to_gen num_vars_to_gen comb) bdd p with No_numeric_solution -> `````` Erwan Jahier committed Mar 17, 2010 399 `````` Hashtbl.replace env_state.snt bdd (zero_sol, zero_sol); `````` Erwan Jahier committed Mar 17, 2010 400 `````` [] `````` Erwan Jahier committed Mar 17, 2010 401