let solve solver request =
S.reset solver.constraints;
let result solve collect var =
if solve solver.constraints var then
let get_assignent () =
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
Success(get_assignent)
else
let get_reasons () = collect solver.constraints var in
Failure(get_reasons)
in
match request with
|Diagnostic_int.Sng (None,i) ->
result S.solve S.collect_reasons (solver.map#vartoint i)
|Diagnostic_int.Lst (None,il) ->
result S.solve_lst S.collect_reasons_lst (List.map solver.map#vartoint il)
|Diagnostic_int.Sng (Some k,i) ->
result S.solve_lst S.collect_reasons_lst (List.map solver.map#vartoint [k;i])
|Diagnostic_int.Lst (Some k,il) ->
result S.solve_lst S.collect_reasons_lst (List.map solver.map#vartoint (k::il))