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(bvisual_any_maxsolver, [any_maxsolver/5]).
6
7		:- use_module(probsrc(module_information),[module_info/2]).
8		:- module_info(group,dot).
9		:- module_info(description,'Tool for generating dot visualization of B predicates and expressions. Finds a maximally satisfiable subset for predicates.').
10
11		%:- use_module(library(ordsets)).
12		%:- use_module(library(timeout)).
13
14		:- use_module(probsrc(bsyntaxtree), [conjunction_to_list/2, conjunct_predicates/2]).
15		:- use_module(dotsrc(bvisual), [get_any/5]).
16		:- use_module(dotsrc(maxsolver)).
17
18		:- use_module(probsrc(error_manager), [add_message/4, time_out_with_enum_warning_one_solution/3, is_time_out_result/1]).
19
20		any_maxsolver(IDs, Condition, State, LocalState, NewLocalState):-
21		conjunction_to_list(Condition, Set),!,
22		length(Set, Count),
23		%Check = bvisual_any_maxsolver:x_check(IDs, LocalState, State), % inlined to enable InfoLog flow analysis
24		x_time_out_by_size(Count, TimeOut),
25		%print(time_out(maxsolver(Check),TimeOut,Res)),nl,
26		time_out_with_enum_warning_one_solution(maxsolver(bvisual_any_maxsolver:x_check(IDs, LocalState, State), Set, Solver0), TimeOut, Res),
27		!,
28		(
29		is_time_out_result(Res) ->
30		add_message(bvisual, 'Time out while searching solution of maximal size, looking for longest satisfiable prefix over ',IDs,Condition),
31		longest_satisfiable_prefix(bvisual_any_maxsolver:x_check(IDs, LocalState, State), Set, Solver, _)
32		;
33		Solver0 = time_out(Solver) ->
34		add_message(bvisual, 'Time out while searching for solution of maximal size over ',IDs,Condition)
35		;
36		Solver = Solver0
37		),
38		conjunct_predicates(Solver, SolverExpr),
39		get_any(IDs, SolverExpr, State, LocalState, NewLocalState).
40
41
42		:- use_module(probsrc(preferences)).
43
44		x_time_out_by_size(0, 10) :- !. % starting from sicstus 4.3, msb(0) throws an error
45		x_time_out_by_size(Size, TimeOut):-
46		preferences:get_preference(time_out, BaseTimeOut),
47		TimeOut is max(10,min(msb(Size), 3) * BaseTimeOut). /* Timeout must be at least 1 */
48
49
50		%
51		% Helpers
52		%
53		:- public x_check/4.
54		x_check(_, _, _, []) :- !.
55		x_check(IDs, LocalState, State, Subset):-
56		conjunct_predicates(Subset, LHS),!,
57		get_any(IDs, LHS, State, LocalState, _).