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 29 KB
Newer Older
1
(*-----------------------------------------------------------------------
2
 ** Copyright (C) 2001, 2002 - Verimag.
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
*)

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

20

21
22
(****************************************************************************)
	  
23
let (lookup: env_in -> subst list -> var_name -> Value.t option) = 
24
25
  fun input pre vn ->  
    try Some(Hashtbl.find input vn)
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
    with 
	Not_found -> 
	  ( try Some(List.assoc vn pre)
	    with 
		Not_found -> 
		  if 
		    Prevar.is_pre_var vn 
		  then 
		    (
		      let cnl = List.flatten (Env_state.current_nodes ()) in
		      let nodes_str = String.concat " " (List.map (string_of_int) cnl) in
		      let node_msg = 
			if 
			  (List.length cnl) = 1
			then
			  ("(current node is " ^ nodes_str ^ ").\n")
			else
			  ("(current nodes are " ^ nodes_str ^ ").\n")
		      in
			print_string ("*** The expression " ^ (Prevar.format vn) ^ 
				      " is undefined at current step " ^ node_msg 
				      ^ "*** You need to rewrite your environment"
				      ^ " spec in such a way that no pre is used"
				      ^ " for that variable at that step. \n"
				    ^ " ");
		      flush stdout;
		      exit 2
		    )
		  else
		    None 
56
57
58
59
	      | e ->
		  print_string ((Printexc.to_string e) ^ "\n");
		  flush stdout;
		  assert false
60
	  )
61
62
63
64
65
      | e ->
	  print_string ((Printexc.to_string e) ^ "\n");
	  flush stdout;
	  assert false

66
67
68

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

69
type comp = SupZero | SupEqZero | EqZero 
70
71
72

let rec (formula_to_bdd : env_in -> formula -> Bdd.t * bool) =
  fun input f ->
73
74
    (** Returns the bdd of [f] where input and pre variables
      have been repaced by their values.
75

76
77
78
      Also returns a flag that is true iff the formula depends on
      input and pre vars. If this flag is false, the formula is
      stored (cached) in a global table ([env_state.bdd_tbl_global]);
79
      otherwise, it is stored in a table that is cleared at each new
80
      step ([env_state.bdd_tbl]).  
81
    *)
82
    try (Env_state.bdd f, true)
83
    with Not_found -> 
84
      try (Env_state.bdd_global f, false)
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
      with Not_found -> 
	let (bdd, dep) =
	  match f with 
	      Not(f1) ->
		let (bdd_not, dep) =  (formula_to_bdd input f1) in
		  (Bdd.dnot bdd_not, dep)

	    | Or(f1, f2) ->
		let (bdd1, dep1) = (formula_to_bdd input f1)
		and (bdd2, dep2) = (formula_to_bdd input f2)
		in
		  (Bdd.dor bdd1 bdd2, dep1 || dep2)

	    | And(f1, f2) -> 
		let (bdd1, dep1) = (formula_to_bdd input f1)
		and (bdd2, dep2) = (formula_to_bdd input f2)
		in
		  (Bdd.dand bdd1 bdd2, dep1 || dep2)
103
104
105
106
107
108

	    | EqB(f1, f2) -> 
		let (bdd1, dep1) = (formula_to_bdd input f1)
		and (bdd2, dep2) = (formula_to_bdd input f2)
		in
		  (Bdd.eq bdd1 bdd2, dep1 || dep2)
109
110
111
112
113
114
115
116
117
118

	    | IteB(f1, f2, f3) -> 
		let (bdd1, dep1) = (formula_to_bdd input f1)
		and (bdd2, dep2) = (formula_to_bdd input f2)
		and (bdd3, dep3) = (formula_to_bdd input f3) 
		in
		  ((Bdd.dor (Bdd.dand bdd1 bdd2) 
		      (Bdd.dand (Bdd.dnot bdd1) bdd3)),
		   dep1 || dep2 || dep3 )
		  
119
120
	    | True ->  (Bdd.dtrue  (Env_state.bdd_manager ()), false)
	    | False -> (Bdd.dfalse (Env_state.bdd_manager ()), false)
121
	    | Bvar(vn) ->    
