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