env_state.ml 21.9 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 | Vertices
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 50 51
  alias_to_formula_or_expr : (string, formula_or_expr) Hashtbl.t;
  (** Associates a formula or a numexpr to a label *)

52
  linear_constraint_to_index: ((Constraint.t, int) Hashtbl.t); 
53 54 55
  (** 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).  *)
56
  index_to_linear_constraint: ((int, Constraint.t) Hashtbl.t); 
57
  (** Ditto in the other way. *)
58

59 60
  global_linear_constraint_to_index: ((Constraint.t, int) Hashtbl.t); 
  index_to_global_linear_constraint: ((int, Constraint.t) Hashtbl.t); 
61 62 63 64 65
  (** 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. *)

66
  mutable index_cpt: int;
67
  (** Counters used to manage the indexes above. *)
68

69 70 71 72
  (** List of currently unused bdd var indexes *)
  mutable free_index_list: int list;

  mutable bdd_manager: Manager.t;
73 74 75 76 77 78 79 80 81 82 83 84 85 86 87
  (** 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. *)
88

89 90 91 92
  mutable current_nodes : node list list;
  (** List of the automata current nodes (there are as many nodes as 
    there are environment run in parallel). *)
  
93 94 95
  mutable transient_nodes : node list;
  (** List of transient nodes *)
  
96
  mutable graph : (node, arc_info) Graph.t ;
97 98 99 100 101 102 103 104 105
  (** 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. *)
106
  
107
  mutable draw_mode : draw_mode;
108
  (** Whether we draw on vertices, edges, or inside the convex hull of solution *)
109

110 111
  mutable verbose : bool;

112
  mutable pre: subst list;
113 114 115 116 117 118
  (** 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   
119
    (** Ditto for local vars. *)
120 121
}

122

123
let (env_state:env_stateT) = {
124 125 126 127 128 129 130 131 132 133 134 135 136
  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           = [];
137
  transient_nodes         = [];
138
  snt                     = Hashtbl.create 3; 
139
  ce_label                = Hashtbl.create 0 ; 
140
  ctrl_state              = Control.new_state (); 
141
  draw_mode               = Inside;
142
  verbose                 = false;
143 144
  bdd_tbl                 = Hashtbl.create 0;
  bdd_tbl_global          = Hashtbl.create 0;
145
  alias_to_formula_or_expr= Hashtbl.create 0 ;
146 147 148 149
  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;
150
  index_cpt               = 0 ;
151
  free_index_list         = []
152 153
}

154 155 156 157 158 159 160 161 162 163 164

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


165 166 167 168 169
let (clear_ima : unit -> unit) =
  fun _ -> 
    Hashtbl.clear env_state.var_names ;
    env_state.graph <- Graph.create () 

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 230 231 232 233 234 235 236 237
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

238 239 240 241 242 243 244 245 246 247 248
(****************************************************************************)
(* 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

249 250 251 252 253 254 255 256 257 258 259 260
(****************************************************************************)
(* 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


261 262 263 264 265 266 267 268 269 270 271 272
(****************************************************************************)
(* Exported *)
let (verbose: unit -> bool) = 
  fun _ ->
    env_state.verbose

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


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

310 311 312 313 314 315 316 317
(****************************************************************************)
let (is_node_transient : node -> bool) = 
  fun n -> 
    List.mem n env_state.transient_nodes
let (set_transient_nodes: node list -> unit) =
  fun nl -> 
    env_state.transient_nodes <- nl

318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334
(****************************************************************************)
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

335

336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357
(****************************************************************************)
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

358 359 360 361
let (clear_bdd_global: unit -> unit) =
  fun _ -> 
    Hashtbl.clear env_state.bdd_tbl_global

362 363
(****************************************************************************)

364 365 366 367 368 369 370 371 372 373 374 375 376 377
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 
378 379 380


(* exported *) 
381
let (linear_constraint_to_index : Constraint.t -> bool -> int) =
382 383 384 385 386
  fun f depend_on_input ->
    if 
      depend_on_input
    then
      (
387
	try Hashtbl.find env_state.linear_constraint_to_index f
388
	with Not_found -> 
389
	  let index = get_an_index () in
390 391
	    Hashtbl.add env_state.linear_constraint_to_index f index;
	    Hashtbl.add env_state.index_to_linear_constraint index f;
392
(* 	    output_string stderr ( *)
393
(* 	      (linear_constraint_to_string f) ^ "\t<-> " ^  *)
394 395 396 397
(* 	      (string_of_int index) ^ "\n" ) ; *)
(* 	    flush stderr; *)

	    index 
398 399 400
      )
    else
      (
401
	try Hashtbl.find env_state.global_linear_constraint_to_index f
402 403
	with Not_found ->
	  let index = get_an_index () in
404 405
	    Hashtbl.add env_state.global_linear_constraint_to_index f index;
	    Hashtbl.add env_state.index_to_global_linear_constraint index f;
406
	    index 
407 408 409 410
      )


(* exported *) 
411
let (index_to_linear_constraint : int -> Constraint.t) =
412
  fun i ->  
413
    try Hashtbl.find env_state.index_to_global_linear_constraint i
414
    with Not_found -> 
415
      Hashtbl.find env_state.index_to_linear_constraint i
416

417

418
(* exported *) 
419
let (clear_linear_constraint_index : unit -> unit) =
420
  fun _ -> 
421 422 423
    let index_to_free = 
      Hashtbl.fold
	(fun index _ acc -> index::acc)
424
	env_state.index_to_linear_constraint
425 426
	[];
    in
427 428
      Hashtbl.clear env_state.index_to_linear_constraint ;
      Hashtbl.clear env_state.linear_constraint_to_index ;
429
      free_indexes index_to_free
430 431

(* exported *) 
432
let (clear_global_linear_constraint_index : unit -> unit) =
433
  fun _ -> 
434 435
    Hashtbl.clear env_state.index_to_global_linear_constraint ;
    Hashtbl.clear env_state.global_linear_constraint_to_index ;
436 437 438 439
    env_state.index_cpt <- 0;
    env_state.free_index_list <- []
    

440 441 442 443 444 445 446 447
(****************************************************************************)
(* exported *) 
let (alias_to_formula_or_expr : string -> formula_or_expr option) =
  fun label -> 
    try 
      Some (Hashtbl.find env_state.alias_to_formula_or_expr label)
    with Not_found -> None

448 449

(****************************************************************************)
450 451 452 453 454 455 456 457 458 459
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
            
      (*
460
	Initializing the linear_constraint <-> index table for 
461 462 463 464 465 466 467 468
	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).
      *)


469
(****************************************************************************)
470 471 472 473
let (ctrl_expr : string -> Control.expr) =
  fun label -> 
    try Hashtbl.find env_state.ce_label label
    with _ -> failwith ("*** Label " ^ label ^ " is undefined.\n")
474

475
(****************************************************************************)
476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496
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"]) 
497
  =  ["_pre1toto"; "_pre2toto"; "_pre3toto"; "_pre1titi"; "_pre2titi"])
