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/

formula_to_bdd.ml 27.6 KB
Newer Older
1
(*-----------------------------------------------------------------------
2
** Copyright (C) - Verimag.
3
** This file may only be copied under the terms of the CeCill
4
** Public License
5
6
7
**-----------------------------------------------------------------------
**
** File: formula_to_bdd.ml
8
** Main author: erwan.jahier@univ-grenoble-alpes.fr
9
10
11
*)

open Value
12
open Exp
13
open Constraint
14

15

16
let output_msg msg =
17
18
  output_string stderr msg;
  flush stderr
19
20


21
(** [lookup input pre vn] looks up the value of vn in [pre] and [input] *)
22
let rec (lookup: Var.env_in -> Var.env -> string -> int -> Exp.var -> Value.t option) =
23
  fun input memory ctx_msg vl var ->
24
25
26
    match (Var.mode var) with
      | Var.Output -> None
      | Var.Local -> None
27
      | Var.Input ->
28
29
30
31
32
33
	       ( try
	           Some(Var.get_val_env_in input (Var.name var))
	         with _ ->
              output_msg ctx_msg;
		        exit 2
	       )
34
      | Var.Pre ->
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
	       (
	         try
	           (* Some(List.assoc (Var.name var) memory) *)
	           Some(Value.OfIdent.get memory (Var.name var))
	         with
		          (* if not in memory, look at a possible init value *)
		          Not_found ->
		            match (Var.init var) with
		              | Some (Numer (Ival i)) -> Some (N (I i))
		              | Some (Numer (Fval f)) -> Some (N (F f))
		              | Some (Numer (Ivar vi)) -> lookup input memory ctx_msg vl vi
		              | Some (Numer (Fvar vf)) -> lookup input memory ctx_msg vl vf
		              | Some (Formu  True) -> Some (B true)
		              | Some (Formu  False) -> Some (B false)
		              | Some (Liste _) -> 
			               assert false (* XXX not sure ...*)
                          (* 		    | Some (Liste [Nu (Ival i)]) ->  *)
                          (* 			Some (N (I i)) *)
			                 
		              | Some _ ->
			               (* Structured expression ougth to have been
			                  flattened before *)
			               output_msg (
			                 "*** Error: the initial value of variable " 
			                 ^ (Prevar.get_root_var_name (Var.name var)) ^
			                   "  is not valid.\n");
			               exit 2
		              | None ->
			               output_msg (
			                 "*** The expression " ^ (Prevar.format (Var.name var))
			                 ^ " is undefined at current step " ^ ctx_msg
			                 ^ "*** You need to rewrite your environment"
			                 ^ " spec in such a way that no pre is used"
			                 ^ " for that variable at that step\n    "
			                 ^ " or to give it an initial value.\n"^ ctx_msg);
			               exit 2
	       )
72
73


74
75
76
77
(****************************************************************************)
(****************************************************************************)

(* Transforming a formula into a bdd is expensive; this is why we
78
   store the result of this transformation in (internal) tables.
79
80
81
82
83

   Moreover, formula that does not depend on pre nor input vars are
   stored in a different table that is not cleared at each new step
   (cf [bdd_global] and [set_bdd_global] versus [bdd] and [set_bdd]).
    Ditto for the linear_constraint <-> bdd index tables.
84
85

   The reason for that is that, formula that depends on pre or input
86
   are not likely to appear twice if they contains numeric values.
87
   For Boolean, well, I could leave them in the global table.
88
89
90
91
92
93
94
*)

(* This counter is used to provide fresh var indexes *)
let index_cpt = ref 0

(* List of currently unused bdd var indexes. When we need an index,
   we first look in this list before creating a new index. This is to avoid
95
   the creation of useless bdd index, which considerably slow down the
96
97
98
99
100
101
102
   Bdd package.
*)
let free_index_list = ref []

(* returns a free index and updates [free_index_list] *)
let (get_an_index : unit -> int) =
  fun _ ->
