Previous  Up  Next

Module Clock_expression


module Clock_expression: sig .. end
Definition of clock expressions and adaptability constraint systems.
Author(s): Louis Mandel, Florence Plateau

Data structures



type word_variable =
| C of int
Unknown word variable: c_n.
module Word_var_set: Set.Make(sig
type t = Clock_expression.word_variable 



val compare : 'a -> 'a -> int
end)
Set of word variables. 
module Word_var_map: Map.Make(sig
type t = Clock_expression.word_variable 



val compare : 'a -> 'a -> int
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 =
| Var of word_variable
| Pbw of Pbword.periodic_binary_word
| On of word_expr * word_expr
Expression on words: w ::= c | p | w on w.

type adaptability_cstr =
| Adaptability of word_expr * word_expr
Adaptability constraints: p_1 on ... <: p_2 on ... and c_x on p_1' <: c_y on p_2'.

type simplified_adaptability_cstr =
| Simpl_adaptability of (word_variable * Pbword.periodic_binary_word)
* (word_variable * Pbword.periodic_binary_word)
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 of (word_variable * Pbword.periodic_binary_word)
* (word_variable * Pbword.periodic_binary_word)
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 of (word_variable * Pbword.periodic_binary_word)
* (word_variable * Pbword.periodic_binary_word)
Precedence constraint: c_x on p_x <= c_y on p_y.
type precedence_cstrs = precedence_cstr list
Precedence constraint system.

type integer_variable =
| Size of word_variable
| Iof of word_variable * int
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 =
| Eq of (int * integer_variable) list * int
| Le of (int * integer_variable) list * int
| Ge of (int * integer_variable) list * int
Integer linear constraints.
type linear_cstrs = linear_cstr list
Linear constraint system.

type iof_and_size_cstrs = {
   choice : choice_of_number_of_1;
   synchronizability : linear_cstrs;
   precedence : linear_cstrs;
   periodicity : linear_cstrs;
   sufficient_size : linear_cstrs;
   sufficient_indexes : linear_cstrs;
   increase_indexes : linear_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 ons 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