1		% (c) 2009-2019 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(solver_interface, [solve_predicate/3, solve_predicate/4, solve_predicate/5,
6		set_up_typed_localstate_for_pred/4,
7		type_check_in_machine_context/2,
8		predicate_uses_unfixed_deferred_set/1, predicate_uses_unfixed_deferred_set/2,
9		unfixed_typed_id_in_list/3,
10		call_with_smt_mode_enabled/1]).
11
12		:- use_module(module_information,[module_info/2]).
13		:- module_info(group,cbc).
14		:- module_info(description,'This module provides an interface to ProB\'s constraint solving kernel.').
15
16		:- use_module(library(lists), [include/3,keys_and_values/3]).
17
18		:- use_module(bmachine, [b_get_machine_variables/1, b_get_machine_constants/1, full_b_machine/1]).
19		:- use_module(btypechecker,[env_empty/1,opentype/5, add_identifiers_to_environment/3, env_store_operator/4, env_store_definition/3]).
20		:- use_module(b_global_sets, [is_b_global_constant/3,
21		b_global_set/1, unfixed_deferred_set/1,
22		contains_unfixed_deferred_set/1]).
23		:- use_module(b_interpreter, [set_up_typed_localstate/6]).
24		:- use_module(tools_timeout, [time_out_with_factor_call/4]).
25		:- use_module(bsyntaxtree, [find_typed_identifier_uses/3, find_typed_identifier_uses/2,
26		map_over_typed_bexpr/3, get_texpr_id/2, get_texpr_type/2, get_texpr_types/2]).
27		:- use_module(error_manager).
28		:- use_module(tools,[assert_once/1,foldl/5,foldl/4]).
29		:- use_module(translate, [translate_bvalue/2, translate_bvalue_with_limit/3]).
30		:- use_module(bmachine_structure,[get_section/3]).
31		:- use_module(debug,[debug_println/2]).
32		:- use_module(preferences).
33		:- use_module(eventhandling,[announce_event/1]).
34		:- use_module(smt_solvers_interface(smt_solvers_interface)).
35		:- use_module(store, [normalise_value_for_var/4]).
36
37		:- meta_predicate call_with_smt_mode_enabled(0).
38		%:- meta_predicate call_with_chr(0).
39		%call_with_chr(Call) :- call_with_preference(Call,use_chr_solver,true).
40
41
42		% :- meta_predicate call_with_smt_mode_enabled(0). % directive above for Spider
43		call_with_smt_mode_enabled(Call) :-
44		temporary_set_preference(use_smt_mode,true,SMT),
45		temporary_set_preference(use_clpfd_solver,true,CLPFD), % we also enable CLPFD
46		% TO DO: also enable CHR
47		call_cleanup( (Call,!),
48		(reset_temporary_preference(use_smt_mode,SMT),
49		reset_temporary_preference(use_clpfd_solver,CLPFD)
50		)).
51
52		% solve predicate finds *one* solution for predicate in State
53		solve_predicate(Pred,State,Res) :- solve_predicate(Pred,State,1,Res).
54		solve_predicate(Pred,State,TimeoutFactor,Res) :-
55		solve_predicate(Pred,State,TimeoutFactor,[use_smt_mode/true,use_clpfd_solver/true],Res).
56
57		% one could add a preference to try Z3 instead/or first:
58		%solve_predicate(Pred,State,TimeoutFactor,Options,RealRes) :-
59		% % preference(solve_predicates_with_z3,true),
60		% !, print(solve_with_z3),nl, translate:print_bexpr(Pred),nl,
61		% ((TimeoutFactor=1,Options=[]) -> true
62		% ; format('TO DO; ignoring Timeout Factor ~w and Options ~w for Z3~n',[TimeoutFactor,Options])),
63		% smt_solvers_interface:smt_solve_predicate(z3,Pred,State,RealRes),
64		% print(z3_result(RealRes)),nl.
65		solve_predicate(Pred,State,TimeoutFactor,Options,RealRes) :-
66		solve_predicate_with_options(Options,[],Pred,State,TimeoutFactor,Res), !,
67		if(solver_result(Res,Pred,State,Options,RealResBeforeFallback),true,
68		(add_internal_error('Unknown solver_result: ',Res),RealResBeforeFallback=error)),
69		fallback_to_smt_if_requested(RealResBeforeFallback,Pred,State,RealRes).
70
71		% no fallback if solution / contradiction
72		fallback_to_smt_if_requested(solution(S),_,_,Res) :- !, Res=solution(S).
73		fallback_to_smt_if_requested(contradiction_found,_,_,Res) :- !,Res=contradiction_found.
74		fallback_to_smt_if_requested(S,_,_,Res) :-
75		\+ preferences:get_preference(smt_supported_interpreter,true), ! , Res = S.
76		fallback_to_smt_if_requested(_,Pred,State,Res) :-
77		smt_solve_predicate(z3,Pred,State,Res), !.
78
79		solve_predicate_with_options([],RestOptions,Pred,State,TimeoutFactor,Res) :-
80		solve_predicate_direct(Pred,State,TimeoutFactor,RestOptions,Res).
81		solve_predicate_with_options([Option|T],RestOptions,Pred,State,TimeoutFactor,Res) :-
82		solve_with_option(Option,T,RestOptions,Pred,State,TimeoutFactor,Res).
83
84		solve_with_option('CHR',T,Rest,Pred,State,TimeoutFactor,Res) :- !,
85		solve_with_option(use_chr_solver/true,T,Rest,Pred,State,TimeoutFactor,Res).
86		solve_with_option('SMT',T,Rest,Pred,State,TimeoutFactor,Res) :- !,
87		solve_with_option(use_smt_mode/true,T,Rest,Pred,State,TimeoutFactor,Res).
88		solve_with_option('KODKOD',T,Rest,Pred,State,TimeoutFactor,Res) :- !,
89		solve_with_option(try_kodkod_on_load/true,T,Rest,Pred,State,TimeoutFactor,Res).
90		solve_with_option('SMT_SUPPORTED_INTERPRETER',T,Rest,Pred,State,TimeoutFactor,Res) :- !,
91		solve_with_option(smt_supported_interpreter/true,T,Rest,Pred,State,TimeoutFactor,Res).
92		solve_with_option('CLPFD',T,Rest,Pred,State,TimeoutFactor,Res) :- !,
93		solve_with_option(use_clpfd_solver/true,T,Rest,Pred,State,TimeoutFactor,Res).
94		solve_with_option(Pref/Val,T,Rest,Pred,State,TimeoutFactor,Res) :- !,
95		call_with_preference(solve_predicate_with_options(T,Rest,Pred,State,TimeoutFactor,Res),Pref,Val).
96		solve_with_option(Opt,T,Rest,Pred,State,TimeoutFactor,Res) :-
97		valid_option(Opt),!,
98		solve_predicate_with_options(T,[Opt|Rest],Pred,State,TimeoutFactor,Res).
99		solve_with_option(Opt,T,Rest,Pred,State,TimeoutFactor,Res) :-
100		add_warning(solve_with_option,'Unrecognised option: ',Opt),
101		solve_predicate_with_options(T,Rest,Pred,State,TimeoutFactor,Res).
102
103		valid_option(full_machine_state).
104		valid_option(solve_in_visited_state(S)) :- atomic(S).
105		valid_option(truncate(Limit)) :- number(Limit). % truncate pretty printing
106		valid_option(truncate). % 10000
107		valid_option(force_evaluation). % force evaluation of symbolic results
108
109		solve_predicate_direct(Pred,State,TimeoutFactor,Options,Res) :-
110		%temporary_set_preference(randomise_enumeration_order,true),
111		%temporary_set_preference(find_abort_values,true), % I am not sure we should do this; we want to find counter-examples quickly, we are less worried with finding WD-problems ?!
112
113		%temporary_set_preference(minint,-2147483648), % disabled to pass tests 1004,1015,..
114		%temporary_set_preference(maxint,2147483647),
115		(real_error_occurred -> reset_real_error_occurred, PrevErr=true ; PrevErr=false),
116
117		smt_solvers_interface:init,
118		announce_event(start_solving),
119		solve_predicate_aux(Pred,State,TimeoutFactor,Options,InnerRes),
120		announce_event(end_solving),
121
122		(InnerRes = overflow -> Res = overflow ; real_error_occurred -> Res = error; Res = InnerRes),
123		(PrevErr -> assert_real_error_occurred ; true). % re-establish real-error occured
124
125		%:- use_module(clpfd_interface,[clpfd_overflow_error_message/0]).
126		solve_predicate_aux(Pred,State,TimeoutFactor,Options,Res) :-
127		enter_new_error_scope(ScopeID,solve_predicate), %print(enter_scope(ScopeID)),nl,
128		call_cleanup(solve_predicate_aux1(Pred,State,TimeoutFactor,Options,Res),
129		exit_error_scope(ScopeID,_,solve_predicate_aux)).
130
131		solve_predicate_aux1(Pred,State,TimeoutFactor,Options,Res) :-
132		solve_predicate_aux2(Pred,State,TimeoutFactor,Options,Res),
133		!, % we only look for one solution
134		clear_enumeration_warnings. % avoid propagating them higher up
135		solve_predicate_aux1(_Pred,State,_TimeoutFactor,_Options,Res) :-
136		critical_enumeration_warning_occured_in_error_scope(A,B,C,D), % we did not find a solution: check for enum warnings
137		!,
138		clear_enumeration_warnings,
139		State = no_state,
140		Res = virtual_time_out(enumeration_warning(A,B,C,D,critical)).
141		solve_predicate_aux1(_Pred,State,_TimeoutFactor,_Options,Res) :-
142		State = no_state,
143		Res = no.
144
145
146		:- use_module(clpfd_interface,[catch_clpfd_overflow_call2/2]).
147		solve_predicate_aux2(Pred,State,TimeoutFactor,Options,Res) :-
148		%predicate_level_optimizations(Pred,OptPred), % is now done in b_interpreter_components; to avoid that CSE disrupts partitioning
149		catch_clpfd_overflow_call2(
150		solve_predicate_aux3(Pred,State,TimeoutFactor,Options,Res),
151		( %print(overflow),nl,trace,
152		%clpfd_interface:clpfd_overflow_warning_message, % message is already printed by catch_clpfd_overflow_call2
153		% we could try and solve without CLPFD ?!!
154		Res=overflow,State=no_state)).
155
156		/*
157		filter_global_identifiers([],[]).
158		filter_global_identifiers([Identifier|IDs],Out) :-
159		filter_global_identifiers(IDs,TempOut),
160		(is_global(Identifier)
161		-> Out = TempOut
162		; Out = [Identifier|TempOut]
163		).
164
165		is_global(Identifier) :-
166		get_texpr_id(Identifier,Name), get_texpr_type(Identifier,Type),
167		Type = global(Set), is_b_global_constant(Set,_Nr,Name).
168		is_global(Identifier) :-
169		get_texpr_id(Identifier,Name), get_texpr_type(Identifier,Type),
170		Type = set(global(Name)), b_global_set(Name).
171		*/
172
173		:- use_module(b_interpreter_components).
174		:- use_module('kodkod/kodkod',[apply_kodkod/3]).
175		:- use_module(specfile,[state_corresponds_to_set_up_constants/2]).
176		:- use_module(state_space,[visited_expression/2]).
177		:- use_module(library(lists),[maplist/2]).
178		solve_predicate_aux3(Pred,State,TimeoutFactor,Options,Res) :-
179		% find all identifiers used in the predicate and create a state
180		% was done by the caller, leading to code duplication
181		(member(full_machine_state,Options) -> get_full_machine_state_typed_identifiers(FilteredIdentifiers)
182		; find_typed_identifier_uses(Pred,FilteredIdentifiers)),
183		!,
184		% global constants should not appear in the state
185		% otherwise they treated are as variables by the solver
186		% -> we now call find_typed_identifier_uses; we used to call filter_global_identifiers(Identifiers,FilteredIdentifiers),
187		% state may be predefined / partially set up
188		apply_kodkod(FilteredIdentifiers,Pred,Pred2),
189		(member(solve_in_visited_state(StateID),Options)
190		-> set_up_typed_localstate_for_pred(FilteredIdentifiers,Pred2,TypedVals,State),
191		(visited_expression(StateID,StateExpr),
192		state_corresponds_to_set_up_constants(StateExpr,FullStore)
193		-> maplist(initialise_localstate(FullStore),State)
194		; StateID=root -> true
195		; add_internal_error('Illegal State:',use_visited_state(StateID))
196		)
197		; var(State)
198		-> set_up_typed_localstate_for_pred(FilteredIdentifiers,Pred2,TypedVals,State)
199		% TypedVals contains typedval(Val,Type,Var,TriggersEnumWarning)
200		% TO DO: add static_symmetry detection b_global_sets:static_symmetry_reduction_for_global_sets(State),
201		; add_warning(solve_predicate,'Non-variable state: ',State)
202		% TypedVals is unbound, is this a problem !?? TO DO: investigate
203		),
204		%tools_printing:print_term_summary(b_trace_test_components(Pred2,State,TypedVals)),nl,
205		b_interpreter_components:reset_component_info(false),
206		time_out_with_factor_call(
207		b_interpreter_components:b_trace_test_components(Pred2,State,TypedVals),
208		TimeoutFactor, [silent],
209		TO='time_out'),
210		(TO==time_out -> Res = TO ; Res = yes).
211
212		% set up a complete typed solver state for machine with all constants and variables, even if typing invariants removed and no reference anymore to variable in Invariant
213		% TypedVals need to be enumerated after calling solve_predicate, in case some variables are not constrained
214		get_full_machine_state_typed_identifiers(TIds) :-
215		b_get_machine_variables(Variables),
216		b_get_machine_constants(Constants), append(Constants,Variables,TIds).
217
218		:- use_module(static_ordering,[sort_ids_by_usage/4,reorder_state/3]).
219		set_up_typed_localstate_for_pred(CV,Pred,TypedVals,State) :-
220		(preferences:preference(use_static_ordering,true)
221		-> static_ordering:sort_ids_by_usage(CV,Pred,SortedVarlist,no_warnings) ,
222		set_up_typed_localstate(SortedVarlist,_FreshVars,TypedVals,[],SortedState,positive),
223		reorder_state(CV,SortedState,State) % SortedState can have issues with pack_state skeleton
224		; set_up_typed_localstate(CV,_FreshVars,TypedVals,[],State,positive)).
225
226		% initialise local state with values found in bind list
227		initialise_localstate(FullStore,bind(Var,Val)) :-
228		(member(bind(Var,VarVal),FullStore)
229		-> Val=VarVal ; true).
230
231		% translate solver_result for use by Disprover/Prover or similar:
232		solver_result(time_out,_P,_State,_,time_out).
233		solver_result(error,_P,_State,_,error).
234		solver_result(no,P,_State,_,Res) :-
235		% there are two cases in which we might have a false negative:
236		% we enumerated a critical variable
237		%\+ event_occurred_in_error_scope(enumeration_warning(_,_,_,_,critical)), % we now check this in solve_predicate_aux1
238		% or there are unfixed / deferred global sets involved.
239		(predicate_uses_unfixed_deferred_set(P,CType)
240		% no unfixed global sets involved -> real contradiction found
241		-> debug_println(10,solver_predicate_contains_unfixed_deferred_set(CType)),
242		Res=no_solution_found(unfixed_deferred_sets)
243		; Res=contradiction_found
244		).
245		solver_result(virtual_time_out(Reason),_P,_State,_,no_solution_found(Reason)) :-
246		true. % this is now checked in solve_predicate_aux1: event_occurred_in_error_scope(enumeration_warning(A,B,C,D,critical)).
247		solver_result(overflow,_P,_State,_,no_solution_found(clpfd_overflow)).
248		solver_result(yes,_P,State,Options,solution(Solution)) :-
249		findall(binding(Id,EValue,PPValue),
250		(member(bind(Id,Value),State),
251		(solver_pp_bvalue(Value,Options,EValue,PPValue) -> true ; PPValue='**pretty-print failed**')),
252		Solution).
253
254		% expand and pretty print solver result values:
255		solver_pp_bvalue(Value,Options,EValue,PPValue) :- member(force_evaluation,Options),!,
256		EXPAND=force,
257		normalise_value_for_var(solver_result,EXPAND,Value,EValue),
258		solver_pp_bvalue2(EValue,Options,PPValue).
259		solver_pp_bvalue(Value,Options,Value,PPValue) :- solver_pp_bvalue2(Value,Options,PPValue).
260
261		solver_pp_bvalue2(Value,Options,PPValue) :- member(truncate(Limit),Options),!,
262		translate_bvalue_with_limit(Value,Limit,PPValue). % should we also control expand_avl_upto ??
263		solver_pp_bvalue2(Value,Options,PPValue) :- member(truncate,Options),!,
264		translate_bvalue_with_limit(Value,10000,PPValue).
265		solver_pp_bvalue2(Value,_,PPValue) :- translate_bvalue(Value,PPValue).
266
267		% check if a typed expression references an unfixed deferred set in some inner node
268		predicate_uses_unfixed_deferred_set(TExpr) :- predicate_uses_unfixed_deferred_set(TExpr,_).
269
270		predicate_uses_unfixed_deferred_set(TExpr,CType) :-
271		unfixed_deferred_set(_), % check first if some unfixed deferred set exists
272		map_over_typed_bexpr(solver_interface:uses_unfixed_ds_aux,TExpr,CType).
273		:- public uses_unfixed_ds_aux/2.
274		uses_unfixed_ds_aux(TExpr,Type) :- get_texpr_type(TExpr,Type),
275		contains_unfixed_deferred_set(Type).
276
277		% find a typed id whose type references an unfixed deferred set
278		unfixed_typed_id_in_list(TID,CType,Constants) :-
279		unfixed_deferred_set(_), % check first if some unfixed deferred set exists
280		member(TID,Constants), get_texpr_type(TID,CType),
281		contains_unfixed_deferred_set(CType).
282
283		:- use_module(library(lists),[maplist/3, include/3]).
284		type_check_in_machine_context(Predicates, TPredicates) :-
285		% create an empty type environment
286		% and store the known types of variables / constants
287		% otherwise, we might be unable to type variables from
288		% machines somewhere in the refinement hierarchy
289		% (their typing predicate might not be in the hypothesis)
290		% Definitions are also added to the environment since the typechecker
291		% inlines definitions.
292		env_empty(E),
293		b_get_machine_variables(V), b_get_machine_constants(C),
294		% add theory operators
295		full_b_machine(Machine),
296		get_section(operators,Machine,Operators),
297		keys_and_values(Operators,Ids,Ops),
298		foldl(env_store_operator,Ids,Ops,E,EWithTheories),
299		get_section(definitions, Machine, Definitions),
300		foldl(env_store_definition, Definitions, EWithTheories, EWithDefinitions),
301		% constants and variables
302		findall(b(identifier(Name),global(GlobalSet),[enumerated_set_element]),is_b_global_constant(GlobalSet,_Nr,Name),GC),
303		findall(b(identifier(Set),set(global(Set)),[given_set]),b_global_set(Set),GS),
304		add_identifiers_to_environment(V,EWithDefinitions,EV),
305		add_identifiers_to_environment(C,EV,EVC),
306		add_identifiers_to_environment(GC,EVC,EVCGC),
307		add_identifiers_to_environment(GS,EVCGC,EOut),
308		opentype(Predicates, EOut, Identifiers, DeferredSets, TPredicates),
309		% DeferredSets should be empty? I.e. should this be allowed to create new types?
310		% currently this would not work as these types have not been added/registered in b_global_sets ! kernel_objects:basic_type would fail
311		(DeferredSets = [] -> true
312		; include(problematic_id(DeferredSets),Identifiers,TErrIds),
313		maplist(get_texpr_id,TErrIds,ErrIds),
314		add_warning(solver_interface,'The types of some variables could not be determined: ',ErrIds),
315		fail).
316		% a possible refactoring for the above - however, it does not type with open identifiers
317		% reverted it for now
318		% bmachine:b_type_expressions(Predicates,[constants],_Types,TPredicates,Errors),
319		% add_all_perrors(Errors,[],type_expression_error),
320		% no_real_perror_occurred(Errors).
321
322		problematic_id(DeferredSets,TID) :- get_texpr_type(TID,Type),
323		uses_def_set(Type,DeferredSets).
324
325		uses_def_set(global(T),DeferredSets) :- member(T,DeferredSets).
326		uses_def_set(set(A),DeferredSets) :- uses_def_set(A,DeferredSets).
327		uses_def_set(seq(A),DeferredSets) :- uses_def_set(A,DeferredSets).
328		uses_def_set(couple(A,_),DeferredSets) :- uses_def_set(A,DeferredSets).
329		uses_def_set(couple(_,A),DeferredSets) :- uses_def_set(A,DeferredSets).
330		uses_def_set(record(F),DS) :- member(field(_,T),F), uses_def_set(T,DS).
331		% TO DO: add freetypes