solver.ml 13.6 KB
Newer Older
1
(* -----------------------------------------------------------------------
2
** Copyright (C) 2001-2003 - Verimag.
3
** This file may only be copied under the terms of the GNU Library General
4
** Public License
5
6
7
8
9
10
**-----------------------------------------------------------------------
**
** File: solver.ml
** Main author: jahier@imag.fr
*)

11
open List
12
open Exp
13
open Constraint
14
open Util
15
open Hashtbl
16
open Gne
17
open Value
18
open Store
19
open Var
20

21
(****************************************************************************)
22
23


24
25
let sol_number = ref Bddd.sol_number
let draw_in_bdd = ref Bddd.draw_in_bdd
26

27
28
29
30
31
32
33
let add_snt_entry = ref Bddd.add_snt_entry

let init_snt = ref Bddd.init_snt
let clear_snt = ref Bddd.clear_snt


let (set_efficient_mode : unit -> unit) =
34
  fun _ ->
35
36
37
38
    sol_number := Bddd.sol_number;
    draw_in_bdd := Bddd.draw_in_bdd;
    add_snt_entry := Bddd.add_snt_entry;
    init_snt := Bddd.init_snt;
39
40
    clear_snt := Bddd.clear_snt;
    !clear_snt ()
41
42

let (set_fair_mode : unit -> unit) =
43
  fun _ ->
44
45
46
47
    sol_number := Fair_bddd.sol_number;
    draw_in_bdd := Fair_bddd.draw_in_bdd;
    add_snt_entry := Fair_bddd.add_snt_entry;
    init_snt := Fair_bddd.init_snt;
48
49
    clear_snt := Fair_bddd.clear_snt;
    !clear_snt ()
50
51


52

53

54
55
56
57
(****************************************************************************)
(****************************************************************************)


58

59
(* Exported *)
60
let (is_satisfiable_bdd: Var.env_in -> Var.env -> int -> string -> formula -> string -> bool*Bdd.t) =
61
  fun input memory vl ctx_msg f msg ->
Erwan Jahier's avatar
Erwan Jahier committed
62
 
63
    let bdd = Formula_to_bdd.f input memory ctx_msg vl f in
64
65
    let is_sat1 = not (Bdd.is_false bdd) 
    and is_sat2 =
66
      (* the formula may be false because of numerics. In that case,
Erwan Jahier's avatar
Erwan Jahier committed
67
	      the solution number is set to (0,0) (if a draw has been tried).
68
      *)
