let iof_and_size_cstrs_solving ?(verbose = false) cstrs =
let add_binding x x' vars =
if Integer_var_map.mem x vars then vars
else Integer_var_map.add x x' vars
in
let cplex_var_of_integer_var x =
match x with
| Size (C n) -> Format.sprintf "size_c%d" n
| Iof (C n, j) -> Format.sprintf "I_c%d_%d" n j
in
let sign_of_int n = if n < 0 then Cplex.Minus else Cplex.Plus in
let cplex_term_of_linear_term (k, x) =
let x' = cplex_var_of_integer_var x in
(x, x'), (sign_of_int k, abs k, x')
in
let cplex_cmp_of_linear_cstr cstr =
match cstr with
| Eq _ -> Cplex.Eq
| Le _ -> Cplex.Leq
| Ge _ -> Cplex.Geq
in
let cplex_cstr_of_linear_cstr vars cstr =
match cstr with
| Eq (terms, c)
| Le (terms, c)
| Ge (terms, c) ->
let vars, terms' =
List.fold_left
(fun (vars, terms') term ->
let (x, x'), term' = cplex_term_of_linear_term term in
add_binding x x' vars, term' :: terms')
(vars, [])
terms
in
vars, (List.rev terms', cplex_cmp_of_linear_cstr cstr, c)
in
let cplex_cstr_of_linear_cstrs vars cstrs =
let vars, cplex_cstrs =
List.fold_left
(fun (vars, cplex_cstrs) cstr ->
let vars, cplex_cstr = cplex_cstr_of_linear_cstr vars cstr in
vars, cplex_cstr :: cplex_cstrs)
(vars, []) cstrs
in
vars, List.rev cplex_cstrs
in
let vars = Integer_var_map.empty in
let vars, synchronizability =
cplex_cstr_of_linear_cstrs vars cstrs.synchronizability
in
let vars, precedence =
cplex_cstr_of_linear_cstrs vars cstrs.precedence
in
let vars, periodicity =
cplex_cstr_of_linear_cstrs vars cstrs.periodicity
in
let vars, sufficient_size =
cplex_cstr_of_linear_cstrs vars cstrs.sufficient_size
in
let vars, sufficient_indexes =
cplex_cstr_of_linear_cstrs vars cstrs.sufficient_indexes
in
let vars, increase_indexes =
cplex_cstr_of_linear_cstrs vars cstrs.increase_indexes
in
let integer =
Integer_var_map.fold (fun _ x acc -> x :: acc) vars []
in
let bounds =
Integer_var_map.fold (fun _ x acc -> (Some 0, x, None) :: acc) vars []
in
let objective =
let l =
Integer_var_map.fold
(fun x x' acc ->
match x with
| Iof _ -> (Cplex.Plus, 1, x') :: acc
| Size _ -> acc) vars []
in
Cplex.Minimize l
in
let subject_to =
synchronizability @
precedence @
periodicity @
sufficient_size @
sufficient_indexes @
increase_indexes
in
let cplex_system =
{ Cplex.env = vars;
integer = integer;
bounds = bounds;
objective = objective;
subject_to = subject_to;
}
in
let cplex_verbose = !Cplex.verbose in
Cplex.verbose := verbose;
if verbose then begin
Format.printf "Indexes of 1s and size constraints solving:@\n @[";
end;
match Cplex.solve cplex_system with
| Cplex.GLP_OPT, cplex_sol ->
Cplex.verbose := cplex_verbose;
let sol =
Integer_var_map.map
(fun x' -> List.assoc x' cplex_sol)
vars
in
if verbose then begin
Format.printf "%a"
fprint_linear_cstrs_sol sol;
Format.printf "@]@\n"
end;
sol
| Cplex.GLP_NOFEAS, _ -> raise Solve
| Cplex.Empty_constraints, _ -> Integer_var_map.empty
| _ -> assert false