122
		( match (lookup input (Env_state.pre ()) vn) with 
123
		      Some(B(bool)) -> 
124
			if bool
125
			then (Bdd.dtrue  (Env_state.bdd_manager ()), true)
126
			else (Bdd.dfalse (Env_state.bdd_manager ()), true)
127
128
129
130
		    | Some(_) -> 
			print_string (vn ^ " is not a boolean!\n");
			assert false
		    | None ->
131
			if List.mem vn (Env_state.pre_var_names ())
132
133
134
135
136
137
			then failwith 
			  ("*** " ^ vn ^ " is unknown at this stage.\n "
			   ^ "*** Make sure you have not used "
			   ^ "a pre on a output var at the 1st step, \n "
			   ^ "*** or a pre on a input var at the second step in "
			   ^ "your formula in the environment.\n ")
138
			else (Bdd.ithvar (Env_state.bdd_manager ())
139
				(Env_state.linear_constraint_to_index (Bv(vn)) false), 
140
				false)
141
		)
142
  		
143
	    | Eq(e1, e2) -> 
144
145
		let gne = expr_to_gne (Diff(e1, e2)) input in 
		  (gne_to_bdd gne EqZero)
146
147
		  
	    | SupEq(e1, e2) ->
148
149
		let gne = expr_to_gne (Diff(e1, e2)) input in
		  (gne_to_bdd gne SupEqZero)
150
151
		  
	    | Sup(e1, e2)   ->
152
153
		let gne = expr_to_gne (Diff(e1, e2)) input in
		  (gne_to_bdd gne SupZero)
154
155
		  
	    | InfEq(e1, e2) ->  
156
157
		let gne = expr_to_gne (Diff(e2, e1)) input in
		  (gne_to_bdd gne SupEqZero)
158
159
		  
	    | Inf(e1, e2)   ->  
160
161
		let gne =  expr_to_gne (Diff(e2, e1)) input in
		  (gne_to_bdd gne SupZero)
162
163
164
165
		  
	in
	  if dep
	  then 
166
	    ( Env_state.set_bdd f bdd;	
167
168
	      match f with 
		  Not(nf) -> () (* Already in the tbl thanks to the rec call *)
169
		| _  -> Env_state.set_bdd (Not(f)) (Bdd.dnot bdd) 
170
	    )
171
172
	  else 
	    (* [f] does not depend on pre nor input vars *)
173
	    ( Env_state.set_bdd_global f bdd ;	
174
175
176
	      match f with 
		  Not(nf) -> () (* Already in the table thanks to the rec call *)
		| _  -> 
177
		    Env_state.set_bdd_global (Not(f)) (Bdd.dnot bdd)
178
179
180
181
	    );

	  (bdd, dep)
and
182
  (expr_to_gne: expr -> env_in -> Gne.t) =
183
184
185
186
  fun e input -> 
    (** Evaluates pre and input vars appearing in [e] and tranlates
      it into a so-called garded normal form. Also returns a flag
      that is true iff [e] depends on pre or input vars. *)
187
    let gne =
188
189
      match e with  
	  Sum(e1, e2) ->
190
191
	    let gne1 = (expr_to_gne e1 input)
	    and gne2 = (expr_to_gne e2 input) 
192
	    in
193
	      Gne.add  gne1 gne2
194
195

	| Diff(e1, e2) -> 
196
197
	    let gne1 = (expr_to_gne e1 input)
	    and gne2 = (expr_to_gne e2 input) 
198
	    in
199
	      Gne.diff gne1 gne2
200
201

	| Prod(e1, e2) -> 
202
203
	    let gne1 = (expr_to_gne e1 input)
	    and gne2 = (expr_to_gne e2 input) 
204
	    in
205
	      Gne.mult gne1 gne2
206
207

	| Quot(e1, e2) -> 
208
209
	    let gne1 = (expr_to_gne e1 input)
	    and gne2 = (expr_to_gne e2 input) 
210
	    in
211
	      Gne.quot gne1 gne2
212
213

	| Mod(e1, e2)  -> 
214
215
	    let gne1 = (expr_to_gne e1 input)
	    and gne2 = (expr_to_gne e2 input) 
216
	    in
217
	      Gne.modulo gne1 gne2
218
219

	| Ivar(str) ->
220
	    ( match (lookup input (Env_state.pre ()) str) with 
221
		  Some(N(I(i))) ->
222
223
224
225
		    (Gne.make 
		       (Ne.make "" (I i)) 
		       (Bdd.dtrue (Env_state.bdd_manager ()))
		       true
226
227
		    )
		| None ->
228
229
230
231
		    (Gne.make 
		       (Ne.make str (I(1)))
		       (Bdd.dtrue (Env_state.bdd_manager ()))
		       false
232
		    )
233
234
235
236
237
238
239
240
241
242
243
		| Some(N(F(f))) -> 
		    print_string ((string_of_float f) 
				  ^ "is a float, but an int is expected.\n");
		    assert false
		| Some(B(f)) -> 
		    print_string ((string_of_bool f) 
				  ^ "is a bool, but an int is expected.\n");
		    assert false
	    )

	| Fvar(str) ->
