module Clock_expression: sig
.. end
Definition of clock expressions and adaptability constraint systems.
Author(s): Louis Mandel, Florence Plateau
Data structures
type
word_variable =
Unknown word variable: c_n
.
module Word_var_set: Set.Make
(
sig
end
)
Set of word variables.
module Word_var_map: Map.Make
(
sig
end
)
Map of word variables.
type
choice_of_number_of_1 = {
|
k : int ; |
|
k' : int ; |
|
nbones_env : (int * int) Word_var_map.t ; |
}
Choice of number of 1s for a set of word variables
type
word_expr =
Expression on words: w ::= c | p | w on w
.
type
adaptability_cstr =
Adaptability constraints:
p_1 on ... <: p_2 on ...
and
c_x on p_1' <: c_y on p_2'
.
type
simplified_adaptability_cstr =
Simplified adaptability constraint: c_x on p_x <: c_y on p_y
.
type
simplified_adaptability_cstrs = simplified_adaptability_cstr list
Simplified adaptability constraint system.
type
synchronizability_cstr =
Synchronizability constraint: c_x on p_x |><| c_y on p_y
.
type
synchronizability_cstrs = synchronizability_cstr list
Synchronizability constraint system.
type
precedence_cstr =
Precedence constraint: c_x on p_x <= c_y on p_y
.
type
precedence_cstrs = precedence_cstr list
Precedence constraint system.
type
integer_variable =
Variables corresponding to the size (i.e., |c_n|
) and the index of
a 1 (i.e., I_{c_n}(j)
) of a word variable c_n
.
module Ordered_integer_var: sig
.. end
Ordered integer variables
module Integer_var_set: Set.Make
(
Ordered_integer_var
)
Set of integer variables.
module Integer_var_map: Map.Make
(
Ordered_integer_var
)
Map of integer variables.
type
linear_cstr =
Integer linear constraints.
type
linear_cstrs = linear_cstr list
Linear constraint system.
type
iof_and_size_cstrs = {
}
Constraints on sizes and indexes of 1s.
Functions on clock expressions
val on_computation : word_expr ->
word_variable option * Pbword.periodic_binary_word
Compute on
s in an expression c on p1 on p2 on ...
or
p1 on p2 on ...
.
Functions on simplified adaptability constraint systems
val samplers : word_variable ->
simplified_adaptability_cstr list ->
Pbword.periodic_binary_word list
Samplers of a variable c_n in a simplified adaptability constraint
system A:
{ p_n | (c_n on p_n <: c_y on p_y) \in A \/
(c_x on p_x <: c_n on p_n) \in A }
.
val vars_of_simpl_adaptability_cstrs : simplified_adaptability_cstr list ->
Word_var_set.t
Set of word variables that appear in a simplified adaptability
constraint system.
Functions on linear constraint systems
val vars_of_linear_constraints : linear_cstr list -> Integer_var_set.t
Set of integer variables that appear in a linear constraint system.
Printing functions
val fprint_word_var : Format.formatter -> word_variable -> unit
val fprint_word_expr : Format.formatter -> word_expr -> unit
val fprint_adaptability_cstr : Format.formatter -> adaptability_cstr -> unit
val fprint_adaptability_cstrs : Format.formatter -> adaptability_cstr list -> unit
val fprint_simpl_adaptability_cstr : Format.formatter -> simplified_adaptability_cstr -> unit
val fprint_simpl_adaptability_cstrs : Format.formatter ->
simplified_adaptability_cstr list -> unit
val fprint_synchronizability_cstr : Format.formatter -> synchronizability_cstr -> unit
val fprint_synchronizability_cstrs : Format.formatter -> synchronizability_cstr list -> unit
val fprint_precedence_cstr : Format.formatter -> precedence_cstr -> unit
val fprint_precedence_cstrs : Format.formatter -> precedence_cstr list -> unit
val fprint_choice_c_n : Format.formatter -> word_variable * (int * int) -> unit
val fprint_choice : Format.formatter -> choice_of_number_of_1 -> unit
val fprint_integer_var : Format.formatter -> integer_variable -> unit
val fprint_linear_cstr : Format.formatter -> linear_cstr -> unit
val fprint_linear_cstrs : Format.formatter -> linear_cstr list -> unit
val fprint_linear_cstrs_sol : Format.formatter -> int Integer_var_map.t -> unit