(*-----------------------------------------------------------------------
** Copyright (C) 2001, 2002 - Verimag.
** This file may only be copied under the terms of the GNU Library General
** Public License
**-----------------------------------------------------------------------
**
** File: env_state.mli
** Author: jahier@imag.fr
*)
(** Defines the environment state data type. All side effects occur
through that state.
*)
open Formula
type draw_mode = Edges | Inside
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.
*)
(** 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. *)
val in_env_unsorted : unit -> vnt list
(** Returns all the output variables, unsorted. *)
val out_env_unsorted : unit -> vnt list
(** Returns all the local variables, unsorted. *)
val loc_env_unsorted : unit -> vnt list
(** 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]).
Ditto for the linear_constraint <-> bdd index tables.
*)
(** 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
(** Returns the index of an atomic formula. The flag ougth to tell
whether or not the formula depends on inputs or pre *)
val linear_constraint_to_index : Constraint.t -> bool -> int
(** Returns the atomic formula of an index. *)
val index_to_linear_constraint : int -> Constraint.t
(** 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
(** 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
(** Returns and sets a mode of draw, namely, whether the draw
is done among the verteces the the convex hull of sol,
on its edges, or inside it. *)
val draw_mode: unit -> draw_mode
val set_draw_mode: draw_mode -> unit
(** outputs various statistic about the size of env_state tables *)
val dump_env_state_stat : out_channel -> unit
val set_verbose: bool -> unit
val verbose: unit -> bool