244
	    ( match (lookup input (Env_state.pre ()) str) with 
245
		  Some(N(F(f))) ->
246
247
248
249
		    ( Gne.make 
			(Ne.make "" (F(f))) 
			(Bdd.dtrue (Env_state.bdd_manager ()))
			true
250
251
		    )
		| None ->
252
253
254
255
		    ( Gne.make 
			(Ne.make str (F(1.))) 
			(Bdd.dtrue (Env_state.bdd_manager ()))
			false
256
257
258
259
260
261
262
263
264
265
266
267
		    )
		| Some(N(I(i))) -> 
		    print_string ((string_of_int i) 
				  ^ "is an int, but a float is expected.\n");
		    assert false
		| Some(B(f)) -> 
		    print_string ((string_of_bool f) 
				  ^ "is a bool, not a float is expected.\n");
		    assert false
	    )

	| Ival(i) ->  
268
269
270
271
	    (Gne.make 
	       (Ne.make "" (I(i))) 
	       (Bdd.dtrue (Env_state.bdd_manager ()))
	       false
272
273
274
	    )

	| Fval(f) -> 
275
276
277
278
	    ( Gne.make 
		(Ne.make "" (F(f))) 
		(Bdd.dtrue (Env_state.bdd_manager ()))
		false
279
280
281
	    )

	| Ite(f, e1, e2) -> 
282
283
	    let (add_formula_to_gne_acc : Bdd.t -> bool -> Ne.t -> 
		   Bdd.t * bool -> Gne.t -> Gne.t) = 
284
	      fun bdd dep1 nexpr (c, dep2) acc -> 
285
		(* Used (by a Gne.fold) to add the condition [c] to every
286
287
		   condition of a garded expression. *)
		let _ = assert (
288
289
		  try
 		    let _ = Gne.find nexpr acc in
290
291
292
293
294
295
296
		      false
		  with Not_found -> true
		) 
		in
		let new_bdd = (Bdd.dand bdd c) in
		  if Bdd.is_false new_bdd
		  then acc
297
		  else Gne.add_ne nexpr new_bdd (dep1 || dep2) acc
298
	    in
299
	    let (bdd, depf) = formula_to_bdd input f in
300
	    let bdd_not = Bdd.dnot bdd
301
302
	    and gne_t = (expr_to_gne e1 input)
	    and gne_e = (expr_to_gne e2 input) in
303
304
305
306
	    let gne1 = 
	      Gne.fold (add_formula_to_gne_acc bdd depf) gne_t (Gne.empty ())
	    in
	    let gne  = Gne.fold (add_formula_to_gne_acc bdd_not depf) gne_e gne1 in
307
	      gne
308
    in
309
      gne
310
	
311
and
312
  (gne_to_bdd : Gne.t -> comp -> Bdd.t * bool) =
313
314
  fun gne cmp -> 
    (** Use [cmp] to compare [gne] with 0 and returns the
315
316
317
318
      corresponding formula.  E.g., if [gne] is bounded to
      [e1 -> c1; e2 -> c2], then [gne_to_bdd gne SupZero] returns
      (the bdd corresponding to) the formula [(c1 and (e1 > 0)) or
      (c2 and (e2 > 0))] *)
319
320
    match cmp with
	SupZero ->
321
	  ( Gne.fold 
322
323
324
	      (fun nexpr (c, dep) (acc, dep_acc) -> 
		 let new_dep = dep || dep_acc 
		 and bdd = 
325
326
		   if 
		     Ne.is_a_constant nexpr
327
		   then 
328
		     let cst = Ne.find "" nexpr in
329
		       match cst with
330
			   Some I(i) -> 
331
			     if i > 0 
332
333
			     then (Bdd.dtrue (Env_state.bdd_manager ()))
			     else (Bdd.dfalse (Env_state.bdd_manager ()))
334
			 | Some F(f) -> 
335
			     if f > 0. 
336
337
			     then (Bdd.dtrue (Env_state.bdd_manager ()))
			     else (Bdd.dfalse (Env_state.bdd_manager ()))
338
339
			 | None -> 
			     (Bdd.dfalse (Env_state.bdd_manager ()))
340
341
		   else 
		     Bdd.ithvar 
342
		       (Env_state.bdd_manager ()) 
343
		       (Env_state.linear_constraint_to_index (Ineq(GZ(nexpr))) dep) 
344
		 in
345
		   (Bdd.dor (Bdd.dand c bdd) acc, new_dep)
346
347
	      )
	      gne 
348
	      ((Bdd.dfalse (Env_state.bdd_manager ())), false)
349
350
	  )
      | SupEqZero ->