103
104
105
106
107
108
109
110
111
112
113
114
    let i = 
      match !free_index_list with
	| [] ->
(* 	  print_string ("new index ("^ (string_of_int (!index_cpt + 1)) ^ ") !\n"); *)
	    index_cpt := !index_cpt + 1;
	    !index_cpt
	| i::tail ->
	    free_index_list := tail;
	    assert (not (List.mem i tail));
	    i
    in
      i
115
	
116
let (free_indexes : int list -> unit) =
117
  fun il ->
118
119
    (* We sort the list because the initial bdd order is generally the best *)
    free_index_list := List.sort (-) (List.rev_append il !free_index_list)
120
121


122
let init_manager () =
123
124
125
(*   let man =  Manager.make 100 0 0 10 cudd_maxmem in *)
(*     Manager.disable_autodyn man; *)
(*     man *)
Pascal Raymond's avatar
Pascal Raymond committed
126
  Bdd.init ~pagesize:50000 ~verbose:true ()
127
128
  
let bdd_manager = ref (init_manager ()) 
129
130
131
132
133
134
135
136
137
138
139

let lc2i_tbl = Hashtbl.create 0
let i2lc_tbl = Hashtbl.create 0
let global_lc2i_tbl = Hashtbl.create 0
let global_i2lc_tbl = Hashtbl.create 0

let bdd_tbl = Hashtbl.create 0
let bdd_tbl_global = Hashtbl.create 0

(* Returns the bdd of a formula if it is available in the cache,
  raises [Not_found] otherwise. *)
140
let (bdd : Exp.formula  -> Bdd.t) =
141
  fun f -> Util.hfind bdd_tbl f
142
143


144
let (bdd_global : Exp.formula  -> Bdd.t) =
145
  fun f -> Util.hfind bdd_tbl_global f
146
147

(** Stores the correspondance between a formula and a bdd. *)
148
149
let (set_bdd : Exp.formula  -> Bdd.t -> unit) =
  fun f bdd ->
150
151
152
    Hashtbl.replace bdd_tbl f bdd

let (set_bdd_global : Exp.formula  -> Bdd.t -> unit) =
153
154
  fun f bdd -> 
    Hashtbl.replace bdd_tbl_global f bdd
155
156


157
158
159
(* exported *)
let (get_index_from_linear_constraint : Constraint.t -> int) =
  fun f -> 
160
    try Util.hfind lc2i_tbl f
161
    with Not_found ->
162
      try Util.hfind global_lc2i_tbl f
163
164
      with Not_found ->
	-1
165
166

let (linear_constraint_to_index : Constraint.t -> bool -> int) =
167
168
  fun f depend_on_input -> 
    let i =
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
      if
        depend_on_input
      then
        (
	       try Util.hfind lc2i_tbl f
	       with Not_found ->
	         let index = get_an_index () in
	         Hashtbl.add lc2i_tbl f index;
	         Hashtbl.add i2lc_tbl index f;
	         index
        )
      else
        (
	       try Util.hfind global_lc2i_tbl f
	       with Not_found ->
	         let index = get_an_index () in
	         Hashtbl.add global_lc2i_tbl f index;
	         Hashtbl.add global_i2lc_tbl index f;
	         index
        )
189
    in
190
191
192
193
      (*       output_msg ((Constraint.to_string_verbose f) ^ " -> " ^ (string_of_int i) *)
      (* 		  ^ (if depend_on_input then " (depends on inputs or memory)" *)
      (* 		     else " (does not depend on inputs nor memory)") ^ "\n"); *)
    i
194
195
196
197


(* exported *)
let (index_to_linear_constraint : int -> Constraint.t) =
198
  fun i ->
199
    try Util.hfind global_i2lc_tbl i
200
    with Not_found ->
Erwan Jahier's avatar
Erwan Jahier committed
201
202
	 try Util.hfind i2lc_tbl i with _ ->
    failwith (Printf.sprintf "Error: can not find index %i in Formula_to_bdd tables\n" i)
