maxsolver

longest_satisfiable_prefix(Eval, Set, Prefix, R) :-
    call(Eval, Set),!, Prefix=Set,
    R=[].

longest_satisfiable_prefix(Eval, Set, Prefix, Complement) :-
    x_longest_satisfiable_prefix(Eval, Set, Prefix, Complement).

longest_satisfiable_segment(Eval, Set, Segment, Prefix, Suffix):-
    findall(
    x(Segment0, Prefix0, Suffix0),
    satisfiable_segment(Eval, Set, Segment0, Prefix0, Suffix0),
    Segments),
    max_member(
    x_shorter_or_same_length_list,
    x(Segment, Prefix, Suffix),
    Segments).

maximal_timeout(Val) :- get_preference(formula_tree_maximal_timeout,Val). % Default 30000

maxsolver(Eval, Set, Solver):-
    maxsolver(automatic, Eval, Set, Solver).

maxsolver(automatic, Eval, Set, Solver):-
    length(Set, L),
    x_method_by_length(Method, MaxLength),
    L =< MaxLength,!,
    call(Method, Eval, Set, Solver).

maxsolver(automatic, Eval, Set, Solver):-
    maxsolver_by_longest_prefix(Eval, Set, Solver).

maxsolver_by_longest_prefix(_, Set, Solver) :- !, Set=1,Solver=1.

maxsolver_by_longest_prefix(Eval, Set, Solver):-
    longest_satisfiable_prefix(Eval, Set, Prefix, Tail),!,
    ( Tail = [_|NewSet] ->
    append(Prefix, SubSolver, Solver),
    maxsolver_by_longest_prefix(
    x_append_and_eval(Eval, Prefix), NewSet, SubSolver)
    ;
    Solver = Prefix
).

maxsolver_by_longest_segment(Eval, Set, Solver) :-
    longest_satisfiable_segment(Eval, Set, Segment, Prefix, Suffix),
    x_maxsolver_by_longest_segment(Eval, Segment, Prefix, Suffix, Solver).

maxsolver_exact_with_marker(Eval, Set, Solver):-
    call(Eval, Set),!, Solver=Set.

maxsolver_exact_with_marker(Eval, Set, Solver):-
    length(Set, Length),
    (Length == 0
    -> PrecalcBound is 1
    ; PrecalcBound is max(msb(Length) - 1, 1)),
    x_precalc(Eval, Set, 1, PrecalcBound, Markers),
    x_maxsolver_exact_with_marker(Eval, Set, Markers, 0, Length, Solver).

minimal_timeout(Val) :- get_preference(formula_tree_minimal_timeout,Val). % Default 1000

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

satisfiable_segment(Eval, Set, Segment, Prefix, Suffix):-
    append(Prefix, Subset, Set),
    Subset\=[],
    longest_satisfiable_prefix(Eval, Subset, Segment, Suffix),
    ( Suffix = [],! ; true ).

x_append_and_eval(Eval, Prefix, Set):-
    append(Prefix, Set, NewSet),
    call(Eval, NewSet).

x_existis_satisfiable_subset_of_length(Eval, Set, Markers, Length, FalseSets):-
    findall(Subset,
    x_false_subset_til_true(Eval, Set, Markers, Length, Subset),
    Sets),!,
    append(FalseSets, [xxx], Sets).

x_false_subset(Eval, Set, L, Subset):-
    length(Subset, L),
    subseq0(Set, Subset),
    \+call(Eval, Subset).

x_false_subset_til_true(Eval, Set, Markers, Length, Subset):-
    length(Subset0,Length),
    subseq0(Set,Subset0),
    \+x_marked_as_false(Markers, Subset0),
    ( call(Eval, Subset0) ->
    !, Subset = xxx
    ;
    Subset = Subset0
).

x_half_length(List, Smaller):-
    length(List, Length),
    Half is Length // 2,
    length(Smaller, Half).

x_longest_satisfiable_prefix(_, [C], [], [C]):-!.