351
	  ( Gne.fold 
352
353
354
	      (fun nexpr (c, dep) (acc, dep_acc) -> 
		 let new_dep = dep || dep_acc 
		 and bdd = 
355
		   if Ne.is_a_constant nexpr
356
		   then 
357
		     let cst = Ne.find "" nexpr in
358
		       match cst with
359
			   Some I(i) -> 
360
			     if i >= 0 
361
362
			     then (Bdd.dtrue (Env_state.bdd_manager ()))
			     else (Bdd.dfalse (Env_state.bdd_manager ()))
363
			 | Some F(f) -> 
364
			     if f >= 0. 
365
366
			     then (Bdd.dtrue (Env_state.bdd_manager ()))
			     else (Bdd.dfalse (Env_state.bdd_manager ()))
367
368
			 | None -> 
			     (Bdd.dtrue (Env_state.bdd_manager ()))
369
370
371

		   else 
		     Bdd.ithvar 
372
		       (Env_state.bdd_manager ()) 
373
		       (Env_state.linear_constraint_to_index (Ineq(GeqZ(nexpr))) dep)
374
		 in
375
		   (Bdd.dor (Bdd.dand c bdd) acc, new_dep)
376
377
	      )
	      gne 
378
	      ((Bdd.dfalse (Env_state.bdd_manager ())), false)
379
380
	  )
      | EqZero -> 
381
	  ( Gne.fold 
382
	      (fun nexpr (c, dep) (acc, dep_acc) -> 
383
384
		 let new_dep = dep || dep_acc 
		 and bdd = 
385
		   if Ne.is_a_constant nexpr
386
		   then 
387
		     let cst = Ne.find "" nexpr in
388
		       match cst with
389
			   Some I(i) -> 
390
			     if i = 0 
391
392
			     then (Bdd.dtrue (Env_state.bdd_manager ()))
			     else (Bdd.dfalse (Env_state.bdd_manager ()))
393
			 | Some F(f) -> 
394
			     if f = 0. 
395
396
			     then (Bdd.dtrue (Env_state.bdd_manager ()))
			     else (Bdd.dfalse (Env_state.bdd_manager ()))
397
398
			 | None -> 
			     (Bdd.dtrue (Env_state.bdd_manager ()))
399
400
401

		   else 
		     Bdd.ithvar 
402
		       (Env_state.bdd_manager ()) 
403
		       (Env_state.linear_constraint_to_index (EqZ(nexpr)) dep)
404
		 in
405
		   (Bdd.dor (Bdd.dand c bdd) acc, new_dep)
406
407
	      )
	      gne 
408
	      ((Bdd.dfalse (Env_state.bdd_manager ())), false)
409
	  )
410

411
412
413
414
415
(****************************************************************************)
(****************************************************************************)


(* Exported *)
416
417
let rec (is_satisfiable: env_in -> formula -> bool) = 
  fun input f -> 
418

419
    let (bdd, _) = formula_to_bdd input f in
420
    let is_sat = 
421
422
423
      not (Bdd.is_false bdd) &&
      ( 
	try 
424
	  let (n, m) = Env_state.sol_number bdd in 
425
	    not ((zero_sol, zero_sol) = (n, m))
426
427
	with 
	    Not_found -> true
428
429
430
431
	  | e ->
	      print_string ((Printexc.to_string e) ^ "\n");
	      flush stdout;
	      assert false
432
      )
433
434
435
436
437
438
439
440
441
442
443
444
    in
(*       if Env_state.verbose () then *)
(* 	( *)
(* 	  print_string "\n => "; *)
(* 	  print_string (formula_to_string f);  *)
(* 	  if is_sat  *)
(* 	  then print_string "\n   is satisfiable...\n" *)
(* 	  else print_string "\n   is not satisfiable...\n"; *)
(* 	  flush stdout *)
(* 	); *)
	
      is_sat
445
446
447
448
      


(****************************************************************************)
449
450
451
452
453
454
455
456
457
(****************************************************************************)


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


458
type var = int
459
460
461
462
463

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
464
465
466
467
468
469
      the solution number table for [bdd] and its negation, 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].  
470
    *)
471
472
473
    let _ = assert (not (Bdd.is_cst bdd) 
		    && (Bdd.topvar comb) = (Bdd.topvar bdd)) 
    in
474
475
476
    let bdd_not = (Bdd.dnot bdd) in
    let (sol_nb, sol_nb_not) =
      try