203
204
205
206
207
208


(****************************************************************************)
(* Clearing table procedures *)

let (clear_linear_constraint_index : unit -> unit) =
209
210
  fun _ ->
    let index_to_free =
211
      Hashtbl.fold
212
213
214
	     (fun index _ acc -> index::acc)
	     i2lc_tbl
	     [];
215
    in
216
217
218
    Hashtbl.clear i2lc_tbl ;
    Hashtbl.clear lc2i_tbl ;
    free_indexes index_to_free
219
220

let (clear_global_linear_constraint_index : unit -> unit) =
221
  fun _ ->
222
223
224
225
226
    Hashtbl.clear i2lc_tbl ;
    Hashtbl.clear lc2i_tbl ;
    Hashtbl.clear global_i2lc_tbl ;
    Hashtbl.clear global_lc2i_tbl ;
    index_cpt := 0;
227
    free_index_list := []
228

229
230
231
232


(* Exported *)
let  (clear_step : unit -> unit) =
233
  fun _ ->
234
235
236
    Hashtbl.clear bdd_tbl ;
    Hashtbl.clear bdd_tbl_global ;
    clear_linear_constraint_index ()
237

238

239
240
(* Exported *)
let (clear_all : unit -> unit) =
241
  fun _ ->
242
243
    Hashtbl.clear bdd_tbl ;
    Hashtbl.clear bdd_tbl_global ;
244
245
    clear_global_linear_constraint_index ();
    bdd_manager := init_manager () 
246

247
248
249
(****************************************************************************)
(****************************************************************************)

250
type comp = SupZero | SupEqZero | EqZero
251

252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
(* 
  The bool associated the bdd says whether or not the result 
   of the translation should be tabulated or not. 

   The heuristic is to avoid the tabulation of expressions that
   depends on 
   - float
   - memory
   - input 

   true means : do not store

   it's just an heuristic anyway
*)

267

268
(* exported *)
269
let rec (f : Var.env_in -> Var.env -> string -> int -> Exp.formula -> Bdd.t) =
270
271
  fun input memory ctx_msg vl f ->
    fst (translate_do input memory ctx_msg vl f)
272
and (translate_do : Var.env_in -> Var.env -> string -> int -> Exp.formula ->
273
      Bdd.t * bool) =
274
  fun input memory ctx_msg vl f ->
275
    try (bdd f, true)
276
    with Not_found ->
277
      try (bdd_global f, false)
278
      with Not_found ->
279
	     let (bdd, dep) =