x_longest_satisfiable_prefix(Eval, Set, Prefix, Complement):-
    x_half_length(Set, Half),
    append(Half, Tail, Set),
    ( call(Eval, Half) ->
    append(Half, NewPrefix, Prefix),
    x_longest_satisfiable_prefix(x_append_and_eval(Eval, Half),
    Tail, NewPrefix, Complement)
    ;
    x_longest_satisfiable_prefix(Eval, Half, Prefix, Suffix),
    append(Suffix, Tail, Complement)
).

x_marked_as_false(Markers, Set):-
    member(FalseSet, Markers),
    subseq0(Set, FalseSet).

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

x_maxsolver_by_longest_segment(Eval, Segment, Prefix, Suffix, Solver):-
    append(Prefix0, [_], Prefix),
    Prefix0 \= [],!,
    maxsolver_by_longest_segment(
    x_prepend_and_eval(Eval, Segment), Prefix0, PrefixSolver),
    append(PrefixSolver, Segment, NewSegment),
    x_maxsolver_by_longest_segment(Eval, NewSegment, [], Suffix, Solver).

x_maxsolver_by_longest_segment(_, Segment, _, [], Segment):-!.

x_maxsolver_by_longest_segment(_, Segment, _, [_], Segment):-!.

x_maxsolver_by_longest_segment(Eval, Segment, _, [_|Suffix], Solver):-
    append(Segment, SuffixSolver, Solver),
    maxsolver_by_longest_segment(
    x_append_and_eval(Eval, Segment), Suffix, SuffixSolver).

x_maxsolver_exact_with_marker(Eval, Set, Markers, L, U, Solver):-
    L is U-1,!,
    % x_print_debug_msg(Markers, L, U),
    x_satisfiable_subset_of_length(Eval, Set, Markers, L, Solver).

x_maxsolver_exact_with_marker(Eval, Set, Markers, L, U, Solver):-
    % x_print_debug_msg(Markers, L, U),
    Half is (L+U) // 2,
    Goal = x_existis_satisfiable_subset_of_length(Eval, Set, Markers, Half, FalseSets),
    minimal_timeout(MinTimeout),
    maximal_timeout(MaxTimeout),
    Time is max(integer(1/(U-L)*MaxTimeout), MinTimeout),
    ( time_out(Goal, Time, Res) ->
    ( Res = time_out ->
    LL is L+1,
    Solver = timeout(Solver0),
    x_maxsolver_exact_with_marker(Eval, Set, Markers, L, LL, Solver0)
    ;
    append(FalseSets, Markers, NewMarkers),
    x_maxsolver_exact_with_marker(Eval, Set, NewMarkers, Half, U, Solver)
    )
    ;
    x_maxsolver_exact_with_marker(Eval, Set, Markers, L, Half, Solver)
).

x_method_by_length(maxsolver_exact_with_marker, 10).

x_method_by_length(maxsolver_by_longest_segment, 18).

x_precalc(_, _, L, U, []):-
    L > U,!.

x_precalc(Eval, Set, L, U, Markers):-
    findall(Subset, x_false_subset(Eval, Set, L, Subset), Subsets),
    append(Subsets, NewMarkers, Markers),
    LL is L+1,
    x_precalc(Eval, Set, LL, U, NewMarkers).

x_prepend_and_eval(Eval, Suffix, Set):-
    append(Set, Suffix, NewSet),
    call(Eval, NewSet).

x_satisfiable_subset_of_length(Eval, Set, Markers, L, Subset):-
    length(Subset, L),
    subseq0(Set, Subset),
    \+x_marked_as_false(Markers, Subset),
    call(Eval, Subset).

x_shorter_or_same_length_list(x(L1,_,_), x(L2,_,_)):-
    shorter_list(L1, L2).

x_shorter_or_same_length_list(x(L1,_,S1), x(L2,_,S2)):-
    same_length(L1, L2),
    ( shorter_list(S1, S2); same_length(S1, S2) ).