477
478
	let (nt, ne) = Env_state.sol_number bdd 
	and (not_nt, not_ne) = Env_state.sol_number bdd_not in
479
480
	  (* solutions numbers in the table are absolute *)
	  ((add_sol_nb nt ne), (add_sol_nb not_nt not_ne))
481
      with Not_found ->
482
483
	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
484
485
	  Env_state.set_sol_number bdd (nt, ne) ;
	  Env_state.set_sol_number bdd_not (not_nt, not_ne) ;
486
487
488
489
490
491
	  ((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 -> 
492
    (* Returns the absolute number of solutions of [sub_bdd] (and its
493
       negation) w.r.t. [comb], where [comb] is the comb of the
494
495
496
497
498
499
500
501
502
503
       father of [sub_bdd].

       The [comb] is used to know which output boolean variables are
       unconstraint along a path in the bdd. Indeed, the comb is made
       of all the boolean output var indexes plus the num contraints
       indexes that appears in the bdd; hence, if the topvar of the
       bdd is different from the topvar of the comb, it means that
       the topvar of the comb is unsconstraint and we need to
       multiply the number of solution of the branch by 2.
    *)
504
    if Bdd.is_cst sub_bdd 
505
    then
506
      let sol_nb = 
507
	if Bdd.is_true comb
508
	then one_sol
509
	else (two_power_of (List.length (Bdd.list_of_support (Bdd.dthen comb)))) 
510
      in
511
512
513
514
515
	if Bdd.is_true sub_bdd
	then (sol_nb, zero_sol) 
	else (zero_sol, sol_nb)
    else 
      let topvar = Bdd.topvar sub_bdd in
516
517
518
519
520
521
522
523
524
525
526
527
      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
	     whch 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)
      in
528
      let (sub_comb, missing_vars_nb) = 
529
	count_missing_vars (Bdd.dthen comb) topvar 0
530
531
532
533
534
      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)
	
535

536

537
538
539
(****************************************************************************)
(****************************************************************************)

540

541
542
543
544
545
546
547
548
549
550
let (toss_up_one_var: var_name -> subst) =
  fun var -> 
   (* *)
    let ran = Random.float 1. in
      if (ran < 0.5) 
      then (var, B(true)) 
      else (var, B(false))


let (toss_up_one_var_index: var -> subst option) =
551
  fun var -> 
552
553
554
555
556
557
558
559
560
    (* if [var] is a index that corresponds to a boolean variable,
       this fonction performs a toss and returns a substitution for
       the corresponding boolean variable. It returns [None]
       otherwise.

       Indeed, if it happens that a numerical constraint does not
       appear along a path, we simply ignore it and hence it will not
       be added to the store.
    *)
561
562
563
    let cstr = Env_state.index_to_linear_constraint var in
      match cstr with 
          Bv(vn) -> Some(toss_up_one_var vn)
564
	| _  -> None
565

566

567
568
let rec (draw_in_bdd: subst list * Store.t -> Bdd.t -> Bdd.t -> 
	   subst list * Store.t * Store.t) = 
569
570
571
572
573
574
  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.
575

576
577
578
      Raises the [No_numeric_solution] exception whenever no valid
      path in [bdd] leads to a satisfiable set of numeric
      constraints.  
579
    *)
580
581
    if 
      Bdd.is_true bdd
582
583
    then
      (* Toss the remaining bool vars. *)
584
585
586
587
588
589
590
591
592
      let (store_int, store_poly) = switch_to_polyhedron_representation store in
	( 
	  (List.append sl
	     (Util.list_map_option 
		toss_up_one_var_index 
		(Bdd.list_of_support comb)) ),
	  store_int,
	  store_poly
	)
593
594
595
    else
      let _ = assert (not (Bdd.is_false bdd)) in 
      let _ = assert (Env_state.sol_number_exists bdd) in
596
      let bddvar = Bdd.topvar bdd in
597
598
      let cstr = (Env_state.index_to_linear_constraint bddvar) in 
	match cstr with
599
	    Bv(var) -> 
600
	      draw_in_bdd_bool var (sl, store) bdd comb
601
602
	  | EqZ(e) -> 
	      draw_in_bdd_eq e (sl, store) bdd comb
603
	  |  Ineq(ineq) ->
604
	      draw_in_bdd_ineq ineq (sl, store) bdd comb
605

606

607
608
and (draw_in_bdd_bool: string -> subst list * Store.t -> Bdd.t -> Bdd.t -> 
       subst list * Store.t * Store.t) = 
609
  fun var (sl, store) bdd comb ->
610
    let bddvar = Bdd.topvar bdd in
