let solve ?tested solver request =
S.reset solver.constraints;
let result solve collect var =
if solve solver.constraints var then
let get_assignent ?(all=true) () =
List.map (fun i ->
if not(Option.is_none tested) then
(Option.get tested).(i) <- true;
solver.map#inttovar i
)(S.assignment_true solver.constraints)
in
Diagnostic_int.Success(get_assignent)
else
let get_reasons () = collect solver.constraints var in
Diagnostic_int.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))