let solve solver request =
S.reset solver.constraints;
let result solve collect var =
if solve solver.constraints var then begin
let get_assignent ?(all=false) () =
let a = S.assignment solver.constraints in
let size = Array.length a in
let rec aux (i,acc) =
if i < size then
let acc =
if (Array.unsafe_get a i) = S.True then i :: acc
else acc
in aux (i+1,acc)
else acc
in
aux (0,[])
in
Diagnostic_int.Success(get_assignent)
end
else
let get_reasons () = collect solver.constraints var in
Diagnostic_int.Failure(get_reasons)
in
match request with
|Diagnostic_int.Sng i ->
result S.solve S.collect_reasons (solver.map#vartoint i)
|Diagnostic_int.Lst il ->
result S.solve_lst S.collect_reasons_lst (List.map solver.map#vartoint il)