611
612
613
614
615
616
617
    let topvar_comb  = Bdd.topvar comb in
      
    if
      bddvar <> topvar_comb 
    then
      (* that condition means that topvar_comb is an unconstraint
	 boolean var; hence we toss it up. *)
618
619
620
621
622
      let new_sl = 
	match toss_up_one_var_index topvar_comb with
	    Some(s) -> s::sl
	  | None -> sl
      in
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
	draw_in_bdd (new_sl, store) bdd (Bdd.dthen comb) 
    else 
      (* bddvar = combvar *) 
      let (n, m) = Env_state.sol_number bdd in
      let _ =
	if ((eq_sol_nb n zero_sol) && (eq_sol_nb m zero_sol))
	then raise No_numeric_solution ;
      in
      let (
	bdd1, bool1, sol_nb1,
	bdd2, bool2, sol_nb2
      ) =
	let ran = Random.float 1. 
	and sol_nb_ratio = 
	  ((float_of_sol_nb n) /. (float_of_sol_nb (add_sol_nb n m))) 
	in
	  if 
	    ran < sol_nb_ratio
	      (* 
		 Depending on the result of a toss (based on the number
		 of solution in each branch), we try the [then] or the
		 [else] branch first.  
	      *)
	  then
	    ((Bdd.dthen bdd), true, n,
	     (Bdd.delse bdd), false, m )
	  else 
	    ((Bdd.delse bdd), false, m,
	     (Bdd.dthen bdd), true, n )
      in
      let (sl1, sl2, new_comb) = (
	((var, B(bool1))::sl), 
	((var, B(bool2))::sl),
	(if Bdd.is_true comb then comb else Bdd.dthen comb) 
657
      )	    
658
659
660
661
662
663
664
665
666
      in
	(* 
	   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]. 
	*)
	try 
	  draw_in_bdd (sl1, store) bdd1 new_comb
667
	with
668
669
670
	    No_numeric_solution ->
	      if Env_state.verbose () then
		print_string "\n..................BACKTRACK!\n";
671
672
673
674
675
676
677
678
	      if not (eq_sol_nb sol_nb2 zero_sol)
	      then draw_in_bdd (sl2, store) bdd2 new_comb
		(* 
		   The second branch is now tried because no path in
		   the first bdd leaded to a satisfiable set of
		   numeric constraints. 
		*) 
	      else raise No_numeric_solution
679
680
681
682
	  | e ->
	      print_string ((Printexc.to_string e) ^ "\n");
	      flush stdout;
	      assert false
683
      
684
685
and (draw_in_bdd_ineq: Constraint.ineq -> subst list * Store.t -> Bdd.t -> Bdd.t -> 
	   subst list * Store.t * Store.t) = 
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
  fun cstr (sl, store) bdd comb ->
    (* 
       When we add to the store an inequality constraint GZ(ne) or
       GeqZ(ne) ([split_store]), 2 stores are returned. The first is a
       store where the inequality has been added; the second is a
       store where its negation has been added.
       
       Whether we choose the first one or the second depends on a toss
       made according the (boolean) solution number in both branches
       of the bdd. If no solution is found into that branch, the other
       branch with the other store is tried.
    *)
    let (n, m) = Env_state.sol_number bdd in
    let _ =
      if ((eq_sol_nb n zero_sol) && (eq_sol_nb m zero_sol))
      then raise No_numeric_solution ;
    in
703
704
705
    let ran = Random.float 1. in
    let cstr_neg = Constraint.neg_ineq cstr in
    let (cstr1, bdd1, sol_nb1, cstr2, bdd2, sol_nb2) =
706
      if 
707
	ran < ((float_of_sol_nb n) /. (float_of_sol_nb (add_sol_nb n m)))
708
      then
709
710
711
	(cstr, (Bdd.dthen bdd), n, cstr_neg, (Bdd.delse bdd), m)
      else 
	(cstr_neg, (Bdd.delse bdd), m, cstr, (Bdd.dthen bdd), n)
712
    in
713
    let store_copy = Store.copy store in
714
    let store1 = add_constraint store (Ineq cstr1) in
715
716
717
718
      (* 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]. *)
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
      
      try
	if not (is_store_satisfiable store1) then raise No_numeric_solution;
	draw_in_bdd (sl, store1) bdd1 comb 
      with 
	  No_numeric_solution -> 
	    let store2 = add_constraint store_copy (Ineq cstr2) in
	      (* 
		 The second branch is tried if no path in the first
		 bdd leaded to a satisfiable set of numeric
		 constraints.  
	      *)
	      if 
		(not (eq_sol_nb sol_nb2 zero_sol)) 
		&& is_store_satisfiable store2
	      then
		draw_in_bdd (sl, store2) bdd2 comb
	      else
		raise No_numeric_solution
	| e ->
	    print_string ((Printexc.to_string e) ^ "\n");
	    flush stdout;
	    assert false