498 499 500 501 502 503 504


(** 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 -> 
505 506 507 508 509 510 511 512 513
    let ic = try open_in file with
	_ -> 
	  (
	    print_string ("*** File " ^ file 
			  ^ " does not exist. Please check its name.\n");
	    flush stdout;
	    exit 2
	  )
    in
514 515 516
    let 
      (* Parses the content of [file]. *)
      Parse_env.Automata(init_node, list_in, list_out, list_loc, 
517 518
			 list_pre, list_ce, trans_nodes_list, 
			 adl, list_arcs) = 
519

520
      try 
521 522 523 524 525 526 527
	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 -> 
528 529 530 531 532 533
	print_string ((Printexc.to_string e) ^ "\n");
	print_string
	  ("\nA parsing error occurred in file " ^ file ^ "\n");
	flush stdout; 
	close_in ic;
	exit 2
534 535 536
    in
    let (list_pre_vn0, _) = List.split list_pre in 
    let list_pre_vn = add_missing_pre list_pre_vn0 in
537

538 539 540 541 542 543 544 545 546 547 548 549
    (* 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
550 551 552 553 554 555 556 557 558 559

      (* Set the transient_nodes field of [env_state].  *)
      set_transient_nodes trans_nodes_list;

      (* Set the formula and expr alias tables *)
      List.iter
	(fun (label, f) -> 
	   Hashtbl.add env_state.alias_to_formula_or_expr label f)
	adl;

560
      List.iter
561 562 563 564 565 566 567 568 569 570 571 572 573 574
	(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
	)
575 576
	list_ce ;
      
577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595
      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 ()));

596

597 598 599 600 601 602 603 604 605 606
	(* 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)
      

607
(****************************************************************************)
608 609 610 611 612
(* 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
613
      Hashtbl.add env_state.ce_label "identity" (fun x -> x);
614 615
      set_current_nodes nodes

616

617 618 619 620 621
(****************************************************************************)
(* Exported *)
let  (clear_step : unit -> unit) =
  fun _ -> 
    clear_bdd () ;
622
    clear_linear_constraint_index () ;    
623 624 625 626 627 628 629 630 631 632 633 634 635 636 637
    
    (* 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 () ;
638
    clear_global_linear_constraint_index () ;
639 640 641 642 643
    clear_ima ();
    clear_step ();
    Manager.free env_state.bdd_manager ;
    env_state.bdd_manager <- Manager.make 10 10 0 0 0
    
644 645 646

(****************************************************************************)
(* Exported *)
647 648
let (dump_env_state_stat : out_channel -> unit) =
  fun res -> 
649 650 651 652 653 654 655 656 657
    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  
658
    let dump x = output_string res x in
659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675
      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";

676 677
      dump ("*** linear_constraint_to_index:" ^ 
	    (string_of_int (hashtbl_size env_state.linear_constraint_to_index)));
678 679
      dump "\n";

680 681
      dump ("*** index_to_linear_constraint:" ^ 
	    (string_of_int (hashtbl_size env_state.index_to_linear_constraint))); 
682 683
      dump "\n";

684 685 686
      dump ("*** global_linear_constraint_to_index:" ^ 
	    (string_of_int 
	       (hashtbl_size env_state.global_linear_constraint_to_index)));
687 688
      dump "\n";

689 690 691
      dump ("*** index_to_global_linear_constraint:" ^ 
	    (string_of_int 
	       (hashtbl_size env_state.index_to_global_linear_constraint))); 
692 693
      dump "\n";

694 695 696 697 698
      dump ("*** cpt_index:" ^ 
	    (string_of_int env_state.index_cpt)); 
      dump "\n";

      dump ("*** free_index_list: " ^ 
699 700
	    (fold_left (fun acc i -> acc ^ ", " ^ (string_of_int i)) "" 
	       env_state.free_index_list));
701 702 703 704
      dump "\n";



705 706 707 708 709 710 711 712 713 714 715 716
      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";

717
      dump ("*** graph:" ^ (size_str env_state.graph)); 
718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741
      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"
742