Erwan Jahier's avatar
Erwan Jahier committed
280
 	       match f with
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
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
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
	           Not(f1) ->
		          let (bdd_not, dep) =  (translate_do input memory ctx_msg vl f1) in
		            (Bdd.dnot bdd_not, dep)

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

	         | And(f1, f2) ->
		          let (bdd1, dep1) = (translate_do input memory ctx_msg vl f1)
		          and (bdd2, dep2) = (translate_do input memory ctx_msg vl f2)
		          in
		            (Bdd.dand bdd1 bdd2, dep1 || dep2)

	         | Impl(f1, f2) ->
		          let (bdd1, dep1) = (translate_do input memory ctx_msg vl f1)
		          and (bdd2, dep2) = (translate_do input memory ctx_msg vl f2)
		          in
		            (Bdd.dor (Bdd.dnot bdd1) bdd2, dep1 || dep2)

	         | Xor(f1, f2) ->
		          let (bdd1, dep1) = (translate_do input memory ctx_msg vl f1)
		          and (bdd2, dep2) = (translate_do input memory ctx_msg vl f2)
		          in
		            (Bdd.xor bdd1 bdd2, dep1 || dep2)

	         | IteB(f1, f2, f3) ->
		          let (bdd1, dep1) = (translate_do input memory ctx_msg vl f1)
		          and (bdd2, dep2) = (translate_do input memory ctx_msg vl f2)
		          and (bdd3, dep3) = (translate_do input memory ctx_msg vl f3)
		          in
		            ((Bdd.ite bdd1 bdd2 bdd3), dep1 || dep2 || dep3 )
		              
	         | True ->  (Bdd.dtrue  !bdd_manager, false)
	         | False -> (Bdd.dfalse !bdd_manager, false)
	         | Bvar(v) ->
		          ( match (lookup input memory ctx_msg vl v) with
		                Some(B(bool)) ->
			               if bool
			               then (Bdd.dtrue  !bdd_manager, true)
			               else (Bdd.dfalse !bdd_manager, true)
		              | Some(x) ->
			               output_msg (
			                 "\n*** Type error: " ^  (Value.to_string x) ^
			                   "(" ^ (formula_to_string f) ^ ")" ^
			                   " ougth to be a Boolean.\n");
			               exit 2
		              | None ->
			               (match (Var.alias v) with
			                    Some (Formu(fa)) -> translate_do input memory ctx_msg vl fa
			                  | Some (Numer(e)) -> assert false
			                  | Some (Liste l)  -> assert false
			                  | None ->
			                      assert ((Var.mode v) <> Var.Input);
			                      (Bdd.ithvar
				                      (linear_constraint_to_index (Bv(v)) false),
				                    false)
			               )
		          )

	         | EqB(f1, f2) ->
		          let (bdd1, dep1) = (translate_do input memory ctx_msg vl f1)
		          and (bdd2, dep2) = (translate_do input memory ctx_msg vl f2)
		          in
		            (Bdd.eq bdd1 bdd2, dep1 || dep2)

	         | Eq(e1, e2) ->
		          let gne = expr_to_gne (Diff(e1, e2)) input memory ctx_msg vl in
		            (gne_to_bdd gne EqZero)
		              
	         | SupEq(e1, e2) ->
		          let gne = expr_to_gne (Diff(e1, e2)) input memory ctx_msg vl in
		            (gne_to_bdd gne SupEqZero)
		              
	         | Sup(e1, e2)   ->
		          let gne = expr_to_gne (Diff(e1, e2)) input memory ctx_msg vl in
		            (gne_to_bdd gne SupZero)
		              
	         | InfEq(e1, e2) ->
		          let gne = expr_to_gne (Diff(e2, e1)) input memory ctx_msg vl in
		            (gne_to_bdd gne SupEqZero)
		              
	         | Inf(e1, e2)   ->
		          let gne =  expr_to_gne (Diff(e2, e1)) input memory ctx_msg vl in
		            (gne_to_bdd gne SupZero)
	     in
Erwan Jahier's avatar
Erwan Jahier committed
369
370
371
372
373
374
          if vl > 1 then (
            Printf.eprintf "%s" (" >>> " ^ (formula_to_string f) ^  " " ^  
                                   (if Bdd.is_false bdd then " is false " else "") ^
                                   (if Bdd.is_true bdd then " is true " else "") ^"\n") ; 
            flush stderr
          );
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
	       if
	         dep
	       then
	         ( set_bdd f bdd;	
	           match f with
		            Not(nf) -> () (* Already in the tbl thanks to the rec call *)
		          | _  -> set_bdd (Not(f)) (Bdd.dnot bdd)
	         )
	       else
	         (* [f] translate_does not depend on pre nor input memory ctx_msg vl vars *)
	         ( set_bdd_global f bdd ;	
	           match f with
		            Not(nf) -> () (* Already in the table thanks to the rec call *)
		          | _  ->
		              set_bdd_global (Not(f)) (Bdd.dnot bdd)
	         );

	       (bdd, dep)
393
and
394
    (num_to_gne: Var.env_in -> Var.env -> string -> int -> Exp.num -> Gne.t) =
395
396
  fun input memory ctx_msg vl e ->
    expr_to_gne e input memory ctx_msg vl
