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/

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

11
open Util
12
open List
13
14
15
16
17
18
open Graph
open Formula

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


19
type draw_mode =  Edges | Inside
20

21
(*
22
23
24
25
26
** The environment is a list of graphs whose arcs are labelled by weighted 
** formula. 
*)

type env_stateT = {
27
28
29
30
  var_names: (string, (vnt list * vnt list * vnt list)) Hashtbl.t;
  (** Var names and types ([vnt]) of input, output, and local vars, 
    given module by module. *)

31
  mutable pre_var_names: var_name list;
32
33
  (** internal names of pre variables. *)

34
  mutable output_var_names: vnt list;
35
36
37
38
39
40
41
42
43
44
45
46
47
48
  (** Output var names and types. *)

  node_to_file_name: (int, string) Hashtbl.t;
  (** Associates each node in the environment automata with its 
    origin file name (i.e., the [.env] file it comes from).

    We need that information to be able to retrieve the list of
    variables that ougth to be generated from a list of nodes (the
    current nodes in the (virtual) automata product). Indeed, some
    variables that should be drawn do no necessarily appear in
    formula; and once the whole bdd has been traversed for the draw,
    we need to be able to know what variables are still to be drawn.
  *)

49
  linear_constraint_to_index: ((Constraint.t, int) Hashtbl.t); 
50
51
52
  (** This indexing of (output and local) variable names is used
    for constructing bdds in the boolean solver (for which variables
    are [int], not [string]s).  *)
53
  index_to_linear_constraint: ((int, Constraint.t) Hashtbl.t); 
54
  (** Ditto in the other way. *)
55

56
57
  global_linear_constraint_to_index: ((Constraint.t, int) Hashtbl.t); 
  index_to_global_linear_constraint: ((int, Constraint.t) Hashtbl.t); 
58
59
60
61
62
  (** The same as the tables above, except that they only contain the
    formula which content does npt depend on input nor pre variables.
    We need to maitain those two kinds of tables because unlike the
    latter, the former needs to be cleared at each step. *)

63
  mutable index_cpt: int;
64
  (** Counters used to manage the indexes above. *)
65

66
67
68
69
  (** List of currently unused bdd var indexes *)
  mutable free_index_list: int list;

  mutable bdd_manager: Manager.t;
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
  (** bdd engine internal state. *)

  bdd_tbl_global: (formula, Bdd.t) Hashtbl.t;
  bdd_tbl: (formula, Bdd.t) Hashtbl.t;
  (** Transforming a formula into a bdd is expensive, therefore we
    store the result of this transformation in a table. Only formula
    does not depend on pre nor input vars are stored in
    [bdd_tbl_global]. The other ones are stored in the table
    [bdd_tbl], which is cleared at each new step. *)

  snt: (Bdd.t, Util.sol_nb * Util.sol_nb) Hashtbl.t;
  (** Associates to a bdd the (absolute) number of solutions
    contained in its lhs (then) and rhs (else) branches. Note that
    adding those two numbers only give a number of solution that is
    relative to which bdd points to it. *)
85

86
87
88
89
90
  mutable current_nodes : node list list;
  (** List of the automata current nodes (there are as many nodes as 
    there are environment run in parallel). *)
  
  mutable graph : (node, arc_info) Graph.t ;
91
92
93
94
95
96
97
98
99
  (** The automata transitions are stored in a Graph.t *)

  mutable ce_label : (string, Control.expr) Hashtbl.t ;
  (** Maps labels (that appear in the automata to control expressions. *)

  mutable ctrl_state : Control.state;
  (** ADT that map idents to counters that are used to control the
    ima flow, e.g., to control the number of times a loop is
    executed. *)
100
  
101
102
103
  mutable draw_mode : draw_mode;
  (** Whether we draw on verteces, edges, or inside the convex hull of solution *)

104
105
  mutable verbose : bool;

106
  mutable pre: subst list;
107
108
109
110
111
112
  (** Stores the values of pre variables. *)
  mutable input : env_in ;  
  (** Ditto for input vars. *)
  mutable output: env_out ; 
  (** Ditto for output vars. *)
  mutable local : env_loc   
113
    (** Ditto for local vars. *)
114
115
}

116

117
let (env_state:env_stateT) = {
118
119
120
121
122
123
124
125
126
127
128
129
130
131
  var_names               = Hashtbl.create 0;
  pre_var_names           = [];
  output_var_names        = [];
  node_to_file_name       = Hashtbl.create 0 ;
  bdd_manager             = Manager.make 10 10 0 0 0;
  graph                   = Graph.create () ;

(** The following values (possibly) change at each step *)
  pre                     = [];
  input                   = Hashtbl.create 0;
  output                  = [];
  local                   = [];
  current_nodes           = [];
  snt                     = Hashtbl.create 3; 
132
  ce_label                = Hashtbl.create 0 ; 
133
  ctrl_state              = Control.new_state (); 
134
  draw_mode               = Inside;
135
  verbose                 = false;
136
137
  bdd_tbl                 = Hashtbl.create 0;
  bdd_tbl_global          = Hashtbl.create 0;
138
139
140
141
  linear_constraint_to_index = Hashtbl.create 0;
  index_to_linear_constraint = Hashtbl.create 0;
  global_linear_constraint_to_index = Hashtbl.create 0;
  index_to_global_linear_constraint = Hashtbl.create 0;
142
  index_cpt               = 0 ;
143
  free_index_list         = []
144
145
}

146
147
148
149
150
151
152
153
154
155
156

(****************************************************************************)
let (var_names: string -> vnt list * vnt list * vnt list) = 
  fun file ->
    Hashtbl.find env_state.var_names file

let (set_var_names : string -> vnt list * vnt list * vnt list -> unit) =
  fun file vntl -> 
    Hashtbl.replace env_state.var_names file vntl


157
158
159
160
161
let (clear_ima : unit -> unit) =
  fun _ -> 
    Hashtbl.clear env_state.var_names ;
    env_state.graph <- Graph.create () 

162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
let (in_env_unsorted : unit -> vnt list) =
  fun _ -> 
    let vnt_list =
      Hashtbl.fold 
	(fun _ (x,_,_) acc -> Util.merge x acc) 
	env_state.var_names
	[] 
    in
      vnt_list
	
let (out_env_unsorted : unit -> vnt list) =
  fun _ -> 
    let vnt_list =
      Hashtbl.fold 
	(fun _ (_,x,_) acc -> Util.merge x acc) 
	env_state.var_names
	[]  
    in
      vnt_list
	
let (loc_env_unsorted : unit -> vnt list) =
  fun _ -> 
    let vnt_list =
      Hashtbl.fold 
	(fun _ (_,_,x) acc -> Util.merge x acc) 
	env_state.var_names
	[]  
    in
      vnt_list


(****************************************************************************)
let (pre_var_names: unit -> var_name list) = 
  fun _ -> 
    env_state.pre_var_names
let (set_pre_var_names: var_name list -> unit) = 
  fun vnl -> 
    env_state.pre_var_names <- vnl


(****************************************************************************)
let (file_name: Formula.node -> string) = 
  fun node -> 
    Hashtbl.find env_state.node_to_file_name node 
    
let (set_file_name: Formula.node -> string -> unit) = 
  fun node file -> 
    Hashtbl.replace env_state.node_to_file_name node file 
      
(****************************************************************************)
let (bdd_manager : unit -> Manager.t) =  
  fun _ -> 
    env_state.bdd_manager 



(****************************************************************************)
(****************************************************************************)
(** The following values change at each step *)

(****************************************************************************)
let (graph : unit -> (node, arc_info) Graph.t) = 
  fun _  -> 
    env_state.graph
let (set_graph : (node, arc_info) Graph.t -> unit) =
  fun g -> 
    env_state.graph <- g

230
231
232
233
234
235
236
237
238
239
240
(****************************************************************************)
(* Exported *)
let (ctrl_state: unit -> Control.state) = 
  fun _ ->
    env_state.ctrl_state

(* Exported *)
let (set_ctrl_state: Control.state -> unit) =
  fun cs -> 
    env_state.ctrl_state <- cs

241
242
243
244
245
246
247
248
249
250
251
252
(****************************************************************************)
(* Exported *)
let (draw_mode: unit -> draw_mode) = 
  fun _ ->
    env_state.draw_mode

(* Exported *)
let (set_draw_mode: draw_mode -> unit) =
  fun dm -> 
    env_state.draw_mode <- dm


253
254
255
256
257
258
259
260
261
262
263
264
(****************************************************************************)
(* Exported *)
let (verbose: unit -> bool) = 
  fun _ ->
    env_state.verbose

(* Exported *)
let (set_verbose: bool -> unit) =
  fun b -> 
    env_state.verbose <- b


265
266
267
268
269
270
271
272
273
274
275
276
277
278
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
305
306
307
308
309
310
311
312
313
314
315
316
317
318
(****************************************************************************)
let (pre: unit ->  subst list) =
  fun _  -> 
    env_state.pre
let (set_pre: subst list -> unit) =
  fun sl -> 
    env_state.pre <- sl

let (input : unit -> env_in)  = 
  fun _  -> 
    env_state.input
let (set_input: env_in -> unit) =
  fun input -> 
    env_state.input <- input

let (output: unit -> env_out) = 
  fun _  -> 
    env_state.output
let (set_output: env_out -> unit) =
  fun output -> 
    env_state.output <- output

let (local : unit -> env_loc) = 
  fun _  -> 
    env_state.local
let (set_local: env_loc -> unit) =
  fun local -> 
    env_state.local <- local

(****************************************************************************)
let (current_nodes : unit -> node list list) = 
  fun _ -> 
    env_state.current_nodes
let (set_current_nodes: node list list -> unit) =
  fun nll -> 
    env_state.current_nodes <- nll

(****************************************************************************)
let (sol_number : Bdd.t -> Util.sol_nb * Util.sol_nb) =
  fun bdd -> 
    Hashtbl.find env_state.snt bdd

let (set_sol_number : Bdd.t -> Util.sol_nb * Util.sol_nb -> unit) =
  fun bdd sol_nb -> 
      Hashtbl.replace env_state.snt bdd sol_nb

let (clear_sol_numbers: unit -> unit) =
  fun _ -> 
    Hashtbl.clear env_state.snt

let (sol_number_exists : Bdd.t -> bool) =
  fun bdd -> 
      Hashtbl.mem env_state.snt bdd

319

320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
(****************************************************************************)
let (bdd : formula -> Bdd.t) =
  fun f -> 
    Hashtbl.find env_state.bdd_tbl f

let (set_bdd : formula -> Bdd.t -> unit) =
  fun f bdd -> 
    Hashtbl.replace env_state.bdd_tbl f bdd

let (clear_bdd: unit -> unit) =
  fun _ -> 
    Hashtbl.clear env_state.bdd_tbl


let (bdd_global : formula -> Bdd.t) =
  fun f -> 
    Hashtbl.find env_state.bdd_tbl_global f

let (set_bdd_global : formula -> Bdd.t -> unit) =
  fun f bdd -> 
    Hashtbl.replace env_state.bdd_tbl_global f bdd

342
343
344
345
let (clear_bdd_global: unit -> unit) =
  fun _ -> 
    Hashtbl.clear env_state.bdd_tbl_global

346
347
(****************************************************************************)

348
349
350
351
352
353
354
355
356
357
358
359
360
361
let (get_an_index : unit -> int) =
  fun _ ->
    match env_state.free_index_list with
	[] -> 
	  env_state.index_cpt <- env_state.index_cpt + 1;
	  env_state.index_cpt
      | i::tail -> 
	  env_state.free_index_list <- tail;
	  i
	  
	  
let (free_indexes : int list -> unit) =
  fun il -> 
    env_state.free_index_list <- append il env_state.free_index_list 
362
363
364


(* exported *) 
365
let (linear_constraint_to_index : Constraint.t -> bool -> int) =
366
367
368
369
370
  fun f depend_on_input ->
    if 
      depend_on_input
    then
      (
371
	try Hashtbl.find env_state.linear_constraint_to_index f
372
	with Not_found -> 
373
	  let index = get_an_index () in
374
375
	    Hashtbl.add env_state.linear_constraint_to_index f index;
	    Hashtbl.add env_state.index_to_linear_constraint index f;
376
(* 	    output_string stderr ( *)
377
(* 	      (linear_constraint_to_string f) ^ "\t<-> " ^  *)
378
379
380
381
(* 	      (string_of_int index) ^ "\n" ) ; *)
(* 	    flush stderr; *)

	    index 
382
383
384
      )
    else
      (
385
	try Hashtbl.find env_state.global_linear_constraint_to_index f
386
387
	with Not_found ->
	  let index = get_an_index () in
388
389
	    Hashtbl.add env_state.global_linear_constraint_to_index f index;
	    Hashtbl.add env_state.index_to_global_linear_constraint index f;
390
	    index 
391
392
393
394
      )


(* exported *) 
395
let (index_to_linear_constraint : int -> Constraint.t) =
396
  fun i ->  
397
    try Hashtbl.find env_state.index_to_global_linear_constraint i
398
    with Not_found -> 
399
      Hashtbl.find env_state.index_to_linear_constraint i
400

401

402
(* exported *) 
403
let (clear_linear_constraint_index : unit -> unit) =
404
  fun _ -> 
405
406
407
    let index_to_free = 
      Hashtbl.fold
	(fun index _ acc -> index::acc)
408
	env_state.index_to_linear_constraint
409
410
	[];
    in
411
412
      Hashtbl.clear env_state.index_to_linear_constraint ;
      Hashtbl.clear env_state.linear_constraint_to_index ;
413
      free_indexes index_to_free
414
415

(* exported *) 
416
let (clear_global_linear_constraint_index : unit -> unit) =
417
  fun _ -> 
418
419
    Hashtbl.clear env_state.index_to_global_linear_constraint ;
    Hashtbl.clear env_state.global_linear_constraint_to_index ;
420
421
422
423
    env_state.index_cpt <- 0;
    env_state.free_index_list <- []
    

424
425

(****************************************************************************)
426
427
428
429
430
431
432
433
434
435
let (output_var_names: unit -> vnt list) = 
  fun _ -> 
    env_state.output_var_names
    
let (set_output_var_names: vnt list -> unit) = 
  fun vntl0 -> 
    let vntl = append vntl0 (loc_env_unsorted ()) in
      env_state.output_var_names <- vntl0
            
      (*
436
	Initializing the linear_constraint <-> index table for 
437
438
439
440
441
442
443
444
	boolean var now and once for all so that boolean var 
	to be generated are stored for small indexes so that 
	we can clear those index table at each step for bigger 
	index values (ie, the ones that will contain numeric 
	constraints).
      *)


445
(****************************************************************************)
446
447
448
449
let (ctrl_expr : string -> Control.expr) =
  fun label -> 
    try Hashtbl.find env_state.ce_label label
    with _ -> failwith ("*** Label " ^ label ^ " is undefined.\n")
450

451
(****************************************************************************)
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
let rec (add_missing_pre: string list -> string list) =
  (* Even if the automata contains "_pre3toto", we need to store
     "_pre2toto", and "_pre1toto". Thefore we add them here to the
     list of pre vars declared in the automata thanks to this
     function. *)
  fun vnl -> 
    List.fold_left (add_missing_pre_acc) [] vnl
and
  (add_missing_pre_acc: string list -> string -> string list) =
  fun acc pren_vn -> 
    let (n, vn) = Util.split_pre_var_string pren_vn in
    let rec (build_list_pre : string list -> int -> string -> string list) =
      fun acc i str ->
	let prei_str = ("_pre" ^ (string_of_int i) ^ str) in
	  if i = 1 
	  then prei_str::acc
	  else build_list_pre (prei_str::acc) (i-1) str
    in
      Util.merge (build_list_pre [] n vn) acc

let _ = assert ( (add_missing_pre ["_pre3toto"; "_pre2titi"; "_pre2toto"]) 
473
  =  ["_pre1toto"; "_pre2toto"; "_pre3toto"; "_pre1titi"; "_pre2titi"])
474
475
476
477
478
479
480


(** Returns the initial node of the automata defined in
  [file]. Also updates the various fields of [env_state] with the
  content of [file].  *)
let (read_env_state_one_file : string -> node) =
  fun file -> 
481
482
483
484
485
486
487
488
489
    let ic = try open_in file with
	_ -> 
	  (
	    print_string ("*** File " ^ file 
			  ^ " does not exist. Please check its name.\n");
	    flush stdout;
	    exit 2
	  )
    in
490
491
492
    let 
      (* Parses the content of [file]. *)
      Parse_env.Automata(init_node, list_in, list_out, list_loc, 
493
			 list_pre, list_ce, list_form_def, list_arcs) = 
494

495
      try 
496
497
498
499
500
501
502
503
504
505
506
507
	let ic = open_in file in
	let aut = Parse_env.parse_automata ic 
	    (Parse_env.lexer(Stream.of_channel ic))
	in 
	  close_in ic;
	  aut
      with e -> 
	    print_string
	    ("\nA parsing error occurred in file " ^ file ^ "\n");
	    flush stdout; 
	    close_in ic;
	    exit 2
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
    in
    let (list_pre_vn0, _) = List.split list_pre in 
    let list_pre_vn = add_missing_pre list_pre_vn0 in
      
    (* Sets the [graph] field of [env_state]. *)
    let node_nb = (List.length (Graph.get_all_nodes (graph ()))) in
    let (add_arc: Parse_env.read_arc -> unit) =
      fun arc ->
	match arc with
	    Parse_env.Arc(node_from, arc_info, node_to) -> 
	      (add_trans
		 (graph ())
		 (node_from+node_nb) 
		 arc_info 
		 (node_to+node_nb));
    in
524
      List.iter
525
526
527
528
529
530
531
532
533
534
535
536
537
538
	(fun (id, ce) -> 
	   if 
	     Hashtbl.mem env_state.ce_label id 
	   then 
	     (
	       print_string ("*** The control expression " ^ id ^ 
			     " has been defined twice, which is bad." ^
			     " Please fix it.\n");
	       flush stdout;
	       exit 2
	     )
	   else 
	     Hashtbl.add env_state.ce_label id ce
	)
539
540
	list_ce ;
      
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
      List.iter (add_arc) list_arcs ;

      (* Checks that there is no hole in the node numbers (which
	 would mean that the node number is not equal to the biggest node) *)
      let new_node_nb = (List.length (get_all_nodes (graph ()))) in
	if (for_all 
	      (fun arc -> 
		 match arc with 
		     Parse_env.Arc(node_from, arc_info, node_to) -> 
		       ( node_from >= new_node_nb ) || (node_to >= new_node_nb) 
	      )
	      list_arcs) 
	then failwith "*** Bad env format. Node numbers should be contiguous.\n";
	
	(* Sets the [node_to_file_name] field of [env_state]. *)
	List.iter
	  (fun node -> set_file_name (node+node_nb) file) 
	  (Graph.get_all_nodes (graph ()));

560

561
562
563
564
565
566
567
568
569
570
	(* Sets the [var_names] and [pre_var_names] fields of [env_state]. *)
	set_var_names file (list_in, list_out, list_loc) ;

	List.iter 
	  (fun vn -> set_pre_var_names (vn::(pre_var_names ())))
	  list_pre_vn;

	(init_node + node_nb)
      

571
(****************************************************************************)
572
573
574
575
576
(* Exported *)
let  (read_env_state : string list list -> unit) =
  fun files_ll -> 
    (** Calls [read_env_state_one_file] on a list of list of files. *)
    let nodes = map (map (read_env_state_one_file)) files_ll in
577
      Hashtbl.add env_state.ce_label "identity" (fun x -> x);
578
579
      set_current_nodes nodes

580

581
582
583
584
585
(****************************************************************************)
(* Exported *)
let  (clear_step : unit -> unit) =
  fun _ -> 
    clear_bdd () ;
586
    clear_linear_constraint_index () ;    
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
    
    (* if (t mod 100) = 0      
       then  
       if Util.hashtbl_size Env_state.snt > 1000  
       then  *)
    clear_sol_numbers () ;       
    set_sol_number 
      (Bdd.dtrue (bdd_manager ())) (Util.one_sol, Util.zero_sol);
    set_sol_number 
      (Bdd.dfalse (bdd_manager ())) (Util.zero_sol, Util.one_sol)

(* Exported *)
let (clear_all : unit -> unit) =
  fun _ -> 
    clear_bdd_global () ;
602
    clear_global_linear_constraint_index () ;
603
604
605
606
607
    clear_ima ();
    clear_step ();
    Manager.free env_state.bdd_manager ;
    env_state.bdd_manager <- Manager.make 10 10 0 0 0
    
608
609
610

(****************************************************************************)
(* Exported *)
611
612
let (dump_env_state_stat : out_channel -> unit) =
  fun res -> 
613
614
615
616
617
618
619
620
621
    let (size_str : ('a, 'b) t -> string) =
      fun g -> 
	let (n1, n2, n3) = Graph.size g in
	  (
	    "table size = " ^ (string_of_int n1) ^
	    ", node nb = " ^ (string_of_int n2) ^
	    ", trans nb = " ^ (string_of_int n3)
	  )    
    in  
622
    let dump x = output_string res x in
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
      dump "***************************************************************\n";
      dump "******************* A few statistics ... **********************\n";
      dump ("*** pre var names: " ^ 
	    (fold_left (fun acc s -> acc ^ ", " ^ s) "" env_state.pre_var_names));
      dump "\n";

      dump ("*** output var names: " ^ 
	    (fold_left 
	       (fun acc (vn, vt) -> 
		  acc ^ ", " ^ vn ^ ":" ^ (Formula.var_type_to_string vt))
	       "" env_state.output_var_names));
      dump "\n";

      dump ("*** node_to_file_name:" ^ 
	    (string_of_int (hashtbl_size env_state.node_to_file_name))); 
      dump "\n";

640
641
      dump ("*** linear_constraint_to_index:" ^ 
	    (string_of_int (hashtbl_size env_state.linear_constraint_to_index)));
642
643
      dump "\n";

644
645
      dump ("*** index_to_linear_constraint:" ^ 
	    (string_of_int (hashtbl_size env_state.index_to_linear_constraint))); 
646
647
      dump "\n";

648
649
650
      dump ("*** global_linear_constraint_to_index:" ^ 
	    (string_of_int 
	       (hashtbl_size env_state.global_linear_constraint_to_index)));
651
652
      dump "\n";

653
654
655
      dump ("*** index_to_global_linear_constraint:" ^ 
	    (string_of_int 
	       (hashtbl_size env_state.index_to_global_linear_constraint))); 
656
657
      dump "\n";

658
659
660
661
662
      dump ("*** cpt_index:" ^ 
	    (string_of_int env_state.index_cpt)); 
      dump "\n";

      dump ("*** free_index_list: " ^ 
663
664
	    (fold_left (fun acc i -> acc ^ ", " ^ (string_of_int i)) "" 
	       env_state.free_index_list));
665
666
667
668
      dump "\n";



669
670
671
672
673
674
675
676
677
678
679
680
      dump ("*** bdd_tbl_global size:" ^ 
	    (string_of_int (hashtbl_size env_state.bdd_tbl_global))); 
      dump "\n";

      dump ("*** bdd_tbl:" ^ 
	    (string_of_int (hashtbl_size env_state.bdd_tbl))); 
      dump "\n";

      dump ("*** snt:" ^ 
	    (string_of_int (hashtbl_size env_state.snt))); 
      dump "\n";

681
      dump ("*** graph:" ^ (size_str env_state.graph)); 
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
      dump "\n";

      dump ("*** ce_label:" ^ 
	    (string_of_int (hashtbl_size env_state.ce_label))); 
      dump "\n";

      dump ("*** control state size:" ^ 
	    (string_of_int (Control.state_size env_state.ctrl_state))); 
      dump "\n";


(*       dump "*** pre variables:"; *)
(*       Formula.print_subst_list env_state.pre stderr; *)
(*  *)
(*       dump "*** input variables:"; *)
(*       Formula.print_env_in env_state.input stderr; *)
(*  *)
(*       dump "*** output variables:"; *)
(*       Formula.print_subst_list env_state.output stderr; *)
(*  *)
(*       dump "*** local variables:"; *)
(*       Formula.print_subst_list env_state.local stderr; *)

      dump "\n"
706