1		% (c) 2009-2025 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('ignore_wd_errors',T,Rest,Pred,State,TimeoutFactor,Res) :- !,
161		solve_with_option(do_not_print_wd_errors/true,T,[ignore_wd_errors|Rest],Pred,State,TimeoutFactor,Res).
162		solve_with_option(Opt,T,Rest,Pred,State,TimeoutFactor,Res) :-
163		valid_solver_option(Opt),!,
164		solve_predicate_with_options(T,[Opt|Rest],Pred,State,TimeoutFactor,Res).
165		solve_with_option(Opt,T,Rest,Pred,State,TimeoutFactor,Res) :-
166		add_warning(solve_with_option,'Unrecognised option: ',Opt),
167		solve_predicate_with_options(T,Rest,Pred,State,TimeoutFactor,Res).
168
169		valid_solver_option(full_machine_state).
170		valid_solver_option(ignore_wd_errors).
171		valid_solver_option(clean_up_pred).
172		valid_solver_option(allow_improving_wd_mode/_). % enable left-propagation of falsity/truth in clean_up
173		valid_solver_option(repair_used_ids).
174		valid_solver_option(solve_in_visited_state(S)) :- atomic(S).
175		valid_solver_option(truncate(Limit)) :- number(Limit). % truncate pretty printing
176		valid_solver_option(truncate). % 10000
177		valid_solver_option(force_evaluation). % force evaluation of symbolic results
178		valid_solver_option(use_smt_mode/_).
179		valid_solver_option(use_clpfd_solver/_).
180		valid_solver_option(use_chr_solver/_).
181		valid_solver_option(use_solver_on_load/_).
182		valid_solver_option(smt_supported_interpreter/_).
183		valid_solver_option(solver_strength/_).
184
185		solve_predicate_direct(Pred,State,TimeoutFactor,Options,Res) :-
186		%temporary_set_preference(randomise_enumeration_order,true),
187		%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 ?!
188
189		%temporary_set_preference(minint,-2147483648), % disabled to pass tests 1004,1015,..
190		%temporary_set_preference(maxint,2147483647),
191		get_total_number_of_errors(Errs),
192
193		announce_event(start_solving),
194		solve_predicate_aux(Pred,State,TimeoutFactor,Options,InnerRes),
195		announce_event(end_solving),
196
197		get_total_number_of_errors(ErrsAfter),
198		(InnerRes = overflow -> Res = overflow ; ErrsAfter>Errs -> Res = error; Res = InnerRes).
199
200		%:- use_module(clpfd_interface,[clpfd_overflow_error_message/0]).
201		solve_predicate_aux(Pred,State,TimeoutFactor,Options,Res) :-
202		enter_new_error_scope(ScopeID,solve_predicate), %print(enter_scope(ScopeID)),nl,
203		call_cleanup(solve_predicate_aux0(Pred,State,TimeoutFactor,Options,Res),
204		exit_err_scope(ScopeID,Options,Res)).
205
206		solve_predicate_aux0(Pred,State,TimeoutFactor,Options,Res) :-
207		clean_solver_predicate(Pred,Options,CleanedPred),
208		(solve_predicate_aux1(CleanedPred,State,TimeoutFactor,Options,SRes)
209		-> (SRes = time_out
210		-> fail % fail if we have a time_out to avoid pending co-routines and return time_out in clause below
211		; !, Res=SRes
212		)
213		; !,
214		add_warning(solver_interface,'solve_predicate failed:',CleanedPred), % this should normally not happen
215		fail % the above can fail when state is provided
216		).
217		solve_predicate_aux0(_,_,_,_,time_out).
218
219		:- use_module(probsrc(b_ast_cleanup), [clean_up_pred/3]).
220		:- use_module(probsrc(bsyntaxtree), [repair_used_ids/3]).
221
222		clean_solver_predicate(Pred,Options,CleanedPred) :-
223		(nonmember(repair_used_ids,Options) -> Pred0=Pred
224		; repair_used_ids(solve_predicate,Pred,Pred0)), % ideally we should not need this; some BMC monolithic predicates are faulty and this allows a repair
225		(nonmember(clean_up_pred,Options) -> CleanedPred=Pred0
226		; clean_up_pred(Pred0, [], CleanedPred)
227		-> (debug_mode(off) -> true ; print(cleaned),nl, translate:print_bexpr(CleanedPred),nl)
228		; add_internal_error('Clean up failed ', solve_predicate_aux3), CleanedPred=Pred0
229		).
230
231		:- use_module(probsrc(error_manager),[wd_error_occured/0, clear_wd_errors/0]).
232		:- use_module(probsrc(debug),[debug_format/3]).
233		exit_err_scope(ScopeID,Options,Res) :-
234		(member(ignore_wd_errors,Options),wd_error_occured
235		-> debug_format(19,'Ignoring WD-Error(s) in solve_predicate (scope: ~w, result: ~w)~n',[ScopeID,Res]),
236		clear_wd_errors
237		; true),
238		exit_error_scope(ScopeID,_,solve_predicate_aux).
239
240		:- use_module(probsrc(store),[normalise_store/2]).
241		solve_predicate_aux1(Pred,State,TimeoutFactor,Options,Res) :- var(State),
242	?	solve_predicate_aux2(Pred,CState,TimeoutFactor,Options,Res),
243		!, % we only look for one solution
244		normalise_solver_store(Res,CState,State),
245		clear_enumeration_warnings. % avoid propagating them higher up
246		solve_predicate_aux1(Pred,State,TimeoutFactor,Options,Res) :- nonvar(State),
247		solve_predicate_aux2(Pred,State,TimeoutFactor,Options,Res),
248		!, % we only look for one solution
249		clear_enumeration_warnings. % avoid propagating them higher up
250		solve_predicate_aux1(_Pred,State,_TimeoutFactor,_Options,Res) :-
251		critical_enumeration_warning_occured_in_error_scope(A,B,C,D), % we did not find a solution: check for enum warnings
252		!,
253		clear_enumeration_warnings,
254		set_no_state(State),
255		Res = virtual_time_out(enumeration_warning(A,B,C,D,critical)).
256		solve_predicate_aux1(Pred,State,_TimeoutFactor,_Options,Res) :- var(State),!,
257		% a variable state means we are in a disprover context; check if deferred sets are involved
258		set_no_state(State),
259		% print('Checking for use of deferred sets in: '), translate:print_bexpr(Pred),nl,
260		(predicate_uses_unfixed_deferred_set(Pred,CType)
261		-> debug_println(10,solver_predicate_contains_unfixed_deferred_set(CType)),
262		Res=unfixed_deferred_sets
263		% if no unfixed global sets involved -> real contradiction found
264		; Res=no
265		).
266		solve_predicate_aux1(_Pred,_State,_TimeoutFactor,_Options,Res) :-
267		% if state is set: we are looking for a solution in the context of the current state
268		% which implicitly includes the valuation of the unfixed deferred sets, hence
269		% we can return no rather than unfixed_deferred_sets
270		%set_no_state(State),
271		Res = no.
272
273		set_no_state(State) :- var(State),!,State=no_state.
274		set_no_state(_).
275
276		normalise_solver_store(yes,Store,NormStore) :- !, normalise_solver_store2(Store,NormStore).
277		normalise_solver_store(_,S,Res) :- !,
278		Res=S. % for error, time_out, ... Store irrelevant; just copy to avoid call_residues
279		normalise_solver_store2(no_state,R) :- !, R=no_state.
280		normalise_solver_store2(CState,State) :- normalise_store(CState,State),!.
281		normalise_solver_store2(CState,Res) :-
282		add_internal_error('Normalising store failed:',normalise_solver_store2(CState,Res)),
283		Res=CState.
284
285		:- use_module(clpfd_interface,[catch_clpfd_overflow_call2/2]).
286
287		solve_predicate_aux2(Pred,State,TimeoutFactor,Options,Res) :-
288		%predicate_level_optimizations(Pred,OptPred),
289		% is now done in b_interpreter_components; to avoid that CSE disrupts partitioning
290	?	catch_clpfd_overflow_call2(
291		solve_predicate_aux3(Pred,State,TimeoutFactor,Options,Res),
292		( debug_println(19,overflow_in_solve_predicate),
293		%clpfd_interface:clpfd_overflow_warning_message, % message is already printed by catch_clpfd_overflow_call2
294		% we could try and solve without CLPFD ?!!
295		Res=overflow,State=no_state)).
296
297
298
299		:- use_module(b_interpreter_components).
300
301		:- use_module(specfile,[state_corresponds_to_set_up_constants/2]).
302		:- use_module(state_space,[visited_expression/2]).
303		:- use_module(library(lists),[maplist/2]).
304
305
306		solve_predicate_aux3(Pred,State,TimeoutFactor,Options,Res) :-
307		% find all identifiers used in the predicate and create a state
308		% was done by the caller, leading to code duplication
309		(member(full_machine_state,Options) -> get_full_machine_state_typed_identifiers(FilteredIdentifiers)
310		; find_typed_identifier_uses(Pred,FilteredIdentifiers)),
311		!,
312		% global constants should not appear in the state
313		% otherwise they treated are as variables by the solver
314		% -> we now call find_typed_identifier_uses; we used to call filter_global_identifiers(Identifiers,FilteredIdentifiers),
315		% state may be predefined / partially set up
316		apply_kodkod_or_other_optimisations(FilteredIdentifiers,Pred,Pred2),
317		(member(solve_in_visited_state(StateID),Options)
318		-> set_up_typed_localstate_for_pred(FilteredIdentifiers,Pred2,TypedVals,State),
319		(visited_expression(StateID,StateExpr),
320		state_corresponds_to_set_up_constants(StateExpr,FullStore)
321		-> maplist(initialise_localstate(FullStore),State)
322		; StateID=root -> true
323		; add_internal_error('Illegal State:',use_visited_state(StateID))
324		)
325		; var(State)
326		-> set_up_typed_localstate_for_pred(FilteredIdentifiers,Pred2,TypedVals,State)
327		% TypedVals contains typedval(Val,Type,Var,TriggersEnumWarning)
328		% TO DO: add static_symmetry detection b_global_sets:static_symmetry_reduction_for_global_sets(State),
329		;
330		set_up_typed_localstate_for_pred(FilteredIdentifiers,Pred2,TypedVals,State2),
331		sort(State,S1),sort(State2,S2),
332		link_bindings(S1,S2)
333		),
334		%tools_printing:print_term_summary(b_trace_test_components(Pred2,State,TypedVals)),nl,
335		b_interpreter_components:reset_component_info(false),
336	?	time_out_with_factor_call(
337		solver_interface:solve_components(Pred2,State,TypedVals),
338		TimeoutFactor, [silent],
339		TO='time_out'),
340		(TO==time_out -> Res = TO ; Res = yes).
341
342		% link up state provided with state set-up by solve_predicate
343		link_bindings([],[]).
344		link_bindings([],[bind(ID,_)|_T]) :- add_error(solve_predicate,'Provided state has no entry for identifier: ',ID),fail.
345		link_bindings([bind(ID,Val)|T1],[bind(ID,Val)|T2]) :- !,link_bindings(T1,T2).
346		link_bindings([bind(_,_)|T],S2) :- % ignore ID in state provided to solver
347		link_bindings(T,S2).
348
349
350		:- public solve_components/3.
351		:- use_module(tools_meta,[call_residue/2]).
352		solve_components(Pred2,State,TypedVals) :-
353	?	call_residue(
354		b_interpreter_components:b_trace_test_components(Pred2,State,TypedVals),
355		Residue),
356		(Residue=[] -> true
357		; add_internal_error('Call residue in solve_predicate: ',Residue)
358		%add_message(solver_interface,'Call residue in solve_predicate: ',Residue)
359		).
360
361		% 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
362		% TypedVals need to be enumerated after calling solve_predicate, in case some variables are not constrained
363		get_full_machine_state_typed_identifiers(TIds) :-
364		b_get_machine_variables(Variables),
365		b_get_machine_constants(Constants), append(Constants,Variables,TIds).
366
367		:- use_module(static_ordering,[sort_ids_by_usage/4,reorder_state/3]).
368		:- use_module(preferences,[preference/2]).
369		set_up_typed_localstate_for_pred(CV,Pred,TypedVals,State) :-
370		(preference(use_static_ordering,true)
371		-> sort_ids_by_usage(CV,Pred,SortedVarlist,no_warnings) ,
372		set_up_typed_localstate(SortedVarlist,_FreshVars,TypedVals,[],SortedState,positive),
373		reorder_state(CV,SortedState,State) % SortedState can have issues with pack_state skeleton
374		; set_up_typed_localstate(CV,_FreshVars,TypedVals,[],State,positive)).
375
376		% initialise local state with values found in bind list
377		initialise_localstate(FullStore,bind(Var,Val)) :-
378		(member(bind(Var,VarVal),FullStore)
379		-> Val=VarVal ; true).
380
381		% translate solver_result for use by Disprover/Prover or similar:
382		solver_result(time_out,_P,_State,_,Res) :- !,Res=time_out.
383		solver_result(error,_P,_State,_,Res) :- !,Res=error.
384		solver_result(no,_P,_State,_,Res) :- !, Res=contradiction_found.
385		solver_result(unfixed_deferred_sets,_,_,_,Res) :- !,
386		Res=no_solution_found(unfixed_deferred_sets).
387		solver_result(virtual_time_out(Reason),_P,_State,_,Res) :- !,
388		Res=no_solution_found(Reason).
389		% this is now checked in solve_predicate_aux1: event_occurred_in_error_scope(enumeration_warning(A,B,C,D,critical)).
390		solver_result(overflow,_P,_State,_,Res) :- !, Res=no_solution_found(clpfd_overflow).
391		solver_result(yes,_P,State,Options,Res) :- !,Res=solution(Solution),
392		findall(binding(Id,EValue,PPValue),
393		(member(bind(Id,Value),State),
394		(solver_pp_bvalue(Value,Options,EValue,PPValue) -> true
395		; EValue=Value, PPValue='**pretty-print failed**')),
396		Solution).
397		solver_result(OTHER,_P,_State,_,no_solution_found(OTHER)) :-
398		add_internal_error('Unknown solver_result:',OTHER).
399
400		% expand and pretty print solver result values:
401		solver_pp_bvalue(Value,Options,EValue,PPValue) :- member(force_evaluation,Options),!,
402		EXPAND=force,
403		normalise_value_for_var(solver_result,EXPAND,Value,EValue), % will suspend if timeout occurs!
404		solver_pp_bvalue2(EValue,Options,PPValue).
405		solver_pp_bvalue(Value,Options,Value,PPValue) :- solver_pp_bvalue2(Value,Options,PPValue).
406
407		solver_pp_bvalue2(Value,Options,PPValue) :- member(truncate(Limit),Options),!,
408		translate_bvalue_with_limit(Value,Limit,PPValue). % should we also control expand_avl_upto ??
409		solver_pp_bvalue2(Value,Options,PPValue) :- member(truncate,Options),!,
410		translate_bvalue_with_limit(Value,10000,PPValue).
411		solver_pp_bvalue2(Value,_,PPValue) :- translate_bvalue(Value,PPValue).
412
413		% check if a typed expression references an unfixed deferred set in some inner node
414		predicate_uses_unfixed_deferred_set(TExpr) :- predicate_uses_unfixed_deferred_set(TExpr,_).
415
416		predicate_uses_unfixed_deferred_set(TExpr,CType) :-
417		unfixed_deferred_set_exists, % check first if some unfixed deferred set exists
418		map_over_typed_bexpr(solver_interface:uses_unfixed_ds_aux,TExpr,CType).
419		:- public uses_unfixed_ds_aux/2.
420		uses_unfixed_ds_aux(TExpr,DSType) :- get_texpr_type(TExpr,Type),
421		contains_unfixed_deferred_set(Type,DSType).
422
423		% find a typed id whose type references an unfixed deferred set
424		unfixed_typed_id_in_list(TID,CType,Constants) :-
425		unfixed_deferred_set_exists, % check first if some unfixed deferred set exists
426		member(TID,Constants), get_texpr_type(TID,CType),
427		contains_unfixed_deferred_set(CType).
428
429		:- use_module(library(lists),[maplist/3, include/3]).
430		type_check_in_machine_context(Predicates, TPredicates) :-
431		% create an empty type environment
432		% and store the known types of variables / constants
433		% otherwise, we might be unable to type variables from
434		% machines somewhere in the refinement hierarchy
435		% (their typing predicate might not be in the hypothesis)
436		% Definitions are also added to the environment since the typechecker
437		% inlines definitions.
438		env_empty(E),
439		b_get_machine_variables(V), b_get_machine_constants(C),
440		% add theory operators
441		full_b_machine(Machine),
442		get_section(operators,Machine,Operators),
443		keys_and_values(Operators,Ids,Ops),
444		foldl(env_store_operator,Ids,Ops,E,EWithTheories),
445		get_section(definitions, Machine, Definitions),
446		foldl(env_store_definition, Definitions, EWithTheories, EWithDefinitions),
447		% constants and variables
448		findall(b(identifier(Name),global(GlobalSet),[enumerated_set_element]),is_b_global_constant(GlobalSet,_Nr,Name),GC),
449		findall(b(identifier(Set),set(global(Set)),[given_set]),b_global_set(Set),GS),
450		add_identifiers_to_environment(V,EWithDefinitions,EV),
451		add_identifiers_to_environment(C,EV,EVC),
452		add_identifiers_to_environment(GC,EVC,EVCGC),
453		add_identifiers_to_environment(GS,EVCGC,EOut),
454		opentype(Predicates, EOut, Identifiers, DeferredSets, TPredicates),
455		% DeferredSets should be empty? I.e. should this be allowed to create new types?
456		% currently this would not work as these types have not been added/registered in b_global_sets ! kernel_objects:basic_type would fail
457		(DeferredSets = [] -> true
458		; include(problematic_id(DeferredSets),Identifiers,TErrIds),
459		maplist(get_texpr_id,TErrIds,ErrIds),
460		add_warning(solver_interface,'The types of some variables could not be determined: ',ErrIds),
461		fail).
462		% a possible refactoring for the above - however, it does not type with open identifiers
463		% reverted it for now
464		% bmachine:b_type_expressions(Predicates,[constants],_Types,TPredicates,Errors),
465		% add_all_perrors(Errors,[],type_expression_error),
466		% no_real_perror_occurred(Errors).
467
468		problematic_id(DeferredSets,TID) :- get_texpr_type(TID,Type),
469		uses_def_set(Type,DeferredSets).
470
471		uses_def_set(global(T),DeferredSets) :- member(T,DeferredSets).
472		uses_def_set(set(A),DeferredSets) :- uses_def_set(A,DeferredSets).
473		uses_def_set(seq(A),DeferredSets) :- uses_def_set(A,DeferredSets).
474		uses_def_set(couple(A,_),DeferredSets) :- uses_def_set(A,DeferredSets).
475		uses_def_set(couple(_,A),DeferredSets) :- uses_def_set(A,DeferredSets).
476		uses_def_set(record(F),DS) :- member(field(_,T),F), uses_def_set(T,DS).
477		% TO DO: add freetypes