69
      (
Erwan Jahier's avatar
Erwan Jahier committed
70
71
72
73
74
75
76
77
78
79
	     try
	       let (n, m) = !sol_number bdd in
	         not ((Sol_nb.zero_sol, Sol_nb.zero_sol) = (n, m))
	     with
	         Not_found -> true
	           (* migth be false because of numerics, but we don't know yet *)
	       | e ->
	           print_string ((Printexc.to_string e) ^ "\n");
	           flush stdout;
	           assert false
80
      )
81
    in
82
      if vl > 2 then
Erwan Jahier's avatar
Erwan Jahier committed
83
84
85
86
87
88
89
90
91
92
	     (
	       print_string ("\n[" ^ msg^ "] -> ");
	       print_string (formula_to_string f);
	       if is_sat1 && is_sat2
	       then print_string "\n   is satisfiable (for the Boolean part).\n"
	       else if is_sat1 
	       then print_string "\n   is not satisfiable (because of numerics).\n"
	       else print_string "\n   is not satisfiable (because of Booleans).\n";
	       flush stdout
	     );
93
94
95
96
97
98
      is_sat1 && is_sat2, bdd

(* Exported *)
let (is_satisfiable: Var.env_in -> Var.env -> int -> string -> formula -> string -> bool) =
  fun input memory vl ctx_msg f msg ->
    fst(is_satisfiable_bdd input memory vl ctx_msg f msg)
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
(* printing bbd's with dot *)


open Sol_nb

let cpt = ref 0 
(* let (bdd_to_int : (Bdd.t, int) Hashtbl.t)= Hashtbl.create 100  *)

let (bdd_to_graph: Bdd.t -> (int -> string) -> bool -> 
       (string * string * string) list) =
  fun bdd index_to_string only_true ->
    let _ =
      cpt := 0;
      Hashtbl.clear Bddd.bdd_to_int 
    in
    let get_label bdd =
      if Bdd.is_true bdd then "True"
      else if Bdd.is_false bdd then "False"
      else 
	let bdd_int = 
	  try
124
	    hfind Bddd.bdd_to_int  bdd
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
185
	  with Not_found -> 
	    incr cpt;
	    Hashtbl.add  Bddd.bdd_to_int bdd !cpt;
	    !cpt
	in
	  ("\"(" ^(string_of_int bdd_int) ^ ")" ^ (index_to_string (Bdd.topvar bdd))) 
    in
    let rec (bdd_to_graph_acc: (string * string * string) list -> Bdd.t list -> 
	       bool -> Bdd.t -> (string * string * string) list * Bdd.t list) =
      fun acc0 visited only_true bdd ->
	if Bdd.is_cst bdd then (acc0, visited)
	else
	  if List.mem bdd visited then (acc0, visited) else
	  let bddt = Bdd.dthen bdd in
	  let bdde = Bdd.delse bdd in
	  let label = get_label  bdd in
	  let labelt = get_label bddt in
	  let labele = get_label bdde in
	  let s1,s2 = try !sol_number bdd with _  -> zero_sol,zero_sol in
	  let s1_str = " (" ^ Sol_nb.string_of_sol_nb s1 ^ ")"
	  and s2_str = " (" ^ Sol_nb.string_of_sol_nb s2 ^ ")" 
	  in
	  let acc1 = 
	    if s1 = zero_sol && only_true then acc0 else 
	      ((label,"\""^ "then" ^ s1_str ^ "\"", labelt)::acc0) 
	  in
	  let acc2 = 
	    if s2 = zero_sol && only_true then acc1 else 
	      ((label, "\""^ "else" ^ s2_str ^ "\"", labele)::acc1) 
	  in
	  let (acc3, visited') = 
	    bdd_to_graph_acc acc2 (bdd::visited) only_true bddt 
	  in
	    bdd_to_graph_acc acc3 visited' only_true bdde
    in
      fst (bdd_to_graph_acc [] [] only_true bdd)



let (print_bdd_with_dot: Bdd.t -> (int -> string) -> string -> bool -> unit) =
  fun bdd index_to_vn label only_true ->
    let arcs = bdd_to_graph bdd (index_to_vn) only_true in
    let dot_file = label ^ ".dot" in
    let ps_file = label ^ ".ps" in
    let dot_oc = open_out dot_file in
    let put = output_string dot_oc in
    let _ =
      put "digraph G {\n\n ordering=out;\n\n";
      put " ratio = compress;\n\n";
      List.iter (fun (n, _, _) -> put ("\t" ^ n ^ "\t ; \n")) arcs ;
      List.iter (fun (f, l, t) -> put ("\t" ^ f ^ " -> " ^ t ^ "\t  [label = " ^ l ^ " ] ; \n")) arcs ;
      put "} \n";
      flush dot_oc ;
      close_out dot_oc
    in
      (*  Calling dot to create the postscript file *)
    let exit_code_dot = Sys.command ("dot -Tps " ^ dot_file ^ " -o " ^ ps_file)
    in if (exit_code_dot <> 0)
      then print_string " Can't call dot; is dot in your path?\n\n"
      else ()

186

187
188
(****************************************************************************)
(****************************************************************************)
189

190
let (compute_default_value : Var.env_in -> Var.env -> int -> string -> Store.t' ->
191
       Exp.var list -> Store.t' * num_subst list) =
192
  fun input memory vl ctx_msg st varl ->
193
    (* [varl] is the list of variable that have not been constrained at all.
194
       For the variables that have a default value, we compute them and remove
195
       them from the variables that still need to be drawned.
196
    *)
197
198
199
    let (maybe_compute_value : Store.t' * num_subst list -> Exp.var ->
	   Store.t' * num_subst list) =
      fun acc var ->
200
	match (Var.default var) with
201
	    None -> acc
202
 	  | Some (Numer e) ->
203
	      let gne = Formula_to_bdd.num_to_gne input memory ctx_msg vl e in
204
		(match Gne.get_constant gne with
205
		     None ->
206
		       print_string (
207
			 "*** Default values should not depend on " ^
208
			 "controllable variables, \nwhich is the case of " ^
209
			 (Exp.num_to_string e) ^ ", the default value of " ^
210
			 (Var.name var) ^ "\n");
211
		       exit 2
212
213
		   | Some (I i) ->
		       Store.remove_var_from_range_store (fst acc) var,
214
		       (((Var.name var), (I i))::(snd acc))
215
216
		   | Some (F f) ->
		       Store.remove_var_from_range_store (fst acc) var,
217
		       (((Var.name var), (F f))::(snd acc))
218
219
		)
	  | Some _ -> assert false
220
    in
221
      List.fold_left (maybe_compute_value) (st, []) varl
222

223

224
let (draw : Var.env_in -> Var.env -> int -> string -> Var.name list list ->
225
      Thickness.numeric -> Var.name list -> var list -> Bdd.t -> Bdd.t ->
226
      (Var.env * Var.env) list) =
227
  fun input memory vl msg output_var_names (k1, k2, vertices_nb) bool_vars_to_gen num_vnt_to_gen comb bdd ->
228
    (** Draw the output and local vars to be generated by the environnent. *)
229

230
    let (bool_subst_l, store_range0, store_poly) =
231
      !draw_in_bdd input memory vl msg num_vnt_to_gen bdd comb
232
    in
233
234
    let num_subst_ll0 =
      if
235
	     num_vnt_to_gen = []
236
      then
237
	     []
238
      else
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
	     let (store_range, sl0) =
	       compute_default_value input memory vl msg store_range0
	         (Store.get_untouched_var store_range0)
	     in
	       (* XXX I should do something there if Draw.inside raises 
	          No_numeric_solution, to be able to backtrack in the bdd,
	          update the snt, and so on. 
	          
	          Not so easy...

	          For that reason, instead of raising that excp when I cannot
	          find any valid integers, i return a wrong one...
	       *)
	     let sll1 = Draw.inside vl store_range store_poly k1 sl0 in
	     let sll2 = Draw.edges vl store_range store_poly k2 sl0 in
	     let sll3 =
	       match vertices_nb with
	         | Thickness.All ->
		          let vl = Draw.get_all_vertices store_range store_poly sl0 in
		            assert (vl <> []);
		            vl
	         | Thickness.AtMost k3 ->
		          Draw.vertices vl store_range store_poly k3 sl0
	     in
	       rev_append sll1 (rev_append sll2 sll3)
264
    in
265
    let numlist2map nl = List.fold_left
266
	   (fun acc (vn, num) -> Value.OfIdent.add acc (vn, N num)) Value.OfIdent.empty nl in
267
    let num_subst_ll =
268
269
      (* List.map (List.map (fun (vn, num) -> (vn, N num))) num_subst_ll0 *)
      List.map numlist2map num_subst_ll0
270
    in
271
    let subst_ll = if num_subst_ll = []
272
273
274
275
276
277
    then
	   [bool_subst_l]
    else
	   List.map
	     (fun num_subst_l -> Value.OfIdent.union bool_subst_l num_subst_l)
	     num_subst_ll
278
    in
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
      (*
        assert (
	     (List.for_all
	     (fun (subst_l:Var.env) ->
	   (*  Checks that we have generated all variables, and not more. *)
	   (* let (gen_vars, _) = List.split subst_l in *)
	     let gen_vars = Value.OfIdent.support subst_l in
	     let num_vars_to_gen =
		  List.map (fun var -> (Var.name var)) num_vnt_to_gen
	     in
	     let vars_to_gen = append bool_vars_to_gen num_vars_to_gen in
	     let gen_vars_sorted = (sort (compare) gen_vars) in
	     let vars_to_gen_sorted = (sort (compare) vars_to_gen) in
		  if gen_vars_sorted = vars_to_gen_sorted then true else
		  (
		  output_string stderr " \ngen vars:   \t";
		  List.iter
		  (fun vn -> output_string stderr (vn ^ " ")) gen_vars_sorted;
		  output_string stderr " \nvars to gen:\t";
		  List.iter
		  (fun vn -> output_string stderr (vn ^ " ")) vars_to_gen_sorted;
		  output_string stderr " \n";
		  (try
		  List.iter2 
		  (fun vn1 vn2 -> 
		  if vn1 <> vn2 then 
305
		  (
306
307
		  output_string stderr ("\n e.g., " ^ vn1 ^ " <> " ^ vn2 ^ "\n");
		  failwith ""
308
		  )
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
		  )
		  gen_vars_sorted 
		  vars_to_gen_sorted
		  with _ -> 
		  ();
		  );
		  print_bdd_with_dot bdd   
		  (fun i ->   
		  Constraint.to_string   
		  (Formula_to_bdd.index_to_linear_constraint i)^"\""  
		  )  
		  "debug_bdd"
		  true;  	
		  print_bdd_with_dot bdd   
		  (fun i ->   
		  Constraint.to_string   
		  (Formula_to_bdd.index_to_linear_constraint i)^"\""  
		  )  
		  "debug_bdd_all"
		  false;
		  false
		  )
	     )
	     subst_ll
	     )
        );
      *)
336
      (* Splits output and local vars. *)
337
338
339
340
341
342
343
344
    let out_vars = List.flatten output_var_names in
	   List.map
	     (fun subst_l ->
	        (Value.OfIdent.partition
		        (fun (vn, _) ->
		           List.exists (fun out_var -> out_var = vn) out_vars)
		        subst_l
	        )
345
	     )
346
	     subst_ll
347

348

349
350
351
352

(****************************************************************************)


353
(* Exported *)
354
let (solve_formula: Var.env_in -> Var.env -> int -> string -> Var.name list list ->
355
      Thickness.formula_draw_nb ->  Thickness.numeric -> formula -> var list -> formula -> 
356
	   (Var.env * Var.env) list) =
357
  fun input memory vl ctx_msg output_var_names p num_thickness bool_vars_to_gen_f num_vars_to_gen f ->
358

359
    let bdd = (Formula_to_bdd.f input memory ctx_msg vl f) in
360
361
    let _ = 
      assert (not (Bdd.is_false bdd));
362
      if vl >= 2 then
363
364
365
366
367
368
369
        (
	       print_string "\n --> ";
	       print_string (formula_to_string f);
	       print_string
	         "\n  has been elected to be the formula in which solutions are drawn.\n";
	       flush stdout
        )
370
    in
371

372
    let comb0 = (Formula_to_bdd.f input memory ctx_msg vl bool_vars_to_gen_f) in
373
    let comb =
374
      (* All Boolean vars should appear in the comb so that when we
375
376
377
378
379
380
381
382
	      find that such a var is missing along a bdd path, we can
	      perform a (fair) toss for it. On the contrary, if a
	      numerical contraint disappear from a bdd (eg, consider [(f
	      && false) || true]), it is not important; fairly tossing a
	      (boolean) value for a num constaint [nc] and performing a
	      fair toss in the resulting domain is equivalent to directly
	      perform the toss in the (unconstraint wrt [nc]) initial
	      domain.
383
      *)
384
      Bdd.dand (Bdd.support bdd) comb0
385
    in	
386
    let bool_vars_to_gen = Exp.support bool_vars_to_gen_f in
387
      try
388
389
390
391
	     let res =
	       (flatten
	          (Util.unfold
		          (draw input memory vl ctx_msg output_var_names num_thickness
392
                   bool_vars_to_gen num_vars_to_gen comb)
393
394
395
396
397
398
		          bdd
		          p
	          )
	       )
	     in
	       res
399
      with
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
	       No_numeric_solution ->
	         if vl >= 3 then (
	           (print_bdd_with_dot bdd   
		           (fun i ->   
		              Constraint.to_string   
		                (Formula_to_bdd.index_to_linear_constraint i)^"\""  
		           )  
		           "debug_bdd"
		           true
	           );  	
	           (print_bdd_with_dot bdd   
		           (fun i ->   
		              Constraint.to_string   
		                (Formula_to_bdd.index_to_linear_constraint i)^"\""  
		           )  
		           "debug_bdd_all"
		           false
	           );  	
	         );
	         !add_snt_entry bdd (Sol_nb.zero_sol, Sol_nb.zero_sol);
	         if vl >= 2 then  
	           (
		          print_string ("[draw] -> " ^ (formula_to_string f) ^ 
			                       "\n    is not satisfiable because of numerics.\n");
424
            
425
426
427
428

              (* 	      Bdd.print_mons bdd; *)
	           );
	         []
429
            
430
431
432
433
	     | e ->
	         print_string ((Printexc.to_string e) ^ "\n");
	         flush stdout;
	         assert false