bvisual_any_maxsolver

any_maxsolver(IDs, Condition, State, LocalState, NewLocalState):-
    conjunction_to_list(Condition, Set),!,
    length(Set, Count),
    %Check = bvisual_any_maxsolver:x_check(IDs, LocalState, State), % inlined to enable InfoLog flow analysis
    x_time_out_by_size(Count, TimeOut),
    %print(time_out(maxsolver(Check),TimeOut,Res)),nl,
    time_out_with_enum_warning_one_solution(maxsolver(bvisual_any_maxsolver:x_check(IDs, LocalState, State), Set, Solver0), TimeOut, Res),
    !,
    (
    is_time_out_result(Res) ->
    add_message(bvisual, 'Time out while searching solution of maximal size, looking for longest satisfiable prefix over ',IDs,Condition),
    longest_satisfiable_prefix(bvisual_any_maxsolver:x_check(IDs, LocalState, State), Set, Solver, _)
    ;
    Solver0 = time_out(Solver) ->
    add_message(bvisual, 'Time out while searching for solution of maximal size over ',IDs,Condition)
    ;
    Solver = Solver0
    ),
    conjunct_predicates(Solver, SolverExpr),
    get_any(IDs, SolverExpr, State, LocalState, NewLocalState).

x_check(_, _, _, []) :- !.

x_check(IDs, LocalState, State, Subset):-
    conjunct_predicates(Subset, LHS),!,
    get_any(IDs, LHS, State, LocalState, _).

x_time_out_by_size(0, 10) :- !. % starting from sicstus 4.3, msb(0) throws an error

x_time_out_by_size(Size, TimeOut):-
    preferences:get_preference(time_out, BaseTimeOut),
    TimeOut is max(10,min(msb(Size), 3) * BaseTimeOut). /* Timeout must be at least 1 */