1		% (c) 2020-2022 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(optimizing_solver,[optimizing_solve_predicate/5,
6		optimizing_solve_predicate/7, % with extra optimizing expression
7		maxsolve_predicate/4,
8		minsolve_predicate/4,
9		b_set_up_maximally_valid_state/2
10		]).
11
12		:- use_module(probsrc(module_information),[module_info/2]).
13		:- module_info(group,cbc).
14		:- module_info(description,'This module can be used to find optimal (maximal/minimal) solutions to a predicate.').
15
16
17		:- use_module(probsrc(b_interpreter),[b_test_boolean_expression/4, b_compute_expression/5,set_up_typed_localstate/6]).
18		:- use_module(probsrc(bsyntaxtree), [get_texpr_type/2]).
19		:- use_module(probsrc(kernel_waitflags)).
20		:- use_module(probsrc(error_manager)).
21		:- use_module(probsrc(b_enumerate), [b_tighter_enumerate_all_values/2]).
22
23
24		% ------------------
25
26		:- use_module(probsrc(state_space),[get_constants_state_for_id/2]).
27		:- use_module(probsrc(store),[normalise_store/2]).
28		:- use_module(probsrc(bmachine),[b_get_machine_constants/1,
29		b_get_machine_variables/1, b_get_invariant_from_machine/1]).
30
31		% find a maximal model to the Invariant based upon current constant valuation
32		b_set_up_maximally_valid_state(ID,ResultState) :-
33		(get_constants_state_for_id(ID,ConstantsState) -> true
34		; b_get_machine_constants([]) -> ConstantsState=[]
35		; add_error(optimizing_solver,'Illegal state, please set-up the constants first:',ID),
36		fail % TO DO: b_get_properties_from_machine
37		),
38		% TO DO: treat case if ID=root and we have Constants !
39		b_get_machine_variables(Variables),
40		b_get_invariant_from_machine(Invariant),
41		% TO DO: use current variable values as first solution
42		maxsolve_predicate(ConstantsState,Variables,Invariant,LocalState),
43		normalise_store(LocalState,NormalisedState),
44		append(ConstantsState,NormalisedState,ResultState).
45
46		% ------------------
47
48		% find a maximal model for TypedPred with free variables Parameters in given expanded state EState
49		% return solution found for Parameters in LocalState
50		maxsolve_predicate(EState, Parameters,TypedPred,LocalState) :-
51		optimizing_solve_predicate(maximizing,EState, Parameters,TypedPred,LocalState).
52		% find a minimal model
53		minsolve_predicate(EState, Parameters,TypedPred,LocalState) :-
54		optimizing_solve_predicate(minimizing,EState, Parameters,TypedPred,LocalState).
55
56		:- use_module(probsrc(bsyntaxtree), [create_couple/2]).
57		% similar to test_bool_exists in eval_strings, but finds optimal solution:
58		optimizing_solve_predicate(OptMode,EState, Parameters,TypedPred,LocalState) :-
59		create_couple(Parameters,OptimizingExpr),
60		optimizing_solve_predicate(OptMode,EState, Parameters,TypedPred,OptimizingExpr,_,LocalState).
61
62		optimizing_solve_predicate(OptMode,EState, Parameters,TypedPred,OptimizingExpr,OptValue,LocalState) :-
63		%init_wait_flags(WF,[expansion_context(optimize_pred,Parameters)]),
64		init_quantifier_wait_flag(no_wf_available,optimize,Parameters,SolTuple,unknown,WF),
65		set_up_typed_localstate(Parameters,SolTuple,TypedVals,[],LocalState,positive),
66		b_tighter_enumerate_all_values(TypedVals,WF), % TODO: check if we can use b_tighter_enumerate_values_in_ctxt
67		b_test_boolean_expression(TypedPred,LocalState,EState,WF), % test predicate to satisfy
68		b_compute_expression(OptimizingExpr,LocalState,EState,OptValue,WF), % compute value to optimise
69		get_texpr_type(OptimizingExpr,OptType), % type of value to optimise
70		format('Starting ~w solver (~w)~n',[OptMode,LocalState]),
71		format('Optimizing: ',[]),translate:print_bexpr(OptimizingExpr),nl,
72		safe_ground_wait_flag0(WF), % avoid doing deterministic computations every time in ground_for_optimal_sol
73
74		% TO DO: we could select a subset of Parameters and SolTuple to optimize
75
76		catch(
77		ground_for_optimal_sol(1,OptMode,OptType,OptValue, WF,LocalState),
78		user_interrupt_signal,
79		(add_warning(optimizing_solver,'Search for optimal solution interrupted by user (CTRL-C): ',OptMode,Parameters),
80		fail)
81		).
82		optimizing_solve_predicate(_, _,_,_,_,OptValue,LocalState) :-
83		get_solution(OptValue,LocalState).
84
85
86
87		% TO DO: check for enumeration warnings, see e.g. gol_v2
88		% TO DO: add version with time-out and maximal number of improvements?
89		% TO DO: allow to pass initial solution (which could be solved using partitioning into components)
90		% TO DO: try to improve by component ? or we simply assume partitioning is done beforehand.
91
92		:- dynamic non_det_flag/0.
93		safe_ground_wait_flag0(WF) :- retractall(non_det_flag),
94		ground_wait_flag0(WF),
95		(non_det_flag -> add_warning(optimizing_solver,'Non-determinsm during WF0 grounding: ',WF)
96		; assertz(non_det_flag)).
97
98		:- dynamic best_sol_found/2.
99		% we store the best solution found
100		% we avoid setting up the constraints completely fresh, we just backtrack to before
101		% grounding waitflags and add the constraint that we should improve
102		ground_for_optimal_sol(Count,OptMode,OptType,OptValue,WF,LocalState) :-
103		((ground_wait_flags(WF)
104		-> format('Found solution at step ~w: ~w~n',[Count,OptValue]),
105		retractall(best_sol_found(_,_)),
106		asserta(best_sol_found(OptValue,LocalState)),
107		fail % backtrack and undo ground_wait_flags above
108		% TO DO: we could experiment with also backtracking beyond last best_sol_found predicate
109		; true % no more optimization possible
110		)
111		-> fail
112		; C1 is Count+1,
113		%print(improve_upon(BestSolTuple)),nl,
114		ground_for_optimal_sol_with_reset(C1,OptMode,OptType,OptValue,WF,LocalState)
115		).
116
117		:-if(1=2).
118		% a version which accumulates the improve constraints and does not remove them
119		ground_for_optimal_sol_with_reset(C1,OptMode,OptType,OptValue,WF,LocalState) :-
120		add_improve_constraint(OptMode,OptType,OptValue,WF),
121		ground_for_optimal_sol(C1,OptMode,OptType,OptValue,WF,LocalState).
122		:- else.
123		% a version which removes the previous improvement constraint and adds a new one
124		% requires transitivity of the improve constraints
125		ground_for_optimal_sol_with_reset(Count,OptMode,OptType,OptValue,WF,LocalState) :-
126		(( add_improve_constraint(OptMode,OptType,OptValue,WF),
127		ground_wait_flags(WF)
128		-> format('Found improved solution at step ~w: ~w~n',[Count,OptValue]),
129		retractall(best_sol_found(_,_)),
130		asserta(best_sol_found(OptValue,LocalState)),
131		fail % backtrack and undo ground_wait_flags and add_improve_constraint above
132		; true % no more optimization possible
133		)
134		-> fail
135		; C1 is Count+1,
136		ground_for_optimal_sol_with_reset(C1,OptMode,OptType,OptValue,WF,LocalState)
137		).
138		:-endif.
139
140		:- use_module(probsrc(kernel_objects),[not_equal_object_wf/3]).
141		add_improve_constraint(OptMode,OptType,OptValue,WF) :-
142		best_sol_found(BestSolSoFar,_),!,
143		copy_wf_start(WF,improve_upon,CWF), % unset WF0 in CWF in case it is set in WF
144		not_equal_object_wf(OptValue,BestSolSoFar,CWF), % avoid finding same solution again
145		(OptMode = maximizing
146		-> better_or_equal(OptType,OptValue,BestSolSoFar,CWF) % find at least as good a solution
147		; better_or_equal(OptType,BestSolSoFar,OptValue,CWF)
148		),
149		copy_wf_finish(WF,CWF).
150
151		get_solution(OptVal,LocalState) :-
152		format('No more optimizing possible~n',[]),
153		retract(best_sol_found(OptVal,LocalState)).
154		%format('Solution=~w~n',[LocalState]).
155
156
157
158
159
160		% TO DO: provide possibility to provide custom optimization function, treat total functions, ... differently
161		% code related to LEQ_SYM_BREAK, LEQ_SYM
162
163		:- use_module(probsrc(kernel_objects),[greater_than_equal/2, less_than_equal_direct/2, check_subset_of_wf/3]).
164		better_or_equal(integer,NewVal,BestVal,_WF) :- greater_than_equal(NewVal,BestVal). % TODO: use absolute value?
165		better_or_equal(boolean,B1,B2,_WF) :- !, bool_geq(B1,B2).
166		better_or_equal(boolean,_,pred_false,_WF).
167		better_or_equal(couple(T1,T2),(N1,N2),(B1,B2),WF) :- better_or_equal(T1,N1,B1,WF), better_or_equal(T2,N2,B2,WF).
168		better_or_equal(set(_),NewVal,BestVal,WF) :- check_subset_of_wf(BestVal,NewVal,WF).
169		better_or_equal(seq(_),NewVal,BestVal,WF) :- check_subset_of_wf(BestVal,NewVal,WF).
170		better_or_equal(string,NewVal,BestVal,_WF) :- NewVal=BestVal. % possibly use length, prefix or @< order ?
171		better_or_equal(global(G),fd(V1,G),fd(V2,G),_WF) :- less_than_equal_direct(V2,V1). % use fd(_,_) numbering
172		better_or_equal(record(Fields),rec(F1),rec(F2),WF) :- better_or_equal_fields(Fields,F1,F2,WF).
173		better_or_equal(freetype(_),V,V,_). % TO DO: add support for freetypes
174
175
176
177		% one of the arguments is instantiated at least; otherwise we would need block declaration
178		bool_geq(B1,B2) :- var(B1),!, (B2=pred_true -> B1=pred_true ; true).
179		bool_geq(pred_true,_).
180		bool_geq(pred_false,pred_false).
181
182		better_or_equal_fields([],[],[],_).
183		better_or_equal_fields([field(Name,Type)|TT],[field(Name,V1)|T1],[field(Name,V2)|T2],WF) :-
184		better_or_equal(Type,V1,V2,WF),
185		better_or_equal_fields(TT,T1,T2,WF).
186
187		% examples for REPL:
188		% :max x:BOOL & y:BOOL & z:BOOL & (x/=y or y/=z)
189		% :max x <: 1..10 & y <: 1..10 & x /\ y = {} & 5 : x \/ y & card(x)=card(y)
190		% :max x:BOOL & y:BOOL & z:BOOL & (x=TRUE => y=TRUE) & (y=TRUE => z=TRUE)
191		% :max n=8 & n1=n-1 & q<:(1..n1)*(1..n1) & !(x,y).(x|->y:q => x/=y)
192