1		% (c) 2009-2024 Lehrstuhl fuer Softwaretechnik und Programmiersprachen,
2		% Heinrich Heine Universitaet Duesseldorf
3		% This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html)
4
5		:-module(maxsolver, [
6		maxsolver/3,
7		maxsolver_by_longest_prefix/3,
8		maxsolver_by_longest_segment/3,
9		maxsolver_exact_with_marker/3,
10		longest_satisfiable_prefix/4
11		]).
12
13		:- use_module(probsrc(module_information)).
14		:- module_info(group,dot).
15		:- module_info(description,'Finds a maximally satisfiable subset for predicates; used by bvisual_any_maxsolver.').
16
17		:- use_module(library(lists)).
18		:- use_module(library(timeout)).
19
20		:- use_module(probsrc(preferences),[get_preference/2]).
21		minimal_timeout(Val) :- get_preference(formula_tree_minimal_timeout,Val). % Default 1000
22		maximal_timeout(Val) :- get_preference(formula_tree_maximal_timeout,Val). % Default 30000
23
24
25		:- meta_predicate maxsolver(1,-,-).
26		:- meta_predicate maxsolver(-,1,-,-).
27		maxsolver(Eval, Set, Solver):-
28		maxsolver(automatic, Eval, Set, Solver).
29
30
31		:- meta_predicate maxsolver_by_longest_prefix(1,-,-).
32
33		maxsolver(automatic, Eval, Set, Solver):-
34		length(Set, L),
35		x_method_by_length(Method, MaxLength),
36		L =< MaxLength,!,
37		call(Method, Eval, Set, Solver).
38
39		maxsolver(automatic, Eval, Set, Solver):-
40		maxsolver_by_longest_prefix(Eval, Set, Solver).
41
42
43		x_method_by_length(maxsolver_exact_with_marker, 10).
44		x_method_by_length(maxsolver_by_longest_segment, 18).
45
46
47
48		:- meta_predicate x_append_and_eval(1,-,-).
49		x_append_and_eval(Eval, Prefix, Set):-
50		append(Prefix, Set, NewSet),
51		call(Eval, NewSet).
52
53		:- meta_predicate x_prepend_and_eval(1,-,-).
54		x_prepend_and_eval(Eval, Suffix, Set):-
55		append(Set, Suffix, NewSet),
56		call(Eval, NewSet).
57
58		x_half_length(List, Smaller):-
59		length(List, Length),
60		Half is Length // 2,
61		length(Smaller, Half).
62
63
64		:- meta_predicate longest_satisfiable_prefix(1,-,-,-).
65		:- meta_predicate x_longest_satisfiable_prefix(1,-,-,-).
66
67		longest_satisfiable_prefix(Eval, Set, Prefix, R) :-
68		call(Eval, Set),!, Prefix=Set,
69		R=[].
70		longest_satisfiable_prefix(Eval, Set, Prefix, Complement) :-
71		x_longest_satisfiable_prefix(Eval, Set, Prefix, Complement).
72
73		x_longest_satisfiable_prefix(_, [C], [], [C]):-!.
74		x_longest_satisfiable_prefix(Eval, Set, Prefix, Complement):-
75		x_half_length(Set, Half),
76		append(Half, Tail, Set),
77		( call(Eval, Half) ->
78		append(Half, NewPrefix, Prefix),
79		x_longest_satisfiable_prefix(x_append_and_eval(Eval, Half),
80		Tail, NewPrefix, Complement)
81		;
82		x_longest_satisfiable_prefix(Eval, Half, Prefix, Suffix),
83		append(Suffix, Tail, Complement)
84		).
85
86
87
88		:- meta_predicate satisfiable_segment(1,-,-,-,-).
89		satisfiable_segment(_, [], [], [], []) :- !.
90		satisfiable_segment(Eval, Set, Segment, Prefix, Suffix):-
91		append(Prefix, Subset, Set),
92		Subset\=[],
93		longest_satisfiable_prefix(Eval, Subset, Segment, Suffix),
94		( Suffix = [],! ; true ).
95
96
97
98		:- meta_predicate longest_satisfiable_segment(1,-,-,-,-).
99		longest_satisfiable_segment(Eval, Set, Segment, Prefix, Suffix):-
100		findall(
101		x(Segment0, Prefix0, Suffix0),
102		satisfiable_segment(Eval, Set, Segment0, Prefix0, Suffix0),
103		Segments),
104		max_member(
105		x_shorter_or_same_length_list,
106		x(Segment, Prefix, Suffix),
107		Segments).
108
109
110		x_shorter_or_same_length_list(x(L1,_,_), x(L2,_,_)):-
111		shorter_list(L1, L2).
112
113		x_shorter_or_same_length_list(x(L1,_,S1), x(L2,_,S2)):-
114		same_length(L1, L2),
115		( shorter_list(S1, S2); same_length(S1, S2) ).
116
117
118		:- meta_predicate maxsolver_by_longest_segment(1,-,-).
119		:- meta_predicate x_maxsolver_by_longest_segment(1,-,-,-,-).
120		maxsolver_by_longest_segment(Eval, Set, Solver) :-
121		longest_satisfiable_segment(Eval, Set, Segment, Prefix, Suffix),
122		x_maxsolver_by_longest_segment(Eval, Segment, Prefix, Suffix, Solver).
123
124
125		x_maxsolver_by_longest_segment(_, [], _, _, []):-!.
126
127		x_maxsolver_by_longest_segment(Eval, Segment, Prefix, Suffix, Solver):-
128		append(Prefix0, [_], Prefix),
129		Prefix0 \= [],!,
130		maxsolver_by_longest_segment(
131		x_prepend_and_eval(Eval, Segment), Prefix0, PrefixSolver),
132		append(PrefixSolver, Segment, NewSegment),
133		x_maxsolver_by_longest_segment(Eval, NewSegment, [], Suffix, Solver).
134
135		x_maxsolver_by_longest_segment(_, Segment, _, [], Segment):-!.
136
137		x_maxsolver_by_longest_segment(_, Segment, _, [_], Segment):-!.
138
139		x_maxsolver_by_longest_segment(Eval, Segment, _, [_|Suffix], Solver):-
140		append(Segment, SuffixSolver, Solver),
141		maxsolver_by_longest_segment(
142		x_append_and_eval(Eval, Segment), Suffix, SuffixSolver).
143
144
145
146		maxsolver_by_longest_prefix(_, Set, Solver) :- !, Set=1,Solver=1.
147		maxsolver_by_longest_prefix(Eval, Set, Solver):-
148		longest_satisfiable_prefix(Eval, Set, Prefix, Tail),!,
149		( Tail = [_|NewSet] ->
150		append(Prefix, SubSolver, Solver),
151		maxsolver_by_longest_prefix(
152		x_append_and_eval(Eval, Prefix), NewSet, SubSolver)
153		;
154		Solver = Prefix
155		).
156
157		%x_print_debug_msg(Markers, L, U):-
158		% print(bounds(L,U)),nl, length(Markers, Length), print(markers(Length)), nl, flush_output.
159
160		:- meta_predicate maxsolver_exact_with_marker(1,-,-).
161		:- meta_predicate x_precalc(1,-,-,-,-).
162		:- meta_predicate x_false_subset_til_true(1,-,-,-,-).
163		:- meta_predicate x_existis_satisfiable_subset_of_length(1,-,-,-,-).
164		:- meta_predicate x_satisfiable_subset_of_length(1,-,-,-,-).
165		:- meta_predicate x_maxsolver_exact_with_marker(1,-,-,-,-,-).
166		:- meta_predicate x_false_subset(1,-,-,-).
167
168
169		maxsolver_exact_with_marker(Eval, Set, Solver):-
170		call(Eval, Set),!, Solver=Set.
171		maxsolver_exact_with_marker(Eval, Set, Solver):-
172		length(Set, Length),
173		(Length == 0
174		-> PrecalcBound is 1
175		; PrecalcBound is max(msb(Length) - 1, 1)),
176		x_precalc(Eval, Set, 1, PrecalcBound, Markers),
177		x_maxsolver_exact_with_marker(Eval, Set, Markers, 0, Length, Solver).
178
179
180		x_precalc(_, _, L, U, []):-
181		L > U,!.
182
183		x_precalc(Eval, Set, L, U, Markers):-
184		findall(Subset, x_false_subset(Eval, Set, L, Subset), Subsets),
185		append(Subsets, NewMarkers, Markers),
186		LL is L+1,
187		x_precalc(Eval, Set, LL, U, NewMarkers).
188
189
190		x_false_subset(Eval, Set, L, Subset):-
191		length(Subset, L),
192		subseq0(Set, Subset),
193		\+call(Eval, Subset).
194
195		x_maxsolver_exact_with_marker(Eval, Set, Markers, L, U, Solver):-
196		L is U-1,!,
197		% x_print_debug_msg(Markers, L, U),
198		x_satisfiable_subset_of_length(Eval, Set, Markers, L, Solver).
199
200		x_maxsolver_exact_with_marker(Eval, Set, Markers, L, U, Solver):-
201		% x_print_debug_msg(Markers, L, U),
202		Half is (L+U) // 2,
203		Goal = x_existis_satisfiable_subset_of_length(Eval, Set, Markers, Half, FalseSets),
204		minimal_timeout(MinTimeout),
205		maximal_timeout(MaxTimeout),
206		Time is max(integer(1/(U-L)*MaxTimeout), MinTimeout),
207		( time_out(Goal, Time, Res) ->
208		( Res = time_out ->
209		LL is L+1,
210		Solver = timeout(Solver0),
211		x_maxsolver_exact_with_marker(Eval, Set, Markers, L, LL, Solver0)
212		;
213		append(FalseSets, Markers, NewMarkers),
214		x_maxsolver_exact_with_marker(Eval, Set, NewMarkers, Half, U, Solver)
215		)
216		;
217		x_maxsolver_exact_with_marker(Eval, Set, Markers, L, Half, Solver)
218		).
219
220
221		x_satisfiable_subset_of_length(Eval, Set, Markers, L, Subset):-
222		length(Subset, L),
223		subseq0(Set, Subset),
224		\+x_marked_as_false(Markers, Subset),
225		call(Eval, Subset).
226
227		:- public x_existis_satisfiable_subset_of_length/5.
228		x_existis_satisfiable_subset_of_length(Eval, Set, Markers, Length, FalseSets):-
229		findall(Subset,
230		x_false_subset_til_true(Eval, Set, Markers, Length, Subset),
231		Sets),!,
232		append(FalseSets, [xxx], Sets).
233
234		x_false_subset_til_true(Eval, Set, Markers, Length, Subset):-
235		length(Subset0,Length),
236		subseq0(Set,Subset0),
237		\+x_marked_as_false(Markers, Subset0),
238		( call(Eval, Subset0) ->
239		!, Subset = xxx
240		;
241		Subset = Subset0
242		).
243
244		x_marked_as_false(Markers, Set):-
245		member(FalseSet, Markers),
246		subseq0(Set, FalseSet).