let check_iof_and_size_sol iof_and_size_cstrs iof_and_size_sol =
let check_linear_cstr cstr sol =
let eval terms =
List.fold_left
(fun acc (k, x) ->
let v =
try Integer_var_map.find x sol
with Not_found -> assert false
in
acc + k * v)
0
terms
in
match cstr with
| Eq (terms, n) -> eval terms = n
| Le (terms, n) -> eval terms <= n
| Ge (terms, n) -> eval terms >= n
in
let check_linear_cstrs cstrs sol =
List.for_all (fun cstr -> check_linear_cstr cstr sol) cstrs
in
check_linear_cstrs iof_and_size_cstrs.synchronizability iof_and_size_sol &&
check_linear_cstrs iof_and_size_cstrs.precedence iof_and_size_sol &&
check_linear_cstrs iof_and_size_cstrs.periodicity iof_and_size_sol &&
check_linear_cstrs iof_and_size_cstrs.sufficient_indexes iof_and_size_sol &&
check_linear_cstrs iof_and_size_cstrs.increase_indexes iof_and_size_sol