742

743
744
and (draw_in_bdd_eq: Ne.t -> subst list * Store.t -> Bdd.t -> Bdd.t -> 
       subst list * Store.t * Store.t) = 
745
  fun ne (sl, store) bdd comb ->
746
    (*
747
748
749
750
751
752
753
754
      We consider 3 stores: 
        - store + [ne = 0]
        - store + [ne > 0]
        - store + [ne < 0]
      
      Whether we choose the first one or not depends on toss made
      according the (boolean) solution number in both branches of the
      bdd. If the else branch is choosen (if it is chosen in the
755
756
757
758
      first place, or if backtracking occurs because no solutions is
      found in the then branch) whether we try the second or the
      third store first is (fairly) tossed up.
    *)
759
760
761
762
763
    let (n, m) = Env_state.sol_number bdd in
    let _ =
      if ((eq_sol_nb n zero_sol) && (eq_sol_nb m zero_sol))
      then raise No_numeric_solution ;
    in
764
765
766
767
768
    let ran0 = Random.float 1. 
    and ran  = Random.float 1. 
    and cstr = (EqZ ne)
    and not_cstr = (Ineq (GZ ne))
    and not_cstr2 = (Ineq (GZ (Ne.neg_nexpr ne)))
769
    and store_copy = Store.copy store 
770
    in
771
772
773
774
775
    let (
      cstr1, bdd1, sol_nb1, 
      cstr2, bdd2, sol_nb2,
      cstr3, bdd3, sol_nb3) =
      let sol_nb_ratio = 
776
777
778
779
780
781
782
783
784
	((float_of_sol_nb n) /. (float_of_sol_nb (add_sol_nb n m))) 
      in
	if 
	  ran0 < 0.5
	    (* 
	       When taking the negation of an equality, we can
	       either try > or <. Here, We toss which one we
	       will try first.  
	    *)
785
	then
786
787
	  if 
	    ran < sol_nb_ratio
788
	      (*
789
790
791
		Depending on the result of a toss (based on the number
		of solution in each branch), we try the [then] or the
		[else] branch first.  
792
793
	      *)
	  then
794
795
796
	    (cstr,                (Bdd.dthen bdd), n,
	     not_cstr,  (Bdd.delse bdd), m,
	     not_cstr2, (Bdd.delse bdd), m)
797
	  else 
798
799
800
	    (not_cstr,  (Bdd.delse bdd), m,
	     cstr,                (Bdd.dthen bdd), n,
	     not_cstr2, (Bdd.delse bdd), m)
801
802
803
804
805
	else
	  if
	    ran < sol_nb_ratio
	      (* Ditto *)
	  then
806
807
808
	    (cstr, (Bdd.dthen bdd), n,
	     not_cstr2, (Bdd.delse bdd), m,
	     not_cstr,  (Bdd.delse bdd), m)
809
	  else 
810
811
812
	    (not_cstr2, (Bdd.delse bdd), m,
	     cstr,                (Bdd.dthen bdd), n,
	     not_cstr,  (Bdd.delse bdd), m)
813
    in    
814
    let store1 = add_constraint store cstr1 in
815
816
817
818
819
      (* 
	 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. 
      *)
820
821
822
823
824
      try
	if not (is_store_satisfiable store1) then raise No_numeric_solution;
	draw_in_bdd (sl, store1) bdd1 comb
      with 
	  No_numeric_solution -> 
825
	    let store_copy2 = Store.copy store_copy in
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
	    (* 
	       The second branch is tried if no path in the first bdd
	       leaded to a satisfiable set of numeric constraints. 
	    *)
	    let store2 = add_constraint store_copy cstr2 in
	      try
		if 
		  not (is_store_satisfiable store2) 
		  || (eq_sol_nb sol_nb2 zero_sol) 
		then 
		  raise No_numeric_solution;
		draw_in_bdd (sl, store2) bdd2 comb
	      with 
		  No_numeric_solution -> 
		    let store3 = add_constraint store_copy2 cstr3 in
		      if 
			not (is_store_satisfiable store3) 
			|| (eq_sol_nb sol_nb2 zero_sol) 
		      then 
			raise No_numeric_solution;
		      draw_in_bdd (sl, store3) bdd3 comb
		| e -> 
		    print_string ((Printexc.to_string e) ^ "\n");
		    flush stdout;
		    assert false
