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