1		% (c) 2009-2026 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(succeed_max,[reset_max_reached/0, reset_max_reached/1,
6		max_reached/0, max_reached/1,
7		succeed_max_call/2, succeed_max_call_id/3,
8		succeed_max_initialise/0,
9		assert_max_reached/1 % mainly for operation caching
10		]).
11
12		:- use_module(tools).
13		:- use_module(debug,[debug_format/3]).
14
15		:- use_module(module_information).
16		:- module_info(group,infrastructure).
17		:- module_info(description,'This module provides a meta call to retrieve a specified maximum number of solutions.').
18
19		:- use_module(extension('counter/counter'),
20		[counter_init/0, new_counter/1, inc_counter/2, reset_counter/1]).
21
22		:- dynamic max_reached/1.
23
24	?	max_reached :- max_reached(_),!.
25
26		% assert that for Id a maximum number of solutions was reached,
27		% typically Id is an operation name; meaning that not all transitions were computed for it
28		assert_max_reached(Id) :-
29		(max_reached(Id) -> true
30		; assertz(max_reached(Id)),
31		debug_format(19,'Maximum solutions reached for ~w~n',[Id])
32		).
33
34		reset_max_reached(Id) :- retractall(max_reached(Id)).
35		reset_max_reached :-
36	?	(max_reached(_) -> retractall(max_reached(_)) ; true). % retractall seems sometimes expensive in SICStus
37
38		:- meta_predicate succeed_max_call(0,-).
39		:- meta_predicate succeed_max_call_id(+,0,-).
40
41		succeed_max_call(Call,MaxNrOfSols) :-
42	?	succeed_max_call_id('$unknown',Call,MaxNrOfSols).
43
44
45		succeed_max_initialise :- counter_init,new_counter(inits_found),new_counter(constants_found),new_counter(ops_found).
46
47		:- use_module(eventhandling,[register_event_listener/3]).
48		:- register_event_listener(specification_initialised,succeed_max_initialise,
49		'Initialise sols_found counter.').
50
51		succeed_max_call_id(Id,Call,MaxNrOfSols) :-
52		get_counter_name(Id,Counter),
53		reset_counter(Counter),
54	?	succeed_max_call_id_aux(Id,Counter,Call,MaxNrOfSols).
55
56		succeed_max_call_id_aux(Id,_,_Call,MaxNrOfSols) :-
57		MaxNrOfSols==0,!,
58		assert_max_reached(Id),fail.
59		succeed_max_call_id_aux(Id,Counter,Call,MaxNrOfSols) :- %print_message(max_call(Call,MaxnrOfSols)),
60	?	call(Call),
61		inc_counter(Counter,X1),
62		% print_message(sol(X1)), %
63		(X1>=MaxNrOfSols
64		-> (!, %print_message(max_sol_found(Call,X1,MaxNrOfSols)),
65		assert_max_reached(Id)
66		)
67		; true).
68
69		% use different counters so that we can have at least one of each succeed_max_call pending without interaction
70		get_counter_name(V,Name) :- var(V),!, Name=ops_found.
71		get_counter_name('$initialise_machine',Name) :- !, Name=inits_found.
72		get_counter_name('$setup_constants',Name) :- !,Name=constants_found.
73		get_counter_name(_,ops_found).
74