397
and
398
    (expr_to_gne: Exp.num -> Var.env_in -> Var.env -> string -> int -> Gne.t) =
399
  fun e input memory ctx_msg vl ->
400
    (** Evaluates pre and input vars appearing in [e] and tranlates
401
        it into a so-called garded normal form.  *)
402
    let gne =
403
      match e with
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
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
470
471
472
473
474
475
476
477
478
479
480
481
482
483
	       Sum(e1, e2) ->
	         let gne1 = (expr_to_gne e1 input memory ctx_msg vl)
	         and gne2 = (expr_to_gne e2 input memory ctx_msg vl)
	         in
	           Gne.add gne1 gne2
	     | Uminus e ->
	         Gne.opposite (expr_to_gne e input memory ctx_msg vl)

	     | Inf_int ->
	         assert false (* should not occur since only weigth can be infinite
			                   and this checked at parsing ... *)

	     | Diff(e1, e2) ->
	         let gne1 = (expr_to_gne e1 input memory ctx_msg vl)
	         and gne2 = (expr_to_gne e2 input memory ctx_msg vl)
	         in
	           Gne.diff gne1 gne2

	     | Prod(e1, e2) ->
	         let gne1 = (expr_to_gne e1 input memory ctx_msg vl)
	         and gne2 = (expr_to_gne e2 input memory ctx_msg vl)
	         in
	           Gne.mult gne1 gne2

	     | Quot(e1, e2) ->
	         let gne1 = (expr_to_gne e1 input memory ctx_msg vl)
	         and gne2 = (expr_to_gne e2 input memory ctx_msg vl)
	         in
	           Gne.div gne1 gne2

	     | Mod(e1, e2)  ->
	         let gne1 = (expr_to_gne e1 input memory ctx_msg vl)
	         and gne2 = (expr_to_gne e2 input memory ctx_msg vl)
	         in
	           Gne.modulo gne1 gne2

	     | Div(e1, e2) ->
	         let gne1 = (expr_to_gne e1 input memory ctx_msg vl)
	         and gne2 = (expr_to_gne e2 input memory ctx_msg vl)
	         in
	           Gne.div gne1 gne2

	     | Ivar(v) ->
	         let str = (Var.name v) in
	           ( match (lookup input memory ctx_msg vl v) with
		              Some(N(I(i))) ->
		                (Gne.make
		                   (Ne.make "" (I i))
		                   true
		                )
		            | None ->
		                (match (Var.alias v) with
			                  Some (Numer(ea)) ->
			                    expr_to_gne ea input memory ctx_msg vl
		                   | Some (Formu(f)) ->
			                    output_msg "\n*** Type error.\n*** ";
			                    output_msg (formula_to_string f) ;
			                    output_msg " ougth to be a numeric expression.\n";
			                    exit 2
		                   | Some (Liste l) ->
			                    assert false
		                   | None ->
			                    (Gne.make
			                       (Ne.make str (I(Num.num_of_int 1)))
			                       false
			                    )
		                )
		            | Some(N(F(f))) ->
		                output_msg "\n*** Warning : type error, ";
		                output_msg ((string_of_float f)
				                      ^ " is a float, but an int is expected.\n");
		                let i = int_of_float f in
                        (Gne.make
		                     (Ne.make "" (I (Num.num_of_int i)))
		                     true
		                  ) 
		            | Some(B(f)) ->
		                output_msg "\n*** Warning : type error, ";
		                output_msg ((string_of_bool f)
				                      ^ " is a bool, but an int is expected. " ^
484
                                  "Continuing with 0.\n");
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
		                (Gne.make
		                   (Ne.make "" (I (Num.num_of_int 0)))
		                   true
		                )
	           )

	     | Fvar(v) ->
	         let str = (Var.name v) in
	           ( match (lookup input memory ctx_msg vl v) with
		              Some(N(F(f))) ->
		                ( Gne.make
			                 (Ne.make "" (F(f)))
			                 true
		                )
		            | None ->
		                (match (Var.alias v) with
			                  Some (Numer(ea)) -> expr_to_gne ea input memory ctx_msg vl
		                   | Some (Formu(f)) ->
			                    output_msg "\n*** Type error.\n*** ";
			                    output_msg (formula_to_string f) ;
			                    output_msg " ougth to be a numeric expression.\n";
			                    assert false
		                   | Some (Liste l) ->
			                    assert false
		                   | None ->
			                    (Gne.make
			                       (Ne.make str (F(1.)))
			                       false
			                    )
		                )
		            | Some(N(I(i))) ->
                      let f = Num.float_of_num i in
		                  output_msg "\n*** Type error, ";
		                  output_msg ((Num.string_of_num i)
				                        ^ " is an int, but a float is expected. I convert it to '"^
                                    (string_of_float f)^"'\n");
                        assert false

		            | Some(B(f)) ->
                      let ff = if f then 0.0 else 1.0 in
		                  output_msg "\n*** Type error, ";
		                  output_msg ((string_of_bool f)
				                        ^ " is a bool, but a float is expected. I convert it to '"^
                                    (string_of_float ff)^"'\n");
                        assert false
	           )

	     | Ival(i) ->
	         (Gne.make
	            (Ne.make "" (I(i)))
	            false
	         )

	     | Fval(f) ->
	         ( Gne.make
		          (Ne.make "" (F(f)))
		          false
	         )

	     | FFC(id, cfunc, type_args, lib_name, args) ->
	         let evaluated_args = eval_ezdl_args input memory ctx_msg vl id args in
	         let _ = if vl > 1 then (
	           print_string ("\t" ^ id ^ " "^ 
			                     (List.fold_left 
			                        (fun acc t  -> acc ^ " " ^(Ezdl.carg_to_string t)) 
			                        "" evaluated_args));
	           flush stdout;
	         )
	         in
	         let res_call = Ezdl.cargs2f cfunc evaluated_args in
	         let _ = if vl > 1 then (
	           print_string (" = " ^ (string_of_float res_call) ^ "\n");
	           flush stdout;
	         )
	         in
	           ( Gne.make
		            (Ne.make "" (F(res_call)))
		            true (* As C functions may perform side-effects, we need 
563
564
565
			                 to recompute the result at each step !
                          not only an heuristic here...
                       *)
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
	           )

	     | IFC(id, cfunc, type_args, lib_name, args) ->
	         let evaluated_args = eval_ezdl_args input memory ctx_msg vl id args in
	         let _ = if vl > 1 then (
	           print_string ("\t" ^ id ^ " "^ 
			                     (List.fold_left 
			                        (fun acc t  -> acc ^ " " ^(Ezdl.carg_to_string t)) 
			                        "" 
			                        evaluated_args));
	           flush stdout;
	         )
	         in
	         let res_call = Ezdl.cargs2i cfunc evaluated_args in
	         let _ = if vl > 1 then (
	           print_string (" = " ^ (string_of_int res_call) ^ "\n");
	           flush stdout;
	         )
	         in
	           (Gne.make
		           (Ne.make "" (I(Num.num_of_int res_call)))
		           true
	           )

	     (* Those one are hard-coded to make things simpler and faster for Lutin. *)
	     | Gcont(a1,a2,a3) -> 
	         let (a1') = eval_int_arg input memory ctx_msg vl "gauss_continue" a1
	         and (a2') = eval_int_arg input memory ctx_msg vl "gauss_continue" a2
	         and (a3') = eval_int_arg input memory ctx_msg vl "gauss_continue" a3
	         in
596
	         let i = LutinUtils.gauss_continue a1' a2' a3' in
597
598
599
600
601
602
603
604
605
606
	           (Gne.make
		           (Ne.make "" (I(Num.num_of_int i)))
		           true
	           )
	             
	     | Gstop(a1,a2,a3) ->
	         let (a1') = eval_int_arg input memory ctx_msg vl "gauss_stop" a1
	         and (a2') = eval_int_arg input memory ctx_msg vl "gauss_stop" a2
	         and (a3') = eval_int_arg input memory ctx_msg vl "gauss_stop" a3
	         in
607
	         let i = LutinUtils.gauss_stop a1' a2' a3' in
608
609
610
611
612
613
614
615
616
617
	           (Gne.make
		           (Ne.make "" (I(Num.num_of_int i)))
		           true
	           )

	     | Icont(a1,a2,a3) ->
	         let (a1') = eval_int_arg input memory ctx_msg vl "interval_continue" a1
	         and (a2') = eval_int_arg input memory ctx_msg vl "interval_continue" a2
	         and (a3') = eval_int_arg input memory ctx_msg vl "interval_continue" a3
	         in
618
	         let i = LutinUtils.interval_continue a1' a2' a3' in
619
620
621
622
623
624
625
626
627
628
	           (Gne.make
		           (Ne.make "" (I(Num.num_of_int i)))
		           true
	           )

	     | Istop(a1,a2,a3) ->
	         let (a1') = eval_int_arg input memory ctx_msg vl "interval_stop" a1
	         and (a2') = eval_int_arg input memory ctx_msg vl "interval_stop" a2
	         and (a3') = eval_int_arg input memory ctx_msg vl "interval_stop" a3
	         in
629
	         let i = LutinUtils.interval_stop a1' a2' a3' in
630
631
632
633
634
	           (Gne.make
		           (Ne.make "" (I(Num.num_of_int i)))
		           true
	           )
	     | Ite(f, e1, e2) ->
635
	         let (bdd, depf) = translate_do input memory ctx_msg vl f 
636
637
	         and gne_t = (expr_to_gne e1 input memory ctx_msg vl)
	         and gne_e = (expr_to_gne e2 input memory ctx_msg vl) in
638
              Gne.of_ite bdd depf gne_t gne_e
639
640
    in
      gne
641
	     
642
and (eval_ezdl_args : Var.env_in -> Var.env -> string -> int -> string -> Exp.t list
643
      -> Ezdl.carg list) =
644
  fun input memory ctx_msg vl id args -> 
645
    List.map
646
647
648
649
650
651
652
653
654
655
656
657
658
659
      (fun arg -> 
         match arg with
	          Formu bool_expr -> assert false
	        | Numer num_expr -> 
	            let gne = num_to_gne input memory ctx_msg vl num_expr in
	              (match Gne.get_constant gne with
		              | None ->
		                  let errmsg = 
			                 "*** Error when calling " ^ id ^ ". " ^
			                   (Exp.num_to_string num_expr) ^ 
			                   " should be bound (i.e., it should depend " ^ 
			                   "only one inputs and memories).\n"
		                  in
			                 failwith errmsg
660
		              | Some (I i) -> Ezdl.Int_carg (Util.int_of_num i)
661
662
663
664
665
		              | Some (F f) -> Ezdl.Double_carg f
		           )
	        | Liste _ -> assert false
	   )
	   args 
666

667
and (eval_int_arg : Var.env_in -> Var.env -> string -> int -> string -> Exp.num -> int) =
668
  fun input memory ctx_msg vl id num_expr -> 
669
    Util.int_of_num (eval_num_arg input memory ctx_msg vl id num_expr)
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690

and (eval_num_arg : Var.env_in -> Var.env -> string -> int -> string -> Exp.num -> Num.num) =
  fun input memory ctx_msg vl id num_expr ->
    	 let gne = num_to_gne input memory ctx_msg vl num_expr in
	   (match Gne.get_constant gne with
	      | Some (I i) ->  i
	      | Some (F f) -> 
		       let errmsg = 
		         "*** Error when calling " ^ id ^ ". " ^
		           (Exp.num_to_string num_expr) ^ " should be an integer.\n"
		       in
		         failwith errmsg
	      | _ ->
		       let errmsg = 
		         "*** Error when calling " ^ id ^ ". " ^
		           (Exp.num_to_string num_expr) ^ 
		           " should be bound (i.e., it should depend " ^ 
		           "only one inputs and memories).\n"
		       in
		         failwith errmsg
	   )
691

692
and
693
    (gne_to_bdd : Gne.t -> comp -> Bdd.t * bool) =
694
  fun gne cmp ->
695
    (** Use [cmp] to compare [gne] with 0 and returns the
696
697
698
699
700
701
702
703
        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))] 

        Also returns a flag that is true iff [e] depends on pre or
        input vars.
    *)
704
    match cmp with
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
	     SupZero ->
	       ( Gne.fold
	           (fun nexpr (c, dep) (acc, dep_acc) ->
		           let new_dep = dep || dep_acc
		           and bdd =
		             if
		               Ne.is_a_constant nexpr
		             then
		               let cst = Ne.find "" nexpr in
		                 match cst with
			                  Some(I(i)) ->
			                    if Num.ge_num i (Num.num_of_int 0)
			                    then (Bdd.dtrue !bdd_manager)
			                    else (Bdd.dfalse !bdd_manager)
			                | Some(F(f)) ->
			                    if f > 0.
			                    then (Bdd.dtrue !bdd_manager)
			                    else (Bdd.dfalse !bdd_manager)
			                | None ->
			                    (Bdd.dfalse !bdd_manager)
		             else
		               Bdd.ithvar
                       (* 		       !bdd_manager *)
		                 (linear_constraint_to_index (Ineq(GZ(nexpr)))
			                 dep)
		           in
		             (Bdd.dor (Bdd.dand c bdd) acc, new_dep)
	           )
	           gne
	           ((Bdd.dfalse !bdd_manager), false)
	       )
736
      | SupEqZero ->
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
	       ( Gne.fold
	           (fun nexpr (c, dep) (acc, dep_acc) ->
		           let new_dep = dep || dep_acc
		           and bdd =
		             if Ne.is_a_constant nexpr
		             then
		               let cst = Ne.find "" nexpr in
		                 match cst with
			                  Some(I(i)) ->
			                    if Num.ge_num i (Num.num_of_int 0) 
			                    then (Bdd.dtrue !bdd_manager)
			                    else (Bdd.dfalse !bdd_manager)
			                | Some(F(f)) ->
			                    if f >= 0.
			                    then (Bdd.dtrue !bdd_manager)
			                    else (Bdd.dfalse !bdd_manager)
			                | None ->
			                    (Bdd.dtrue !bdd_manager)

		             else
		               Bdd.ithvar
		                 (linear_constraint_to_index (Ineq(GeqZ(nexpr)))
			                 dep)
		           in
		             (Bdd.dor (Bdd.dand c bdd) acc, new_dep)
	           )
	           gne
	           ((Bdd.dfalse !bdd_manager), false)
	       )
766
      | EqZero ->
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
	       ( Gne.fold
	           (fun nexpr (c, dep) (acc, dep_acc) ->
		           let new_dep = dep || dep_acc
		           and bdd =
		             if Ne.is_a_constant nexpr
		             then
		               let cst = Ne.find "" nexpr in
		                 match cst with
			                  Some(I(i)) ->
			                    if Num.eq_num i (Num.num_of_int 0) 
			                    then (Bdd.dtrue !bdd_manager)
			                    else (Bdd.dfalse !bdd_manager)
			                | Some(F(f)) ->
			                    if f = 0.
			                    then (Bdd.dtrue !bdd_manager)
			                    else (Bdd.dfalse !bdd_manager)
			                | None ->
			                    (Bdd.dtrue !bdd_manager)

		             else
		               Bdd.ithvar
		                 (linear_constraint_to_index (EqZ(nexpr)) dep)
		           in
		             (Bdd.dor (Bdd.dand c bdd) acc, new_dep)
	           )
	           gne
	           ((Bdd.dfalse !bdd_manager), false)
	       )
795
796

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