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 2.91 KB
Newer Older
1
2
3
4
5
(*-----------------------------------------------------------------------
** Copyright (C) 2001 - Verimag.
** This file may only be copied under the terms of the GNU Library General
** Public License 
**-----------------------------------------------------------------------
6
**
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
** File: env_state.ml
** Main author: jahier@imag.fr
*)

open Graph
open Formula
open Wtree

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


(* 
** The environment is a list of graphs whose arcs are labelled by weighted 
** formula. 
*)

type env_stateT = {
  (* var names and types given file by file *)
25
  mutable var_names: (string, (vnt list * vnt list * vnt list)) Hashtbl.t;
26
  mutable pre_var_names: var_name list;
27
  mutable output_var_names: vnt list;
28
  mutable node_to_file_name: (int, string) Hashtbl.t;
29
30
  mutable atomic_formula_to_index: ((atomic_formula, int) Hashtbl.t);
  mutable index_to_atomic_formula: ((int, atomic_formula) Hashtbl.t);
31
  mutable index_cpt: int;
32
  mutable bdd_manager: Manager.t;
33
  mutable bdd_tbl_global: (formula, Bdd.t) Hashtbl.t;
34
  mutable bdd_tbl: (formula, Bdd.t) Hashtbl.t;
35
  mutable snt: (Bdd.t, Util.sol_nb * Util.sol_nb) Hashtbl.t;
36
37
38
  mutable current_nodes: node list list;
  mutable graph: (node, arc_info) Graph.t ;
  mutable wtree_table: Wtree.wtree_table ;
39
  mutable pre: subst list;
40
41
42
43
44
  mutable input : env_in ;
  mutable output: env_out ;
  mutable local : env_loc 
}

45

46
47

let (env_state:env_stateT) = {
48
  var_names = Hashtbl.create 0 ;
49
  pre_var_names = [];
50
  output_var_names = [];
51
  node_to_file_name = Hashtbl.create 0 ;
52
53
54
  atomic_formula_to_index = Hashtbl.create 0 ;
  index_to_atomic_formula = Hashtbl.create 0 ;
  index_cpt = 0 ;
55
  bdd_manager = Manager.make 10 10 0 0 0;
56
  bdd_tbl = Hashtbl.create 0;
57
  bdd_tbl_global = Hashtbl.create 0;
58
  snt = Hashtbl.create 3; 
59
60
61
  current_nodes = [];
  graph = Graph.create () ;
  wtree_table = Hashtbl.create 0 ;
62
  pre = [] ;
63
  input = Hashtbl.create 0 ;
64
  output = [] ;
65
66
67
  local = [] 
}

68
69
70
71
72
73
74
75
76
77
78
79
let (atomic_formula_to_index : atomic_formula -> int) =
  fun f ->  
    try Hashtbl.find env_state.atomic_formula_to_index f
    with Not_found -> 
      env_state.index_cpt <- (env_state.index_cpt + 1);
      Hashtbl.add env_state.atomic_formula_to_index f env_state.index_cpt;
      Hashtbl.add env_state.index_to_atomic_formula env_state.index_cpt f;
      env_state.index_cpt

let (index_to_atomic_formula : int -> atomic_formula) =
  fun i ->  
    Hashtbl.find env_state.index_to_atomic_formula i
80
81
82


let in_env_unsorted _ = 
83
84
85
86
87
88
89
90
  let vnt_list =
    Hashtbl.fold 
      (fun _ (x,_,_) acc -> Util.merge x acc) 
      env_state.var_names
      [] 
  in
    vnt_list

91

92
93
let out_env_unsorted _ =  
  let vnt_list =
94
95
96
  Hashtbl.fold 
    (fun _ (_,x,_) acc -> Util.merge x acc) 
    env_state.var_names
97
98
99
    []  
  in
    vnt_list
100
101


102
103
104

let loc_env_unsorted _ =  
  let vnt_list =
105
106
107
  Hashtbl.fold 
    (fun _ (_,_,x) acc -> Util.merge x acc) 
    env_state.var_names
108
109
110
111
    []  
  in
    vnt_list

112
113