851
	      
852

853
(****************************************************************************)
854

855
856
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 ->
857
    
858
    (** Draw the output and local vars to be generated by the environnent. *)
859
    let (bool_subst_l, store_range, store_poly) = 
860
       draw_in_bdd ([], (new_store num_vnt_to_gen)) bdd comb
861
    in
862
    let num_subst_l0 = 
863
864
865
866
867
      if 
	num_vnt_to_gen = []
      then
	[]
      else
868
	  match Env_state.draw_mode () with
869
870
871
872
873
874
875
876
877
878
879
	    | Env_state.Edges ->
		let sl = draw_edges store_poly [] in
		  draw_edges store_range sl
	    | Env_state.Inside ->
		let sl = draw_inside store_poly [] in
		  draw_inside store_range sl
    in
    let num_subst_l = 
      List.map 
	(fun (vn, num) -> (vn, N num)) 
	num_subst_l0
880
    in
881
    let subst_l = append bool_subst_l num_subst_l in
882
    let (out_vars, _) = List.split (Env_state.output_var_names ()) 
883
884
885
    in
      assert ( 
	(*  Checks that we generated all variables. *)
886
887
	let (gen_vars, _) = List.split subst_l in
	let (num_vars_to_gen, _) = List.split num_vnt_to_gen in
888
	let vars_to_gen = append bool_vars_to_gen num_vars_to_gen in
889
890
891
892
893
894
895
896
          if (sort (compare) gen_vars) = (sort (compare) vars_to_gen) 
	  then true
	  else
	    (
	      output_string stderr " \ngen vars :";
              List.iter (fun vn -> output_string stderr (vn ^ " ")) gen_vars;
	      output_string stderr " \nvar to gen:";
	      List.iter (fun vn -> output_string stderr (vn ^ " ")) vars_to_gen;
897
	      output_string stderr " \n";
898
899
	      false
	    )
900
901
902
903
904
      );
      (* Splits output and local vars. *)
      List.partition 
	(fun (vn, _) -> List.mem vn out_vars) 
	subst_l
905

906

907
908
909
910
911

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


912
(* Exported *)
913
914
let (solve_formula: env_in -> int -> formula -> formula -> vnt list ->
       (subst list * subst list) list option) =
915
916
917
918
  fun input p f bool_vars_to_gen_f num_vars_to_gen  ->
    
    let _ = if Env_state.verbose () then
      (
919
	print_string "\n --> ";
920
	print_string (formula_to_string f); 
921
	print_string "\n   has been elected to be the formula in which solutions are drawn.\n";
922
923
	flush stdout
      )
924
    in
925

926
    let bdd = 
927
      (* The bdd of f has necessarily been computed (by is_satisfiable) *)
928
      try Env_state.bdd f
929
930
931
932
933
934
935
      with 
	  Not_found -> Env_state.bdd_global f
	| e ->
	    print_string ((Printexc.to_string e) ^ "\n");
	    flush stdout;
	    assert false

936

937
    in
938
939
940
941
942
943
944
945
946
947
948
949
950
    let (comb0, _) = formula_to_bdd input bool_vars_to_gen_f in
    let comb = 
      (* All boolean vars should appear in the comb so that when we
	 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.  
      *)
      Bdd.dand (Bdd.support bdd) comb0 
951
952
    in	
    let bool_vars_to_gen = Formula.support bool_vars_to_gen_f in
953
    let _ =
954
      if not (Env_state.sol_number_exists bdd)
955
      then
956
957
958
959
960
	let rec skip_unconstraint_bool_var_at_top comb v =
	  (* [build_sol_nb_table] supposes that the bdd and its comb 
	     have the same top var. 
	  *)
	  if Bdd.is_true comb then comb
961
962
	  else 
	    let topvar = (Bdd.topvar comb) in
963
964
	      if v = topvar then comb 
	      else skip_unconstraint_bool_var_at_top (Bdd.dthen comb) v
965
	in
966
	let comb2 = skip_unconstraint_bool_var_at_top comb (Bdd.topvar bdd) in 
967
968
	let _ = build_sol_nb_table bdd comb2 in
	  ()
969
    in
970
      try 	
971
	Some(Util.unfold (draw bool_vars_to_gen num_vars_to_gen comb) bdd p)
972
973
974
975
976
      with 
	  No_numeric_solution -> 
	    Env_state.set_sol_number bdd (zero_sol, zero_sol);
	    None
	| e ->
977
978
	    print_string ((Printexc.to_string e) ^ "\n");
	    flush stdout;
979
	    assert false