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

11
12
13
(** Defines the environment state data type. All side effects occur
  through that state.
*)
14
15
16

open Formula

17
type draw_mode = Edges | Inside | Vertices
18

19
20
21
22
23
24
25
26
27
28
29
30
31
val read_env_state : string list list -> unit
  (** [read_env_state files_ll] updates the global variable
    [env_state] using the automata defined in the list of list
    [files_ll]. The idea behind having a list of list there is that
    automata given in inner lists should be run as a product, and
    outer ones should be run in parallel.  For example,
    [read_env_state [["foo1"; "foo2"]; ["foo3"]]] means that the
    automata given in ["foo1"] and ["foo2"] are run as if their
    automata were multiplied (in the classical sense of the automata
    product), and ["foo3"] is run in parallel. Of course, ["foo3"]
    should not share any variables with ["foo1"] and ["foo2"] then.
    *)

32
33
34
35
36
37
38
39
40
(** Returns the names and types of input, output, and local vars of
  an environment automata.
*)
val var_names : string -> vnt list * vnt list * vnt list

(** Sets the var names and types of an env automata. *)
val set_var_names : string -> vnt list * vnt list * vnt list -> unit

(** Returns all the input variables, unsorted. *)
41
42
val in_env_unsorted : unit -> vnt list

43
(** Returns all the output variables, unsorted. *)
44
45
val out_env_unsorted : unit -> vnt list

46
(** Returns all the local variables, unsorted. *)
47
48
val loc_env_unsorted : unit -> vnt list

49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139

(** Pre variables (internal) names. *)
val pre_var_names: unit -> var_name list

(** Sets (internal) names of pre variables. *)
val set_pre_var_names: var_name list -> unit


(** Returns the output var names and types. *)
val output_var_names: unit -> vnt list

(** Sets the output var names and types. *)
val set_output_var_names: vnt list -> unit

(** Returns the file name where a node is defined.
  
  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 not 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.
*)
val file_name: Formula.node -> string

(** Sets the file name where a node is defined *)
val set_file_name: Formula.node -> string -> unit

(** Returns the Bdd engine internal state. *)
val bdd_manager : unit -> Manager.t


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


(** Returns the graph containing the automata nodes and arcs. *)
val graph : unit -> (node, arc_info) Graph.t

(** Sets the current environment graph. *)
val set_graph : (node, arc_info) Graph.t -> unit

(** Returns the values of pre variables. *)
val pre: unit -> subst list

(** Sets the values of pre variables. *)
val set_pre: subst list -> unit

(** Returns the values of input variables. *)
val output: unit -> env_out 

(** Sets the values of input variables. *)
val set_output: env_out -> unit

(** Returns the values of output variables. *)
val input : unit -> env_in

(** Sets the values of output variables. *)
val set_input : env_in -> unit

(** Returns the values of local variables. *)
val local : unit -> env_loc

(** Sets the values of local variables. *)
val set_local : env_loc -> unit

(** Returns the current nodes (there are as many nodes as there are
  environment run in parallel). *) 
val current_nodes : unit -> node list list

(** Sets the values of the current nodes. *)
val set_current_nodes : node list list -> unit

(** Returns the (absolute) number of solutions contained in the lhs
    (then) and the rhs (else) branches of a bdd. Note that adding
    those two numbers only give a number of solution that is relative
    to which bdd points to it.
*)
val sol_number : Bdd.t -> Util.sol_nb * Util.sol_nb

(** Sets the number of solution of a bdd else and then branches. *)
val set_sol_number : Bdd.t -> Util.sol_nb * Util.sol_nb -> unit

(** Tests whether sol numbers of a given bdd is available. *)
val sol_number_exists : Bdd.t -> bool


(** Transforming a formula into a bdd is expensive; this is why we
   store the result of this transformation a (internal)
   table. 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]).
140
    Ditto for the linear_constraint <-> bdd index tables.
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
*)

(** Returns the bdd of a formula if it is available in [env_state],
  raises [Not_found] otherwise. *)
val bdd : formula -> Bdd.t

(** Stores the correspondance between a formula and a bdd in an
  internal table. *)
val set_bdd : formula -> Bdd.t -> unit

(** Cf [bdd], but for formula that do not depend on pre nor
  input vars. *)
val bdd_global : formula -> Bdd.t

(** Cf [set_bdd], but for formula that do not depend on pre nor
  input vars (stored in a table that is not cleaned up). *)
val set_bdd_global : formula -> Bdd.t -> unit

159
160
(** Returns the index of an atomic formula. The flag ougth to tell
  whether or not the formula depends on inputs or pre *)
161
val linear_constraint_to_index : Constraint.t -> bool -> int
162

163
(** Returns the atomic formula of an index. *)
164
val index_to_linear_constraint : int -> Constraint.t
165
166


167
168
169
170
171
172
173
174
175
176
177
(** Clean-up all the [env_state] fields that migth have been filled
  by (non-regressios) asssertions. 
*) 
val clear_all : unit -> unit

(** Clean-up the [env_state] fields that contain information that
    depends on input or pre. Indeed, this information is very likely
    to change (especially wrt floats!) at each step, therefore we do
    not keep that information to avoid memory problems. 
*)
val clear_step : unit -> unit
178

179
180
181
182
183
184
185
186
187
188
(** Returns the control expression associated to a label *)
val ctrl_expr : string -> Control.expr

  
(** Returns and sets a Control.state, an ADT that maps ident to
  counters that are used to control the ima flow, e.g., to control
  the number of times a loop is executed. *)
val ctrl_state: unit -> Control.state
val set_ctrl_state: Control.state -> unit

189
(** Returns and sets a mode of draw, namely, whether the draw
190
  is done among the vertices the the convex hull of sol, 
191
192
193
194
195
  on its edges, or inside it. *)
val draw_mode: unit -> draw_mode
val set_draw_mode: draw_mode -> unit


196
(** outputs various statistic about the size of env_state tables *)
197
val dump_env_state_stat : out_channel -> unit
198

199
200
201

val set_verbose: bool -> unit
val verbose: unit -> bool