Vous avez reçu un message "Your GitLab account has been locked ..." ? Pas d'inquiétude : lisez cet article https://docs.gricad-pages.univ-grenoble-alpes.fr/help/unlock/

solver.ml 13.4 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
(****************************************************************************)
(****************************************************************************)

(* Exported *)
Erwan Jahier's avatar
Erwan Jahier committed
55
56
57
let (is_satisfiable_bdd:
       Var.env_in -> Var.env -> int -> string -> formula -> string -> bool*Bdd.t) =
  fun input memory vl ctx_msg f msg -> 
58
    let bdd = Formula_to_bdd.f input memory ctx_msg vl f in
59
60
    let is_sat1 = not (Bdd.is_false bdd) 
    and is_sat2 =
61
      (* the formula may be false because of numerics. In that case,
Erwan Jahier's avatar
Erwan Jahier committed
62
	      the solution number is set to (0,0) (if a draw has been tried).
63
      *)
64
      (
Erwan Jahier's avatar
Erwan Jahier committed
65
66
67
68
69
70
71
72
73
74
	     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
75
      )
76
    in
77
      if vl > 2 then
Erwan Jahier's avatar
Erwan Jahier committed
78
79
80
81
82
83
84
85
86
87
	     (
	       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
	     );
88
89
90
91
92
93
      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)
94

95
(****************************************************************************)
96

97
(****************************************************************************)
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
(* 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
118
	    hfind Bddd.bdd_to_int  bdd
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
	  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)


Erwan Jahier's avatar
Erwan Jahier committed
157
158
159
160
161
162
163
164
let index_to_vn i = (
  try
    Constraint.to_string (Formula_to_bdd.index_to_linear_constraint i)^"\""
    with _ -> "\""
)
  
let (print_bdd_with_dot: Bdd.t -> string -> bool -> unit) =
  fun bdd label only_true ->
165
166
    let arcs = bdd_to_graph bdd (index_to_vn) only_true in
    let dot_file = label ^ ".dot" in
Erwan Jahier's avatar
Erwan Jahier committed
167
    let pdf = label ^ ".pdf" in
168
169
170
171
172
173
174
175
176
177
178
    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
Erwan Jahier's avatar
Erwan Jahier committed
179
180
181
182
183
184
    (*  Calling dot to create the postscript file *)
    let cmd = ("dot -Tpdf " ^ dot_file ^ " -o " ^ pdf) in
    let exit_code_dot = Sys.command cmd in
    if (exit_code_dot <> 0)
    then Printf.printf "The sys call '%s' failed (exit code %i)\n\n" cmd exit_code_dot
    else (Printf.printf "%s generated (with '%s')" pdf cmd)
185

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
(* Exported *)
351
let (solve_formula: Var.env_in -> Var.env -> int -> string -> Var.name list list ->
Erwan Jahier's avatar
Erwan Jahier committed
352
353
354
355
     Thickness.formula_draw_nb ->  Thickness.numeric -> formula -> var list ->
     formula -> (Var.env * Var.env) list) =
  fun input memory vl ctx_msg output_var_names p num_thickness bool_vars_to_gen_f
    num_vars_to_gen f ->
356

357
    let bdd = (Formula_to_bdd.f input memory ctx_msg vl f) in
358
359
    let _ = 
      assert (not (Bdd.is_false bdd));
360
      if vl >= 2 then
361
362
363
364
365
366
367
        (
	       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
        )
368
    in
369

370
    let comb0 = (Formula_to_bdd.f input memory ctx_msg vl bool_vars_to_gen_f) in
371
    let comb =
372
      (* All Boolean vars should appear in the comb so that when we
373
374
375
376
377
378
379
380
	      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.
381
      *)
382
      Bdd.dand (Bdd.support bdd) comb0
383
    in	
384
    let bool_vars_to_gen = Exp.support bool_vars_to_gen_f in
385
      try
386
387
388
389
	     let res =
	       (flatten
	          (Util.unfold
		          (draw input memory vl ctx_msg output_var_names num_thickness
390
                   bool_vars_to_gen num_vars_to_gen comb)
391
392
393
394
395
396
		          bdd
		          p
	          )
	       )
	     in
	       res
397
      with
398
399
	       No_numeric_solution ->
	         if vl >= 3 then (
Erwan Jahier's avatar
Erwan Jahier committed
400
401
	           (print_bdd_with_dot bdd "debug_bdd" true);  	
	           (print_bdd_with_dot bdd "debug_bdd_all" false);  	
402
403
404
405
406
407
	         );
	         !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");
408
            
409
410
411
412

              (* 	      Bdd.print_mons bdd; *)
	           );
	         []
413
            
414
415
416
417
	     | e ->
	         print_string ((Printexc.to_string e) ^ "\n");
	         flush stdout;
	         assert false