1 % (c) 2009-2025 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 :- meta_predicate maxsolver(1,-,-).
18 :- meta_predicate maxsolver(-,1,-,-).
19 :- meta_predicate maxsolver_by_longest_prefix(1,-,-).
20 :- meta_predicate x_append_and_eval(1,-,-).
21 :- meta_predicate x_prepend_and_eval(1,-,-).
22
23 :- meta_predicate longest_satisfiable_prefix(1,-,-,-).
24 :- meta_predicate x_longest_satisfiable_prefix(1,-,-,-).
25 :- meta_predicate successful_call(1,-).
26 :- meta_predicate satisfiable_segment(1,-,-,-,-).
27 :- meta_predicate longest_satisfiable_segment(1,-,-,-,-).
28 :- meta_predicate maxsolver_by_longest_segment(1,-,-).
29 :- meta_predicate x_maxsolver_by_longest_segment(1,-,-,-,-).
30
31 :- meta_predicate maxsolver_exact_with_marker(1,-,-).
32 :- meta_predicate x_precalc(1,-,-,-,-).
33 :- meta_predicate x_false_subset_til_true(1,-,-,-,-).
34 :- meta_predicate x_existis_satisfiable_subset_of_length(1,-,-,-,-).
35 :- meta_predicate x_satisfiable_subset_of_length(1,-,-,-,-).
36 :- meta_predicate x_maxsolver_exact_with_marker(1,-,-,-,-,-).
37 :- meta_predicate x_false_subset(1,-,-,-).
38
39 :- use_module(library(lists)).
40 :- use_module(library(timeout)).
41 :- use_module(probsrc(error_manager), [time_out_with_enum_warning_one_solution/4, is_time_out_result/1]).
42
43
44 :- use_module(probsrc(preferences),[get_preference/2]).
45 minimal_timeout(Val) :- get_preference(formula_tree_minimal_timeout,Val). % Default 1000
46 maximal_timeout(Val) :- get_preference(formula_tree_maximal_timeout,Val). % Default 30000
47
48
49
50 maxsolver(Eval, Set, Solver):-
51 maxsolver(automatic, Eval, Set, Solver).
52
53
54
55 maxsolver(automatic, Eval, Set, Solver):-
56 length(Set, L),
57 x_method_by_length(Method, MaxLength),
58 L =< MaxLength,!,
59 call(Method, Eval, Set, Solver).
60
61 maxsolver(automatic, Eval, Set, Solver):-
62 maxsolver_by_longest_prefix(Eval, Set, Solver).
63
64
65 x_method_by_length(maxsolver_exact_with_marker, 10).
66 x_method_by_length(maxsolver_by_longest_segment, 18).
67
68
69
70 x_append_and_eval(Eval, Prefix, Set):-
71 append(Prefix, Set, NewSet),
72 successful_call(Eval, NewSet).
73
74 x_prepend_and_eval(Eval, Suffix, Set):-
75 append(Set, Suffix, NewSet),
76 successful_call(Eval, NewSet).
77
78
79 longest_satisfiable_prefix(Eval, Set, Prefix, R) :-
80 successful_call(Eval, Set),!, Prefix=Set,
81 R=[].
82 longest_satisfiable_prefix(Eval, Set, Prefix, Complement) :-
83 x_longest_satisfiable_prefix(Eval, Set, Prefix, Complement).
84
85 x_longest_satisfiable_prefix(_, [C], [], [C]) :- !.
86 % x_longest_satisfiable_prefix(_, [], [], []) :- !. TODO: Check if this needs to be added
87 x_longest_satisfiable_prefix(Eval, Set, Prefix, Complement):-
88 length(Set, Length),
89 HalfLength is Length // 2,
90 append_length(Half, Tail, Set,HalfLength),
91 ( successful_call(Eval, Half) ->
92 append(Half, NewPrefix, Prefix),
93 x_longest_satisfiable_prefix(x_append_and_eval(Eval, Half),
94 Tail, NewPrefix, Complement)
95 ;
96 x_longest_satisfiable_prefix(Eval, Half, Prefix, Suffix),
97 append(Suffix, Tail, Complement)
98 ).
99
100 % perform call (bvisual_any_maxsolver:x_check) with time-out and catch enum warnings
101 successful_call(Eval,Set) :- length(Set,Len),
102 minimal_timeout(MinTimeout),
103 maximal_timeout(MaxTimeout),
104 Time is min(MaxTimeout, Len*MinTimeout),
105 time_out_with_enum_warning_one_solution(call(Eval, Set), Time, Res,clear_errors),
106 \+ is_time_out_result(Res).
107
108
109
110 satisfiable_segment(_, [], [], [], []) :- !.
111 satisfiable_segment(Eval, Set, Segment, Prefix, Suffix):-
112 append(Prefix, Subset, Set),
113 Subset\=[],
114 longest_satisfiable_prefix(Eval, Subset, Segment, Suffix),
115 ( Suffix = [],! ; true ).
116
117
118
119 longest_satisfiable_segment(Eval, Set, Segment, Prefix, Suffix):-
120 findall(
121 x(Segment0, Prefix0, Suffix0),
122 satisfiable_segment(Eval, Set, Segment0, Prefix0, Suffix0),
123 Segments),
124 max_member(
125 x_shorter_or_same_length_list,
126 x(Segment, Prefix, Suffix),
127 Segments).
128
129
130 x_shorter_or_same_length_list(x(L1,_,_), x(L2,_,_)):-
131 shorter_list(L1, L2).
132
133 x_shorter_or_same_length_list(x(L1,_,S1), x(L2,_,S2)):-
134 same_length(L1, L2),
135 ( shorter_list(S1, S2); same_length(S1, S2) ).
136
137
138 maxsolver_by_longest_segment(Eval, Set, Solver) :-
139 longest_satisfiable_segment(Eval, Set, Segment, Prefix, Suffix),
140 x_maxsolver_by_longest_segment(Eval, Segment, Prefix, Suffix, Solver).
141
142
143 x_maxsolver_by_longest_segment(_, [], _, _, []):-!.
144
145 x_maxsolver_by_longest_segment(Eval, Segment, Prefix, Suffix, Solver):-
146 append(Prefix0, [_], Prefix),
147 Prefix0 \= [],!,
148 maxsolver_by_longest_segment(
149 x_prepend_and_eval(Eval, Segment), Prefix0, PrefixSolver),
150 append(PrefixSolver, Segment, NewSegment),
151 x_maxsolver_by_longest_segment(Eval, NewSegment, [], Suffix, Solver).
152
153 x_maxsolver_by_longest_segment(_, Segment, _, [], Segment):-!.
154
155 x_maxsolver_by_longest_segment(_, Segment, _, [_], Segment):-!.
156
157 x_maxsolver_by_longest_segment(Eval, Segment, _, [_|Suffix], Solver):-
158 append(Segment, SuffixSolver, Solver),
159 maxsolver_by_longest_segment(
160 x_append_and_eval(Eval, Segment), Suffix, SuffixSolver).
161
162
163
164 maxsolver_by_longest_prefix(_, Set, Solver) :- !, Set=1,Solver=1.
165 maxsolver_by_longest_prefix(Eval, Set, Solver):-
166 longest_satisfiable_prefix(Eval, Set, Prefix, Tail),!,
167 ( Tail = [_|NewSet] ->
168 append(Prefix, SubSolver, Solver),
169 maxsolver_by_longest_prefix(
170 x_append_and_eval(Eval, Prefix), NewSet, SubSolver)
171 ;
172 Solver = Prefix
173 ).
174
175 %x_print_debug_msg(Markers, L, U):-
176 % print(bounds(L,U)),nl, length(Markers, Length), print(markers(Length)), nl, flush_output.
177
178
179
180 maxsolver_exact_with_marker(Eval, Set, Solver):-
181 successful_call(Eval, Set),!, Solver=Set.
182 maxsolver_exact_with_marker(Eval, Set, Solver):-
183 length(Set, Length),
184 (Length == 0
185 -> PrecalcBound is 1
186 ; PrecalcBound is max(msb(Length) - 1, 1)),
187 x_precalc(Eval, Set, 1, PrecalcBound, Markers),
188 x_maxsolver_exact_with_marker(Eval, Set, Markers, 0, Length, Solver).
189
190
191 x_precalc(_, _, L, U, []):-
192 L > U,!.
193
194 x_precalc(Eval, Set, L, U, Markers):-
195 findall(Subset, x_false_subset(Eval, Set, L, Subset), Subsets),
196 append(Subsets, NewMarkers, Markers),
197 LL is L+1,
198 x_precalc(Eval, Set, LL, U, NewMarkers).
199
200
201 x_false_subset(Eval, Set, L, Subset):-
202 length(Subset, L),
203 subseq0(Set, Subset),
204 \+ successful_call(Eval, Subset).
205
206 x_maxsolver_exact_with_marker(Eval, Set, Markers, L, U, Solver):-
207 L is U-1,!,
208 % x_print_debug_msg(Markers, L, U),
209 x_satisfiable_subset_of_length(Eval, Set, Markers, L, Solver).
210
211 x_maxsolver_exact_with_marker(Eval, Set, Markers, L, U, Solver):-
212 % x_print_debug_msg(Markers, L, U),
213 Half is (L+U) // 2,
214 Goal = x_existis_satisfiable_subset_of_length(Eval, Set, Markers, Half, FalseSets),
215 minimal_timeout(MinTimeout),
216 maximal_timeout(MaxTimeout),
217 Time is max(integer(1/(U-L)*MaxTimeout), MinTimeout),
218 ( time_out_with_enum_warning_one_solution(Goal, Time, Res,clear_errors) ->
219 ( is_time_out_result(Res) ->
220 LL is L+1,
221 Solver = timeout(Solver0),
222 x_maxsolver_exact_with_marker(Eval, Set, Markers, L, LL, Solver0)
223 ;
224 append(FalseSets, Markers, NewMarkers),
225 x_maxsolver_exact_with_marker(Eval, Set, NewMarkers, Half, U, Solver)
226 )
227 ;
228 x_maxsolver_exact_with_marker(Eval, Set, Markers, L, Half, Solver)
229 ).
230
231
232 x_satisfiable_subset_of_length(Eval, Set, Markers, L, Subset):-
233 length(Subset, L),
234 subseq0(Set, Subset),
235 \+x_marked_as_false(Markers, Subset),
236 successful_call(Eval, Subset).
237
238 :- public x_existis_satisfiable_subset_of_length/5.
239 x_existis_satisfiable_subset_of_length(Eval, Set, Markers, Length, FalseSets):-
240 findall(Subset,
241 x_false_subset_til_true(Eval, Set, Markers, Length, Subset),
242 Sets),!,
243 append(FalseSets, [xxx], Sets).
244
245 x_false_subset_til_true(Eval, Set, Markers, Length, Subset):-
246 length(Subset0,Length),
247 subseq0(Set,Subset0),
248 \+x_marked_as_false(Markers, Subset0),
249 ( successful_call(Eval, Subset0) ->
250 !, Subset = xxx
251 ;
252 Subset = Subset0
253 ).
254
255 x_marked_as_false(Markers, Set):-
256 member(FalseSet, Markers),
257 subseq0(Set, FalseSet).