let constraint_system_solving ?(verbose = false) k k' subtyping_cstrs =
if verbose then begin
Format.printf "Subtyping constraints:@\n @[%a@]@\n"
fprint_subtyping_cstrs subtyping_cstrs
end;
let adaptability_cstrs =
adaptability_cstrs_of_subtyping_cstrs subtyping_cstrs
in
if verbose then begin
Format.printf "Adaptability constraints:@\n @[%a@]@\n"
fprint_adaptability_cstrs adaptability_cstrs
end;
let iof_and_size_cstrs =
iof_and_size_cstrs_of_adaptability_cstrs ~verbose:verbose
k k' adaptability_cstrs
in
if verbose then begin
Format.printf "Indexes of 1s and size constraints:@\n @[";
Format.printf "Simplified synchronizability constraints:@\n @[%a@]@\n"
fprint_linear_cstrs iof_and_size_cstrs.synchronizability;
Format.printf "Simplified precedence constraints:@\n @[%a@]@\n"
fprint_linear_cstrs iof_and_size_cstrs.precedence;
Format.printf "Periodicity constraints:@\n @[%a@]@\n"
fprint_linear_cstrs iof_and_size_cstrs.periodicity;
Format.printf "Sufficent size constraints:@\n @[%a@]@\n"
fprint_linear_cstrs iof_and_size_cstrs.sufficient_size;
Format.printf "Sufficent indexes constraints:@\n @[%a@]@\n"
fprint_linear_cstrs iof_and_size_cstrs.sufficient_indexes;
Format.printf "Increasing indexes:@\n @[%a@]@\n"
fprint_linear_cstrs iof_and_size_cstrs.increase_indexes;
Format.printf "@]@\n"
end;
let iof_and_size_sol =
iof_and_size_cstrs_solving ~verbose:verbose iof_and_size_cstrs
in
assert (check_iof_and_size_sol iof_and_size_cstrs iof_and_size_sol);
let adaptability_sol =
pbwords_of_iof_and_size_sol iof_and_size_cstrs.choice iof_and_size_sol
in
if verbose then begin
Format.printf "Solution of adaptability constraints:@\n @[";
Word_var_map.iter
(fun c_n p ->
Format.printf "%a = %a@\n" fprint_word_var c_n fprint_pbw p)
adaptability_sol;
Format.printf "@]@\n"
end;
assert (check_adaptability_sol adaptability_sol adaptability_cstrs);
adaptability_sol