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(solver_interface, [solve_predicate/3, solve_predicate/4, solve_predicate/5,
6		valid_solver_option/1,
7		set_up_typed_localstate_for_pred/4,
8		strip_outer_exists/2,
9		type_check_in_machine_context/2,
10		predicate_uses_unfixed_deferred_set/1, predicate_uses_unfixed_deferred_set/2,
11		unfixed_typed_id_in_list/3,
12		call_with_smt_mode_enabled/1,
13		apply_kodkod_or_other_optimisations/3, apply_kodkod_or_other_optimisations/4,
14		solver_pp_bvalue/4
15		]).
16
17		:- use_module(module_information,[module_info/2]).
18		:- module_info(group,cbc).
19		:- module_info(description,'This module provides an interface to ProB\'s constraint solving kernel.').
20
21		:- meta_predicate call_with_smt_mode_enabled(0).
22		%:- meta_predicate call_with_chr(0).
23
24		:- use_module(library(lists), [include/3,keys_and_values/3]).
25
26		:- use_module(bmachine, [b_get_machine_variables/1, b_get_machine_constants/1, full_b_machine/1]).
27		:- use_module(btypechecker,[env_empty/1,opentype/5, add_identifiers_to_environment/3, env_store_operator/4, env_store_definition/3]).
28		:- use_module(b_global_sets, [is_b_global_constant/3,
29		b_global_set/1, unfixed_deferred_set_exists/0,
30		contains_unfixed_deferred_set/1, contains_unfixed_deferred_set/2]).
31		:- use_module(b_interpreter, [set_up_typed_localstate/6]).
32		:- use_module(tools_timeout, [time_out_with_factor_call/4]).
33		:- use_module(bsyntaxtree, [find_typed_identifier_uses/2,
34		map_over_typed_bexpr/3, get_texpr_id/2, get_texpr_type/2]).
35		:- use_module(error_manager).
36		:- use_module(tools,[foldl/5,foldl/4]).
37		:- use_module(translate, [translate_bvalue/2, translate_bvalue_with_limit/3]).
38		:- use_module(bmachine_structure,[get_section/3]).
39		:- use_module(debug,[debug_println/2, debug_mode/1]).
40		:- use_module(preferences).
41		:- use_module(eventhandling,[announce_event/1]).
42		:- use_module(smt_solvers_interface(smt_solvers_interface),[smt_solve_predicate/4]).
43		:- use_module(store, [normalise_value_for_var/4]).
44
45		%call_with_chr(Call) :- call_with_preference(Call,use_chr_solver,true).
46
47
48		% :- meta_predicate call_with_smt_mode_enabled(0). % directive above for Spider
49		call_with_smt_mode_enabled(Call) :-
50		temporary_set_preference(use_smt_mode,true,SMT),
51		temporary_set_preference(use_clpfd_solver,true,CLPFD), % we also enable CLPFD
52		% TO DO: also enable CHR
53		call_cleanup( (Call,!),
54		(reset_temporary_preference(use_smt_mode,SMT),
55		reset_temporary_preference(use_clpfd_solver,CLPFD)
56		)).
57
58
59		% -------------------------------------
60
61		:- use_module(kodkodsrc(kodkod), [replace_by_kodkod/3]).
62		:- use_module(bsyntaxtree, [get_texpr_ids/2]).
63		:- use_module(b_ast_cleanup, [perform_do_not_enumerate_analysis/5]).
64
65		% high-level interface to Kodkod transformation
66		apply_kodkod_or_other_optimisations(Identifiers,Predicate,NewPredicate) :-
67		get_preference(use_solver_on_load,kodkod),
68		!,
69		(replace_by_kodkod(Identifiers,Predicate,NewPredicate) -> true
70		; get_texpr_ids(Identifiers,Ids),
71		add_warning(kodkod_fail,'Could not use KODKOD to translate predicate to SAT, identifiers = ', Ids, Predicate),
72		(get_preference(kodkod_for_components,full)
73		-> throw(enumeration_warning(translating_for_kodkod,Ids,[],kodkod,critical))
74		; true),
75		NewPredicate = Predicate
76		).
77		apply_kodkod_or_other_optimisations(Identifiers,Predicate,NewPredicate) :-
78		Span=Predicate,
79		perform_do_not_enumerate_analysis(Identifiers,Predicate,'EXISTS',Span,NewPredicate).
80		% TODO: other top-level optimisations??
81
82
83		create_id(Id,Type,b(identifier(Id),Type,[])).
84
85		% a version which takes ids and types list:
86		apply_kodkod_or_other_optimisations(Ids,Types,Predicate,NewPredicate) :-
87		get_preference(use_solver_on_load,kodkod),
88		maplist(create_id,Ids,Types,Identifiers),
89		!,
90		apply_kodkod_or_other_optimisations(Identifiers,Predicate,NewPredicate).
91		apply_kodkod_or_other_optimisations(_Identifiers,_Types,Predicate,Predicate).
92
93		% -------------------------------------
94
95		% strip_outer_exists: remove outer exists of let_predicate, putting them as full decision variables
96		% can be useful in improving solving performance, e.g., public_examples/SMT/QF_IDL/queens_bench/n_queen/queen3-1.smt2
97		:- use_module(probsrc(bsyntaxtree), [conjunct_predicates/2]).
98		:- use_module(library(lists), [maplist/4]).
99		strip_outer_exists(b(exists(Paras,Pred),pred,_),Res) :-
100		debug_println(9,stripping_exists(Paras)),
101		strip_outer_exists(Pred,Res).
102		strip_outer_exists(b(let_predicate(Paras,Exprs,Pred),pred,_),R) :- !,
103		debug_println(9,stripping_let(Paras,Exprs)),
104		maplist(create_equality,Paras,Exprs,Equals),
105		append(Equals,[Pred],List),
106		conjunct_predicates(List,NewPred),
107		strip_outer_exists(NewPred,R).
108		strip_outer_exists(R,R).
109
110		:- use_module(probsrc(bsyntaxtree), [create_equality/3]).
111
112
113		% -------------------------------------------------------
114
115		% solve predicate finds *one* solution for predicate in State
116		solve_predicate(Pred,State,Res) :- solve_predicate(Pred,State,1,Res).
117		% TimeoutFactor can also be fixed_time_out(Nr)
118		solve_predicate(Pred,State,TimeoutFactor,Res) :-
119		solve_predicate(Pred,State,TimeoutFactor,[use_smt_mode/true,use_clpfd_solver/true],Res).
120
121		% one could add a preference to try Z3 instead/or first:
122		%solve_predicate(Pred,State,TimeoutFactor,Options,RealRes) :-
123		% % preference(solve_predicates_with_z3,true),
124		% !, print(solve_with_z3),nl, translate:print_bexpr(Pred),nl,
125		% ((TimeoutFactor=1,Options=[]) -> true
126		% ; format('TO DO; ignoring Timeout Factor ~w and Options ~w for Z3~n',[TimeoutFactor,Options])),
127		% smt_solvers_interface:smt_solve_predicate(z3,Pred,State,RealRes),
128		% print(z3_result(RealRes)),nl.
129		solve_predicate(Pred,State,TimeoutFactor,Options,RealRes) :-
130		solve_predicate_with_options(Options,[],Pred,State,TimeoutFactor,Res), !,
131		if(solver_result(Res,Pred,State,Options,RealResBeforeFallback),true,
132		(add_internal_error('Unknown solver_result: ',Res),RealResBeforeFallback=error)),
133		fallback_to_smt_if_requested(RealResBeforeFallback,Pred,State,RealRes).
134
135		% no fallback if solution / contradiction
136		fallback_to_smt_if_requested(solution(S),_,_,Res) :- !, Res=solution(S).
137		fallback_to_smt_if_requested(contradiction_found,_,_,Res) :- !,Res=contradiction_found.
138		fallback_to_smt_if_requested(S,_,_,Res) :-
139		\+ preferences:get_preference(smt_supported_interpreter,true), ! , Res = S.
140		fallback_to_smt_if_requested(_,Pred,State,Res) :-
141		smt_solve_predicate(z3,Pred,State,Res), !.
142
143		solve_predicate_with_options([],RestOptions,Pred,State,TimeoutFactor,Res) :-
144		solve_predicate_direct(Pred,State,TimeoutFactor,RestOptions,Res).
145		solve_predicate_with_options([Option|T],RestOptions,Pred,State,TimeoutFactor,Res) :-
146		solve_with_option(Option,T,RestOptions,Pred,State,TimeoutFactor,Res).
147
148		solve_with_option('CHR',T,Rest,Pred,State,TimeoutFactor,Res) :- !,
149		solve_with_option(use_chr_solver/true,T,Rest,Pred,State,TimeoutFactor,Res).
150		solve_with_option('SMT',T,Rest,Pred,State,TimeoutFactor,Res) :- !,
151		solve_with_option(use_smt_mode/true,T,Rest,Pred,State,TimeoutFactor,Res).
152		solve_with_option('KODKOD',T,Rest,Pred,State,TimeoutFactor,Res) :- !,
153		solve_with_option(use_solver_on_load/kodkod,T,Rest,Pred,State,TimeoutFactor,Res).
154		solve_with_option('SMT_SUPPORTED_INTERPRETER',T,Rest,Pred,State,TimeoutFactor,Res) :- !,
155		solve_with_option(smt_supported_interpreter/true,T,Rest,Pred,State,TimeoutFactor,Res).
156		solve_with_option('CLPFD',T,Rest,Pred,State,TimeoutFactor,Res) :- !,
157		solve_with_option(use_clpfd_solver/true,T,Rest,Pred,State,TimeoutFactor,Res).
158		solve_with_option(Pref/Val,T,Rest,Pred,State,TimeoutFactor,Res) :- !,
159		call_with_preference(solve_predicate_with_options(T,Rest,Pred,State,TimeoutFactor,Res),Pref,Val).
160		solve_with_option(Opt,T,Rest,Pred,State,TimeoutFactor,Res) :-
161		valid_solver_option(Opt),!,
162		solve_predicate_with_options(T,[Opt|Rest],Pred,State,TimeoutFactor,Res).
163		solve_with_option(Opt,T,Rest,Pred,State,TimeoutFactor,Res) :-
164		add_warning(solve_with_option,'Unrecognised option: ',Opt),
165		solve_predicate_with_options(T,Rest,Pred,State,TimeoutFactor,Res).
166
167		valid_solver_option(full_machine_state).
168		valid_solver_option(ignore_wd_errors).
169		valid_solver_option(clean_up_pred).
170		valid_solver_option(allow_improving_wd_mode/_). % enable left-propagation of falsity/truth in clean_up
171		valid_solver_option(repair_used_ids).
172		valid_solver_option(solve_in_visited_state(S)) :- atomic(S).
173		valid_solver_option(truncate(Limit)) :- number(Limit). % truncate pretty printing
174		valid_solver_option(truncate). % 10000
175		valid_solver_option(force_evaluation). % force evaluation of symbolic results
176		valid_solver_option(use_smt_mode/_).
177		valid_solver_option(use_clpfd_solver/_).
178		valid_solver_option(use_chr_solver/_).
179		valid_solver_option(use_solver_on_load/_).
180		valid_solver_option(smt_supported_interpreter/_).
181		valid_solver_option(solver_strength/_).
182
183		solve_predicate_direct(Pred,State,TimeoutFactor,Options,Res) :-
184		%temporary_set_preference(randomise_enumeration_order,true),
185		%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 ?!
186
187		%temporary_set_preference(minint,-2147483648), % disabled to pass tests 1004,1015,..
188		%temporary_set_preference(maxint,2147483647),
189		get_total_number_of_errors(Errs),
190
191		announce_event(start_solving),
192		solve_predicate_aux(Pred,State,TimeoutFactor,Options,InnerRes),
193		announce_event(end_solving),
194
195		get_total_number_of_errors(ErrsAfter),
196		(InnerRes = overflow -> Res = overflow ; ErrsAfter>Errs -> Res = error; Res = InnerRes).
197
198		%:- use_module(clpfd_interface,[clpfd_overflow_error_message/0]).
199		solve_predicate_aux(Pred,State,TimeoutFactor,Options,Res) :-
200		enter_new_error_scope(ScopeID,solve_predicate), %print(enter_scope(ScopeID)),nl,
201		call_cleanup(solve_predicate_aux0(Pred,State,TimeoutFactor,Options,Res),
202		exit_err_scope(ScopeID,Options,Res)).
203
204		solve_predicate_aux0(Pred,State,TimeoutFactor,Options,Res) :-
205		clean_solver_predicate(Pred,Options,CleanedPred),
206		(solve_predicate_aux1(CleanedPred,State,TimeoutFactor,Options,SRes)
207		-> (SRes = time_out
208		-> fail % fail if we have a time_out to avoid pending co-routines and return time_out in clause below
209		; !, Res=SRes
210		)
211		; !,
212		add_warning(solver_interface,'solve_predicate failed:',CleanedPred), % this should normally not happen
213		fail % the above can fail when state is provided
214		).
215		solve_predicate_aux0(_,_,_,_,time_out).
216
217		:- use_module(probsrc(b_ast_cleanup), [clean_up_pred/3]).
218		:- use_module(probsrc(bsyntaxtree), [repair_used_ids/3]).
219
220		clean_solver_predicate(Pred,Options,CleanedPred) :-
221		(nonmember(repair_used_ids,Options) -> Pred0=Pred
222		; repair_used_ids(solve_predicate,Pred,Pred0)), % ideally we should not need this; some BMC monolithic predicates are faulty and this allows a repair
223		(nonmember(clean_up_pred,Options) -> CleanedPred=Pred0
224		; clean_up_pred(Pred0, [], CleanedPred)
225		-> (debug_mode(off) -> true ; print(cleaned),nl, translate:print_bexpr(CleanedPred),nl)
226		; add_internal_error('Clean up failed ', solve_predicate_aux3), CleanedPred=Pred0
227		).
228
229		:- use_module(probsrc(error_manager),[wd_error_occured/0, clear_wd_errors/0]).
230		:- use_module(probsrc(debug),[debug_format/3]).
231		exit_err_scope(ScopeID,Options,Res) :-
232		(member(ignore_wd_errors,Options),wd_error_occured
233		-> debug_format(19,'Ignoring WD-Error(s) in solve_predicate (scope: ~w, result: ~w)~n',[ScopeID,Res]),
234		clear_wd_errors
235		; true),
236		exit_error_scope(ScopeID,_,solve_predicate_aux).
237
238		:- use_module(probsrc(store),[normalise_store/2]).
239		solve_predicate_aux1(Pred,State,TimeoutFactor,Options,Res) :- var(State),
240	?	solve_predicate_aux2(Pred,CState,TimeoutFactor,Options,Res),
241		!, % we only look for one solution
242		normalise_solver_store(Res,CState,State),
243		clear_enumeration_warnings. % avoid propagating them higher up
244		solve_predicate_aux1(Pred,State,TimeoutFactor,Options,Res) :- nonvar(State),
245	?	solve_predicate_aux2(Pred,State,TimeoutFactor,Options,Res),
246		!, % we only look for one solution
247		clear_enumeration_warnings. % avoid propagating them higher up
248		solve_predicate_aux1(_Pred,State,_TimeoutFactor,_Options,Res) :-
249	?	critical_enumeration_warning_occured_in_error_scope(A,B,C,D), % we did not find a solution: check for enum warnings
250		!,
251		clear_enumeration_warnings,
252		set_no_state(State),
253		Res = virtual_time_out(enumeration_warning(A,B,C,D,critical)).
254		solve_predicate_aux1(Pred,State,_TimeoutFactor,_Options,Res) :- var(State),!,
255		% a variable state means we are in a disprover context; check if deferred sets are involved
256		set_no_state(State),
257		% print('Checking for use of deferred sets in: '), translate:print_bexpr(Pred),nl,
258	?	(predicate_uses_unfixed_deferred_set(Pred,CType)
259		-> debug_println(10,solver_predicate_contains_unfixed_deferred_set(CType)),
260		Res=unfixed_deferred_sets
261		% if no unfixed global sets involved -> real contradiction found
262		; Res=no
263		).
264		solve_predicate_aux1(_Pred,_State,_TimeoutFactor,_Options,Res) :-
265		% if state is set: we are looking for a solution in the context of the current state
266		% which implicitly includes the valuation of the unfixed deferred sets, hence
267		% we can return no rather than unfixed_deferred_sets
268		%set_no_state(State),
269		Res = no.
270
271		set_no_state(State) :- var(State),!,State=no_state.
272		set_no_state(_).
273
274		normalise_solver_store(yes,Store,NormStore) :- !, normalise_solver_store2(Store,NormStore).
275		normalise_solver_store(_,S,Res) :- !,
276		Res=S. % for error, time_out, ... Store irrelevant; just copy to avoid call_residues
277		normalise_solver_store2(no_state,R) :- !, R=no_state.
278		normalise_solver_store2(CState,State) :- normalise_store(CState,State),!.
279		normalise_solver_store2(CState,Res) :-
280		add_internal_error('Normalising store failed:',normalise_solver_store2(CState,Res)),
281		Res=CState.
282
283		:- use_module(clpfd_interface,[catch_clpfd_overflow_call2/2]).
284
285		solve_predicate_aux2(Pred,State,TimeoutFactor,Options,Res) :-
286		%predicate_level_optimizations(Pred,OptPred),
287		% is now done in b_interpreter_components; to avoid that CSE disrupts partitioning
288	?	catch_clpfd_overflow_call2(
289		solve_predicate_aux3(Pred,State,TimeoutFactor,Options,Res),
290		( debug_println(19,overflow_in_solve_predicate),
291		%clpfd_interface:clpfd_overflow_warning_message, % message is already printed by catch_clpfd_overflow_call2
292		% we could try and solve without CLPFD ?!!
293		Res=overflow,State=no_state)).
294
295
296
297		:- use_module(b_interpreter_components).
298
299		:- use_module(specfile,[state_corresponds_to_set_up_constants/2]).
300		:- use_module(state_space,[visited_expression/2]).
301		:- use_module(library(lists),[maplist/2]).
302
303
304		solve_predicate_aux3(Pred,State,TimeoutFactor,Options,Res) :-
305		% find all identifiers used in the predicate and create a state
306		% was done by the caller, leading to code duplication
307		(member(full_machine_state,Options) -> get_full_machine_state_typed_identifiers(FilteredIdentifiers)
308		; find_typed_identifier_uses(Pred,FilteredIdentifiers)),
309		!,
310		% global constants should not appear in the state
311		% otherwise they treated are as variables by the solver
312		% -> we now call find_typed_identifier_uses; we used to call filter_global_identifiers(Identifiers,FilteredIdentifiers),
313		% state may be predefined / partially set up
314		apply_kodkod_or_other_optimisations(FilteredIdentifiers,Pred,Pred2),
315		(member(solve_in_visited_state(StateID),Options)
316		-> set_up_typed_localstate_for_pred(FilteredIdentifiers,Pred2,TypedVals,State),
317		(visited_expression(StateID,StateExpr),
318		state_corresponds_to_set_up_constants(StateExpr,FullStore)
319		-> maplist(initialise_localstate(FullStore),State)
320		; StateID=root -> true
321		; add_internal_error('Illegal State:',use_visited_state(StateID))
322		)
323		; var(State)
324		-> set_up_typed_localstate_for_pred(FilteredIdentifiers,Pred2,TypedVals,State)
325		% TypedVals contains typedval(Val,Type,Var,TriggersEnumWarning)
326		% TO DO: add static_symmetry detection b_global_sets:static_symmetry_reduction_for_global_sets(State),
327		;
328	?	set_up_typed_localstate_for_pred(FilteredIdentifiers,Pred2,TypedVals,State2),
329		sort(State,S1),sort(State2,S2),
330	?	link_bindings(S1,S2)
331		),
332		%tools_printing:print_term_summary(b_trace_test_components(Pred2,State,TypedVals)),nl,
333		b_interpreter_components:reset_component_info(false),
334	?	time_out_with_factor_call(
335		solver_interface:solve_components(Pred2,State,TypedVals),
336		TimeoutFactor, [silent],
337		TO='time_out'),
338		(TO==time_out -> Res = TO ; Res = yes).
339
340		% link up state provided with state set-up by solve_predicate
341		link_bindings([],[]).
342		link_bindings([],[bind(ID,_)|_T]) :- add_error(solve_predicate,'Provided state has no entry for identifier: ',ID),fail.
343	?	link_bindings([bind(ID,Val)|T1],[bind(ID,Val)|T2]) :- !,link_bindings(T1,T2).
344		link_bindings([bind(_,_)|T],S2) :- % ignore ID in state provided to solver
345	?	link_bindings(T,S2).
346
347
348		:- public solve_components/3.
349		:- use_module(tools_meta,[call_residue/2]).
350		solve_components(Pred2,State,TypedVals) :-
351	?	call_residue(
352		b_interpreter_components:b_trace_test_components(Pred2,State,TypedVals),
353		Residue),
354		(Residue=[] -> true
355		; add_internal_error('Call residue in solve_predicate: ',Residue)
356		%add_message(solver_interface,'Call residue in solve_predicate: ',Residue)
357		).
358
359		% 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
360		% TypedVals need to be enumerated after calling solve_predicate, in case some variables are not constrained
361		get_full_machine_state_typed_identifiers(TIds) :-
362		b_get_machine_variables(Variables),
363		b_get_machine_constants(Constants), append(Constants,Variables,TIds).
364
365		:- use_module(static_ordering,[sort_ids_by_usage/4,reorder_state/3]).
366		:- use_module(preferences,[preference/2]).
367		set_up_typed_localstate_for_pred(CV,Pred,TypedVals,State) :-
368		(preference(use_static_ordering,true)
369		-> sort_ids_by_usage(CV,Pred,SortedVarlist,no_warnings) ,
370		set_up_typed_localstate(SortedVarlist,_FreshVars,TypedVals,[],SortedState,positive),
371		reorder_state(CV,SortedState,State) % SortedState can have issues with pack_state skeleton
372	?	; set_up_typed_localstate(CV,_FreshVars,TypedVals,[],State,positive)).
373
374		% initialise local state with values found in bind list
375		initialise_localstate(FullStore,bind(Var,Val)) :-
376		(member(bind(Var,VarVal),FullStore)
377		-> Val=VarVal ; true).
378
379		% translate solver_result for use by Disprover/Prover or similar:
380		solver_result(time_out,_P,_State,_,Res) :- !,Res=time_out.
381		solver_result(error,_P,_State,_,Res) :- !,Res=error.
382		solver_result(no,_P,_State,_,Res) :- !, Res=contradiction_found.
383		solver_result(unfixed_deferred_sets,_,_,_,Res) :- !,
384		Res=no_solution_found(unfixed_deferred_sets).
385		solver_result(virtual_time_out(Reason),_P,_State,_,Res) :- !,
386		Res=no_solution_found(Reason).
387		% this is now checked in solve_predicate_aux1: event_occurred_in_error_scope(enumeration_warning(A,B,C,D,critical)).
388		solver_result(overflow,_P,_State,_,Res) :- !, Res=no_solution_found(clpfd_overflow).
389		solver_result(yes,_P,State,Options,Res) :- !,Res=solution(Solution),
390		findall(binding(Id,EValue,PPValue),
391		(member(bind(Id,Value),State),
392		(solver_pp_bvalue(Value,Options,EValue,PPValue) -> true
393		; EValue=Value, PPValue='**pretty-print failed**')),
394		Solution).
395		solver_result(OTHER,_P,_State,_,no_solution_found(OTHER)) :-
396		add_internal_error('Unknown solver_result:',OTHER).
397
398		% expand and pretty print solver result values:
399		solver_pp_bvalue(Value,Options,EValue,PPValue) :- member(force_evaluation,Options),!,
400		EXPAND=force,
401		normalise_value_for_var(solver_result,EXPAND,Value,EValue), % will suspend if timeout occurs!
402		solver_pp_bvalue2(EValue,Options,PPValue).
403		solver_pp_bvalue(Value,Options,Value,PPValue) :- solver_pp_bvalue2(Value,Options,PPValue).
404
405		solver_pp_bvalue2(Value,Options,PPValue) :- member(truncate(Limit),Options),!,
406		translate_bvalue_with_limit(Value,Limit,PPValue). % should we also control expand_avl_upto ??
407		solver_pp_bvalue2(Value,Options,PPValue) :- member(truncate,Options),!,
408		translate_bvalue_with_limit(Value,10000,PPValue).
409		solver_pp_bvalue2(Value,_,PPValue) :- translate_bvalue(Value,PPValue).
410
411		% check if a typed expression references an unfixed deferred set in some inner node
412		predicate_uses_unfixed_deferred_set(TExpr) :- predicate_uses_unfixed_deferred_set(TExpr,_).
413
414		predicate_uses_unfixed_deferred_set(TExpr,CType) :-
415		unfixed_deferred_set_exists, % check first if some unfixed deferred set exists
416	?	map_over_typed_bexpr(solver_interface:uses_unfixed_ds_aux,TExpr,CType).
417		:- public uses_unfixed_ds_aux/2.
418		uses_unfixed_ds_aux(TExpr,DSType) :- get_texpr_type(TExpr,Type),
419	?	contains_unfixed_deferred_set(Type,DSType).
420
421		% find a typed id whose type references an unfixed deferred set
422		unfixed_typed_id_in_list(TID,CType,Constants) :-
423		unfixed_deferred_set_exists, % check first if some unfixed deferred set exists
424	?	member(TID,Constants), get_texpr_type(TID,CType),
425		contains_unfixed_deferred_set(CType).
426
427		:- use_module(library(lists),[maplist/3, include/3]).
428		type_check_in_machine_context(Predicates, TPredicates) :-
429		% create an empty type environment
430		% and store the known types of variables / constants
431		% otherwise, we might be unable to type variables from
432		% machines somewhere in the refinement hierarchy
433		% (their typing predicate might not be in the hypothesis)
434		% Definitions are also added to the environment since the typechecker
435		% inlines definitions.
436		env_empty(E),
437		b_get_machine_variables(V), b_get_machine_constants(C),
438		% add theory operators
439		full_b_machine(Machine),
440		get_section(operators,Machine,Operators),
441		keys_and_values(Operators,Ids,Ops),
442		foldl(env_store_operator,Ids,Ops,E,EWithTheories),
443		get_section(definitions, Machine, Definitions),
444		foldl(env_store_definition, Definitions, EWithTheories, EWithDefinitions),
445		% constants and variables
446		findall(b(identifier(Name),global(GlobalSet),[enumerated_set_element]),is_b_global_constant(GlobalSet,_Nr,Name),GC),
447		findall(b(identifier(Set),set(global(Set)),[given_set]),b_global_set(Set),GS),
448		add_identifiers_to_environment(V,EWithDefinitions,EV),
449		add_identifiers_to_environment(C,EV,EVC),
450		add_identifiers_to_environment(GC,EVC,EVCGC),
451		add_identifiers_to_environment(GS,EVCGC,EOut),
452		opentype(Predicates, EOut, Identifiers, DeferredSets, TPredicates),
453		% DeferredSets should be empty? I.e. should this be allowed to create new types?
454		% currently this would not work as these types have not been added/registered in b_global_sets ! kernel_objects:basic_type would fail
455		(DeferredSets = [] -> true
456		; include(problematic_id(DeferredSets),Identifiers,TErrIds),
457		maplist(get_texpr_id,TErrIds,ErrIds),
458		add_warning(solver_interface,'The types of some variables could not be determined: ',ErrIds),
459		fail).
460		% a possible refactoring for the above - however, it does not type with open identifiers
461		% reverted it for now
462		% bmachine:b_type_expressions(Predicates,[constants],_Types,TPredicates,Errors),
463		% add_all_perrors(Errors,[],type_expression_error),
464		% no_real_perror_occurred(Errors).
465
466		problematic_id(DeferredSets,TID) :- get_texpr_type(TID,Type),
467		uses_def_set(Type,DeferredSets).
468
469		uses_def_set(global(T),DeferredSets) :- member(T,DeferredSets).
470		uses_def_set(set(A),DeferredSets) :- uses_def_set(A,DeferredSets).
471		uses_def_set(seq(A),DeferredSets) :- uses_def_set(A,DeferredSets).
472		uses_def_set(couple(A,_),DeferredSets) :- uses_def_set(A,DeferredSets).
473		uses_def_set(couple(_,A),DeferredSets) :- uses_def_set(A,DeferredSets).
474		uses_def_set(record(F),DS) :- member(field(_,T),F), uses_def_set(T,DS).
475		% TO DO: add freetypes