(<:) [Pbword] 
The adaptability test of two ultimately periodic binary words:
p_1 <: p_2 .

(><) [Pbword] 
The synchronizability test of two ultimately periodic binary words:
p_1 >< p_2 <=> rate p1 = rate p2 .

A  
adaptability_cstr_of_subtyping_cstr [Resolution] 
Rewrite a subtyping constraint
'a_x on p_x on p_x' on ... <: 'a_y on p_y on p_y' on ... into
an adaptability constraint
c_x on p_x on p_x' on ... <: c_y on p_y on p_y' on ... or into
p_x on p_x' on ... <: p_y on p_y' on ... if 'a_x = 'a_y .

adaptability_cstrs_of_subtyping_cstrs [Resolution] 
Rewrite a subtyping constraint system into an adaptability
constraint system.

adjust_size [Resolution] 
Rewrite
c on p into c on p' such that p = p' and
p'.u = max { p''.u  p'' \in samplers_c(A) } and
p'.v = lcm { p''.v  p'' \in samplers_c(A) } .

adjusted_adaptability_cstrs_of_simplified_adaptability_cstrs [Resolution] 
Adjuste the size of each sampler in each constraint of a
simplified adaptability constraint system.

B  
build_increasing_index_cstrs [Resolution] 
Build increasing indexes constraint system.

build_increasing_index_cstrs_of_c_n [Resolution] 
Build increasing indexes constraint:
I_{c_n}(j')  I_{c_n}(j) >= j'  j .

build_pbword [Resolution] 
Build an ultimately periodic binary word from the number of 1s of
its prefix and periodic part, the size of its prefix and periodic part,
and the indexes of its 1s.

build_periodicity_cstr [Resolution] 
Build the periodicity constraint associated to a variable
I_{c_n}(j') .

build_periodicity_cstrs [Resolution] 
Build the set of periodicity constraints.

build_sufficient_index_cstr [Resolution] 
Build sufficient indexes constraints from and index on 1 variable
I_{c_n}(j) :
I_{c_n}(j) >= j .

build_sufficient_index_cstrs [Resolution] 
Build the set of sufficient indexes constraints.

build_sufficient_size_cstr [Resolution] 
Build sufficient size constraint from the choice of number of 1s of a
word variable:
1 + I_{c_n}(c_n.u_1 + c_n.u_1)  I_{c_n}(c_n.u_1 + 1) <= c_n.v .

build_sufficient_size_cstrs [Resolution] 
Build the set of sufficient size constraints.

C  
check_adaptability_sol [Resolution] 
Check the solution of an adaptability constraint system.

check_iof_and_size_sol [Resolution] 
Check the solution of a system of constraints on indexes of 1s and sizes.

choose_nbones [Resolution] 
Choose for a variable c_n the number of 1s in the prefix
(
c_n.u_1 ) and in the periodic part (c_n.v_1 ) such that
c_n.u_1 = p_n.u + k * p_n.v ( = p'_n.u + k * p'_n.v = ...) and
c_n.n_1 = k' * p_n.v ( = k' * p'_n.v = ...)
with p_n \in samplers_{c_n}(A) , p'_n \in samplers_{c_n}(A) , ...

compare [Clock_expression.Ordered_integer_var]  
compute_size_c_n_u [Resolution] 
Compute the prefix size of a variable c_n.

constraint_system_solving [Resolution] 
Solve a subtyping constraint system.

F  
fprint_adaptability_cstr [Clock_expression]  
fprint_adaptability_cstrs [Clock_expression]  
fprint_bool [Pbword]  
fprint_choice [Clock_expression]  
fprint_choice_c_n [Clock_expression]  
fprint_clock_type [Clock_type]  
fprint_clock_type_var [Clock_type]  
fprint_integer_var [Clock_expression]  
fprint_linear_cstr [Clock_expression]  
fprint_linear_cstrs [Clock_expression]  
fprint_linear_cstrs_sol [Clock_expression]  
fprint_list [Misc] 
Print a list of elements.

fprint_pbw [Pbword]  
fprint_precedence_cstr [Clock_expression]  
fprint_precedence_cstrs [Clock_expression]  
fprint_simpl_adaptability_cstr [Clock_expression]  
fprint_simpl_adaptability_cstrs [Clock_expression]  
fprint_subtyping_cstr [Clock_type]  
fprint_subtyping_cstrs [Clock_type]  
fprint_synchronizability_cstr [Clock_expression]  
fprint_synchronizability_cstrs [Clock_expression]  
fprint_word [Pbword]  
fprint_word_expr [Clock_expression]  
fprint_word_var [Clock_expression]  
G  
gcd [Misc] 
Greatest common divisor.

I  
increase_prefix [Pbword] 
Increase prefix size of
n bits:
u(vv') = uv(v'v) with v = n .

iof [Pbword] 
Index of the jth 1 of an ultimately periodic binary word
p :
I_p(j) .

iof_and_size_cstrs_C' [Resolution]  
iof_and_size_cstrs_of_adaptability_cstrs [Resolution] 
Build directely the indexes of 1s and size constraints corresponding to
adaptability constraints.

iof_and_size_cstrs_of_synchronizability_and_precedence_cstrs [Resolution] 
Build indexes of 1s and size constraints corresponding to
synchronizability and precedence constraints.

iof_and_size_cstrs_solving [Resolution] 
Solve the linear constraints on the indexes of 1s and sizes.

L  
lcm [Misc] 
Least common multiple.

M  
make_choice [Resolution] 
Choose for each variable in an adjusted adaptability constraint
system its number of 1s in the prefix and periodic part.

N  
nbones [Pbword] 
Number of 1s a finite word
u :
u_1 .

O  
on [Pbword] 
Computation of the
on operator:
u_3(v_3) = u_1(v_1) on u_2(v_2)
with u_3 = max (u_1, I_{p_1}(u_2)) ,
v_3 = (lcm (v_1_1, v_2) / v_1_1) * v_1
and for all 1 <= i <= u_3 , u_3[i] = (p_1 on p_2)[i]
and for all 1 <= i <= v_3 , v_3[i] = (p_1 on p_2)[u_3 + i]

on_computation [Clock_expression] 
Compute
on s in an expression c on p1 on p2 on ... or
p1 on p2 on ... .

one [Pbword] 
The ultimately periodic binary word
(1) .

P  
pbwords_of_iof_and_size_sol [Resolution] 
Build the ultimately periodic binary words corresponding to the
solution of sizes and indexes of 1s.

prece [Pbword] 
The precedence test of two ultimately periodic binary words:
p_1 <= p_2 <=> I_{p_1}(j) <= I_{p_2}(j) ,
for all 1 <= j <= h
with h = max (p_1.u_1,p_2.u_1) + lcm (p_1.v_1,p_2.v_1) .

R  
rate [Pbword] 
Computation of the rate of an ultimately periodic binary word:
rate p = p.v_1 / p.v .

repeat_periodic_pattern [Pbword] 
Repeat periodic pattern:
u(v) = u(v^k) .

S  
samplers [Clock_expression] 
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 } .

simplified_adaptability_cstrs_of_adaptability_cstrs [Resolution] 
Rewrite an adaptability constraint system into an equivalent one
where all the constraints have the simple shape
c_x on p_x <: c_y on p_y .

simplify_adaptability_cstr [Resolution] 
Simplify an adaptability constraint
c_x on p_1 on p_1' on ... <: c_y on p_2 on p_2' on ... into
c_x on p_x <: c_y on p_y or check that an adaptability constraint
p_1 on p_1' on ... <: p_2 on p_2' on ... is satisfied.

simplify_precedence_cstr [Resolution] 
Simplify a precedence constraint
c_x on p_x <= c_y on p_y into
constraints on the indexes of 1s:
for all 1 <= j <= h ,
I_{c_x}(I_{p_x}(j)) <= I_{c_x}(I_{p_x}(j))
with h = max (p_x.u_1 + k * p_x.v_1, p_y.u_1 + k * p_y.v_1) +
lcm (k' * p_x.v_1, k' * p_y.v_1) .

simplify_precedence_cstrs [Resolution] 
Simplify a precedence constraint system.

simplify_synchronizability_cstr [Resolution] 
Simplify a synchronizability constraint
c_x on p_x >< c_y on p_y into
a constraint on the size of the word variables:
p_y.v_1 * c_x = p_x.v_1 * c_y .

simplify_synchronizability_cstrs [Resolution] 
Simplify a synchronizability constraint system.

size [Pbword] 
Size of a finite word
u :
u .

split_adaptability_cstr [Resolution] 
Split an adaptability constraint
c_x on p_x <: c_y on p_y into
a synchronizability constraint c_x on p_x >< c_y on p_y and
a precedence constraint c_x on p_x <= c_y on p_y .

split_clock_type [Resolution] 
Separate the type variable and the word expression in a clock type.

subtyping_cstrs_C' [Resolution]  
synchronizability_and_precedence_cstrs_of_adjusted_adaptability_cstrs [Resolution] 
Split an adaptability constraint system into equivalent
synchronizability and precedence constraint systems.

V  
vars_of_linear_constraints [Clock_expression] 
Set of integer variables that appear in a linear constraint system.

vars_of_simpl_adaptability_cstrs [Clock_expression] 
Set of word variables that appear in a simplified adaptability
constraint system.
