1		% (c) 2009-2026 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(eval_strings,[
6		add_last_expression_to_unit_tests/0, print_last_expression/0, print_last_value_to_file/1,
7		indent_print_last_expression/0,
8		unsat_core_last_expression/0,
9		recheck_pp_of_last_expression/3,
10		last_expression_type/1, last_expression/2, get_last_result_value/3, clear_last_expression/0,
11		print_last_info/0, print_last_value/0, browse_repl_lets/0,
12		toggle_eval_det/0, toggle_normalising/0,
13		eval_string/2,eval_string/3,eval_string/4,eval_string_with_time_out/4,
14		eval_codes/6,
15		eval_expression_codes/7,
16		eval_file/6,
17		toggle_observe_evaluation/0,
18		set_eval_dot_file/1, unset_eval_dot_file/0,
19		turn_normalising_on/0, turn_normalising_off/0,
20		get_error_positions/1]).
21
22		:- use_module(library(lists)).
23		:- use_module(library(codesio),[format_to_codes/3]).
24		:- use_module(library(statistics),[min_max/3]).
25
26		:- use_module(error_manager).
27		:- use_module(tools).
28		:- use_module(debug).
29		:- use_module(external_functions,[observe_parameters/2]).
30		:- use_module(kernel_objects,[max_cardinality/2]).
31		%:- use_module(b_ast_cleanup,[get_sorted_ids/2,not_occurs_in_predicate/2]). % TO DO: move predicate calling this to another module
32		:- use_module(preferences,[get_computed_preference/2, get_preference/2,
33		temporary_set_preference/3, reset_temporary_preference/2]).
34
35		:- use_module(typing_tools,[create_maximal_type_set/2]).
36
37		:- use_module(module_information,[module_info/2]).
38		:- module_info(group,repl).
39		:- module_info(description,'Tools to evaluate B expressions and predicates passed as strings.').
40
41		:- use_module(bmachine,[b_get_machine_constants/1,b_get_machine_variables/1,
42		b_parse_machine_expression_from_codes/6,
43		b_parse_machine_predicate_from_codes_open/5,
44		b_parse_machine_subsitutions_from_codes/6]).
45		:- use_module(wdsrc(well_def_analyser),[analyse_wd_for_expr/4, annotate_wd/2]).
46		:- use_module(smt_solvers_interface(solver_dispatcher),[smt_solver_version/2, smt_solver_header_version/2]).
47		:- use_module(kernel_waitflags).
48		:- use_module(b_enumerate,[b_tighter_enumerate_values_in_ctxt/3]).
49		:- use_module(bsyntaxtree).
50		:- use_module(eval_let_store,[stored_let_value/3, add_stored_let_value/3,
51		retract_stored_let_value/3, reset_let_values/0,
52		extend_state_with_stored_lets/2, get_stored_let_typing_scope/1]).
53		:- use_module(logger,[writeln_log/1]).
54		:- use_module(probsrc(tools), [start_ms_timer/1,stop_ms_timer_with_debug_msg/2, get_elapsed_walltime/2]).
55
56
57		:- set_prolog_flag(double_quotes, codes).
58
59		% GENERAL EVAL for Expressions & Predicates
60
61		eval_string(String,StringResult) :- eval_string(String,StringResult,_EnumWarning,_).
62		eval_string(String,StringResult,EnumWarning) :- eval_string(String,StringResult,EnumWarning,_).
63		eval_string(String,StringResult,EnumWarning,LocalState) :- % String is an atom
64		atom_codes(String,Codes),
65		eval_codes(Codes,exists,StringResult,EnumWarning,LocalState,_).
66
67		eval_string_with_time_out(String,StringResult,EnumWarning,LocalState) :-
68		atom_codes(String,Codes),
69		eval_codes_with_time_out(Codes,exists,StringResult,EnumWarning,LocalState,_).
70
71		% evaluate a single formula from a file
72		% Solver is either default, or one of the solver names recognised in the REPL (sat, sat-z3, cdclt, prob, z3,...)
73		eval_file(Solver,Filename,OuterQuantifier,StringResult,EnumWarning,TypeInfo) :-
74		format('Solving ~w with ~w~n',[Filename,Solver]),
75		safe_read_string_from_file(Filename,utf8,Codes),
76		(Solver=default -> FullCodes=Codes
77		; translate_solver_to_prefix(Solver,Prefix) -> append(Prefix,Codes,FullCodes)
78		; add_error(eval_file,'Unknown solver name: ',Solver),
79		FullCodes=Codes
80		),
81		eval_codes_with_time_out(FullCodes,OuterQuantifier,StringResult,EnumWarning,_,TypeInfo),
82		debug_println(19,eval_file(Filename,StringResult,EnumWarning)).
83
84		%:- use_module(library(timeout)).
85		:- use_module(tools_meta,[safe_time_out/3]).
86		eval_codes_with_time_out(Codes,OuterQuantifier,StringResult,EnumWarning,LocalState,TypeInfo) :-
87		%format("Eval: ~s~n",[Codes]),
88		get_computed_preference(debug_time_out,DTO),
89		%print(debug_time_out(DTO)),nl,
90		safe_time_out(eval_codes(Codes,OuterQuantifier,StringResult,EnumWarning,LocalState,TypeInfo),DTO,TimeOutRes),
91		(TimeOutRes=time_out ->
92		StringResult = '**** TIME-OUT ****', print(StringResult), print(' ('),print(DTO), print('ms)'),nl,
93		EnumWarning = time_out
94		; true).
95
96		:- use_module(tools_meta,[call_residue/2]).
97		:- volatile current_codes/1.
98		:- dynamic current_codes/1.
99		set_current_codes(C) :- retractall(current_codes(_)), assertz(current_codes(C)).
100		%eval_codes(C,_,Res,E,L) :- print(eval_codes(C)),nl,fail.
101		eval_codes(E,Q,Res,EnumWarning,LS,TypeInfo) :-
102		call_residue(eval_codes2(E,Q,Res,EnumWarning,LS,TypeInfo),Residue),
103		check_residue_for_eval_strings_call(Residue,eval_codes(E,Q,Res,EnumWarning,LS,TypeInfo)).
104		eval_codes2(E,Q,Res,EnumWarning,LS,TypeInfo) :-
105		set_error_context(eval_codes),
106		reset_repl_lets, % remove invalid lets if required
107		catch(
108		eval_codes_aux0(E,Q,Res,EnumWarning,LS,TypeInfo),
109		enumeration_warning(Cause,ID,_,_,_),
110		(get_time_out_message(Cause,ID,CauseStr),
111		format_with_colour_nl(user_output,[red,bold],'VIRTUAL TIME-OUT forced by ~w',[CauseStr]),
112		EnumWarning = true,
113		Res = 'TIME-OUT'
114		)),
115		clear_error_context.
116
117		get_time_out_message(kodkod_timeout,_ProblemId,Msg) :- !, Msg = 'KODKOD'.
118		get_time_out_message(kodkod_error,_ProblemId,Msg) :- !, Msg = 'KODKOD ERROR'.
119		get_time_out_message(translating_for_kodkod,_Ids,Msg) :- !, Msg = 'UNABLE TO TRANSLATE TO KODKOD'.
120		get_time_out_message(_,_,'ENUMERATION WARNING').
121
122		:- use_module(library(between),[between/3]).
123
124		eval_codes_aux0("$$",_,Res,false,[],print_last_expression) :- !, Res='',
125		print_last_expression.
126		eval_codes_aux0("$",_,Res,false,[],print_last_info) :- !, Res='',
127		print_last_info.
128		eval_codes_aux0(":col",_,Res,false,[],print_last_expression) :- !, Res='',
129		toggle_colouring.
130		eval_codes_aux0(":recheck",_,Res,EnumWarning,[],recheck_pp_of_last_expression) :- !,
131		recheck_pp_of_last_expression(ascii,Res,EnumWarning).
132		eval_codes_aux0(Codes,_,Res,false,[],set_eval_repeat) :- append("!r",Rest,Codes),
133		number_codes(Nr,Rest), !, Res='',
134		set_eval_repeat(Nr).
135		eval_codes_aux0(Codes,OuterQuantifier,Res,EnumWarning,LocalState,TypeInfo) :-
136		append(":repeat ",RestC,Codes),!,
137		(scan_integer(RestC,Nr,RestC2) -> true
138		; eval_repeat(Nr) -> RestC2=RestC ; Nr=100,RestC2=RestC),
139		(Nr>0 -> Nr2=Nr ; add_warning(eval_strings,'Number of repetitions must be at least 1: ',Nr),Nr2=1),
140		start_ms_timer(T0),
141		repeat_eval_codes(1,Nr2,Walltimes,RestC2,OuterQuantifier,Res,EnumWarning,LocalState,TypeInfo),
142		get_elapsed_walltime(T0,Wall), Avg is Wall/Nr2,
143		min_max(Walltimes,Min,Max),
144		format('Walltime for ~w repetitions: ~w ms (average ~w ms, min ~w ms, max ~w ms)~n',[Nr2,Wall,Avg,Min,Max]).
145		eval_codes_aux0(Codes,_OuterQuantifier,Res,false,LocalState,list) :-
146		( append(":list ",Rest,Codes),
147		scan_identifier(Rest,IDCodes,Rest2), atom_codes(ID,IDCodes)
148		;
149		Codes = ":list", ID=help, Rest2=[]),
150		!,
151		(just_whitespace(Rest2) -> true ; add_error(eval_strings,'Ignoring extra argument: ',Rest2)),
152		list_information(ID,Res,LocalState).
153		eval_codes_aux0(Codes,OuterQuantifier,Res,EnumWarning,LocalState,TypeInfo) :-
154		match_command(":print", Codes,PredCodes),
155		TypeInfo=predicate(_),
156		!, EnumWarning=false,LocalState=[],
157		repl_parse_predicate_allow_ws(PredCodes,OuterQuantifier,Typed,TypeInfo),
158		nested_print_repl_expression(Typed),
159		Res=''.
160		eval_codes_aux0(Codes,OuterQuantifier,Res,EnumWarning,LocalState,TypeInfo) :-
161		match_command(":sym", Codes,PredCodes),
162		TypeInfo=predicate(_),
163		!, EnumWarning=false,LocalState=[],
164		repl_parse_predicate_allow_ws(PredCodes,OuterQuantifier,ExTyped,TypeInfo),
165		(is_existential_quantifier(ExTyped,_,Typed) -> true ; Typed=ExTyped),
166		format('Computing symmetry breaking predicate for: ',[]),
167		translate:print_bexpr(Typed),nl,
168		smt_symmetry_breaking:get_top_level_symmetry_breaking_predicates_decomposed(Typed,TS),
169		format('Symmetry breaking: ',[]), translate:print_bexpr(TS),nl,
170		Res=''.
171		eval_codes_aux0(Codes,OuterQuantifier,Res,EnumWarning,LocalState,TypeInfo) :-
172		match_command(":check-ast",Codes,PredCodes),
173		TypeInfo=predicate(_),
174		!, EnumWarning=false,LocalState=[],
175		format('Checking generated AST (Abstract Syntax Tree)~n',[]),
176		repl_parse_predicate_allow_ws(PredCodes,OuterQuantifier,Typed,TypeInfo),
177		(bsyntaxtree:check_ast(Typed) -> Res='TRUE' ; Res='FALSE').
178		eval_codes_aux0(Codes,_OuterQuantifier,Res,EnumWarning,LocalState,TypeInfo) :-
179		match_command(":components", Codes,PredCodes),
180		TypeInfo=predicate(_),
181		!, EnumWarning=false,LocalState=[],
182		repl_parse_predicate_allow_ws(PredCodes,no_quantifier,Typed,TypeInfo),
183		predicate_components(Typed,Components),
184		maplist(print_component,Components),
185		Res=''.
186		eval_codes_aux0(Codes,OuterQuantifier,Res,EnumWarning,LocalState,TypeInfo) :-
187		match_command(":compile",Codes,PredCodes),
188		TypeInfo=predicate(_),
189		!, EnumWarning=false,LocalState=[],
190		(repl_parse_predicate_allow_ws(PredCodes,OuterQuantifier,Typed,TypeInfo)
191		-> write('Compiling: '), translate:print_bexpr(Typed),nl,
192		get_cur_state_for_repl(Typed,State),
193		b_compiler:b_optimize(Typed,[],[],State,NewTyped,no_wf_available),
194		nested_print_repl_expression(NewTyped), Res=''
195		; add_error(eval_strings,'Illegal predicate for compiling'),
196		Res='ERROR').
197		eval_codes_aux0(":wd",_,Res,EnumWarning,LocalState,analyse_wd_for_machine) :- !,
198		EnumWarning=false,LocalState=[],
199		well_def_analyser:analyse_wd_for_machine(_,_,Res).
200		eval_codes_aux0(":pinv",_,Res,EnumWarning,LocalState,analyse_wd_for_machine) :- !,
201		EnumWarning=false,LocalState=[],
202		start_timer(T1,W1),
203		well_def_analyser:analyse_invariants_for_machine(UnchangedNr,ProvenNr,UnProvenNr,TotPOsNr,[]),
204		stop_timer('% Time to run wd-prover on all invariant POs: ',T1,W1),
205		(TotPOsNr>0 -> Perc is (UnchangedNr+ProvenNr)*100/ TotPOsNr ; Perc = 100.0),
206		format('Proof summary for ~w POs (~2f % discharged): ~w unchanged, ~w proven, ~w unproven~n',
207		[TotPOsNr,Perc,UnchangedNr,ProvenNr,UnProvenNr]), Res=ProvenNr.
208		eval_codes_aux0(Codes,OuterQuantifier,Res,EnumWarning,LocalState,TypeInfo) :-
209		append(":wd ",PredCodes,Codes),
210		!,
211		set_current_codes(PredCodes),
212		(TypeInfo=predicate(_),repl_parse_predicate_allow_ws(PredCodes,OuterQuantifier,Typed,TypeInfo)
213		-> EnumWarning=false,LocalState=[],
214		analyse_wd_for_expr(Typed,_ResStr,Discharged,message), Res=Discharged
215		; eval_codes_error(Res,EnumWarning,LocalState,TypeInfo)
216		).
217		eval_codes_aux0(Codes,OuterQuantifier,Res,EnumWarning,LocalState,TypeInfo) :-
218		match_command(":wde",Codes,PredCodes), % perform WD analysis and solve transformed predicate
219		TypeInfo=predicate(_),
220		!,
221		set_current_codes(PredCodes),
222		repl_parse_predicate_allow_ws(PredCodes,OuterQuantifier,Typed,TypeInfo),
223		annotate_wd(Typed,NewTyped),
224		eval_predicate_in_cur_state(NewTyped,Res,EnumWarning,LocalState).
225		eval_codes_aux0(Codes,OuterQuantifier,Res,EnumWarning,LocalState,TypeInfo) :-
226		append(":check ",Rest,Codes),
227		TypeInfo=predicate(_),
228		!,
229		debug_println(20,check_recognised),
230		(eval_codes_aux(Rest,OuterQuantifier,Res,EnumWarning,LocalState,TypeInfo)
231		-> (Res== 'TRUE' -> true ;
232		atom_codes(S,Rest), add_error(check,':check predicate not TRUE: ',S)
233		)
234		; atom_codes(S,Rest), add_error(check,':check illegal predicate: ',S)
235		).
236		eval_codes_aux0(Codes,_OuterQuantifier,RRes,EnumWarning,LocalState,TypeInfo) :-
237		append(":exec ",Rest,Codes),
238		TypeInfo=subst,
239		!,
240		debug_println(4,'parsing substitution'),
241		repl_parse_substitution(Rest,Statement),
242		pp_eval_expr(Statement),
243		enter_new_error_scope(ScopeID,eval_codes_aux0),clear_all_errors_in_error_scope(ScopeID),
244		(tcltk_interface:tcltk_add_user_executed_statement(Statement,Updates,NewID)
245		-> format('Successfully executed statement leading to state: ~w~n',[NewID]),
246		Res = 'TRUE',LocalState=Updates
247		; translate:translate_substitution(Statement,Str),
248		format_with_colour_nl(user_output,[red],'Could not execute statement: ~w',[Str]),
249		Res = 'FALSE',LocalState=[]
250		),
251		EnumWarning=false,
252		print('Execution result: '),display_and_set_result(ScopeID,Res,RRes,EnumWarning),
253		(LocalState=[] -> true
254		; display_solution('Updates:~n',unknown,LocalState)).
255		eval_codes_aux0(Codes,OuterQuantifier,Res,EnumWarning,LocalState,TypeInfo) :- % let ID = EXPR construct
256		(append("let ",Rest,Codes),DotForm=false ; append(":let ",Rest,Codes), DotForm=true),
257		scan_identifier(Rest,IDCodes,Rest2),
258		atom_codes(ID,IDCodes),
259		(scan_to_equal(Rest2,Rest3) -> true
260		; DotForm=false -> debug_println(19,'Missing = sign for let-construction'),
261		fail % let mod 2 = 0 is a valid predicate
262		; debug_println(19,'Inserting missing = for :let'), Rest3=Rest2
263		),
264		!,
265		debug_println(20,let_recognised(ID)),
266		eval_codes_aux(Rest3,OuterQuantifier,Res,EnumWarning,LocalState,TypeInfo),
267		(store_let_id_last_value(ID) -> true ;
268		format_with_colour_nl(user_error,[red],'### Could not store let: ~w',[ID])).
269		eval_codes_aux0(Codes,_,Res,EnumWarning,LocalState,TypeInfo) :- % :s ID : store ID extracted from last predicate
270		(append(":s ",Rest,Codes) ; append(":store ",Rest,Codes)),
271		scan_identifier(Rest,IDCodes,Rest2),
272		atom_codes(ID,IDCodes),
273		Rest2=[], % TO DO: allow whitespace
274		!,
275		(get_last_predicate_value_for_id(ID,T,Val)
276		-> store_let_id_last_value(ID), translate_bvalue_with_limit_and_col(Val,50,VS),
277		format('Stored ~w = ~w~n',[ID,VS]), Res=Val, TypeInfo = T
278		; format_with_colour_nl(user_error,[red],'### Could not find value for ~w in last predicate',[ID]),
279		Res=error, TypeInfo=error),
280		EnumWarning=false, LocalState=[].
281		eval_codes_aux0(Codes,_,Res,EnumWarning,LocalState,TypeInfo) :- % :u ID : remove let for ID
282		(append(":u ",Rest,Codes) ; append(":unlet ",Rest,Codes)),
283		scan_identifier(Rest,IDCodes,Rest2),
284		atom_codes(ID,IDCodes),
285		Rest2=[], % TO DO: allow whitespace
286		!,
287		(retract_stored_let_value(ID,_,_) ->
288		format('Undefined let ~w~n',[ID]), Res=ID, TypeInfo = unlet,
289		reset_parse_cache % TO DO: maybe remove just all cached expressions using ID
290		; format_with_colour_nl(user_error,[red],'### Could not find let for ~w. Use :b to browse your lets.',[ID]), Res=error, TypeInfo=error),
291		EnumWarning=false, LocalState=[].
292		eval_codes_aux0(":b",_,Res,EnumWarning,LocalState,browsing) :-
293		!,EnumWarning=false, LocalState=[],
294		get_repl_lets_info(Res), print(repl_lets(Res)),nl.
295		eval_codes_aux0(Codes,_,Res,EnumWarning,LocalState,typing) :-
296		(append(":t ",Expression,Codes) ; append(":type ",Expression,Codes)),
297		% :t Expression Haskell like command
298		!, EnumWarning=false, LocalState=[],
299		repl_typing_scope(TypingScope),
300		(b_parse_machine_expression_from_codes(Expression,TypingScope,_Typed,Type,true,Error)
301		-> (Error=none
302		-> %translate:pretty_type(Type,PrettyType), % will print seq(.)
303		create_maximal_type_set(Type,MaxTS), translate_bexpression(MaxTS,PrettyType),
304		(max_cardinality(Type,Card) -> true ; Card='??'),
305		ajoin([PrettyType,' /* card=',Card,' */'],Res),
306		print(Res),nl
307		; (Error=type_error -> get_type_error(Res) ; Res = 'SYNTAX ERROR'),
308		print_red('Not a valid expression'),nl)
309		; print_red('Parsing failed'),nl,
310		Res = 'SYNTAX ERROR').
311		% TO DO: add bind(VAR,EXPR_Val) for next eval
312		eval_codes_aux0(Codes,_,Res,EnumWarning,LocalState,TypeInfo) :-
313		append(":find-value ",Codes1,Codes),
314		find_value_options(Options,Codes1,ExpressionCodes),
315		EnumWarning=false, LocalState=[],
316		!,
317		(repl_parse_expression(ExpressionCodes,TExpr,TypeInfo,Error),
318		Error = none ->
319		eval_expression_direct(TExpr,GoalValue),
320		get_texpr_type(TExpr,Type),
321		(Options = [Opt1|_], GoalValue \= string(_)
322		-> add_warning(find_value,':find-value option only useful when using string as target: ',Opt1)
323		; true),
324		findall(list([ID,Kind,MatchMsg]),
325		(tcltk_interface:find_value_in_cur_state(GoalValue,Type,Options,match(Kind,ID,Path)),
326		format_to_codes('~w~n',[Path],MatchMsgC),
327		with_translation_mode(unicode, translate_bvalue_with_limit_and_col_always(Path,10000,PathS)), % always use colour; useful to show match
328		format('* match inside ~w ~w @ path: ~w~n',[Kind,ID,PathS]),
329		atom_codes(MatchMsg,MatchMsgC)),Res)
330		; eval_codes_error(Res,EnumWarning,LocalState,TypeInfo)
331		).
332		eval_codes_aux0(Codes,_OuterQuantifier,OuterRes,false,LocalState,TypeInfo) :- TypeInfo=predicate(_),
333	?	available_krt_prover(_,Provers,CommandStr),
334		match_command(CommandStr,Codes,PredCodes), % commands like :pp, :ml, :krt
335		!,
336		% we ignore OuterQuantifier for proof commands and use forall:
337		temporary_set_preference(use_common_subexpression_elimination,false,CHG),
338		call_cleanup(repl_parse_predicate_allow_ws(PredCodes,forall,ExTyped,TypeInfo),
339		reset_temporary_preference(use_common_subexpression_elimination,CHG)),
340		LocalState=[],
341		prove_sequent_with_krt_provers(Provers,ExTyped,Res),
342		format('Universally quantified predicate is ',[]),
343		(Res=proved
344		-> print_green('PROVED'),
345		OuterRes='TRUE' % for -evalt
346		; print_red(Res),
347		OuterRes = 'UNKNOWN' % for -evalu
348		),
349		format(' with ~w~n',[Provers]).
350		eval_codes_aux0(Codes,_OuterQuantifier,Res,EnumWarning,LocalState,TypeInfo) :- TypeInfo=predicate(_),
351		append(":forall ",PredCodes,Codes), % like krt, ml, pp command, but using ProB
352		!,
353		eval_codes_aux(PredCodes,forall,Res,EnumWarning,LocalState,TypeInfo).
354		eval_codes_aux0(Codes,OuterQuantifier,Res,false,LocalState,TypeInfo) :- TypeInfo=predicate(_),
355	?	available_smt_solver(Solver,CommandStr), % :z3, :cvc5, ...
356		append(CommandStr,PredCodes,Codes),
357		!,
358		solve_using_smt_solver(Solver,PredCodes,no_prolog,OuterQuantifier,Res,LocalState,TypeInfo).
359		eval_codes_aux0(Codes,OuterQuantifier,Res,false,LocalState,TypeInfo) :- TypeInfo=predicate(_),
360		append(":fuzz ",Codes2,Codes), % like krt, ml, pp command, but using ProB
361		available_smt_solver(Solver,[_|CommandStr]), % :z3-double-check, :prob-chr-double-check, ... without :
362		append(CommandStr,PredCodes,Codes2),
363		% typical command :fuzz prob-chr-double-check @FUZZ or :fuzz prob-double-check @FUZZ-ARITH-WD
364		!,
365		format('Fuzzing solver ~w~n',[Solver]),
366		bb_put(fuzz_counter_nr,0),
367		(repeat,
368		bb_get(fuzz_counter_nr,Nr), Nr1 is Nr+1, bb_put(fuzz_counter_nr,Nr1),
369		format('Fuzzing attempt ~w~n',[Nr1]),
370		solve_using_smt_solver(Solver,PredCodes,no_prolog,OuterQuantifier,Res,LocalState,TypeInfo),
371		check_error_occured(double_check_smt_result,_)
372		).
373		eval_codes_aux0(":z3-version",_,Res,false,LS,TypeInfo) :- LS=[], TypeInfo=string,
374		smt_solver_version(z3,Version),
375		smt_solver_header_version(z3,HVersion),
376		!,
377		format('Z3 version is ~w (ProB was compiled against ~w)~n',[Version,HVersion]),
378		Res = Version.
379		eval_codes_aux0(Codes,OuterQuantifier,Res,false,LocalState,TypeInfo) :- TypeInfo=predicate(_),
380	?	available_smt_solver_for_file(Solver,FileCommandStr), % :z3-file, ...
381		append(FileCommandStr,FileCodes,Codes),
382		!,
383		solve_using_smt_solver_from_file(Solver,FileCodes,OuterQuantifier,Res,LocalState,TypeInfo).
384		eval_codes_aux0(Codes,OuterQuantifier,Res,EnumWarning,LocalState,TypeInfo) :- %TypeInfo=predicate(_),
385		append(":kodkod ",PredCodes,Codes), !,
386		temporary_set_preference(use_solver_on_load,kodkod,CHG),
387		call_cleanup(eval_codes_aux(PredCodes,OuterQuantifier,Res,EnumWarning,LocalState,TypeInfo),
388		reset_temporary_preference(use_solver_on_load,CHG)).
389		eval_codes_aux0(Codes,OuterQuantifier,Res,EnumWarning,LocalState,TypeInfo) :-
390		append(":chr ",PredCodes,Codes), !,
391		temporary_set_preference(use_chr_solver,true,CHG),
392		call_cleanup(eval_codes_aux(PredCodes,OuterQuantifier,Res,EnumWarning,LocalState,TypeInfo),
393		reset_temporary_preference(use_chr_solver,CHG)).
394		eval_codes_aux0(Codes,OuterQuantifier,Res,EnumWarning,LocalState,TypeInfo) :-
395		append(":cse ",PredCodes,Codes), !,
396		temporary_set_preference(use_common_subexpression_elimination,true,CHG),
397		call_cleanup(eval_codes_aux(PredCodes,OuterQuantifier,Res,EnumWarning,LocalState,TypeInfo),
398		reset_temporary_preference(use_common_subexpression_elimination,CHG)).
399		eval_codes_aux0(Codes,_OuterQuantifier,Res,EnumWarning,LocalState,TypeInfo) :-
400		get_minmax_command(Codes,OptMode,LambdaExprC), % :min or :max
401		repl_parse_expression(LambdaExprC,LambdaExpr,TypeInfo,Error),
402		Error=none,
403		closures:is_lambda_comprehension_set(LambdaExpr,Parameters,TypedPred,OptExpr),
404		format(' ~w lambda expression of type ~w~n',[OptMode,TypeInfo]),
405		!,
406		get_cur_state_for_repl(LambdaExpr,EState),
407		optimizing_solve_predicate(OptMode,EState, Parameters,TypedPred,OptExpr,OptVal,LocalState),
408		translate:translate_bvalue(OptVal,OS),
409		format('OPTIMAL VALUE = ~w~nFOR SOLUTION:~n',[OS]),
410		display_solution('',Parameters,LocalState),
411		Res = OS,EnumWarning=false.
412		eval_codes_aux0(Codes,OuterQuantifier,Res,EnumWarning,LocalState,TypeInfo) :-
413		get_minmax_command(Codes,OptMode,PredCodes),
414		!,
415		set_eval_mode(optimizing(OptMode)),
416		call_cleanup(eval_codes_aux(PredCodes,OuterQuantifier,Res,EnumWarning,LocalState,TypeInfo),
417		unset_eval_mode).
418
419		eval_codes_aux0(Codes,OuterQuantifier,Res,EnumWarning,LocalState,TypeInfo) :-
420		eval_codes_aux(Codes,OuterQuantifier,Res,EnumWarning,LocalState,TypeInfo).
421
422		eval_codes_aux(Expression,_,Res,EnumWarning,LocalState,TypeInfo) :- TypeInfo=expression(_),
423		repl_parse_expression(Expression,Typed,Type,Error),
424		(Error=none ; Error=type_error),
425		!,
426		eval_expression_codes2(Typed,Type,Error,Res,EnumWarning,LocalState,TypeInfo,[]).
427		eval_codes_aux(Expression,OuterQuantifier,Res,EnumWarning,LocalState,TypeInfo) :-
428		TypeInfo=predicate(_),
429		repl_parse_predicate_for_solving(Expression,OuterQuantifier,Typed,TypeInfo),
430		!,
431		eval_predicate_in_cur_state(Typed,Res,EnumWarning,LocalState).
432		eval_codes_aux(_E,_,Res,EnumWarning,LocalState,TypeInfo) :- eval_codes_error(Res,EnumWarning,LocalState,TypeInfo).
433
434		% an error occured: provide user feedback
435		eval_codes_error(Res,false,[],TypeInfo) :-
436		%findall(S,check_error_occured(S,_),L), print(errs(L)),nl,
437		(check_error_occured(type_expression_error,_) -> Res = 'TYPE ERROR', TI = error
438		; Res = 'SYNTAX ERROR', TI = syntax_error
439		),
440		show_error_pos,
441		((nonvar(TypeInfo),TypeInfo=predicate(_)) -> write('Not a valid predicate'),nl
442		; (nonvar(TypeInfo),TypeInfo=expression(_)) -> write('Not a valid expression'),nl
443		; write('Not a valid expression or predicate'),nl
444		),
445		TypeInfo=TI.
446
447
448		repeat_eval_codes(Try,Nr,[Wall|TWall],RestC,OuterQuantifier,Res,EnumWarning,LocalState,TypeInfo) :- Try >= Nr,!,
449		formatsilent('>>> (~w/~w)~n',[Try,Nr]),
450		start_ms_timer(T1),
451		eval_codes_aux0(RestC,OuterQuantifier,Res,EnumWarning,LocalState,TypeInfo),
452		TWall=[],get_elapsed_walltime(T1,Wall).
453		repeat_eval_codes(Try,Nr,[Wall|TWall],RestC,OuterQuantifier,Res,EnumWarning,LocalState,TypeInfo) :-
454		formatsilent('>>> (~w/~w)~n',[Try,Nr]),
455		start_ms_timer(T1),
456		eval_codes_aux0(RestC,OuterQuantifier,_Res,_EnumWarning,_LocalState,_TypeInfo),
457		get_elapsed_walltime(T1,Wall),
458		reset_errors,
459		Try1 is Try+1,
460		repeat_eval_codes(Try1,Nr,TWall,RestC,OuterQuantifier,Res,EnumWarning,LocalState,TypeInfo).
461
462		% ------------------
463
464		% a separate predicate for evaluating expressions
465		eval_expression_codes(Expression,Res,EnumWarning,LocalState,Typed,TypeInfo,Options) :-
466		repl_parse_expression(Expression,Typed,Type,Error),
467		(Error=none ; Error=type_error),
468		eval_expression_codes2(Typed,Type,Error,Res,EnumWarning,LocalState,TypeInfo,Options).
469		eval_expression_codes2(Typed,Type,Error,Res,EnumWarning,LocalState,TypeInfo,Options) :-
470		(Error=type_error
471		-> show_error_pos,print('TYPE ERROR'),nl,
472		get_type_error(Res), EnumWarning=false, LocalState=[], TypeInfo=error
473		; pp_eval_expr(Typed),
474		(Type=pred
475		-> eval_predicate_in_cur_state(Typed,Res,EnumWarning,LocalState) % happens for DEFINITIONS ??
476		% TypeInfo unification will fail ??? TO DO : investigate !!
477		; eval_expression(Typed,Res,Options),
478		EnumWarning=false,LocalState=[]),
479		extract_type_information(Typed,TypeInfo)
480		).
481
482		% optionally cache parsing results, avoid overhead of Java B parser call and socket communication
483		% especially useful for latex_processor with while loops
484		:- dynamic parse_expr_cache/5, parse_pred_cache/5.
485		:- use_module(library(terms),[term_hash/2]).
486		%:- use_module(covsrc(hit_profiler),[add_profile_hit/1]).
487		% TO DO: try number_codes, TRUE, FALSE, simple identifier to avoid calling Java
488		repl_parse_expression(Expression,Typed,Type,Error) :-
489		get_preference(repl_cache_parsing,true),
490		term_hash(Expression,H),!,
491		(parse_expr_cache(H,Expression,CTyped,CType,CError) -> true
492		; parse_pred_cache(H,Expression,_,_,_)
493		-> !, fail % we have already parsed it as a predicate; fail so that we call repl_parse_predicate later
494		; repl_parse_expression_direct(Expression,CTyped,CType,CError), %format('Cached: ~s~n',[Expression]),
495		assertz(parse_expr_cache(H,Expression,CTyped,CType,CError))
496		),
497		Typed=CTyped, Type=CType, Error=CError.
498		%hit_profiler:add_profile_hit(parse_expr_cache).
499		repl_parse_expression(Expression,Typed,Type,Error) :-
500		repl_parse_expression_direct(Expression,Typed,Type,Error).
501
502		repl_parse_expression_direct(Expression,Typed,Type,Error) :-
503		%hit_profiler:add_profile_hit(parse_expr),
504		set_current_codes(Expression),
505		debug_format(20,"parsing_as_expression: '~s'~n",[Expression]),
506		%open('repl_parsing.txt',append,S),format(S,'~s~n',[Expression]),close(S),
507		repl_typing_scope(TypingScope),
508		b_parse_machine_expression_from_codes(Expression,TypingScope,Typed,Type,type_errors_only,Error),
509		debug_println(20,parse_result(Error,Type)). %translate:print_bexpr(Typed),nl,
510
511
512		:- use_module(bmachine,[b_get_properties_from_machine/1,b_get_invariant_from_machine/1]).
513		repl_parse_predicate_allow_ws(WS,_OuterQuantifier,Typed,TypeInfo) :-
514		is_whitspace(WS), !, % no argument provided; use last expr
515		(last_expression(pred,Typed,_)
516		-> extract_type_information(Typed,TypeInfo)
517		; last_expression(_,_,_) -> add_error(repl_parse_predicate,'Last REPL expression is not a predicate'),fail
518		; add_error(repl_parse_predicate,'Evaluate a predicate first or provide it as an argument'),fail
519		).
520		repl_parse_predicate_allow_ws(PredCodes,OuterQuantifier,Typed,TypeInfo) :-
521		repl_parse_predicate(PredCodes,OuterQuantifier,Typed,TypeInfo).
522
523		repl_parse_predicate_for_solving(PredCodes,OuterQuantifier,Typed,TypeInfo) :-
524		% allow some left propagations of failure/truth in ast_cleanup which would be done by the solver anyway:
525		call_cleanup((temporary_set_preference(allow_improving_wd_mode,true,Change),
526		repl_parse_predicate(PredCodes,OuterQuantifier,Typed,TypeInfo)),
527		reset_temporary_preference(allow_improving_wd_mode,Change)).
528
529		:- use_module(b_operation_guards,[get_unsimplified_operation_guard/2]).
530		repl_parse_predicate("@INVARIANT",_OuterQuantifier,Typed,TypeInfo) :-
531		b_get_invariant_from_machine(Invariant),!,
532		Typed=Invariant,extract_type_information(Typed,TypeInfo).
533		repl_parse_predicate("@PROPERTIES",_OuterQuantifier,Typed,TypeInfo) :-
534		b_get_properties_from_machine(Properties),!,
535		Typed=Properties,extract_type_information(Typed,TypeInfo).
536		%TODO: @ASSERTIONS for b_get_assertions_from_main_machine
537		repl_parse_predicate(Codes,_OuterQuantifier,Typed,TypeInfo) :-
538		append("@GUARD-",SOp,Codes),
539		atom_codes(Operation,SOp),
540		(get_unsimplified_operation_guard(Operation,Guard) -> true
541		; add_error(eval_strings,'Unknown operation: ',Operation),
542		Guard = b(falsity,pred,[])
543		),
544		Typed=Guard,extract_type_information(Typed,TypeInfo).
545		repl_parse_predicate(Codes,_OuterQuantifier,Typed,TypeInfo) :-
546		append("@FUZZ",Qualifier,Codes),
547		% can be useful, e.g., in !r10000 and :repeat :prove-double-check @FUZZ-BF-IMP
548		!,
549		parse_fuzz_qualifier(Qualifier,RequireWD,Fuzzer),
550		generate_fuzz_pred(Typed,RequireWD,Fuzzer),
551		write('@FUZZ = '),translate:print_bexpr_with_limit_and_typing(Typed,20000,all),nl, flush_output,
552		(debug_mode(on)
553		-> tools_printing:nested_write_term_to_codes(Typed,Cs), format('% Prolog term:~n~s~n',[Cs]) ; true),
554		extract_type_information(Typed,TypeInfo).
555		repl_parse_predicate(Codes,OuterQuantifier,Typed,TypeInfo) :-
556		append("@RANDOMISE",Rest,Codes),!,
557		% example use :prove-double-check @RANDOMISE x:@INT..@INT => x*@INT <= @INT
558		randomiser(NewCodes,Rest,[]),
559		formatsilent('Transformed input into ~s~n',[NewCodes]),
560		repl_parse_predicate(NewCodes,OuterQuantifier,Typed,TypeInfo).
561		repl_parse_predicate([First|PredCodes],OuterQuantifier,Typed,TypeInfo) :-
562		(First = 35 ; First = 64), % # or @ or #file or @file
563		( append("file",[Code1|FileCodes],PredCodes) -> true
564		; append("FILE",[Code1|FileCodes],PredCodes)
565		),
566		(Code1=32 -> true ; Code1=61), % space or equal = sign
567		(FileCodes = [46,Code2|_] % 46 is the dot.
568		-> Code2 \= 32, Code2 \= 40 % we do not have existential quantifer #file .(PRED)
569		% TODO: check for other whitespace than 32 (40 is open parenthesis)
570		; true),
571		!,
572		atom_codes(Filename,FileCodes),
573		format('Reading predicate from file: ~w~n',[Filename]),
574		statistics(walltime,[T1,_]),
575		safe_read_string_from_file(Filename,utf8,Codes),
576		%format('Read:~n~s~n',[Codes]),nl,
577		statistics(walltime,[T2,_]), Delta1 is T2-T1,
578		(debug_mode(off) -> true ; length(Codes,NrC), format('Read ~w characters in ~w ms~n',[NrC,Delta1])),
579		(repl_get_prolog_predicate(Codes,clean_up_pred,Typed,TypeInfo)
580		-> true
581		; repl_parse_predicate_direct(Codes,OuterQuantifier,Typed,TypeInfo)
582		),
583		statistics(walltime,[T3,_]), Delta2 is T3-T2,
584		(debug_mode(off) -> true ; format('Parsed and typechecked predicate in ~w ms~n',[Delta2])).
585		repl_parse_predicate(PredCodes,OuterQuantifier,Typed,TypeInfo) :-
586		repl_parse_predicate2(PredCodes,OuterQuantifier,Typed,TypeInfo).
587
588		repl_parse_predicate2(PredCodes,OuterQuantifier,Typed,TypeInfo) :-
589		get_preference(repl_cache_parsing,true),
590		term_hash(PredCodes,H),!,
591		(parse_pred_cache(H,PredCodes,OuterQuantifier,CTyped,CTypeInfo) -> true
592		; repl_parse_predicate_direct(PredCodes,OuterQuantifier,CTyped,CTypeInfo),
593		assertz(parse_pred_cache(H,PredCodes,OuterQuantifier,CTyped,CTypeInfo))
594		),
595		Typed=CTyped, TypeInfo=CTypeInfo.
596		repl_parse_predicate2(PredCodes,OuterQuantifier,Typed,TypeInfo) :-
597		repl_parse_predicate_direct(PredCodes,OuterQuantifier,Typed,TypeInfo).
598
599		repl_parse_predicate_direct(PredCodes,OuterQuantifier,Typed,TypeInfo) :-
600		repl_typing_scope(TypingScope),
601		b_parse_machine_predicate_from_codes_open(OuterQuantifier,PredCodes,
602		% will also mark outer variables so that they are not removed
603		[],TypingScope,Typed),!,
604		pp_eval_expr(Typed),
605		extract_type_information(Typed,TypeInfo).
606
607
608		:- use_module(probsrc(tools), [split_chars/3]).
609		parse_fuzz_qualifier(Codes,RequireWD,Fuzzer) :-
610		split_chars(Codes,"-",Options),
611		(Options = [ [] | Opt2] -> true ; Opt2=Options),
612		qualifiers2fuzzer(Opt2,RequireWD,Fuzzer).
613
614		% parse qualifiers like @FUZZ-AB-EWD or @FUZZ-SAT ....
615		% EWD suffix: ensure WD by construction
616		% WD suffix: filter WD by checking and failing if not WD
617		% no suffix: accept what has been generated by the fuzzer
618		qualifiers2fuzzer(["CLASSIC"|T],RequireWD,classic) :- !, qualifiers2reqwd(T,RequireWD,_).
619		qualifiers2fuzzer(["IMP"|T],ReqWD,banditfuzz(Opts,implication,EnsureWD)) :- !,
620		get_opts(T,Opts,TT), qualifiers2reqwd(TT,ReqWD,EnsureWD).
621		qualifiers2fuzzer([Opt|T],ReqWD,banditfuzz([BFOpt|Opts],TopLevelOperator,EnsureWD)) :-
622		core_bf_opt(Opt,BFOpt,TopLevelOperator), !,
623		get_opts(T,Opts,TT), qualifiers2reqwd(TT,ReqWD,EnsureWD).
624		qualifiers2fuzzer(T,ReqWD,banditfuzz(Opts,implication,EnsureWD)) :- get_opts(T,Opts,TT), Opts \= [], !,
625		qualifiers2reqwd(TT,ReqWD,EnsureWD).
626		qualifiers2fuzzer(T,ReqWD,banditfuzz(EnsureWD)) :- !, qualifiers2reqwd(T,ReqWD,EnsureWD).
627
628		core_bf_opt("AB",atelierb_safe,implication).
629		core_bf_opt("ARITH",arithmetic_only,implication).
630		core_bf_opt("CNF",cnf,conjunct).
631		core_bf_opt("SAT",sat_only,implication).
632		core_bf_opt("Z3",z3safe,implication).
633
634		get_opts(["NOREAL"|T],[use_reals(false)|OT],Rest) :- !, get_opts(T,OT,Rest).
635		get_opts(["NOSTRING"|T],[use_strings(false)|OT],Rest) :- !, get_opts(T,OT,Rest).
636		get_opts(["NOINF"|T],[disallow_inf_sets(true)|OT],Rest) :- !, get_opts(T,OT,Rest).
637		get_opts(["SHALLOW"|T],[size(2)|OT],Rest) :- !, get_opts(T,OT,Rest).
638		get_opts(["DEEP"|T],[size(5)|OT],Rest) :- !, get_opts(T,OT,Rest).
639		get_opts([SIZEN|T],[size(Size)|OT],Rest) :-
640		append("SIZE",Digits,SIZEN), get_nr(Digits,0,Size),!, % Note : with Size=1 fuzz_node fails
641		get_opts(T,OT,Rest).
642		get_opts(T,[],T).
643
644		get_nr([],Acc,Acc).
645		get_nr([N|T],Acc,Res) :- Size is N-0'0, Size =< 9,
646		NewAcc is Acc*10+Size,
647		get_nr(T,NewAcc,Res).
648
649		qualifiers2reqwd([],RequireWD,EnsureWD) :- !, RequireWD=false,EnsureWD=no.
650		qualifiers2reqwd(["WD"],RequireWD,EnsureWD) :- !, RequireWD=true,EnsureWD=no.
651		qualifiers2reqwd(["EWD"],RequireWD,EnsureWD) :- !, RequireWD=false,EnsureWD=ensure_wd.
652		qualifiers2reqwd([Rest|_],true,false) :- format('Unrecognised @FUZZ qualifier: ~s~n',[Rest]).
653
654
655		% generate a fuzzed predicated
656		generate_fuzz_pred(Typed,RequireWD,Fuzzer) :-
657		(current_prolog_flag(system_type,development) -> true
658		; add_warning(eval_string,'@FUZZ only available when running probcli from source!'),
659		fail),
660		fuzz_predicate(Fuzzer,Pred),
661		%nl,write(Pred),nl,
662		clean_up_pred(Pred,[],Typed),
663		(RequireWD=false -> true
664		; % write('CHECKING WD: '), translate:print_bexpr(Typed),nl,
665		analyse_wd_for_expr(Typed,_ResStr,Discharged,silent) % use message to see output
666		-> (Discharged='TRUE' -> true
667		; generate_fuzz_pred(Typed,RequireWD,Fuzzer) %try again
668		)
669		).
670
671		:- use_module(bsyntaxtree, [find_typed_identifier_uses/2,create_exists/3]).
672		fuzz_predicate(classic,Pred) :-
673		use_module(extension('prolog_fuzzer/fuzzing')),
674		(generate(prob_ast_pred([]), Pred) -> true
675		; generate(prob_ast_pred([]), Pred) -> true % generation sometimes fails; try again
676		; Pred = b(truth,pred,[])
677		).
678		fuzz_predicate(banditfuzz(EnsureWD),RPred) :-
679		use_module(extension('banditfuzz/fuzzer'),[qfuzz/1]),
680		use_module(extension('banditfuzz/welldef'),[ensure_wd/2]),
681		(fuzzer:qfuzz(Pred) -> true
682		; write(retry),nl,fuzzer:qfuzz(Pred) -> true),
683		(find_typed_identifier_uses(Pred,Ids) -> true),
684		create_exists(Ids,Pred,QPred),
685		(EnsureWD=ensure_wd, % EnsureWD by adding WD POs
686		clean_up_pred(QPred,[],Pred2),ensure_wd(Pred2,RPred)
687		-> true
688		; RPred=QPred).
689		fuzz_predicate(banditfuzz(FOpts,TLOperator,EnsureWD),RPred) :- % fuzz with a particular top-level operator as target
690		use_module(extension('banditfuzz/bf_env'),[env/2]),
691		use_module(extension('banditfuzz/fuzzer'),[fuzz/3]),
692		use_module(extension('banditfuzz/welldef'),[ensure_wd/2]),
693		(bf_env:env(FOpts,Env),fuzzer:fuzz_node(TLOperator, Env, _, Pred) -> true
694		; add_warning(banditfuzz,'Fuzzing failed with options: ',[TLOperator,EnsureWD|FOpts]), fail),
695		(EnsureWD=ensure_wd,clean_up_pred(Pred,[],Pred2),ensure_wd(Pred2,RPred) -> true ; RPred=Pred).
696
697		% -----------------
698
699		:- use_module(library(random),[random/3, random/1]).
700		randomiser(Res) --> "@",random_int(Low,Up),!,
701		{random(Low, Up, R),
702		number_codes(R,Codes),
703		append(Codes,T,Res)},
704		randomiser(T).
705		randomiser([H|T]) --> [H],!, randomiser(T).
706		randomiser([]) --> "".
707
708		random_int(-9223372036854775809,9223372036854775808) --> "INTEGER".
709		random_int(-1024,1024) --> "INT".
710		random_int(1,1024) --> "NAT1".
711		random_int(0,1024) --> "NAT".
712
713
714		% ------------------
715
716		is_whitspace(Codes) :- is_whitspace(Codes,[]).
717		is_whitspace --> " ",is_whitspace.
718		is_whitspace --> "".
719
720		match_command(Command,Codes,Arguments) :-
721		append(Command,Args,Codes), % command matched
722		(Args = [32|Rest] -> Arguments = Rest
723		; Args=[] -> Arguments = []). % no whitespace after; also allow as command without args
724
725		repl_parse_substitution(Codes,Typed) :-
726		repl_typing_scope(TypingScope),
727		delete(TypingScope,variables,IntScope), % remove variables; otherwise we get clash warnings
728		delete(IntScope,variables_and_additional_defs,SubstScope), % ditto; but makes additional defs unavailable
729		% we could also always allow calling operations in expressions?
730		b_parse_machine_subsitutions_from_codes(Codes,[operation_bodies|SubstScope],
731		Typed,_Type,true,Error),
732		(Error=none -> true ; add_error(eval_strings,'Error occured while parsing substitution: ',Error),fail).
733
734
735		% repeat a pretty-printed version of the expression/predicate that is evaluated
736		pp_eval_expr(Typed) :-
737		%nl,nl,print('SOLVING:'),nl,nested_print_bexpr(Typed),nl,nl,
738		(preferences:get_preference(repl_unicode,true) ->
739		translate_subst_or_bexpr_in_mode(unicode,Typed,UnicodeString),
740		format(' ~w ~w~n',['\x21DD\',UnicodeString])
741		; true).
742
743		extract_type_information(b(exists(Parameters,_Typed),pred,_),predicate(exists(Parameters))) :- !.
744		extract_type_information(b(forall(Parameters,_LHS,_RHS),pred,_),predicate(forall(Parameters))) :- !.
745		extract_type_information(b(_,pred,_),predicate(no_outer_quantifier)) :- !.
746		extract_type_information(b(_,T,_),expression(T)).
747
748		%:- use_module(library(timeout)).
749		%:- use_module(library(file_systems)).
750
751		%
752		%
753		% eval_rule_file removed; now use: probcli -eval_rule_file /Users/leuschel/svn_root/NewProBPrivate/examples/B/Siemens/RuleValidation/Deploy/AssociativityXY_3_type.v /Users/leuschel/svn_root/NewProBPrivate/examples/B/Siemens/RuleValidation/MainRuleBaseFile.mch
754
755		% performance benchmark:
756		% time(eval_strings:test_parser('examples/Rules/sample.rule')).
757		% time(eval_strings:test_parser('examples/Rules/sample2.rule')).
758		% time(eval_strings:test_parser('examples/Rules/sudoku.rule')).
759		:- public test_parser/1.
760		test_parser(File) :- print(processing_rule_file(File)),nl,
761		safe_read_string_from_file(File,utf8,Codes),print(parsing),nl,
762		repl_typing_scope(TypingScope),
763		b_parse_machine_predicate_from_codes_open(exists,Codes,[],TypingScope,
764		_Typed),
765		print(done),nl.
766
767
768		% ----------
769		% EXPRESSIONS
770		% ----------
771
772		:- use_module(state_space,[current_state_id/1]).
773		:- use_module(store).
774		:- use_module(translate).
775		:- use_module(b_interpreter).
776
777		:- meta_predicate probcli_clpfd_overflow_mnf_call1(0).
778		:- meta_predicate probcli_clpfd_overflow_call1(0).
779
780		:- dynamic last_expansion_time/1.
781
782		:- use_module(eval_let_store,[extend_state_with_probids_and_lets/2]).
783		:- use_module(specfile, [get_current_state_for_b_formula/2]).
784		% get state for REPL as required by the provided typed expression/predicate
785		get_cur_state_for_repl(Typed,State) :-
786		retractall(last_expansion_time(_)),
787		statistics(walltime,[T1,_]),
788		get_current_state_for_b_formula(Typed,State1),
789		extend_state_with_probids_and_lets(State1,State),
790		statistics(walltime,[T2,_]), Delta is T2-T1,
791		assertz(last_expansion_time(Delta)).
792
793
794
795		:- use_module(kodkodsrc(kodkod), [current_solver_is_not_incremental/0]).
796		replace_expression_by_kodkod_if_enabled(Typed,NewExpression) :-
797		(replace_expression_by_kodkod_if_enabled_aux(Typed,NewExpression) -> true
798		; NewExpression=Typed).
799		replace_expression_by_kodkod_if_enabled_aux(Typed,NewExpression) :-
800		% do :kodkod replacment inside set comprehensions
801		get_texpr_expr(Typed,comprehension_set(Ids,Pred)),
802		get_preference(use_solver_on_load,kodkod),
803		\+ current_solver_is_not_incremental, % otherwise we cannot get all solutions
804		replace_kodkod_if_enabled(Ids,Pred,NewPred), % TO DO: we could pass a parameter that says we want all solutions here
805		get_preference(kodkod_symmetry_level,Symm),
806		(Symm > 0 , Pred \= NewPred
807		-> get_texpr_ids(Ids,I),
808		add_warning(kodkod,'KODKOD_SYMMETRY > 0, not all solutions to set comprehension may be computed: ',I,Typed)
809		% it seems too late now to set symmetry to 0; problem already loaded ?!?
810		; true),
811		get_texpr_info(Typed,Info),get_texpr_type(Typed,Type),
812		create_texpr(comprehension_set(Ids,NewPred),Type,Info,NewExpression).
813
814
815		eval_expression_direct(Typed,Value) :-
816		get_cur_state_for_repl(Typed,EState),
817		eval_expression_direct(Typed,EState,Value).
818		eval_expression_direct(Typed,EState,Value) :-
819		probcli_clpfd_overflow_mnf_call1(b_interpreter:b_compute_expression_nowf(Typed,[],EState,Value,'none',0)).
820
821		eval_expression(Typed,RRes,Options) :- eval_expression(Typed,RRes,_PrologTerm,Options).
822
823		% EnumWarnings are no longer returned but thrown if problematic
824		eval_expression(Typed,RRes,NValue,Options) :- %% print('Start Eval Expression: '),nl,flush_output,
825		enter_new_error_scope(ScopeID,eval_expression),
826		clear_all_errors_in_error_scope(ScopeID),
827		replace_expression_by_kodkod_if_enabled(Typed,Typed2),
828		set_last_expression(expr,Typed2,exception),
829		debug_println(5,'Start Eval Expression'),
830		%profile_reset, set_prolog_flag(profiling,on), % comment in to profile individual expression evaluations
831		(eval_expression_direct(Typed2,Value)
832		-> true
833		; set_last_expression(expr,Typed2,error),fail % probably wd-error
834		),
835		!,
836		%set_prolog_flag(profiling,off), print_profile, % comment in to profile individual expression evaluations
837		debug_println(5,'Normalising Value'),
838		normalise_eval_value(Value,NValue),
839		set_last_expression(expr,Typed2,NValue),
840		(member(silent_no_string_result,Options) -> RRes = '?'
841		;
842		debug_println(5,'Translating Value'),
843		translate_bvalue_with_col(NValue,Typed2,Result),
844		%get_only_critical_enum_warning(EnumWarning),
845		start_terminal_colour([dark_gray],user_output),
846		format(user_output,'Expression Value = ~n',[]), % TO DO: make output optional, e.g., for json trace replay
847		reset_terminal_colour(user_output),
848		display_and_set_result(ScopeID,Result,RRes,false),
849		display_dot_expr_result(Typed2,NValue) % TO DO: if we have a let with ID: use ID rather than result
850		).
851		eval_expression(_,Cause,error,_) :-
852		get_fail_error_cause(Cause), % TO DO: refactor and use abort_error_occured_in_error_scope,...
853		exit_error_scope(_ScopeID,_,eval_expression).
854
855
856		:- dynamic normalising_off/0.
857		toggle_normalising :- print('% Normalising Result Values: '),
858		(retract(normalising_off) -> print('ON')
859		; assertz(normalising_off),print('OFF')),nl.
860		turn_normalising_off :- (normalising_off -> true ; assertz(normalising_off)).
861		turn_normalising_on :- retractall(normalising_off).
862
863		normalise_eval_value(Value,NValue) :- normalising_off,!,
864		start_norm_timer(NT,NWT),
865		NValue=Value, stop_norm_timer(NT,NWT).
866		normalise_eval_value(Value,NValue) :-
867		%EXPAND=limit(100000), % expand up until 100,000 elements; don't expand SYMBOLIC
868		EXPAND=force, % don't expand definitely infinite sets + sets known larger than 20,000
869		% but sets marked with prob_annotation('SYMBOLIC') may be expanded!
870		debug_println(20,normalising(Value)),
871		start_norm_timer(NT,NWT),
872		( store:normalise_value_for_var(repl_result,EXPAND,Value,NValue),
873		stop_norm_timer(NT,NWT)
874		-> true
875		; stop_norm_timer(NT,NWT),
876		print_red('Could not normalise value:'),nl,
877		NValue=Value
878		).
879
880		get_fail_error_cause(Cause) :-
881		logged_error(identifier_not_found,_B,_C,_D), % print(logged_error(identifier_not_found,B,_C,_D)),
882		%atom_codes(B,Codes), append("Cannot find identifier",_,Codes),
883		!,
884		Cause = 'IDENTIFIER(S) NOT YET INITIALISED; INITIALISE MACHINE FIRST'.
885		get_fail_error_cause('NOT-WELL-DEFINED').
886
887		get_type_error(Cause) :- logged_error(A,B,_C,_D), % print(logged_error(A,B,C,D)),
888		A=type_expression_error,
889		atom_codes(B,Codes),
890		append("Unknown identifier",_,Codes),!,
891		Cause = 'UNKNOWN IDENTIFIER(S)'.
892		get_type_error('TYPE ERROR').
893
894
895		% -----------------
896
897
898
899		% options in REPL for :find-value
900		find_value_options([prefix]) --> "prefix ".
901		find_value_options([suffix]) --> "suffix ".
902		find_value_options([exact]) --> "exact ".
903		find_value_options([fuzzy]) --> "fuzzy ".
904		find_value_options([infix]) --> "infix ".
905		find_value_options([]) --> "".
906
907
908		% ----------
909		% PREDICATES
910		% ----------
911
912
913		:- volatile eval_repeat/1.
914		:- dynamic eval_repeat/1.
915
916		set_eval_repeat(X) :- format('Finding ~w first solutions for predicates~n',[X]),
917		retractall(eval_repeat(_)),assertz(eval_repeat(X)).
918
919		:- use_module(succeed_max,[succeed_max_call_id/3]). %succeed_max_call_id('$setup_constants',member(_,_),1)
920		test_bool_exists(EState, Parameters,Typed,LocalState,WF) :- eval_repeat(Nr),
921		format_with_colour_nl(user_output,[dark_gray],'** Finding first ~w solutions',[Nr]),
922		call_residue(succeed_max_call_id(test_bool_exists,
923		eval_strings:test_bool_exists2(EState, Parameters,Typed,LocalState,WF),Nr),Residue),
924		display_solution('Solution:~n',Parameters,LocalState),
925		(Residue = [] -> true ; print_red('RESIDUE = '), print_red(Residue),nl),
926		flush_output,
927		fail.
928		test_bool_exists(EState, Parameters,Typed,LocalState,WF) :-
929	?	test_bool_exists2(EState, Parameters,Typed,LocalState,WF).
930
931		:- use_module(extrasrc(optimizing_solver),[optimizing_solve_predicate/5,optimizing_solve_predicate/7]).
932		get_minmax_command(Codes,maximizing,PredCodes) :- append(":max ",PredCodes,Codes).
933		get_minmax_command(Codes,minimizing,PredCodes) :- append(":min ",PredCodes,Codes).
934		test_bool_exists2(EState, Parameters,Typed,LocalState,_WF) :- eval_mode(optimizing(OptMode)), !,
935		optimizing_solve_predicate(OptMode,EState, Parameters,Typed,LocalState).
936		test_bool_exists2(EState, Parameters,Typed,LocalState,WF) :- \+ eval_det, !,
937		% evaluate component wise
938		%init_wait_flags(WF,[expansion_context(test_bool_exists2,Parameters)]),
939		init_quantifier_wait_flag(no_wf_available,exists,Parameters,FreshOutputVars,unknown,WF),
940		b_interpreter:set_up_typed_localstate(Parameters,FreshOutputVars,TypedVals,[],LocalState,positive),
941		append(LocalState,EState,State),
942		b_interpreter_components:reset_unsat_component_info,
943		% NOTE: WF not passed to b_interpreter_components !
944	?	b_interpreter_components:b_trace_test_components_wf(Typed,State,TypedVals,WF),
945		\+ b_interpreter_components:unsat_component_exists.
946		test_bool_exists2(EState, Parameters,Typed,LocalState,WF) :-
947		%init_wait_flags(WF,[expansion_context(test_bool_exists2,Parameters)]),
948		init_quantifier_wait_flag(no_wf_available,exists,Parameters,FreshOutputVars,unknown,WF),
949	?	b_interpreter:set_up_typed_localstate(Parameters,FreshOutputVars,TypedVals,[],LocalState,positive),
950		b_tighter_enumerate_values_in_ctxt(TypedVals,Typed,WF),
951		b_interpreter:b_test_boolean_expression(Typed,LocalState,EState,WF).
952
953
954		:- use_module(eventhandling,[announce_event/1]).
955		%:- use_module(bmachine, [determine_type_of_formula/2]).
956
957		eval_predicate_in_cur_state(ExTyped,RRes,EnumWarning,LocalState) :-
958		get_cur_state_for_repl(ExTyped,State),!,
959		announce_event(start_solving),
960		eval_predicate(State,ExTyped,RRes,EnumWarning,LocalState),
961		announce_event(end_solving).
962		eval_predicate_in_cur_state(_ExTyped,RRes,EnumWarning,LocalState) :-
963		format_with_colour_nl(user_output,[red,bold],'UNKNOWN',[]),
964		RRes = 'UNKNOWN', EnumWarning=false, LocalState=[].
965
966		:- use_module(probsrc(solver_interface),[apply_kodkod_or_other_optimisations/3]).
967		replace_kodkod_if_enabled(Parameters,Typed,NewPredicate) :-
968		b_get_machine_constants(Constants),
969		b_get_machine_variables(Variables),
970		get_repl_lets_tids(LetIds),
971		append([Parameters,Variables,Constants,LetIds],Identifiers),
972		apply_kodkod_or_other_optimisations(Identifiers,Typed,NewPredicate).
973
974		eval_predicate(State,Typed,RRes,EnumWarning,LocalState) :-
975		%b_ast_cleanup:predicate_level_optimizations(Typed,Typed2),
976		% detect set partitions, ... no longer necessary ! as already called in b_ast_cleanup now
977		eval_predicate_aux(State,Typed,RRes,EnumWarning,LocalState).
978		eval_predicate_aux(State,ExTyped,RRes,EnumWarning,LocalState) :-
979		%ExTyped=b(exists(Parameters,Typed),pred,_I),
980		is_existential_quantifier(ExTyped,Parameters,Typed),
981		!,
982		%print('Existentially Quantified Predicate is '),flush_output,
983		replace_kodkod_if_enabled(Parameters,Typed,NTyped),
984		enter_new_error_scope(ScopeID,eval_predicate_exists), clear_all_errors_in_error_scope(ScopeID),
985		set_last_expression(pred,ExTyped,exception), % in case an exception occurs
986		(observe_parameters(true) -> observe_parameters(Parameters,LocalState) ; true),
987		(probcli_clpfd_overflow_call1((test_bool_exists(State, Parameters,NTyped,LocalState,WF),
988		eval_ground_wf(WF)))
989		-> get_only_critical_enum_warning(EnumWarning),
990		(eval_det -> Res = 'POSSIBLY TRUE' ; Res = 'TRUE'),
991		set_last_expression(pred,ExTyped,pred_true)
992		; get_enum_warning(EnumWarning),
993		% The result has to be ground for the eclipse interface to work as intended.
994		% Hence, we need to bind the LocalState (?)
995		LocalState = [],
996		Res = 'FALSE', set_last_expression(pred,ExTyped,pred_false)),
997		(eval_det, debug_level_active_for(20) -> portray_waitflags_and_frozen_state_info(WF,(LocalState,State)) ; true),
998		print('Existentially Quantified Predicate over '), print_parameters(Parameters),
999		print(' is '),display_and_set_result(ScopeID,Res,RRes,EnumWarning),
1000		(Res='FALSE' -> true
1001		; display_solution('Solution:~n',Parameters,LocalState)
1002		).
1003		eval_predicate_aux(State, ExTyped,RRes,EnumWarning,LocalState) :-
1004		ExTyped=b(forall(Parameters,TypedLHS,TypedRHS),pred,_I),!,
1005		%print('Universally Quantified Predicate is '),flush_output,
1006		enter_new_error_scope(ScopeID,eval_predicate_forall), clear_all_errors_in_error_scope(ScopeID),
1007		safe_create_texpr(negation(TypedRHS),pred,[try_smt],NegRHS),
1008		conjunct_predicates([TypedLHS,NegRHS],Conjunction), % LHS & not(RHS)
1009		replace_kodkod_if_enabled(Parameters,Conjunction,NConjunction),
1010		%translate:print_bexpr(Conjunction),
1011		set_last_expression(pred,ExTyped,exception), % in case an exception occurs
1012		(probcli_clpfd_overflow_call1((test_bool_exists(State, Parameters,NConjunction,LocalState,WF),
1013		eval_ground_wf(WF)))
1014		-> get_only_critical_enum_warning(EnumWarning),
1015		(eval_det -> Res = 'POSSIBLY TRUE' ; Res = 'FALSE'),
1016		set_last_expression(pred,ExTyped,pred_false)
1017		; get_enum_warning(EnumWarning),
1018		% The result has to be ground for the eclipse interface to work as intended.
1019		% Hence, we need to bind the LocalState (?)
1020		LocalState = [],
1021		Res = 'TRUE', set_last_expression(pred,ExTyped,pred_true)),
1022		print('Universally Quantified Predicate over '), print_parameters(Parameters),
1023		print(' is '),display_and_set_result(ScopeID,Res,RRes,EnumWarning),
1024		(Res='TRUE' -> true
1025		; display_solution('Counter example:~n',Parameters,LocalState)
1026		).
1027		eval_predicate_aux(State, Typed,RRes,EnumWarning,[]) :-
1028		enter_new_error_scope(ScopeID,eval_predicate), clear_all_errors_in_error_scope(ScopeID),
1029		debug_println(20,test_boolean_expression(Typed)),
1030		replace_kodkod_if_enabled([],Typed,NTyped),
1031		set_last_expression(pred,NTyped,exception), % in case an exception occurs
1032		% TO DO: the next does not decompose into components !?; either call solve_predicate if State=[] or call b_trace_test_components inside b_test_boolean_expression_cs
1033		(probcli_clpfd_overflow_call1(b_interpreter:b_test_boolean_expression_cs(NTyped,[],State,'none',0))
1034		-> Res='TRUE',set_last_expression(pred,Typed,pred_true),
1035		get_only_critical_enum_warning(EnumWarning)
1036		; Res='FALSE',set_last_expression(pred,Typed,pred_false),
1037		get_enum_warning(EnumWarning)
1038		),
1039		print('Predicate is '),display_and_set_result(ScopeID,Res,RRes,EnumWarning).
1040
1041		get_enum_warning(EnumWarning) :-
1042		(event_occurred_in_error_scope(enumeration_warning(_,_,_,_,_Critical))
1043		-> EnumWarning=true %,print(' ** ENUM WARNING ** ')
1044		; EnumWarning=false).
1045		get_only_critical_enum_warning(EnumWarning) :- EnumWarning=false.
1046		% we no longer distinguish between critical & non-critical; also assuming_finite_closure now fails (renamed to checking_finite_closure)
1047		% Enumeration warning means that not all cases have been looked at, but if a result is true then it is guaranteed to be true
1048
1049
1050		display_and_set_result(ScopeID,Res,RRes,EnumWarning) :-
1051		%error_manager:print_error_scopes,
1052		findall(TE,(specific_event_occurred_at_level(ScopeID,E),translate_error_event(E,TE)), Errors),
1053		(abort_error_occured_in_error_scope -> WDError=true ; WDError=false),
1054		(specific_event_occurred_at_level(ScopeID,identifier_not_found) -> IdNotFound=true ; IdNotFound=false),
1055		exit_error_scope(ScopeID,ErrOcc,display_and_set_result),
1056		ErrOcc=true, % TO DO: check which kind of error occured: could be CLPFD overflow
1057		!,
1058		show_error_pos,
1059		(WDError=true
1060		-> format_with_colour(user_output,[red,bold],'NOT-WELL-DEFINED (~w)',[Res]),
1061		RRes = 'NOT-WELL-DEFINED'
1062		; IdNotFound=true -> % should no longer happen; we check requirements first
1063		format_with_colour(user_output,[red,bold],'IDENTIFIER-NOT-FOUND-ERROR ~w',[Errors]),
1064		RRes = 'IDENTIFIER(S) NOT YET INITIALISED; INITIALISE MACHINE FIRST'
1065		; format_with_colour(user_output,[red,bold],'UNKNOWN ~w',[Errors]),
1066		RRes = 'UNKNOWN'
1067		),
1068		print_enum_warning(EnumWarning), nl.
1069		display_and_set_result(_,Res,RRes,EnumWarning) :-
1070		print_result(Res,EnumWarning), nl,
1071		(EnumWarning=false -> RRes=Res
1072		% ; Res = 'TRUE' -> RRes=Res % enumeration warning does not matter when solution found,
1073		% unless this is a universally quantified formula!
1074		% inner enum warnings are not propagated to EnumWarning anymore; so we remove this case above
1075		; RRes= 'UNKNOWN').
1076
1077		print_result('FALSE',false) :- !,
1078		start_terminal_colour(light_red,user_output),
1079		write('FALSE'),reset_terminal_colour(user_output).
1080		print_result('TRUE',false) :- !,
1081		start_terminal_colour(green,user_output),
1082		write('TRUE'),reset_terminal_colour(user_output).
1083		print_result(Res,false) :- !, write(Res).
1084		print_result(Res,_) :-
1085		(debug_mode(on)
1086		-> format_with_colour(user_output,[red,bold],'UNKNOWN [~w with ** ENUMERATION WARNING **]',[Res])
1087		; format_with_colour(user_output,[red,bold],'UNKNOWN',[])
1088		).
1089
1090
1091		:- use_module(tools_printing,[print_red/1,print_green/1,format_with_colour/4, format_with_colour_nl/4]).
1092		print_enum_warning(false) :- !.
1093		print_enum_warning(_) :- print_red(' [** ENUMERATION WARNING **]').
1094
1095		:- use_module(dotsrc(state_as_dot_graph),[print_cstate_graph/2]).
1096		display_sol_required :- silent_mode(off),!.
1097		display_sol_required :- eval_dot_file(_),!.
1098		%display_sol_required :- format(user_output,'Not showing solution~n',[]),trace,fail.
1099
1100		display_solution(HeaderStr,Parameters,LocalState) :-
1101		set_last_solution(Parameters,LocalState),
1102		(display_sol_required
1103		-> format(HeaderStr,[]),
1104		display_solution_aux(Parameters,LocalState),
1105		flush_output
1106		; true).
1107		display_solution_aux(Parameters,LocalState) :-
1108		(eval_det
1109		-> % copy_term(LocalState,CLS), % avoid triggering co-routines via numbervars
1110		% tools_meta:safe_numbervars(CLS,0,_),
1111		print_visible_solution_with_type(Parameters,LocalState)
1112		; debug_println(19,normalising_solution(LocalState)),
1113		normalise_solution(LocalState,NState)
1114		-> %translate:print_bstate(NState)
1115		print_visible_solution_with_type(Parameters,NState),
1116		%visualize_graph:tcltk_print_state_as_graph_for_dot(NState,'~/Desktop/out.dot')
1117		display_dot_solution(NState)
1118		; print_red('Could not normalise value(s):'),nl,
1119		translate:print_bstate(LocalState)
1120		),nl.
1121
1122		normalise_solution(LocalState,NormState) :- normalising_off,!, NormState=LocalState.
1123		normalise_solution(LocalState,NormState) :-
1124		start_norm_timer(NT,NWT),
1125		(normalise_store(LocalState,NormState) -> stop_norm_timer(NT,NWT) ; stop_norm_timer(NT,NWT),fail).
1126
1127		display_dot_expr_result(Expr,Value) :-
1128		(eval_dot_file(File)
1129		-> get_dot_expr_state(Expr,Value,NState,[]),
1130		debug_println(9,writing_dot_file(File)),
1131		print_cstate_graph(NState,File)
1132		; true).
1133
1134		% try and decompose an expression value into subvalues for better dot rendering
1135		get_dot_expr_state(b(couple(A,B),_,_),(VA,VB)) --> !,
1136		get_dot_expr_state(A,VA),
1137		get_dot_expr_state(B,VB).
1138		get_dot_expr_state(b(identifier(ID),_,_),Val) --> !, [bind(ID,Val)].
1139		get_dot_expr_state(_,Val) --> [bind(result,Val)].
1140
1141		% display_dot_solution([bind(result,NValue)]).
1142		display_dot_solution(NState) :-
1143		(eval_dot_file(File)
1144		-> debug_println(9,writing_dot_file(File)),
1145		print_cstate_graph(NState,File) ; true).
1146
1147		:- dynamic last_solution/2.
1148		set_last_solution(Parameters,LocalState) :-
1149		retractall(last_solution(_,_)),
1150		assertz(last_solution(Parameters,LocalState)).
1151
1152		% small utility to extract last result; if we had a predicate with just one existential variable extract its value:
1153		get_last_result_value(Parameter,Type,Value) :-
1154		get_last_predicate_value_for_typed_id(Parameter,[],T,V), % only allow single parameter; otherwise confusion may exist
1155		!,Value=V, Type=T.
1156		get_last_result_value(Expr,Type,Value) :- get_last_expr_type_and_value(Expr,Type,Value).
1157
1158		convert_result(T,V,Type,Value) :-
1159		(convert_aux(T,V,Type,Value) -> true ; Type=T,Value=V).
1160		convert_aux(pred,pred_true,boolean,pred_true).
1161		convert_aux(pred,pred_false,boolean,pred_false).
1162
1163		% try and extract a value for a give parameter from last solution for a predicate
1164		get_last_predicate_value_for_id(ID,Type,Val) :-
1165		get_texpr_id(Parameter,ID),get_last_predicate_value_for_typed_id(Parameter,_,Type,Val).
1166		get_last_predicate_value_for_typed_id(Parameter,Rest,Type,Value) :-
1167		last_expression(pred,_,pred_true), % we solved a predicate, look in solution environment
1168		last_solution(Parameters,LocalState),
1169		select(Parameter,Parameters,Rest),
1170		get_texpr_id(Parameter,ParameterID),
1171		get_texpr_type(Parameter,Type),
1172		member(bind(ParameterID,Value),LocalState).
1173
1174		:- volatile eval_dot_file/1, observe_parameters/1.
1175		:- dynamic eval_dot_file/1, observe_parameters/1.
1176		observe_parameters(false).
1177
1178		toggle_observe_evaluation :-
1179		(observe_parameters(false)
1180		-> print('Observing parameters'),nl,
1181		set_observe_evaluation(true)
1182		; print('Observing OFF'),nl,
1183		set_observe_evaluation(false)).
1184		set_observe_evaluation(T) :- retractall(observe_parameters(_)), assertz(observe_parameters(T)).
1185		set_eval_dot_file(F) :- unset_eval_dot_file,
1186		debug_println(5,setting_eval_dot_file(F)),
1187		assertz(eval_dot_file(F)).
1188		unset_eval_dot_file :- retractall(eval_dot_file(_)).
1189
1190		% ----------------
1191
1192		% print solution using type information of non-generated ids (unless in debug mode)
1193		print_visible_solution_with_type(Ids,Bindings) :- Ids = [_|_],
1194		debug_mode(off),
1195		exclude(generated_id,Ids,VisibleIds),!,
1196		print_solution_with_type2(VisibleIds,Bindings).
1197		print_visible_solution_with_type(Ids,Bindings) :- print_solution_with_type1(Ids,Bindings).
1198
1199		generated_id(b(_,_,I)) :- member(generated,I).
1200
1201		% print solution using type information
1202		print_solution_with_type1([],Bindings) :- !,print_solution_with_type2(unknown,Bindings).
1203		print_solution_with_type1(T,Bindings) :- print_solution_with_type2(T,Bindings).
1204
1205		print_solution_with_type2([],_) :- !. % can be non-empty due to generated ids being removed
1206		print_solution_with_type2([Identifier|TT],Bindings) :-
1207		def_get_texpr_id(Identifier,Varname),
1208		select(bind(Varname,Value), Bindings, VT),
1209		!,
1210		translate_bvalue_with_col(Value,Identifier,Result),
1211		print_binding(Varname,Result),
1212		(TT=[] -> nl ; print(' &'),nl,print_solution_with_type2(TT,VT)).
1213		print_solution_with_type2(unknown,[bind(Varname,Value)|VT]) :- !,
1214		(debug_mode(on) -> Lim=500 ; Lim=200),
1215		translate_bvalue_with_limit_and_col(Value,Lim,Result),
1216		print_binding(Varname,Result),
1217		(VT=[] -> nl ; print(' &'),nl,print_solution_with_type2(unknown,VT)).
1218		print_solution_with_type2(unknown,[]) :- !.
1219		print_solution_with_type2([Identifier|TT],Bindings) :-
1220		def_get_texpr_id(Identifier,Varname), !,
1221		% possibly ast_cleanup has removed all predicates involving Identifier, appears in test 2168 for level 1
1222		% add_internal_error('No binding for variable: ', print_solution_with_type2(Varname,Bindings)),
1223		get_texpr_type(Identifier,Type),
1224		print_no_binding(Varname,Type),
1225		(TT=[] -> nl ; print(' &'),nl,print_solution_with_type2(TT,Bindings)).
1226		print_solution_with_type2(P,State) :-
1227		add_internal_error('Illegal call: ', print_solution_with_type2(P,State)).
1228
1229		print_binding(Varname,Result) :-
1230		format(' ~w = ~w',[Varname,Result]).
1231		print_no_binding(Varname,Type) :-
1232		pretty_type(Type,PrettyType),
1233		format(' ~w : ~w',[Varname,PrettyType]).
1234
1235		% translate a value with optional colouring
1236		:- dynamic colour_values/1.
1237		colour_values(false).
1238		toggle_colouring :- retract(colour_values(V)),
1239		(V=false -> V2=true ; V2=false),
1240		assertz(colour_values(V2)),
1241		format('Colouring of values is now ~w~n',[V2]).
1242		translate_bvalue_with_col(Value,Identifier,Result) :- colour_values(false),!,
1243		translate_bvalue_for_expression(Value,Identifier,Result).
1244		translate_bvalue_with_col(Value,Identifier,Result) :-
1245		temporary_set_preference(pp_with_terminal_colour,true,C),
1246		call_cleanup(translate_bvalue_for_expression(Value,Identifier,Result),
1247		reset_temporary_preference(pp_with_terminal_colour,C)).
1248
1249		translate_bvalue_with_limit_and_col(Value,Limit,Result) :- colour_values(false),!,
1250		translate_bvalue_with_limit(Value,Limit,Result).
1251		translate_bvalue_with_limit_and_col(Value,Limit,Result) :-
1252		translate_bvalue_with_limit_and_col_always(Value,Limit,Result).
1253		translate_bvalue_with_limit_and_col_always(Value,Limit,Result) :-
1254		temporary_set_preference(pp_with_terminal_colour,true,C),
1255		call_cleanup(translate_bvalue_with_limit(Value,Limit,Result),
1256		reset_temporary_preference(pp_with_terminal_colour,C)).
1257
1258		% ------------------
1259
1260		% translate a solver name to the prefix to be used on the REPL:
1261		translate_solver_to_prefix(Solver,Prefix) :- available_smt_solver(Solver,Prefix).
1262		translate_solver_to_prefix('sat',":sat "). % entry for eval_file
1263		translate_solver_to_prefix(prob,":prob "). % for eval_file
1264		translate_solver_to_prefix('prob-chr',":prob "). % for eval_file
1265		translate_solver_to_prefix('sat-z3',":sat-z3 "). % entry for eval_file
1266		translate_solver_to_prefix(kodkod,":kodkod "). % entry for eval_file
1267
1268		available_smt_solver(cvc4,":cvc ").
1269		available_smt_solver(cvc4,":cvc5 ").
1270		available_smt_solver(nostate(cvc4),":cvc5-free ").
1271		available_smt_solver(z3,":z3 ").
1272		available_smt_solver(z3sat,":z3-sat ").
1273		available_smt_solver(z3axm,":z3-axm ").
1274		available_smt_solver(z3cns,":z3-cns ").
1275		available_smt_solver(nostate(z3),":z3-free ").
1276		available_smt_solver(nostate(z3sat),":z3-sat-free ").
1277		available_smt_solver(nostate(z3axm),":z3-axm-free ").
1278		available_smt_solver(nostate(z3cns),":z3-cns-free ").
1279		available_smt_solver(double_check(z3),":z3-double-check ").
1280		available_smt_solver(double_check(z3axm),":z3-axm-double-check ").
1281		available_smt_solver(double_check(z3cns),":z3-cns-double-check ").
1282		available_smt_solver(double_check(nostate(z3)),":z3-free-double-check ").
1283		available_smt_solver(cdcl_sat,":cdcl-sat ").
1284		available_smt_solver(nostate(cdcl_sat),":cdcl-sat-free ").
1285		available_smt_solver(cdclt,":cdclt ").
1286		available_smt_solver(nostate(cdclt),":cdclt-free ").
1287		available_smt_solver(double_check(cdclt),":cdclt-double-check ").
1288		available_smt_solver(double_check(nostate(cdclt)),":cdclt-free-double-check ").
1289		available_smt_solver(idl,":idl ").
1290		available_smt_solver(setlog,":slog ").
1291		available_smt_solver(double_check(setlog),":slog-double-check ").
1292		available_smt_solver(clingo,":clingo ").
1293		available_smt_solver(double_check(clingo),":clingo-double-check ").
1294		available_smt_solver(prob(default),":prob "). % solve with SMT
1295		available_smt_solver(prob(strong),":prob-chr ").
1296		available_smt_solver(prob(no_opts),":prob-no-opts ").
1297		available_smt_solver(double_check(prob(strong)),":prob-chr-double-check ").
1298		available_smt_solver(double_check(prob(no_opts)),":prob-double-check ").
1299		available_smt_solver(double_check(prob(kodkod)),":kodkod-double-check "). % solve with Kodkod, check with ProB
1300		available_smt_solver(prob(eval),":eval "). % solve without SMT option; like default REPL eval
1301		available_smt_solver('prob-unsat-core',":core ").
1302		available_smt_solver('prob-unsat-core-no-chr',":ccore ").
1303		available_smt_solver('prob-unsat-cores',":cores ").
1304		available_smt_solver('prob-fast-unsat-core',":fcore ").
1305		available_smt_solver('prob-fast-unsat-core',":fast-core ").
1306		available_smt_solver('prob-min-core',":mcore ").
1307		available_smt_solver('prob-min-core',":min-core ").
1308		available_smt_solver('smt-unsat-core'(z3),":z3-core ").
1309		available_smt_solver('smt-quick-bup-unsat-core'(z3),":z3-qcore ").
1310		available_smt_solver('smt-quick-bup-unsat-core'(z3cns),":z3-cns-qcore ").
1311		available_smt_solver('smt-quick-bup-unsat-core'(z3axm),":z3-axm-qcore "). % z3axm best for bup-unsat core?
1312		available_smt_solver('smt-unsat-core'(z3cns),":z3-cns-core ").
1313		available_smt_solver('smt-unsat-core'(z3axm),":z3-axm-core ").
1314		available_smt_solver('cdclt-unsat-core',":cdclt-core ").
1315		available_smt_solver('satsolver'(glucose,with_state),":sat ").
1316		available_smt_solver('satsolver'(glucose,nostate),":sat-free ").
1317		available_smt_solver('satsolver'(z3,with_state),":sat-z3 ").
1318		available_smt_solver('satsolver'(z3,nostate),":sat-z3-free ").
1319		available_smt_solver(double_check('satsolver'(glucose,with_state)),":sat-double-check ").
1320		available_smt_solver(double_check('satsolver'(glucose,nostate)),":sat-free-double-check ").
1321		available_smt_solver(double_check('satsolver'(z3,with_state)),":sat-z3-double-check ").
1322
1323
1324		available_smt_solver_for_file(cdclt,":cdclt-file ").
1325		available_smt_solver_for_file(nostate(cdclt),":cdclt-free-file ").
1326		available_smt_solver_for_file(idl,":idl-file ").
1327		available_smt_solver_for_file(z3,":z3-file ").
1328		available_smt_solver_for_file(z3sat,":z3-sat-file ").
1329		available_smt_solver_for_file(z3axm,":z3-axm-file ").
1330		available_smt_solver_for_file(z3cns,":z3-cns-file ").
1331		available_smt_solver_for_file(nostate(z3),":z3-free-file ").
1332		available_smt_solver_for_file('smt-unsat-core'(z3),":z3-core-file ").
1333		available_smt_solver_for_file(cvc4,":cvc5-file ").
1334		available_smt_solver_for_file(nostate(cvc4),":cvc5-free-file ").
1335		available_smt_solver_for_file(prob(default),":prob-file ").
1336		available_smt_solver_for_file(prob(strong),":prob-chr-file ").
1337		available_smt_solver_for_file('prob-unsat-core',":prob-core-file ").
1338
1339		:- use_module(extrasrc(atelierb_provers_interface),[prove_sequent_with_provers/3]).
1340		available_krt_prover(krt,[ml,pp],":krt").
1341		available_krt_prover(ml,[ml],":ml").
1342		available_krt_prover(mldc, krt_double_check([ml],[prob(strong)]),":ml-double-check").
1343		available_krt_prover(mldcz3,krt_double_check([ml],[prob(strong),z3]),":ml-double-check-z3").
1344		available_krt_prover(pp,[pp],":pp").
1345		available_krt_prover(ppdc, krt_double_check([pp],[prob(strong)]),":pp-double-check").
1346		available_krt_prover(ppdcz3,krt_double_check([pp],[prob(strong),z3]),":pp-double-check-z3").
1347		available_krt_prover(probwd,['prob-wd-prover'(no_double_check)],":prove"). % not a krt prover
1348		available_krt_prover(probwddc1,['prob-wd-prover'([prob(strong)])],":prove-double-check").
1349		available_krt_prover(probwddc2,['prob-wd-prover'([prob(strong),z3])],":prove-double-check-z3").
1350		available_krt_prover(probwddc2,['wd-krt-prover'([ml],[prob(strong)])],":prove-bench").
1351
1352		prove_sequent_with_krt_provers(['prob-wd-prover'(DC)],Typed,Result) :- !,
1353		debug_format(19,'Calling ProB WD Prover~n',[]),
1354		(prove_sequent(Typed)
1355		-> Result = 'proved',
1356		(DC = no_double_check -> true ; double_check_proven_sequent(DC,Typed,_))
1357		; Result = 'unproved'
1358		).
1359		prove_sequent_with_krt_provers(['wd-krt-prover'(Provers,DC)],Typed,Result) :- !,
1360		bb_inc(prove_bench_counter,BCNr),
1361		debug_format(19,'Calling ProB WD Prover (~w)~n',[BCNr]),
1362		writeln_log(proving_with_wd_and_krt(BCNr,Typed)),
1363		(prove_sequent(Typed)
1364		-> Result = 'proved', WDResult=Result, bb_inc(prove_bench_wd_proved,_),
1365		prove_sequent_with_provers(Provers,Typed,KRTResult),
1366		(KRTResult='proved'
1367		-> format_with_colour_nl(user_output,[green],'Proven by WD & ~w',[Provers]),
1368		bb_inc(prove_bench_krt_proved,_)
1369		; format_with_colour_nl(user_output,[blue],'Proven by WD but *not* by ~w',[Provers])
1370		), % TODO: count number of proven/unproven by each prover
1371		(DC = no_double_check -> DCResult=DC ; double_check_proven_sequent(DC,Typed,DCResult))
1372		; WDResult='unproven', Result=KRTResult,
1373		debug_format(19,'Proving with Atelier-B provers ~w (~w)~n',[Provers,BCNr]),
1374		prove_sequent_with_provers(Provers,Typed,KRTResult),
1375		(Result='proved'
1376		-> format_with_colour_nl(user_output,[orange],'Proven by ~w but *not* by WD',[Provers]),
1377		bb_inc(prove_bench_krt_proved,_)
1378		; format_with_colour_nl(user_output,[grey],'Unproven by WD and ~w',[Provers])
1379		),
1380		(DC = no_double_check -> DCResult=DC
1381		; Result='proved' -> double_check_proven_sequent(DC,Typed,DCResult)
1382		; DCResult = not_required)
1383		), writeln_log(prove_status(BCNr,WDResult,KRTResult,DCResult)),
1384		portray_prove_bench_stats.
1385		prove_sequent_with_krt_provers(krt_double_check(Provers,DC),ExTyped,Res) :- !,
1386		debug_format(19,'Proving with Atelier-B provers ~w~n',[Provers]),
1387		prove_sequent_with_provers(Provers,ExTyped,Res),
1388		(Res='proved' -> double_check_proven_sequent(DC,ExTyped,_) ; true).
1389		prove_sequent_with_krt_provers(Provers,ExTyped,Res) :-
1390		debug_format(19,'Proving with Atelier-B provers ~w~n',[Provers]),
1391		prove_sequent_with_provers(Provers,ExTyped,Res).
1392
1393		portray_prove_bench_stats :- bb_sget(prove_bench_counter,Tot),
1394		bb_sget(prove_bench_krt_proved,KRT),
1395		bb_sget(prove_bench_wd_proved,WD),
1396		format(':prove-bench statistics: total: ~w KRT:~w WD-Prover:~w~n',[Tot,KRT,WD]).
1397
1398		bb_inc(Counter,OldNr) :- bb_get(Counter,OldNr), !, N1 is OldNr+1, bb_put(Counter,N1).
1399		bb_inc(Counter,1) :- bb_put(Counter,2).
1400		bb_sget(Counter,Nr) :- (bb_get(Counter,R) -> Nr=R ; Nr=0).
1401
1402		double_check_proven_sequent(DCProvers,Typed,counter_example_found) :-
1403		create_negation(Typed,NegTyped),
1404		member(Solver,DCProvers),
1405		%member(Solver,[prob(strong),z3]),
1406		(debug_mode(off) -> true
1407		; format_with_colour_nl(user_output,[dark_gray],'Double checking proof using ~w',[Solver])),
1408		statistics(walltime,[W1,_]),
1409		%solve_typed_pred_using_smt_solver(Solver,NegTyped,Res,_),
1410		temporary_set_preference(strict_raise_enum_warnings,false,Chng),
1411		(solve_using_smt_solver_aux(Solver,[],NegTyped,_,Res) -> true),
1412		reset_temporary_preference(strict_raise_enum_warnings,Chng),
1413		statistics(walltime,[W2,_]), W is W2-W1,
1414		(Res=solution(_)
1415		-> Col=[red,bold],
1416		format_with_colour_nl(user_output,Col,'Double checking proven sequent with ~w after ~w ms: ~w',[Solver,W,Res])
1417		; silent_mode(on) -> true
1418		; Col = [dark_gray],
1419		format_with_colour_nl(user_output,Col,'Double checking proven sequent with ~w after ~w ms: ~w',[Solver,W,Res])
1420		),
1421		(Res=solution(_) ; Res='TRUE'),
1422		!,
1423		add_error(double_check_proven_sequent,'Counter example for proven sequent found:',Typed,Typed).
1424		%nl,print_quoted(Typed),nl,nl,trace, prove_sequent(Typed).
1425		double_check_proven_sequent(_,_,ok).
1426
1427
1428
1429
1430		solve_using_smt_solver_from_file(Solver,FileCodes,OuterQuantifier,Res,LocalState,TypeInfo) :-
1431		atom_codes(File,FileCodes),
1432		format_with_colour_nl(user_output,[dark_gray],'Reading B predicate for ~w from file ~w',[Solver,File]),
1433		start_ms_timer(T0),
1434		safe_read_string_from_file(File,utf8,PredCodes),
1435		stop_ms_timer_with_debug_msg(T0,reading_file(File)),
1436		debug_format(19,'Predicate read from file:~n~s~n',[PredCodes]),
1437		solve_using_smt_solver(Solver,PredCodes,try_prolog,OuterQuantifier,Res,LocalState,TypeInfo).
1438
1439		:- use_module(state_space,[current_state_id/1]).
1440		:- use_module(smt_solvers_interface(smt_solvers_interface),[smt_solve_predicate_in_state/5,
1441		smt_solve_predicate/4]).
1442		solve_using_smt_solver(Solver,PredCodes,TryProlog,OuterQuantifier,Res,LocalState,TypeInfo) :-
1443		(TryProlog=try_prolog,
1444		repl_get_prolog_predicate(PredCodes,clean_up_pred,ExTyped,TypeInfo) -> true
1445		; repl_parse_predicate_for_solving(PredCodes,OuterQuantifier,ExTyped,TypeInfo) % TO DO: make lets,... available
1446		),
1447		solve_typed_pred_using_smt_solver(Solver,ExTyped,Res,LocalState).
1448
1449		solve_typed_pred_using_smt_solver(Solver,ExTyped,Res,LocalState) :-
1450		set_last_expression(pred,ExTyped,exception), % in case an exception occurs
1451		start_ms_timer(T0),
1452		(is_existential_quantifier(ExTyped,Parameters,Typed)
1453		-> get_clashing_identifiers(Parameters,ClashParas),
1454		% we cannot peel off quantified variables which clash with current state variables, constants, ...
1455		create_exists_opt_liftable(ClashParas,Typed,NewTyped),
1456		% we could also remove the ClashParas from the state passed to the smt solver
1457		(debug_mode(on), ClashParas=[_|_]
1458		-> get_texpr_ids(ClashParas,CP),
1459		add_message(eval_strings,'Existentially quantified variables have global definition: ',CP)
1460		; true
1461		)
1462		; Parameters=[],ExTyped = NewTyped),
1463		stop_ms_timer_with_debug_msg(T0,existential_quantifier_lifting(Solver)),
1464		start_timer(T1,WT1),
1465		(call_residue(solve_using_smt_solver_aux0(Solver,Parameters,NewTyped,LocalState,Result),Residue)
1466		-> ajoin(['% Solve using solver ',Solver,':'],Msg),
1467		stop_timer(Msg,T1,WT1),
1468		%print(smt_result(Solver,Result)),nl,
1469		print('PREDICATE is '),display_smt_result(Result,Parameters,ExTyped,Res),
1470		check_residue_for_eval_strings_call(Residue,Solver)
1471		; ajoin(['% Solve using solver ',Solver,' FAILED:'],Msg),
1472		stop_timer(Msg,T1,WT1),
1473		Res = 'FAILED',
1474		set_last_expression(pred,ExTyped,failed),
1475		LocalState=[]).
1476
1477		%:- use_module(tools_fastread,[read_term_from_string/2]).
1478		:- use_module(library(codesio),[read_from_codes/2]).
1479		%:- use_module(bsyntaxtree,[repair_used_ids/3]).
1480		:- use_module(b_ast_cleanup,[clean_up_pred/3]).
1481		% detect if we have a Prolog AST terminated by a dot and read it in:
1482		repl_get_prolog_predicate(PredPrologASTCodes,Cleanup,CTyped,TypeInfo) :-
1483		append("b(",_,PredPrologASTCodes),
1484		reverse(PredPrologASTCodes,RC),
1485		skip_ws(RC,RC2),
1486		(RC2 = [0'., 0')|_] -> true % we end in ")."
1487		; append("/*",_,RC2)
1488		-> add_message(eval_strings,'Predicate could be a Prolog AST term; remove final comment'),
1489		fail % we end in a Prolog comment, but it could also be a B comment
1490		; add_debug_message(eval_strings,'Predicate could be a Prolog AST term; add final dot',''),
1491		fail
1492		),
1493		add_message(eval_strings,'Predicate seems to be in Prolog AST format, trying to read it'),
1494		read_from_codes(PredPrologASTCodes,Typed),
1495		repair_used_ids(repl_get_prolog_predicate,Typed,RTyped),
1496		bsyntaxtree:check_ast(RTyped),
1497		(Cleanup = clean_up_pred,
1498		clean_up_pred(RTyped,[],CTyped) -> true
1499		; CTyped=RTyped),
1500		extract_type_information(CTyped,TypeInfo),
1501		add_message(eval_strings,'Successfully read Prolog AST format:'),
1502		nested_print_repl_expression(CTyped).
1503
1504		skip_ws([32|T],R) :- !, skip_ws(T,R).
1505		skip_ws([10|T],R) :- !, skip_ws(T,R).
1506		skip_ws([13|T],R) :- !, skip_ws(T,R).
1507		skip_ws([9|T],R) :- !, skip_ws(T,R).
1508		skip_ws(R,R).
1509
1510		:- use_module(bsyntaxtree,[get_global_identifiers/1]).
1511		:- use_module(library(ordsets),[ord_member/2]).
1512		clash(SIds,TID) :- def_get_texpr_id(TID,ID), ord_member(ID,SIds).
1513		get_clashing_identifiers(Parameters,ClashParas) :-
1514		get_repl_ids(TIds),
1515		get_texpr_ids(TIds,Ids), get_global_identifiers(Csts),
1516		append(Csts,Ids,AllIds),
1517		sort(AllIds,SIds),
1518		include(clash(SIds),Parameters,ClashParas).
1519
1520		get_repl_ids(Identifiers) :-
1521		b_get_machine_constants(Constants),
1522		b_get_machine_variables(Variables),
1523		get_repl_lets_tids(LetIds),
1524		% TO DO: add enumerated set global constants
1525		append([Variables,Constants,LetIds],Identifiers).
1526
1527		:- use_module(probsrc(solver_interface), [solve_predicate/3, solve_predicate/5]).
1528		:- use_module(wdsrc(well_def_analyser),[prove_sequent/1]).
1529		:- use_module(library(terms),[term_size/2]).
1530
1531		solve_with_cdclt_in_state(_Paras,Typed,LocalState,SolvedPred,Result) :- !,
1532		get_current_state_full_store(Typed, FullStore),
1533		LocalState=[],
1534		cdclt_solve_predicate_in_state(Typed,FullStore,SolvedPred,Result).
1535
1536		solve_with_cdclt_no_state(Paras,Typed,LocalState,SolvedPred,Result) :- !,
1537		solver_clash_feedback(cdclt,Paras,Typed),
1538		LocalState=[],
1539		cdclt_solve_predicate(Typed,SolvedPred,Result).
1540
1541		solve_with_cdcl_sat_in_state(_Paras,Typed,LocalState,Result) :- !,
1542		get_current_state_full_store(Typed, FullStore),
1543		LocalState=[],
1544		cdcl_sat_solve_predicate_in_state(Typed,FullStore,Result).
1545
1546		solve_with_cdcl_sat_no_state(Paras,Typed,LocalState,Result) :- !,
1547		solver_clash_feedback(cdclt,Paras,Typed),
1548		LocalState=[],
1549		cdcl_sat_solve_predicate(Typed,Result).
1550
1551		solve_using_smt_solver_aux0(Solver,Parameters,NewTyped,LocalState,Result) :- eval_repeat(Nr),
1552		format('Trying to find ~w solutions using ~w:~n',[Nr,Solver]),
1553		succeed_max_call_id(solve_using_smt_solver_aux,
1554		solve_using_smt_solver_aux(Solver,Parameters,NewTyped,LocalState,Result),
1555		Nr),
1556		print('PREDICATE is '),display_smt_result(Result,Parameters,NewTyped,_),
1557		fail.
1558		solve_using_smt_solver_aux0(Solver,Parameters,NewTyped,LocalState,Result) :-
1559		solve_using_smt_solver_aux(Solver,Parameters,NewTyped,LocalState,Result).
1560
1561		:- use_module(cdclt_solver('cdclt_solver')).
1562		:- use_module(cdclt_solver('difference_logic/difference_logic_solver'), [solve_idl_conj/2]).
1563		:- use_module(extrasrc(b2setlog), [solve_pred_with_setlog/3]).
1564		:- use_module(extension('b2asp/b2asp'),[solve_pred_with_clingo/5]).
1565		%solve_using_smt_solver_aux(Solver,_Paras,Typed,_,_) :-
1566		% format('Solving with ~w:~n',[Solver]), translate:print_bexpr(Typed),nl,fail.
1567		solve_using_smt_solver_aux(nostate(cdcl_sat),Paras,Typed,LocalState,Result) :- !,
1568		solve_with_cdcl_sat_no_state(Paras,Typed,LocalState,Result).
1569		solve_using_smt_solver_aux(cdcl_sat,Paras,Typed,LocalState,Result) :- !,
1570		solve_with_cdcl_sat_in_state(Paras,Typed,LocalState,Result).
1571		solve_using_smt_solver_aux(nostate(cdclt),Paras,Typed,LocalState,Result) :- !,
1572		solve_with_cdclt_no_state(Paras,Typed,LocalState,_SolvedPred,Result).
1573		solve_using_smt_solver_aux(cdclt,Paras,Typed,LocalState,Result) :- !,
1574		solve_with_cdclt_in_state(Paras,Typed,LocalState,_SolvedPred,Result).
1575		solve_using_smt_solver_aux(idl,_,Typed,LocalState,Result) :- !,
1576		LocalState=[],
1577		solve_idl_conj(Typed,Result). % :idl
1578		solve_using_smt_solver_aux(setlog,_,Typed,LocalState,Result) :- !,
1579		solve_pred_with_setlog(Typed,LocalState,Result).
1580		solve_using_smt_solver_aux(clingo,_,Typed,LocalState,Result) :- !,
1581		solve_pred_with_clingo(Typed,1,LocalState,Result,_Exhaustive).
1582		solve_using_smt_solver_aux(double_check(nostate(cdclt)),Paras,Typed,LocalState,Result) :- !,
1583		solve_with_cdclt_no_state(Paras, Typed, LocalState, SolvedPred, Result),
1584		% cdclt possibly adds wd conditions; SolvedPred is always well-defined which is not guaranteed for the input
1585		double_check_smt_result(nostate(cdclt),Paras,SolvedPred,LocalState,Result).
1586		solve_using_smt_solver_aux(double_check(cdclt),Paras,Typed,LocalState,Result) :- !,
1587		start_ms_timer(T0),
1588		solve_with_cdclt_in_state(Paras, Typed, LocalState, SolvedPred, Result),
1589		stop_ms_timer_with_debug_msg(T0,cdclt),start_ms_timer(T1),
1590		double_check_smt_result(cdclt,Paras,SolvedPred,LocalState,Result),
1591		stop_ms_timer_with_debug_msg(T1,double_check).
1592		solve_using_smt_solver_aux(double_check(Solver),Paras,Typed,LocalState,Result) :- !,
1593		solve_using_smt_solver_aux(Solver,Paras,Typed,LocalState,Result),
1594		double_check_smt_result(Solver,Paras,Typed,LocalState,Result).
1595		solve_using_smt_solver_aux(prob(POpts),Paras,Typed,LocalState,Result) :- !,
1596		solver_clash_feedback(prob,Paras,Typed),
1597		start_ms_timer(T0),
1598		(POpts=default -> Opts = [use_smt_mode/true,use_clpfd_solver/true]
1599		; POpts=eval -> Opts = [use_smt_mode/false,use_clpfd_solver/true]
1600		; POpts=no_opts -> Opts = [use_smt_mode/false,use_clpfd_solver/true,optimize_ast/false]
1601		; POpts=strong -> Opts=[use_smt_mode/true,use_clpfd_solver/true,use_chr_solver/true,solver_strength/200]
1602		; POpts=kodkod -> Opts = [use_smt_mode/false,use_clpfd_solver/true,use_solver_on_load/kodkod] % like :kodkod
1603		; Opts=POpts), %other options could be allow_improving_wd_mode, clean_up_pred, smt_supported_interpreter, ...
1604		solve_predicate(Typed,LocalState,1,Opts,Result),
1605		stop_ms_timer_with_debug_msg(T0,solve_predicate).
1606		solve_using_smt_solver_aux('prob-unsat-core',_,Typed,LocalState,Result) :- !, LocalState=[],
1607		% TODO: provide unsat core in state
1608		unsat_core_predicate(Typed,1500,[auto_time_out_factor(180),
1609		min_time_out(20),use_chr_solver/true],_Core,_,Result).
1610		solve_using_smt_solver_aux('prob-unsat-core-no-chr',_,Typed,LocalState,Result) :- !, LocalState=[],
1611		% TODO: provide unsat core in state
1612		unsat_core_predicate(Typed,1500,[auto_time_out_factor(180),
1613		min_time_out(20),use_chr_solver/false],_Core,_,Result).
1614		solve_using_smt_solver_aux('prob-fast-unsat-core',_,Typed,LocalState,Result) :- !, LocalState=[],
1615		unsat_core_predicate(Typed,20,[inspect_nested_conjuncts(false),use_chr_solver/true],_Core,_,Result).
1616		solve_using_smt_solver_aux('smt-unsat-core'(Solver),_,Typed,LocalState,Result) :- !, LocalState=[],
1617		unsat_core_predicate(Typed,1500,[auto_time_out_factor(180), use_smt_solver(Solver), use_chr_solver/true,
1618		unsat_core_target(contradiction_found)],_Core,_,Result).
1619		solve_using_smt_solver_aux('smt-quick-bup-unsat-core'(Solver),_,Typed,LocalState,Result) :- !, LocalState=[],
1620		quick_bup_unsat_core_predicate(Typed,[use_smt_solver(Solver), use_chr_solver/true,
1621		try_prob_solver_first(fixed_time_out(5))],Result).
1622		solve_using_smt_solver_aux('cdclt-unsat-core',_,Typed,LocalState,Result) :- !, LocalState=[],
1623		unsat_core_predicate(Typed,1500,[auto_time_out_factor(180), use_chr_solver/true,
1624		min_time_out(20), use_cdclt_solver],_Core,_,Result).
1625		solve_using_smt_solver_aux('prob-unsat-cores',_,Typed,LocalState,Result) :- !, LocalState=[],
1626		findall(Len-R,unsat_core_predicate(Typed,1000,[use_chr_solver/true],_Core,Len,R),All),
1627		length(All,Len),
1628		min_member(MinL-Result,All),
1629		format('~nFound ~w unsat cores, minimum number of conjuncts ~w~n',[Len,MinL]).
1630		solve_using_smt_solver_aux('satsolver'(SOLVER,STATE),_,Typed,_LocalState,Result) :- !, % :sat
1631		(STATE = nostate
1632		-> b2sat:solve_predicate_with_satsolver_free(Typed,_,Result,[use_satsolver(SOLVER)])
1633		% the local state is set up by b2sat
1634		; get_cur_state_for_repl(Typed,CState),
1635		b2sat:solve_predicate_with_satsolver_in_state(Typed,CState,Result,[use_satsolver(SOLVER)])
1636		).
1637		solve_using_smt_solver_aux('prob-min-core',_,Typed,LocalState,Result) :- !, LocalState=[],
1638		findall(core(Len,Sz,Core,R),
1639		(unsat_core_predicate(Typed,1000,[use_chr_solver/true,
1640		branch_and_bound,auto_time_out_factor(160),no_print],Core,Len,R),
1641		term_size(Core,Sz)),
1642		All),
1643		length(All,Len),
1644		min_member(core(MinL,_,MinCore,Result),All),
1645		format(user_output,'~nFound ~w unsat cores~n% MINIMAL UNSAT CORE (~w conjuncts):~n',[Len,MinL]),
1646		translate:nested_print_bexpr_as_classicalb(MinCore),
1647		format(user_output,'% END OF MIN UNSAT CORE (~w conjuncts)~n',[MinL]).
1648		solve_using_smt_solver_aux(Solver,Parameters,Typed,LocalState,Result) :-
1649		(solver_call_should_ignore_state(Solver,Solver2)
1650		-> solver_clash_feedback(Solver2,Parameters,Typed),
1651		smt_solve_predicate(Solver2,Typed,LocalState,Result)
1652		; current_state_id(SID), SID \= root
1653		-> smt_solve_predicate_in_state(SID,Solver,Typed,LocalState,Result)
1654		; smt_solve_predicate(Solver,Typed,LocalState,Result)
1655		).
1656
1657		%is_already_declared_in_state(State,TID) :- def_get_texpr_id(TID,ID), member(bind(ID,_),State).
1658
1659		solver_call_should_ignore_state(nostate(Solver),Solver).
1660		solver_call_should_ignore_state('satsolver'(_,nostate),'satsolver').
1661
1662		% -------------
1663		% provide feedback when solver ignores variables/constants in current state
1664
1665		solver_clash_feedback(Solver,Parameters,Typed) :-
1666		current_state_id(SID),
1667		potential_clash_in_state(Parameters,Typed,SID,Clashes),
1668		Clashes \= [],
1669		!,
1670		(silent_mode(on) -> true
1671		; format_with_colour_nl(user_output,[dark_gray],
1672		'Calling solver ~w, ignoring values ~w in state ~w',[Solver,Clashes,SID])).
1673		solver_clash_feedback(Solver,_,_) :-
1674		debug_format(19,'Calling ~w solver via solve_predicate~n',[Solver]).
1675
1676		potential_clash_in_state(_,_,root,IDs) :- !, IDs=[].
1677		potential_clash_in_state(Parameters,Typed,_StateID,IDs) :-
1678		get_texpr_ids(Parameters,ParaIDs),
1679		find_identifier_uses_top_level(Typed,UsedIds),
1680		findall(ID,(member(ID,UsedIds), is_var_or_const(_,ID), nonmember(ID,ParaIDs)),IDs).
1681
1682		is_var_or_const(constant,ID) :- bmachine:b_is_constant(ID).
1683		is_var_or_const(variable,ID) :- bmachine:b_is_variable(ID).
1684
1685		% -----------
1686
1687		:- use_module(probsrc(specfile),[get_state_for_b_formula/3]).
1688		%:- use_module(probsrc(bsyntaxtree),[find_identifier_uses_top_level/2]).
1689
1690		get_current_state_full_store(Typed, FullStore) :-
1691		( current_state_id(StateID)
1692		-> get_state_for_b_formula(StateID, Typed, StateBindings)
1693		; StateBindings = []
1694		),
1695		find_identifier_uses_top_level(Typed, UsedIds), % do not include global sets
1696		% add unbound variables for all used identifiers
1697		findall(bind(Id,_), (member(Id, UsedIds), \+ member(bind(Id,_), StateBindings)), Bindings),
1698		append(Bindings, StateBindings, FullStore).
1699
1700		double_check_smt_result(Solver,_Parameters,Typed,_LocalState,solution(Bindings)) :- !,
1701		maplist(get_bind,Bindings,State),
1702		( solver_call_should_ignore_state(Solver, Solver2)
1703		-> find_identifier_uses_top_level(Typed, UsedIds),
1704		findall(bind(IdName,_), (member(IdName,UsedIds), \+ member(bind(IdName,_),State)), FreeBindings),
1705		append(State, FreeBindings, FullStore)
1706		; Solver2 = Solver,
1707		get_current_state_full_store(Typed, TFullStore),
1708		findall(bind(IdName,_), (member(bind(IdName,_),TFullStore), \+ member(bind(IdName,_),State)), TFullStore2),
1709		append(State, TFullStore2, FullStore)
1710		),
1711		debug_format(19,'Double-checking solution of ~w with ProB solver using solve_predicate~n',[Solver]),
1712		%print(bindings(Bindings)),nl,
1713		(solve_predicate(Typed,FullStore,DCResult), %print(DCResult),nl,
1714		check_dc_sol(DCResult,Solver2,solution(_)) -> true
1715		; add_error(double_check_smt_result,'Double checking NOT successful, solution not confirmed: ',Typed,Typed)).
1716		double_check_smt_result(Solver,_Parameters, Typed, _LocalState, Res) :- functor(Res,FRes,_),
1717		( solver_call_should_ignore_state(Solver, Solver2)
1718		-> % FullStore is var
1719		debug_format(19,'Double checking result ~w of ~w with ProB solver (ignoring current state)~n',[FRes,Solver2])
1720		; get_current_state_full_store(Typed, FullStore),
1721		Solver2 = Solver,
1722		debug_format(19,'Double checking result ~w of ~w with ProB solver (in current state)~n',[FRes,Solver2])
1723		),
1724		( solve_predicate(Typed, FullStore, TDCResult)
1725		-> DCResult = TDCResult
1726		; % solve_predicate did fail if contradiction with current state
1727		% should no longer happen
1728		add_warning(double_check_smt_result,'solve_predicate failed: ',Typed, Typed),
1729		DCResult = contradiction_found
1730		),
1731		( check_dc_sol(DCResult, Solver2, Res)
1732		-> true
1733		; add_error(double_check_smt_result,'Double checking NOT successful', Typed, Typed)
1734		).
1735
1736		get_bind(binding(Var,Val,_PP),bind(Var,Val)).
1737		get_bind(bind(Var,Val),bind(Var,Val)).
1738
1739		check_dc_sol(X,_,X) :- !,
1740		print_green('Double check ok'),nl.
1741		check_dc_sol(no_solution_found(R1),_,no_solution_found(R2)) :-
1742		functor(R1,F,N), functor(R2,F,N), !,
1743		print_green('Double check ok (small difference in reason for not finding solution)'),nl.
1744		check_dc_sol(no_solution_found(unfixed_deferred_sets),_,contradiction_found) :-
1745		% Z3, CDCL(T) do not check for unfixed_deferred sets; see test 2060
1746		!, print_green('Double check of contradiction_found ok'),nl.
1747		check_dc_sol(time_out,Solver,E) :- !, X=time_out,
1748		format_with_colour_nl(user_error,[orange,bold],
1749		'Double check not completed:~n * ~w reported: ~w~n * ProB double check reported: ~w',[Solver,E,X]),
1750		fail. % change to fail to report error, true to accept as ok
1751		check_dc_sol(X,Solver,solution(Var)) :- var(Var), !, % above we pass solution(_) to check_dc_sol
1752		format_with_colour_nl(user_error,[red,bold],
1753		'Double check unexpected result:~n * ~w reported: solution(...)~n * ProB double check of solution reported: ~w',[Solver,X]),
1754		fail.
1755		check_dc_sol(X,Solver,E) :-
1756		format_with_colour_nl(user_error,[red,bold],
1757		'Double check unexpected result:~n * ~w reported: ~w~n * ProB double check reported: ~w',[Solver,E,X]),
1758		fail.
1759
1760		display_smt_result(solution(Bindings),Parameters,ExTyped,Res) :- !,
1761		set_last_expression(pred,ExTyped,pred_true),
1762		print_green('TRUE'),nl,
1763		( Bindings=[]
1764		-> set_last_solution(Parameters,[])
1765		; silent_mode(off), write('Solution: '),nl,Bindings=[bind(_,_)|_]
1766		-> print_visible_solution_with_type(Parameters, Bindings),
1767		set_last_solution(Parameters,Bindings)
1768		; Bindings = [bind(_,_)|_] -> set_last_solution(Parameters,Bindings)
1769		; findall(bind(ID,Val),member(binding(ID,Val,_),Bindings),LocalState),
1770		set_last_solution(Parameters,LocalState),
1771		findall(1,(member(binding(ID2,_,S2),Bindings),print_binding(ID2,S2),nl),_)
1772		), Res = 'TRUE'.
1773		display_smt_result(contradiction_found,_,ExTyped,Res) :- !,
1774		format_with_colour(user_output,[light_red],'FALSE',[]),nl,
1775		set_last_expression(pred,ExTyped,pred_false),
1776		Res = 'FALSE'.
1777		display_smt_result(contradiction_found(UnsatCore),_,ExTyped,Res) :- !,
1778		display_smt_result(contradiction_found,_,ExTyped,'FALSE'),
1779		translate_bexpression(UnsatCore, PrettyUnsatCore),
1780		format_with_colour_nl(user_output,[dark_gray],'Unsat Core: ~w',[PrettyUnsatCore]),
1781		Res = 'FALSE'.
1782		display_smt_result(no_solution_found(no_idl_constraint),_,_,'UNKNOWN') :- !,
1783		print_red('UNKNOWN: '),nl,
1784		format_with_colour_nl(user_output,[light_red],'Constraint can not be transformed to integer difference logic.',[]).
1785		display_smt_result(no_solution_found(cvc4_unknown),_,ExTyped,'UNKNOWN') :- !,
1786		print_red('UNKNOWN'),nl,
1787		set_last_expression(pred,ExTyped,unknown).
1788		display_smt_result(no_solution_found(Reason),_,ExTyped,'UNKNOWN') :- !,
1789		print_red('UNKNOWN: '),print(Reason),nl,
1790		set_last_expression(pred,ExTyped,unknown).
1791		display_smt_result(error,_,ExTyped,'UNKNOWN') :- !,
1792		print_red('UNKNOWN: '),print('(due to error, possibly well-definedness error)'),nl,
1793		set_last_expression(pred,ExTyped,unknown).
1794		display_smt_result(Other,_,ExTyped,'UNKNOWN') :- !,
1795		print_red('*** UNKNOWN SMT RESULT ***: '),print(Other),nl,
1796		set_last_expression(pred,ExTyped,unknown).
1797
1798
1799		%:- use_module(bsyntaxtree,[def_get_texpr_id/2]).
1800		print_parameters([]).
1801		print_parameters([TID]) :- !, print_id(TID).
1802		print_parameters([TID|T]) :- print_id(TID), print(','), print_parameters(T).
1803		print_id(TID) :- def_get_texpr_id(TID,ID), print(ID).
1804
1805
1806
1807		%indent(X) :- X<1,!.
1808		%indent(X) :- print('+ '), X1 is X-1, indent(X1).
1809
1810		% TOOLS
1811		% -----
1812
1813
1814		% detecting existential quantifiers: so that the REPL can print the solutions for them
1815		% an example is the following test:
1816		% probcli -eval "#active,ready,waiting,rr.(active : POW(PID) & ready : POW(PID) & waiting : POW(PID) & active <: PID & ready <: PID & waiting <: PID & (ready /\ waiting = {}) & (active /\ (ready \/ waiting)) = {} & card(active) <= 1 & rr : waiting & active = {})" ../prob_examples/public_examples/B/Benchmarks/scheduler.mch
1817		% alternative would be to avoid optimizer to run at top-level
1818		is_existential_quantifier(TE,Par,Body) :- is_existential_quantifier(TE,recur,Par,Body).
1819		is_existential_quantifier(b(EXISTS,pred,_),Recur,FullParameters,FullTypedBody) :-
1820		is_existential_aux(EXISTS,Parameters,TypedBody),
1821		!,
1822		(Recur=recur,
1823		is_existential_quantifier(TypedBody,Recur,InnerPar,InnerBody) % recursively look inside
1824		-> append(Parameters,InnerPar,FullParameters),
1825		FullTypedBody = InnerBody
1826		; FullTypedBody = TypedBody, FullParameters=Parameters).
1827		is_existential_aux(Var,_,_) :- var(Var),!, add_internal_error('Illegal call:',is_existential_aux(Var,_,_)),fail.
1828		is_existential_aux(exists(Parameters,TypedBody),Parameters,TypedBody).
1829		is_existential_aux(let_predicate(Parameters,AssignmentExprs,Pred),Parameters,TypedBody) :-
1830		generate_let_equality_pred(Parameters,AssignmentExprs,EqPreds),
1831		append(EqPreds,[Pred],AllPreds),
1832		conjunct_predicates(AllPreds,TypedBody).
1833		is_existential_aux(conjunct(A,B),Parameters,TypedBody) :-
1834		is_existential_quantifier(A,no_recur,Parameters,TAA),
1835		!, % then do not look if B is existential quantifier below
1836		b_ast_cleanup:get_sorted_ids(Parameters,SIds),
1837		b_ast_cleanup:not_occurs_in_predicate(SIds,B),
1838		\+ is_existential_quantifier(B,no_recur,_,_),
1839		conjunct_predicates([TAA,B],TypedBody),!.
1840		is_existential_aux(conjunct(A,B),Parameters,TypedBody) :-
1841		is_existential_quantifier(B,no_recur,Parameters,TBB),
1842		!,
1843		b_ast_cleanup:get_sorted_ids(Parameters,SIds),
1844		b_ast_cleanup:not_occurs_in_predicate(SIds,A),
1845		conjunct_predicates([A,TBB],TypedBody).
1846		% TO DO: treat lazy_let_pred
1847
1848		generate_let_equality_pred([],[],[]).
1849		generate_let_equality_pred([ID|T],[Exp|TE],[EqPred|TR]) :-
1850		EqPred = b(equal(ID,Exp),pred,[]), % TO DO: update WD info
1851		generate_let_equality_pred(T,TE,TR).
1852
1853
1854
1855		:- use_module(clpfd_interface,[clpfd_overflow_error_message/0]).
1856
1857
1858		:- use_module(tools_meta,[call_residue/2]).
1859		:- use_module(clpfd_interface,[catch_clpfd_overflow_call2/2]).
1860		probcli_clpfd_overflow_mnf_call1(Call) :-
1861		call_residue(probcli_clpfd_overflow_mnf_call2(Call),Residue),
1862		check_residue_for_eval_strings_call(Residue,Call).
1863		probcli_clpfd_overflow_mnf_call2(Call) :- start_timer(T1,WT1),
1864		catch_clpfd_overflow_call2(
1865		(Call->stop_timer(T1,WT1)
1866		; stop_timer('% ProB evaluation: ',T1,WT1),show_error_pos,
1867		print_red('Expression not well-defined !'),nl,
1868		fail),
1869		( stop_timer('% ProB evaluation: ',T1,WT1),clpfd_overflow_error_message, fail)).
1870
1871		:- use_module(kernel_tools,[check_residue_for_call/2, portray_residue/1]).
1872		check_residue_for_eval_strings_call([],_) :- !.
1873		check_residue_for_eval_strings_call(Residue,_Call) :- eval_det,!,
1874		write('Call residue in eval_codes: '),nl,portray_residue(Residue).
1875		check_residue_for_eval_strings_call(Residue,Call) :- check_residue_for_call(Residue,Call).
1876
1877		probcli_clpfd_overflow_call1(Call) :-
1878		call_residue(probcli_clpfd_overflow_call2(Call),Residue),
1879		check_residue_for_eval_strings_call(Residue,Call).
1880		probcli_clpfd_overflow_call2(Call) :- start_timer(T1,WT1),
1881		catch_clpfd_overflow_call2(
1882		(Call -> stop_timer(T1,WT1) ; stop_timer(T1,WT1),fail),
1883		( stop_timer(T1,WT1),clpfd_interface:clpfd_overflow_error_message, fail)).
1884
1885
1886		:- volatile last_eval_time/2.
1887		:- dynamic last_eval_time/2.
1888		start_timer(T1,WT1) :- retractall(last_eval_time(_,_)), retractall(last_norm_time(_,_)),
1889		statistics(runtime,[T1,_]),
1890		statistics(walltime,[WT1,_]).
1891		stop_timer(T1,WT1) :-
1892		statistics(runtime,[T2,_]), TotTime is T2-T1,
1893		statistics(walltime,[WT2,_]), WTotTime is WT2-WT1,
1894		retractall(last_eval_time(_,_)),
1895		%debug_println(20,stopped_timer(TotTime,T2,T1)),
1896		(debug_mode(off) -> true
1897		; format_with_colour_nl(user_output,[dark_gray],'stopped timer ~w ms (~w ms walltime).',[TotTime,WTotTime])),
1898		assertz(last_eval_time(TotTime,WTotTime)).
1899		stop_timer(Msg,T1,WT1) :-
1900		statistics(runtime,[T2,_]), TotTime is T2-T1,
1901		statistics(walltime,[WT2,_]), WTotTime is WT2-WT1,
1902		(silent_mode(on) -> true
1903		; format_with_colour_nl(user_output,[dark_gray],'~w ~w ms (~w ms walltime).',[Msg,TotTime,WTotTime])
1904		),
1905		assertz(last_eval_time(TotTime,WTotTime)).
1906
1907		:- volatile last_norm_time/2.
1908		:- dynamic last_norm_time/2.
1909		start_norm_timer(T1,WT1) :- retractall(last_norm_time(_,_)),
1910		statistics(runtime,[T1,_]),
1911		statistics(walltime,[WT1,_]).
1912		stop_norm_timer(T1,WT1) :-
1913		statistics(runtime,[T2,_]), TotTime is T2-T1,
1914		statistics(walltime,[WT2,_]), WTotTime is WT2-WT1,
1915		retractall(last_norm_time(_,_)),
1916		debug_println(20,stopped_norm_timer(TotTime,T2,T1)),
1917		assertz(last_norm_time(TotTime,WTotTime)).
1918
1919
1920		:- volatile eval_mode/1.
1921		:- dynamic eval_mode/1.
1922		eval_det :- eval_mode(eval_det).
1923
1924		toggle_eval_det :- retract(eval_mode(_)),!,
1925		format('% Going back to ordinary enumeration~n',[]).
1926		toggle_eval_det :- set_eval_det,
1927		format('% Going to deterministic mode (for existentially quantified formulas)~n',[]).
1928
1929		set_eval_det :- set_eval_mode(eval_det).
1930		set_eval_mode(M) :- retractall(eval_mode(_)), assertz(eval_mode(M)).
1931		unset_eval_mode :- retractall(eval_mode(_)).
1932
1933		eval_ground_wf(WF) :- (eval_det -> ground_det_wait_flag(WF) ; ground_wait_flags(WF)).
1934
1935
1936
1937
1938
1939		show_error_pos :-
1940		%File = null, % console text typed by user
1941		findall(error_pos(Line,Col,EndLine,EndCol),
1942		(check_error_span_file_linecol(_Src,File,Line,Col,EndLine,EndCol), file_unknown(File)),
1943		Errs),
1944		!,
1945		remove_dups(Errs,Errs2),
1946		LastLine is -100, show_error_pos(Errs2,LastLine).
1947
1948		file_unknown(null).
1949		file_unknown(unknown(_)).
1950		file_unknown(unknown).
1951
1952		:- use_module(tools_printing,[start_terminal_colour/2, reset_terminal_colour/1]).
1953		show_line(Line,FromCol,ToCol) :- % highlight if possible FromCol ToCol, Columns start at 0, ToCol is not included ?!
1954		% TO DO: handle multiple errors on line
1955		(current_codes(E),get_line(E,Line,ErrLine)
1956		-> append(ErrLine,[32],Errline2), % add one whitespace at end
1957		prefix_length(Errline2,Prefix,FromCol),
1958		format(user_output,'~n### ~s',[Prefix]),
1959		Len is ToCol - FromCol,
1960		sublist(Errline2,ErrStr,FromCol,Len,_),
1961		% start_terminal_colour([red_background,white,bold],user_output),
1962		start_terminal_colour([red,underline,bold],user_output),
1963		format(user_output,'~s',[ErrStr]), % Print Error Part in RED
1964		reset_terminal_colour(user_output),
1965		sublist(Errline2,Suffix,ToCol,_,0),
1966		format(user_output,'~s~n',[Suffix])
1967		; true).
1968		show_line(Line) :-
1969		(current_codes(E),get_line(E,Line,ErrLine)
1970		-> format('~n### ~s~n',[ErrLine])
1971		; true).
1972		show_error_pos([],_).
1973		show_error_pos([error_pos(Line,Col,EL,EC)|T],LastLine) :- % print(pos(Line,Col,EL,EC)),nl,
1974		% first display source code of line with error:
1975		(LastLine==Line -> true ; EL==Line,show_line(Line,Col,EC) -> true ; show_line(Line)),
1976		print('### '), indent_ws(Col),
1977		(EL=Line,EC>Col -> Len is EC-Col ; Len=1),
1978		underline(Len),nl,
1979		(Line>1 -> print('### Line: '), print(Line),
1980		print(' Column: '), print(Col),nl
1981		; true),
1982		show_error_pos(T,Line).
1983
1984		indent_ws(X) :- X<1,!.
1985		indent_ws(X) :- print(' '), X1 is X-1, indent_ws(X1).
1986		underline(0) :- !.
1987		underline(N) :- N>0, print('^'), N1 is N-1, underline(N1).
1988
1989		get_line(_,Nr,R) :- Nr<1,!,R=[].
1990		get_line([],_,R) :- !, R=[].
1991		get_line(Codes,Nr,Res) :- is_newline(Codes,T),!, N1 is Nr-1, get_line(T,N1,Res).
1992		get_line([H|T],1,Res) :- !, Res=[H|RT], get_line(T,1,RT).
1993		get_line([_H|T],Nr,Res) :- get_line(T,Nr,Res).
1994
1995		is_newline([10,13|T],T).
1996		is_newline([10|T],T).
1997		is_newline([13|T],T).
1998
1999		%%%%% to show error position in Tcl/Tk console %%%%%
2000		get_error_positions(EPos) :-
2001		findall(error_pos(Line,Col,EndLine,EndCol),check_error_span_file_linecol(_Src,_File,Line,Col,EndLine,EndCol),Errs),!,
2002		get_error_position_string_l(Errs,EPos).
2003
2004		get_error_position_string_l(List,EPos) :-
2005		maplist(get_error_position,List,StringList),
2006		haskell_csp:convert_string_list_to_string(StringList,EPos).
2007
2008		get_error_position(error_pos(Line,Col,EL,EC),String) :-
2009		((current_codes(E),get_line(E,Line,ErrLine))
2010		-> atom_codes(N,ErrLine),
2011		atom_concat('### ',N, FirstLineAtom),
2012		atom_concat(FirstLineAtom,';',FirstLineAtom1)
2013		; FirstLineAtom1 = '### ;'),
2014		get_ident_ws(Col,'',WS),
2015		(EL=Line,EC>Col -> Len is EC-Col ; Len=1),
2016		get_underlines(Len,'',Underlines),
2017		atom_concat('### ',WS,SecondLineAtom),
2018		atom_concat(SecondLineAtom,Underlines,SecondLineAtom1),
2019		atom_concat(SecondLineAtom1,';',SecondLineAtom2),
2020		atom_concat(FirstLineAtom1,SecondLineAtom2,String).
2021
2022		get_ident_ws(X,WS,WS) :-
2023		X<1,!.
2024		get_ident_ws(X,WS,Res) :-
2025		atom_concat(WS,' ',WS1),
2026		X1 is X-1,
2027		get_ident_ws(X1,WS1,Res).
2028
2029		get_underlines(0,U,U) :- !.
2030		get_underlines(X,U,Res) :-
2031		X>0,
2032		atom_concat(U,'^',U1),
2033		X1 is X-1,
2034		get_underlines(X1,U1,Res).
2035
2036		:- volatile last_expression/2, last_expression_value/1.
2037		:- dynamic last_expression/2, last_expression_value/1.
2038		last_expression(Type,Expr,Value) :-
2039		last_expression(Type,Expr), last_expression_value(Value).
2040		set_last_expression(Type,Expr,Value) :-
2041		clear_last_expression, %print(assert),debug:nl_time,
2042		assertz(last_expression(Type,Expr)),
2043		% can be expensive; we could pack the value: mypack(Value,PackedValue),debug:nl_time,
2044		PackedValue=Value,
2045		assertz(last_expression_value(PackedValue)). % print(done),debug:nl_time.
2046
2047		%mypack(Atom,PVal) :- atom(Atom),!,PVal=Atom.
2048		%mypack(Val,PVal) :- state_packing:pack_value(Val,PVal).
2049
2050		last_expression_type(Type) :- last_expression(Type,_).
2051
2052		clear_last_expression :-
2053		retractall(last_expression(_,_)), retractall(last_expression_value(_)).
2054
2055		%:- use_module(bsyntaxtree,[get_texpr_type/2]).
2056
2057		%print_last_info :- stream_property(A,mode(M)), write(open_stream(A,M)),nl,fail.
2058		print_last_info :- \+ last_expression(_,_Expr),!,
2059		print_red('Please evaluate an expression or predicate first.'),nl.
2060		print_last_info :- last_expression(Type,Expr),
2061		% for insertion into unit tests
2062		print('% Type: '), print_quoted(Type),
2063		(Type=expr,get_texpr_type(Expr,ET),pretty_type(ET,PrettyType)
2064		-> print(' : '), print(PrettyType),
2065		print(' [Card='),
2066		(max_cardinality(ET,Card) -> print(Card) ; print('??')), print(']')
2067		; true),nl,
2068
2069		print('% Eval Time: '),
2070		(last_eval_time(Time,WTime)
2071		-> format('~w ms (~w ms walltime)',[Time,WTime]),
2072		(last_norm_time(NTime,NWTime)
2073		-> format(' + Normalisation: ~w ms (~w ms walltime)',[NTime,NWTime])
2074		; true),
2075		(last_expansion_time(EWT) -> format(' + State expansion: ~w ms walltime',[EWT]) ; true)
2076		; print_red('*UNKNOWN*')
2077		),nl.
2078
2079
2080		print_last_value :- \+ last_expression(_,_Expr),!,
2081		print_red('Please evaluate an expression or predicate first.'),nl.
2082		print_last_value :- last_expression_value(Value),
2083		print('Last Expression Value = '),nl,
2084		translate:print_bvalue(Value),nl.
2085
2086		:- use_module(probsrc(tools_io),[safe_intelligent_open_file/3]).
2087		print_last_value_to_file(_F) :- \+ last_expression(_,_Expr),!,
2088		print_red('Please evaluate an expression or predicate first.'),nl.
2089		print_last_value_to_file(F) :- last_expression(_Type,_Expr,Value),
2090		format('Re-normalising last expression value before writing to file ~w~n',[F]),
2091		temporary_set_preference(comprehension_set_symbolic_limit,10000000,Old), % increase to 10 million from default 20000
2092		call_cleanup(store:normalise_value_for_var(repl_result,force,Value,NValue),
2093		reset_temporary_preference(comprehension_set_symbolic_limit,Old)),
2094		format('Writing last expression value to file ~w~n',[F]),
2095		safe_intelligent_open_file(F,write,Stream),
2096		translate:nested_print_bvalue(Stream,NValue,-1),
2097		nl(Stream),
2098		close(Stream).
2099
2100		print_last_expression :- \+ last_expression(_,_Expr),!,
2101		print_red('Please evaluate an expression or predicate first.'),nl.
2102		print_last_expression :- last_expression(_Type,Expr,Value),
2103		print_last_info,
2104		print('% '), translate:print_bexpr(Expr),nl,
2105		(Value = false -> print_quoted(must_fail_det(1,"",Expr)),print('.'),nl
2106		; print_quoted(Expr),nl,
2107		print('% = '),print_quoted(Value),nl).
2108
2109		indent_print_last_expression :- \+ last_expression(_,_Expr),!,
2110		print_red('Please evaluate an expression or predicate first.'),nl.
2111		indent_print_last_expression :- last_expression(_Type,Expr),
2112		nested_print_bexpr(Expr).
2113
2114		nested_print_repl_expression(Typed) :-
2115		set_unicode_mode, temporary_set_preference(pp_with_terminal_colour,true,C),
2116		call_cleanup((nested_print_bexpr(Typed),nl),
2117		(unset_unicode_mode, reset_temporary_preference(pp_with_terminal_colour,C))).
2118		print_component(component(Pred,Ids)) :- format('Component over ~w :~n',[Ids]), translate:print_bexpr(Pred),nl.
2119
2120		:- use_module(extrasrc(unsat_cores),[unsat_core_wth_auto_time_limit/5, quick_bup_core/4]).
2121		unsat_core_last_expression :- \+ last_expression(pred,_Expr),!,
2122		print_red('Please evaluate a predicate first.'),nl.
2123		unsat_core_last_expression :- \+ last_expression(pred,_Expr,pred_false),!,
2124		print('The UNSAT CORE can only be computed for false predicates.'),nl.
2125		unsat_core_last_expression :- last_expression(pred,Expr),
2126		last_eval_time(_Time,WTime),
2127		unsat_core_predicate(Expr,WTime,[use_chr_solver/true],_,_,_). % we could use without auto
2128
2129		unsat_core_predicate(Pred,MaxTimeOut,Options,Core,Len,Result) :-
2130		start_timer(T1,W1),
2131		print('% COMPUTING UNSAT CORE: '), translate:print_bexpr(Pred),nl,
2132		% maybe strip top-level existential quantifier
2133		unsat_core_wth_auto_time_limit(Pred,MaxTimeOut,Options,Result,Core),
2134		nl,stop_timer('% Time to compute core: ',T1,W1),
2135		print_unsat_core(Pred,Core,Options,Result,Len).
2136
2137
2138		quick_bup_unsat_core_predicate(Pred,Options,Result) :-
2139		start_timer(T1,W1),
2140		print('% Trying to compute UNSAT CORE in bottom-up fashion: '), translate:print_bexpr(Pred),nl,
2141		quick_bup_core(Pred,Options,Core,Result),!,
2142		nl,stop_timer('% Time to compute core: ',T1,W1),
2143		print_unsat_core(Pred,Core,Options,Result,_).
2144		quick_bup_unsat_core_predicate(_,_,'UNKNOWN') :-
2145		print('% No unsat core found in bottom-up fashion. Use regular unsat core instead.'),nl.
2146
2147
2148		print_unsat_core(Pred,Core,Options,Result,Len) :-
2149		size_of_conjunction(Pred,OrigSize),
2150		length(Core,Len),
2151		(member(no_print,Options) -> true
2152		; format('% UNSAT CORE (~w conjuncts out of ~w): ~w~n',[Len,OrigSize,Result]),
2153		translate:nested_print_bexpr_as_classicalb(Core),
2154		format('% END OF UNSAT CORE (~w conjuncts)~n',[Len])
2155		).
2156
2157		% test that we obtain same value with pretty-printed version of last expression:
2158		recheck_pp_of_last_expression(_,_,_) :- \+ last_expression(_,_Expr),!,
2159		print_red('Please evaluate an expression or predicate first.'),nl.
2160		recheck_pp_of_last_expression(Mode,NewResult,EnumWarning) :- last_expression(_Type,Expr,Value),
2161		translate_subst_or_bexpr_in_mode(Mode,Expr,Str), % Mode=unicode or ascii
2162		translate_bvalue(Value,ExpectedRes),
2163		format('Rechecking pretty-printed version of last formula (expecting ~w): ~w~n',[ExpectedRes,Str]),
2164		(eval_string(Str,NewResult,EnumWarning)
2165		-> (NewResult = ExpectedRes -> print_green('OK'),nl
2166		; add_error(recheck_pp_of_last_expression,'Unexpected result: ',NewResult),
2167		last_expression(_Type2,Expr2),
2168		translate_subst_or_bexpr_in_mode(Mode,Expr2,Str2),
2169		format(' Re-Pretty-printed version of re-checked formula: ~w~n',[Str2]))
2170		; add_error(recheck_pp_of_last_expression,'Evaluation failed:',Str),
2171		NewResult='FAIL', EnumWarning=false
2172		).
2173
2174		:- use_module(library(system)).
2175		add_last_expression_to_unit_tests :- \+ last_expression(_,_Expr),!,
2176		print_red('Please evaluate an expression or predicate first.'),nl.
2177		add_last_expression_to_unit_tests :- last_expression(Type,Expr,Value),
2178		open_unit_test_file(S), !, write(S,' & '), nl(S), write(S,' ( '),
2179		(print_unit_test_assertion(Type,Expr,Value,S) -> true ; print('PRINTING FAILED'),nl),
2180		write(S,' ) '), datime(datime(Yr,Mon,Day,Hr,Min,_Sec)),
2181		format(S,'/* ~w/~w/~w ~w:~w */',[Day,Mon,Yr,Hr,Min]),
2182		nl(S), close(S).
2183		add_last_expression_to_unit_tests :- print('Could not save expression to unit test file ($PROB_EX_DIR/B/Laws/REPL_UNIT_TESTS.def).'),nl.
2184
2185		open_unit_test_file(S) :-
2186		environ('PROB_EX_DIR',Dir),
2187		atom_concat(Dir,'/B/Laws/REPL_UNIT_TESTS.def',REPLFILE),
2188		print(opening(REPLFILE)),nl,
2189		my_open(REPLFILE,append,S).
2190
2191
2192		my_open(File,Mode,S) :-
2193		catch(open(File,Mode,S),
2194		error(existence_error(_,_),E),
2195		add_error_fail(my_open,'File does not exist: ',File:E)).
2196
2197		%:- use_module(bsyntaxtree,[create_texpr/4, safe_create_texpr/4]).
2198		print_unit_test_assertion(pred,Typed,true,S) :-
2199		print_bexpr_stream(S,Typed).
2200		print_unit_test_assertion(pred,Typed,false,S) :-
2201		safe_create_texpr(negation(Typed),pred,[],Neg),
2202		print_bexpr_stream(S,Neg).
2203		print_unit_test_assertion(expr,Typed,Val,S) :-
2204		print_bexpr_stream(S,Typed), write(S,' = '), print_bvalue_stream(S,Val).
2205
2206
2207		:- use_module(tools_printing,[print_term_summary/1]).
2208		portray_waitflags_and_frozen_state_info(WF,StateTerm) :-
2209		portray_waitflags(WF),
2210		print_term_summary(frozen_info_for_state(StateTerm)),
2211		term_variables(StateTerm,Vars),
2212		translate:l_print_frozen_info(Vars).
2213
2214		%% Utilities for defining values inside the REPL using let :
2215		% ----------------------
2216		% scanning code utilities to recognize let construct
2217		scan_identifier([32|T],ID,Rest) :- scan_identifier(T,ID,Rest).
2218		scan_identifier([H|T],[H|TID],Rest) :- letter(H),
2219		scan_identifier2(T,TID,Rest).
2220		scan_identifier2([],[],[]).
2221		scan_identifier2([32|T],[],T).
2222		scan_identifier2([61|T],[],[61|T]).
2223		scan_identifier2([H|T],[H|TID],Rest) :- ( letter(H) ; H = 95 ; H=45 ; digit(H)),
2224		scan_identifier2(T,TID,Rest).
2225		letter(X) :- (X >= 97, X =< 122) ; (X >= 65, X=< 90). % underscore = 95, minus = 45
2226		digit(X) :- X >= 48, X =< 57.
2227
2228		scan_integer([32|T],Nr,RestCodes) :- scan_integer(T,Nr,RestCodes).
2229		scan_integer([H|T],Nr,RestCodes) :- digit(H),
2230		scan_scan_integer2(T,Codes,RestCodes), number_codes(Nr,[H|Codes]).
2231		scan_scan_integer2([],[],[]).
2232		scan_scan_integer2([32|T],[],T).
2233		scan_scan_integer2([H|T],[H|TID],Rest) :- digit(H),
2234		scan_identifier2(T,TID,Rest).
2235
2236		scan_to_equal([32|T],Rest) :- scan_to_equal(T,Rest).
2237		scan_to_equal([61|T],T). % "=" = [61]
2238
2239		just_whitespace([32|T]) :- just_whitespace(T).
2240		just_whitespace([]).
2241
2242		store_let_id_last_value(ID) :-
2243		retract_stored_let_value(ID,LastType,_),
2244		!,
2245		get_last_value(ID,Type,Value), %print(updating(ID)),nl,
2246		add_stored_let_value(ID,Type,Value),
2247		(LastType=Type -> true
2248		; reset_parse_cache). % type has changed
2249		store_let_id_last_value(ID) :-
2250		get_cur_state_for_repl(b(truth,pred,[]),State), member(bind(ID,_),State),!,
2251		add_error(store_let_id_last_value,'Cannot redefine existing identifier using let: ',ID).
2252		store_let_id_last_value(ID) :-
2253		get_last_value(ID,Type,Value),
2254		add_stored_let_value(ID,Type,Value),
2255		reset_parse_cache.
2256
2257		% construct the scope that the typechecker will use
2258		repl_typing_scope([IdScope,prob_ids(visible),S|L]) :- % promoted if we allow operation_call_in_expr
2259		get_stored_let_typing_scope(IdScope), % identifier(Ids)
2260		!,
2261		get_main_repl_scope(S),external_libraries(L).
2262		repl_typing_scope([prob_ids(visible),S|L]) :- get_main_repl_scope(S),external_libraries(L).
2263
2264		external_libraries([external_library(all_available_libraries)]).
2265
2266		get_main_repl_scope(assertions_scope_and_additional_defs) :-
2267		get_preference(allow_operation_calls_in_expr,true),!.
2268		get_main_repl_scope(variables_and_additional_defs).
2269
2270		get_last_value(ID,Type,Value) :- % first try and see if we had a predicate with identifier ID
2271		get_last_predicate_value_for_id(ID,T,V),
2272		!,
2273		Type=T, Value=V.
2274		get_last_value(_ID,Type,Value) :- get_last_expr_type_and_value(_,Type,Value).
2275
2276		get_last_expr_type_and_value(Expr,Type,Value) :-
2277		last_expression(_,Expr,V),
2278		get_texpr_type(Expr,T),
2279		convert_result(T,V,Type,Value).
2280
2281		% display information about stored lets
2282		browse_repl_lets :- \+ \+ stored_let_value(_,_,_),
2283		print('Available let definitions:'),nl,
2284		stored_let_value(ID,_,Value),
2285		translate_bvalue_with_limit_and_col(Value,50,VS),
2286		format(' ~w = ~w~n',[ID,VS]),
2287		fail.
2288		browse_repl_lets.
2289
2290		get_repl_lets_info(Lets) :-
2291		findall(S, (stored_let_value(ID,_,Value),
2292		translate_bvalue_with_limit_and_col(Value,50,VS),
2293		ajoin([ID,' = ',VS,'\n'],S)),
2294		Lets).
2295
2296		get_repl_lets_tids(List) :-
2297		findall(b(identifier(ID),Type,[repl_let]), stored_let_value(ID,Type,_),List).
2298
2299
2300		list_information(INFO,Res,[INFO/BList]) :- !,
2301		external_functions:'PROJECT_INFO'(string(INFO),BList,unknown,no_wf_available),
2302		!,
2303		translate_bvalue_with_limit_and_col(BList,5000,Res),
2304		format('~w~n',[Res]).
2305		list_information(Arg,Res,[]) :- add_error(eval_strings,'Unknown argument for :list: ',Arg),
2306		Res='ERROR'.
2307
2308
2309		:- use_module(eventhandling,[register_event_listener/3]).
2310		:- register_event_listener(clear_specification,reset_eval_strings,
2311		'Reset REPL (lets, caches, ...)').
2312
2313		reset_eval_strings :- clear_last_expression,
2314		retractall(last_solution(_,_)),
2315		reset_parse_cache,
2316		set_observe_evaluation(false),
2317		retractall(eval_dot_file(_)),
2318		retractall(stored_let_value(_,_,_)),
2319		retractall(eval_repeat(_)),
2320		unset_eval_mode,
2321		(reset_required -> true ; assertz(reset_required)). % before next evaluation we need to remove invalid lets
2322
2323		reset_parse_cache :-
2324		retractall(parse_expr_cache(_,_,_,_,_)),
2325		retractall(parse_pred_cache(_,_,_,_,_)).
2326
2327		:- dynamic reset_required/0.
2328
2329		reset_repl_lets :- retract(reset_required),!,
2330		reset_let_values.
2331		reset_repl_lets.
2332
2333
2334		%% ------------------------------------
2335		%% DETERMINISTIC PROPAGATION UNIT TESTS
2336		%% ------------------------------------
2337
2338
2339		% check that certain predicates are determined to be failing without enumeration
2340		% to do: also add positive tests: certain predicates succeed with instantiating all variables
2341		% eval_strings:must_fail_tests.
2342
2343		must_fail_tests :- set_eval_det,
2344	?	must_fail_det(Nr,Str,ExTyped),
2345		check_failed(Nr,ExTyped),
2346		Str \= [],
2347		% print('PARSING: '),nl,name(SS,Str), print(SS),nl,
2348		repl_typing_scope(TypingScope),
2349		( b_parse_machine_predicate_from_codes_open(exists,Str,[],TypingScope,NewTyped) ->
2350		check_same_ast(Nr,NewTyped,ExTyped)
2351		;
2352		print('*** Could not parse: '), print(Nr), nl
2353		%add_error(must_fail_tests,'Could not parse saved string: ',Nr)
2354		),
2355		fail.
2356		must_fail_tests :- preferences:preference(use_clpfd_solver,true),
2357	?	must_fail_clpfd_det(Nr,ExTyped),
2358		test_enabled(Nr),
2359		check_failed(Nr,ExTyped),fail.
2360		must_fail_tests :- unset_eval_mode.
2361
2362		check_failed(Nr,ExTyped) :-
2363		nl,print(Nr), print(' >>> '), translate:print_bexpr(ExTyped),nl,
2364		(eval_predicate_in_cur_state(ExTyped,Res,_,_)
2365		-> (Res='FALSE' -> true ;
2366		add_error(must_fail_tests,'Test has not failed deterministically: ',Nr))
2367		; add_error(must_fail_tests,'eval_predicate failed: ',Nr)
2368		).
2369
2370		:- use_module(self_check).
2371
2372		:- assert_must_succeed(must_fail_tests).
2373
2374		check_same_ast(Nr,A_New,B_Old) :- % check equivalent to stored AST B, apart from pos
2375		(compare(A_New,B_Old) -> true
2376		; add_error(check_same_ast,'AST not identical: ',Nr),
2377		print('New AST:'),nl,print(A_New),nl,
2378		print('Stored AST :'),nl,print(B_Old),nl,
2379		tools_printing:trace_unify(A_New,B_Old)
2380		).
2381
2382		compare(A,B) :- atomic(A),!,B=A.
2383		compare(b(A,TA,IA),b(B,TB,IB)) :- !,
2384		TA=TB,
2385		exclude(remove_this,IA,IA1), sort(IA1,SIA1),
2386		exclude(remove_this,IB,IB1), sort(IB1,SIB1),
2387		compare_infos(SIA1,SIB1),
2388		compare(A,B).
2389		compare(A,B) :- A=..[F|As], B=..[F|Bs],
2390		maplist(compare,As,Bs).
2391
2392		compare_infos([],[]).
2393		compare_infos([H|TA],[H|TB]) :- !, compare_infos(TA,TB).
2394		compare_infos([used_ids(_)|TA],TB) :- TB \= [used_ids(_)|_], % skip additional new used_ids field
2395		compare_infos(TA,TB).
2396
2397		remove_this(removed_typing). % new info field
2398		remove_this(nodeid(_)). % new AST sometimes has more nodeids than old stored ones
2399		remove_this(prob_annotation('DO_NOT_ENUMERATE'('$$NONE$$'))). % this field now shows when enumeration order analysis was run and nothing found
2400
2401		:- load_files(library(system), [when(compile_time), imports([environ/2])]).
2402		:- if(environ(prob_release,true)).
2403		must_fail_det(_Nr,_Str,_ExTyped) :- fail.
2404		must_fail_clpfd_det(_Nr,_ExTyped) :- fail.
2405		:- else.
2406		%
2407		must_fail_det(1,"#(x,y,z).(x:BOOL & x=z & z=y & x /= y)",
2408		%b(exists([b(identifier(x),boolean,[do_not_optimize_away,nodeid(pos(nan,1,1,3,1,3)),introduced_by(exists)]),b(identifier(y),boolean,[do_not_optimize_away,nodeid(pos(nan,1,1,5,1,5)),introduced_by(exists)]),b(identifier(z),boolean,[do_not_optimize_away,nodeid(pos(nan,1,1,7,1,7)),introduced_by(exists)])],b(conjunct(b(conjunct(b(equal(b(identifier(x),boolean,[nodeid(pos(nan,1,1,20,1,20)),introduced_by(exists)]),b(identifier(z),boolean,[nodeid(pos(nan,1,1,22,1,22)),introduced_by(exists)])),pred,[nodeid(pos(nan,1,1,20,1,22))]),b(equal(b(identifier(z),boolean,[nodeid(pos(nan,1,1,26,1,26)),introduced_by(exists)]),b(identifier(y),boolean,[nodeid(pos(nan,1,1,28,1,28)),introduced_by(exists)])),pred,[nodeid(pos(nan,1,1,26,1,28))])),pred,[nodeid(pos(nan,1,1,11,1,28))]),b(not_equal(b(identifier(x),boolean,[nodeid(pos(nan,1,1,32,1,32)),introduced_by(exists)]),b(identifier(y),boolean,[nodeid(pos(nan,1,1,37,1,37)),introduced_by(exists)])),pred,[nodeid(pos(nan,1,1,32,1,37))])),pred,[nodeid(pos(nan,1,1,11,1,37))])),pred,[used_ids([]),nodeid(pos(nan,1,1,1,1,38))])).
2409		b(exists([b(identifier(x),boolean,[do_not_optimize_away,nodeid(pos(3,-1,1,3,1,3)),introduced_by(exists)]),b(identifier(y),boolean,[do_not_optimize_away,nodeid(pos(4,-1,1,5,1,5)),introduced_by(exists)]),b(identifier(z),boolean,[do_not_optimize_away,nodeid(pos(5,-1,1,7,1,7)),introduced_by(exists)])],b(conjunct(b(conjunct(b(conjunct(b(equal(b(identifier(x),boolean,[nodeid(pos(13,-1,1,20,1,20)),introduced_by(exists)]),b(identifier(z),boolean,[nodeid(pos(14,-1,1,22,1,22)),introduced_by(exists)])),pred,[nodeid(pos(12,-1,1,20,1,22))]),b(equal(b(identifier(z),boolean,[nodeid(pos(16,-1,1,26,1,26)),introduced_by(exists)]),b(identifier(y),boolean,[nodeid(pos(17,-1,1,28,1,28)),introduced_by(exists)])),pred,[nodeid(pos(15,-1,1,26,1,28))])),pred,[nodeid(pos(7,-1,1,11,1,28))]),b(not_equal(b(identifier(x),boolean,[nodeid(pos(19,-1,1,32,1,32)),introduced_by(exists)]),b(identifier(y),boolean,[nodeid(pos(20,-1,1,37,1,37)),introduced_by(exists)])),pred,[nodeid(pos(18,-1,1,32,1,37))])),pred,[nodeid(pos(6,-1,1,11,1,37))]),b(external_pred_call('LEQ_SYM',[b(identifier(x),boolean,[do_not_optimize_away,nodeid(pos(3,-1,1,3,1,3)),introduced_by(exists)]),b(identifier(y),boolean,[do_not_optimize_away,nodeid(pos(4,-1,1,5,1,5)),introduced_by(exists)])]),pred,[do_not_optimize_away,nodeid(pos(3,-1,1,3,1,3)),introduced_by(exists)])),pred,[])),pred,[used_ids([]),prob_symmetry(x,y),nodeid(pos(2,-1,1,1,1,38))])). % with symmetry breaking
2410
2411
2412		%
2413		must_fail_det(2,"#x.(x:BOOL & (x=FALSE <=> x=TRUE))", b(exists([b(identifier(x),boolean,[do_not_optimize_away,nodeid(pos(nan,1,1,2,1,2)),introduced_by(exists)])],b(equivalence(b(equal(b(identifier(x),boolean,[nodeid(pos(nan,1,1,15,1,15)),introduced_by(exists)]),b(boolean_false,boolean,[nodeid(pos(nan,1,1,17,1,17))])),pred,[nodeid(pos(nan,1,1,15,1,17))]),b(equal(b(identifier(x),boolean,[nodeid(pos(nan,1,1,27,1,27)),introduced_by(exists)]),b(boolean_true,boolean,[nodeid(pos(nan,1,1,29,1,29))])),pred,[nodeid(pos(nan,1,1,27,1,29))])),pred,[nodeid(pos(nan,1,1,15,1,29))])),pred,[used_ids([]),nodeid(pos(nan,1,1,1,1,34))])).
2414
2415		%
2416		must_fail_det(3,"#(b,c).(b:BOOL & b=c & b/=c)",
2417		b(exists([b(identifier(b),boolean,[do_not_optimize_away,nodeid(pos(nan,1,1,3,1,3)),introduced_by(exists)]),b(identifier(c),boolean,[do_not_optimize_away,nodeid(pos(nan,1,1,5,1,5)),introduced_by(exists)])],b(conjunct(b(equal(b(identifier(b),boolean,[nodeid(pos(nan,1,1,18,1,18)),introduced_by(exists)]),b(identifier(c),boolean,[nodeid(pos(nan,1,1,20,1,20)),introduced_by(exists)])),pred,[nodeid(pos(nan,1,1,18,1,20))]),b(not_equal(b(identifier(b),boolean,[nodeid(pos(nan,1,1,24,1,24)),introduced_by(exists)]),b(identifier(c),boolean,[nodeid(pos(nan,1,1,27,1,27)),introduced_by(exists)])),pred,[nodeid(pos(nan,1,1,24,1,27))])),pred,[nodeid(pos(nan,1,1,9,1,27))])),pred,[used_ids([]),nodeid(pos(nan,1,1,1,1,28))])).
2418
2419
2420		%
2421		must_fail_det(4,"#(e,s).(s<:INT & e:s & e/:s)", b(exists([b(identifier(e),integer,[do_not_optimize_away,nodeid(pos(3,-1,1,3,1,4)),introduced_by(exists)]),b(identifier(s),set(integer),[do_not_optimize_away,nodeid(pos(4,-1,1,5,1,6)),introduced_by(exists)])],b(conjunct(b(conjunct(b(subset(b(identifier(s),set(integer),[nodeid(pos(8,-1,1,9,1,10)),introduced_by(exists)]),b(interval(b(min_int,integer,[nodeid(pos(9,-1,1,12,1,15))]),b(max_int,integer,[nodeid(pos(9,-1,1,12,1,15))])),set(integer),[was(integer_set('INT')),nodeid(pos(9,-1,1,12,1,15))])),pred,[nodeid(pos(7,-1,1,9,1,15))]),b(member(b(identifier(e),integer,[nodeid(pos(11,-1,1,18,1,19)),introduced_by(exists)]),b(identifier(s),set(integer),[nodeid(pos(12,-1,1,20,1,21)),introduced_by(exists)])),pred,[nodeid(pos(10,-1,1,18,1,21))])),pred,[nodeid(pos(6,-1,1,9,1,21))]),b(not_member(b(identifier(e),integer,[nodeid(pos(14,-1,1,24,1,25)),introduced_by(exists)]),b(identifier(s),set(integer),[nodeid(pos(15,-1,1,27,1,28)),introduced_by(exists)])),pred,[nodeid(pos(13,-1,1,24,1,28))])),pred,[nodeid(pos(5,-1,1,9,1,28))])),pred,[used_ids([]),nodeid(pos(2,-1,1,1,1,29))])).
2422
2423		%
2424		must_fail_det(5,"#(x,y,z,v,xz).(x:BOOL & x/=y & v/=z & x=v & (x=z <=> xz=TRUE) & (xz=FALSE => x=TRUE) & (xz=FALSE => x=FALSE))", b(exists([b(identifier(x),boolean,[do_not_optimize_away,nodeid(pos(3,-1,1,3,1,4)),introduced_by(exists)]),b(identifier(y),boolean,[do_not_optimize_away,nodeid(pos(4,-1,1,5,1,6)),introduced_by(exists)]),b(identifier(z),boolean,[do_not_optimize_away,nodeid(pos(5,-1,1,7,1,8)),introduced_by(exists)]),b(identifier(v),boolean,[do_not_optimize_away,nodeid(pos(6,-1,1,9,1,10)),introduced_by(exists)]),b(identifier(xz),boolean,[do_not_optimize_away,nodeid(pos(7,-1,1,11,1,13)),introduced_by(exists)])],b(conjunct(b(conjunct(b(conjunct(b(conjunct(b(conjunct(b(not_equal(b(identifier(x),boolean,[nodeid(pos(18,-1,1,25,1,26)),introduced_by(exists)]),b(identifier(y),boolean,[nodeid(pos(19,-1,1,28,1,29)),introduced_by(exists)])),pred,[removed_typing,nodeid(pos(17,-1,1,25,1,29))]),b(not_equal(b(identifier(v),boolean,[nodeid(pos(21,-1,1,32,1,33)),introduced_by(exists)]),b(identifier(z),boolean,[nodeid(pos(22,-1,1,35,1,36)),introduced_by(exists)])),pred,[nodeid(pos(20,-1,1,32,1,36))])),pred,[nodeid(pos(12,-1,1,16,1,36))]),b(equal(b(identifier(x),boolean,[nodeid(pos(24,-1,1,39,1,40)),introduced_by(exists)]),b(identifier(v),boolean,[nodeid(pos(25,-1,1,41,1,42)),introduced_by(exists)])),pred,[nodeid(pos(23,-1,1,39,1,42))])),pred,[nodeid(pos(11,-1,1,16,1,42))]),b(equivalence(b(equal(b(identifier(x),boolean,[nodeid(pos(28,-1,1,46,1,47)),introduced_by(exists)]),b(identifier(z),boolean,[nodeid(pos(29,-1,1,48,1,49)),introduced_by(exists)])),pred,[nodeid(pos(27,-1,1,46,1,49))]),b(equal(b(identifier(xz),boolean,[nodeid(pos(31,-1,1,54,1,56)),introduced_by(exists)]),b(boolean_true,boolean,[nodeid(pos(32,-1,1,57,1,61))])),pred,[nodeid(pos(30,-1,1,54,1,61))])),pred,[nodeid(pos(26,-1,1,46,1,61))])),pred,[nodeid(pos(10,-1,1,16,1,61))]),b(implication(b(equal(b(identifier(xz),boolean,[nodeid(pos(35,-1,1,66,1,68)),introduced_by(exists)]),b(boolean_false,boolean,[nodeid(pos(36,-1,1,69,1,74))])),pred,[nodeid(pos(34,-1,1,66,1,74))]),b(equal(b(identifier(x),boolean,[nodeid(pos(38,-1,1,78,1,79)),introduced_by(exists)]),b(boolean_true,boolean,[nodeid(pos(39,-1,1,80,1,84))])),pred,[nodeid(pos(37,-1,1,78,1,84))])),pred,[nodeid(pos(33,-1,1,66,1,84))])),pred,[nodeid(pos(9,-1,1,16,1,84))]),b(implication(b(equal(b(identifier(xz),boolean,[nodeid(pos(42,-1,1,89,1,91)),introduced_by(exists)]),b(boolean_false,boolean,[nodeid(pos(43,-1,1,92,1,97))])),pred,[nodeid(pos(41,-1,1,89,1,97))]),b(equal(b(identifier(x),boolean,[nodeid(pos(45,-1,1,101,1,102)),introduced_by(exists)]),b(boolean_false,boolean,[nodeid(pos(46,-1,1,103,1,108))])),pred,[nodeid(pos(44,-1,1,101,1,108))])),pred,[nodeid(pos(40,-1,1,89,1,108))])),pred,[nodeid(pos(8,-1,1,16,1,108))])),pred,[removed_typing,used_ids([]),nodeid(pos(2,-1,1,1,1,110))])).
2425
2426		%
2427		must_fail_det(6,"#(x,xz).((x : BOOL & xz : BOOL) & (((x = TRUE) <=> not(x = TRUE)) <=> (xz = TRUE) & ((x = TRUE) <=> not(x = TRUE)) <=> (xz = FALSE)))", b(exists([b(identifier(x),boolean,[do_not_optimize_away,nodeid(pos(nan,1,1,3,1,3)),introduced_by(exists)]),b(identifier(xz),boolean,[do_not_optimize_away,nodeid(pos(nan,1,1,5,1,5)),introduced_by(exists)])],b(conjunct(b(equivalence(b(equivalence(b(equal(b(identifier(x),boolean,[nodeid(pos(nan,1,1,38,1,38)),introduced_by(exists)]),b(boolean_true,boolean,[nodeid(pos(nan,1,1,42,1,42))])),pred,[nodeid(pos(nan,1,1,38,1,42))]),b(negation(b(equal(b(identifier(x),boolean,[nodeid(pos(nan,1,1,56,1,56)),introduced_by(exists)]),b(boolean_true,boolean,[nodeid(pos(nan,1,1,60,1,60))])),pred,[nodeid(pos(nan,1,1,56,1,60))])),pred,[nodeid(pos(nan,1,1,52,1,64))])),pred,[nodeid(pos(nan,1,1,37,1,64))]),b(equal(b(identifier(xz),boolean,[nodeid(pos(nan,1,1,72,1,72)),introduced_by(exists)]),b(boolean_true,boolean,[nodeid(pos(nan,1,1,77,1,77))])),pred,[nodeid(pos(nan,1,1,72,1,77))])),pred,[nodeid(pos(nan,1,1,36,1,81))]),b(equivalence(b(equivalence(b(equal(b(identifier(x),boolean,[nodeid(pos(nan,1,1,87,1,87)),introduced_by(exists)]),b(boolean_true,boolean,[nodeid(pos(nan,1,1,91,1,91))])),pred,[nodeid(pos(nan,1,1,87,1,91))]),b(negation(b(equal(b(identifier(x),boolean,[nodeid(pos(nan,1,1,105,1,105)),introduced_by(exists)]),b(boolean_true,boolean,[nodeid(pos(nan,1,1,109,1,109))])),pred,[nodeid(pos(nan,1,1,105,1,109))])),pred,[nodeid(pos(nan,1,1,101,1,113))])),pred,[nodeid(pos(nan,1,1,86,1,113))]),b(equal(b(identifier(xz),boolean,[nodeid(pos(nan,1,1,121,1,121)),introduced_by(exists)]),b(boolean_false,boolean,[nodeid(pos(nan,1,1,126,1,126))])),pred,[nodeid(pos(nan,1,1,121,1,126))])),pred,[nodeid(pos(nan,1,1,85,1,131))])),pred,[nodeid(pos(nan,1,1,36,1,131))])),pred,[used_ids([]),nodeid(pos(nan,1,1,1,1,133))])).
2428
2429		%
2430		must_fail_det(7,"#(x,z,x2,xz).((((x : BOOL & z : BOOL) & x2 : BOOL) & xz : BOOL) & (((x2 /= z & x = x2) & ((x = TRUE) <=> (x2 = FALSE)) <=> (xz = TRUE)) & ((x = TRUE) <=> (x2 = FALSE)) <=> (xz = FALSE)))", b(exists([b(identifier(x),boolean,[do_not_optimize_away,nodeid(pos(nan,1,1,3,1,3)),introduced_by(exists)]),b(identifier(z),boolean,[do_not_optimize_away,nodeid(pos(nan,1,1,5,1,5)),introduced_by(exists)]),b(identifier(x2),boolean,[do_not_optimize_away,nodeid(pos(nan,1,1,7,1,7)),introduced_by(exists)]),b(identifier(xz),boolean,[do_not_optimize_away,nodeid(pos(nan,1,1,10,1,10)),introduced_by(exists)])],b(conjunct(b(conjunct(b(conjunct(b(not_equal(b(identifier(x2),boolean,[nodeid(pos(nan,1,1,70,1,70)),introduced_by(exists)]),b(identifier(z),boolean,[nodeid(pos(nan,1,1,76,1,76)),introduced_by(exists)])),pred,[nodeid(pos(nan,1,1,70,1,76))]),b(equal(b(identifier(x),boolean,[nodeid(pos(nan,1,1,80,1,80)),introduced_by(exists)]),b(identifier(x2),boolean,[nodeid(pos(nan,1,1,84,1,84)),introduced_by(exists)])),pred,[nodeid(pos(nan,1,1,80,1,84))])),pred,[nodeid(pos(nan,1,1,70,1,84))]),b(equivalence(b(equivalence(b(equal(b(identifier(x),boolean,[nodeid(pos(nan,1,1,92,1,92)),introduced_by(exists)]),b(boolean_true,boolean,[nodeid(pos(nan,1,1,96,1,96))])),pred,[nodeid(pos(nan,1,1,92,1,96))]),b(equal(b(identifier(x2),boolean,[nodeid(pos(nan,1,1,107,1,107)),introduced_by(exists)]),b(boolean_false,boolean,[nodeid(pos(nan,1,1,112,1,112))])),pred,[nodeid(pos(nan,1,1,107,1,112))])),pred,[nodeid(pos(nan,1,1,91,1,117))]),b(equal(b(identifier(xz),boolean,[nodeid(pos(nan,1,1,125,1,125)),introduced_by(exists)]),b(boolean_true,boolean,[nodeid(pos(nan,1,1,130,1,130))])),pred,[nodeid(pos(nan,1,1,125,1,130))])),pred,[nodeid(pos(nan,1,1,90,1,134))])),pred,[nodeid(pos(nan,1,1,69,1,134))]),b(equivalence(b(equivalence(b(equal(b(identifier(x),boolean,[nodeid(pos(nan,1,1,141,1,141)),introduced_by(exists)]),b(boolean_true,boolean,[nodeid(pos(nan,1,1,145,1,145))])),pred,[nodeid(pos(nan,1,1,141,1,145))]),b(equal(b(identifier(x2),boolean,[nodeid(pos(nan,1,1,156,1,156)),introduced_by(exists)]),b(boolean_false,boolean,[nodeid(pos(nan,1,1,161,1,161))])),pred,[nodeid(pos(nan,1,1,156,1,161))])),pred,[nodeid(pos(nan,1,1,140,1,166))]),b(equal(b(identifier(xz),boolean,[nodeid(pos(nan,1,1,174,1,174)),introduced_by(exists)]),b(boolean_false,boolean,[nodeid(pos(nan,1,1,179,1,179))])),pred,[nodeid(pos(nan,1,1,174,1,179))])),pred,[nodeid(pos(nan,1,1,139,1,184))])),pred,[nodeid(pos(nan,1,1,68,1,184))])),pred,[used_ids([]),nodeid(pos(nan,1,1,1,1,186))])).
2431
2432		%
2433		must_fail_det(8,"#(a,b).((a : BOOL & b : BOOL) & ((b = TRUE) <=> ((a = TRUE) <=> not(a = TRUE)) & (b = FALSE) <=> ((a = FALSE) <=> (a = TRUE))))", b(exists([b(identifier(a),boolean,[do_not_optimize_away,nodeid(pos(nan,1,1,3,1,3)),introduced_by(exists)]),b(identifier(b),boolean,[do_not_optimize_away,nodeid(pos(nan,1,1,5,1,5)),introduced_by(exists)])],b(conjunct(b(equivalence(b(equal(b(identifier(b),boolean,[nodeid(pos(nan,1,1,35,1,35)),introduced_by(exists)]),b(boolean_true,boolean,[nodeid(pos(nan,1,1,39,1,39))])),pred,[nodeid(pos(nan,1,1,35,1,39))]),b(equivalence(b(equal(b(identifier(a),boolean,[nodeid(pos(nan,1,1,51,1,51)),introduced_by(exists)]),b(boolean_true,boolean,[nodeid(pos(nan,1,1,55,1,55))])),pred,[nodeid(pos(nan,1,1,51,1,55))]),b(negation(b(equal(b(identifier(a),boolean,[nodeid(pos(nan,1,1,69,1,69)),introduced_by(exists)]),b(boolean_true,boolean,[nodeid(pos(nan,1,1,73,1,73))])),pred,[nodeid(pos(nan,1,1,69,1,73))])),pred,[nodeid(pos(nan,1,1,65,1,77))])),pred,[nodeid(pos(nan,1,1,50,1,77))])),pred,[nodeid(pos(nan,1,1,34,1,78))]),b(equivalence(b(equal(b(identifier(b),boolean,[nodeid(pos(nan,1,1,83,1,83)),introduced_by(exists)]),b(boolean_false,boolean,[nodeid(pos(nan,1,1,87,1,87))])),pred,[nodeid(pos(nan,1,1,83,1,87))]),b(equivalence(b(equal(b(identifier(a),boolean,[nodeid(pos(nan,1,1,100,1,100)),introduced_by(exists)]),b(boolean_false,boolean,[nodeid(pos(nan,1,1,104,1,104))])),pred,[nodeid(pos(nan,1,1,100,1,104))]),b(equal(b(identifier(a),boolean,[nodeid(pos(nan,1,1,116,1,116)),introduced_by(exists)]),b(boolean_true,boolean,[nodeid(pos(nan,1,1,120,1,120))])),pred,[nodeid(pos(nan,1,1,116,1,120))])),pred,[nodeid(pos(nan,1,1,99,1,124))])),pred,[nodeid(pos(nan,1,1,82,1,125))])),pred,[nodeid(pos(nan,1,1,34,1,125))])),pred,[used_ids([]),nodeid(pos(nan,1,1,1,1,127))])).
2434
2435		%
2436		must_fail_det(9,[], % let predicate now also optimizes bool equalities:
2437		%"#(a,b,c).(((a : BOOL & b : BOOL) & c : BOOL) & ((((b = TRUE) <=> (a = TRUE => a = FALSE) & b = TRUE) & (a = FALSE => c = FALSE)) & (a = FALSE => c = TRUE)))",
2438		b(let_predicate([b(identifier(b),boolean,[nodeid(pos(nan,1,1,5,1,5)),introduced_by(exists)])],[b(boolean_true,boolean,[nodeid(pos(nan,1,1,96,1,96))])],b(exists([b(identifier(a),boolean,[nodeid(pos(nan,1,1,3,1,3)),introduced_by(exists)]),b(identifier(c),boolean,[nodeid(pos(nan,1,1,7,1,7)),introduced_by(exists)])],b(conjunct(b(conjunct(b(equivalence(b(equal(b(identifier(b),boolean,[nodeid(pos(nan,1,1,52,1,52)),introduced_by(exists)]),b(boolean_true,boolean,[nodeid(pos(nan,1,1,56,1,56))])),pred,[nodeid(pos(nan,1,1,52,1,56))]),b(implication(b(equal(b(identifier(a),boolean,[nodeid(pos(nan,1,1,67,1,67)),introduced_by(exists)]),b(boolean_true,boolean,[nodeid(pos(nan,1,1,71,1,71))])),pred,[nodeid(pos(nan,1,1,67,1,71))]),b(equal(b(identifier(a),boolean,[nodeid(pos(nan,1,1,79,1,79)),introduced_by(exists)]),b(boolean_false,boolean,[nodeid(pos(nan,1,1,83,1,83))])),pred,[nodeid(pos(nan,1,1,79,1,83))])),pred,[nodeid(pos(nan,1,1,67,1,83))])),pred,[nodeid(pos(nan,1,1,51,1,88))]),b(implication(b(equal(b(identifier(a),boolean,[nodeid(pos(nan,1,1,105,1,105)),introduced_by(exists)]),b(boolean_false,boolean,[nodeid(pos(nan,1,1,109,1,109))])),pred,[nodeid(pos(nan,1,1,105,1,109))]),b(equal(b(identifier(c),boolean,[nodeid(pos(nan,1,1,118,1,118)),introduced_by(exists)]),b(boolean_false,boolean,[nodeid(pos(nan,1,1,122,1,122))])),pred,[nodeid(pos(nan,1,1,118,1,122))])),pred,[nodeid(pos(nan,1,1,105,1,122))])),pred,[]),b(implication(b(equal(b(identifier(a),boolean,[nodeid(pos(nan,1,1,133,1,133)),introduced_by(exists)]),b(boolean_false,boolean,[nodeid(pos(nan,1,1,137,1,137))])),pred,[nodeid(pos(nan,1,1,133,1,137))]),b(equal(b(identifier(c),boolean,[nodeid(pos(nan,1,1,146,1,146)),introduced_by(exists)]),b(boolean_true,boolean,[nodeid(pos(nan,1,1,150,1,150))])),pred,[nodeid(pos(nan,1,1,146,1,150))])),pred,[nodeid(pos(nan,1,1,133,1,150))])),pred,[])),pred,[used_ids([b]),used_ids([b]),used_ids([a,b,c])])),pred,[nodeid(pos(nan,1,1,1,1,156))])).
2439
2440		%
2441		must_fail_det(10,"#(a,b,c).(((a : BOOL & b : BOOL) & c : BOOL) & (((b = TRUE) <=> (a = TRUE => a = FALSE) & (c = TRUE) <=> (a = b)) & (c = TRUE) <=> not(a = b)))", b(exists([b(identifier(a),boolean,[do_not_optimize_away,nodeid(pos(nan,1,1,3,1,3)),introduced_by(exists)]),b(identifier(b),boolean,[do_not_optimize_away,nodeid(pos(nan,1,1,5,1,5)),introduced_by(exists)]),b(identifier(c),boolean,[do_not_optimize_away,nodeid(pos(nan,1,1,7,1,7)),introduced_by(exists)])],b(conjunct(b(conjunct(b(equivalence(b(equal(b(identifier(b),boolean,[nodeid(pos(nan,1,1,51,1,51)),introduced_by(exists)]),b(boolean_true,boolean,[nodeid(pos(nan,1,1,55,1,55))])),pred,[nodeid(pos(nan,1,1,51,1,55))]),b(implication(b(equal(b(identifier(a),boolean,[nodeid(pos(nan,1,1,66,1,66)),introduced_by(exists)]),b(boolean_true,boolean,[nodeid(pos(nan,1,1,70,1,70))])),pred,[nodeid(pos(nan,1,1,66,1,70))]),b(equal(b(identifier(a),boolean,[nodeid(pos(nan,1,1,78,1,78)),introduced_by(exists)]),b(boolean_false,boolean,[nodeid(pos(nan,1,1,82,1,82))])),pred,[nodeid(pos(nan,1,1,78,1,82))])),pred,[nodeid(pos(nan,1,1,66,1,82))])),pred,[nodeid(pos(nan,1,1,50,1,87))]),b(equivalence(b(equal(b(identifier(c),boolean,[nodeid(pos(nan,1,1,92,1,92)),introduced_by(exists)]),b(boolean_true,boolean,[nodeid(pos(nan,1,1,96,1,96))])),pred,[nodeid(pos(nan,1,1,92,1,96))]),b(equal(b(identifier(a),boolean,[nodeid(pos(nan,1,1,107,1,107)),introduced_by(exists)]),b(identifier(b),boolean,[nodeid(pos(nan,1,1,111,1,111)),introduced_by(exists)])),pred,[nodeid(pos(nan,1,1,107,1,111))])),pred,[nodeid(pos(nan,1,1,91,1,112))])),pred,[nodeid(pos(nan,1,1,50,1,112))]),b(equivalence(b(equal(b(identifier(c),boolean,[nodeid(pos(nan,1,1,118,1,118)),introduced_by(exists)]),b(boolean_true,boolean,[nodeid(pos(nan,1,1,122,1,122))])),pred,[nodeid(pos(nan,1,1,118,1,122))]),b(negation(b(equal(b(identifier(a),boolean,[nodeid(pos(nan,1,1,136,1,136)),introduced_by(exists)]),b(identifier(b),boolean,[nodeid(pos(nan,1,1,140,1,140)),introduced_by(exists)])),pred,[nodeid(pos(nan,1,1,136,1,140))])),pred,[nodeid(pos(nan,1,1,132,1,141))])),pred,[nodeid(pos(nan,1,1,117,1,141))])),pred,[nodeid(pos(nan,1,1,49,1,141))])),pred,[used_ids([]),nodeid(pos(nan,1,1,1,1,143))])
2442		).
2443
2444		% "#(x,y,z).(((x : BOOL & y : BOOL) & z : BOOL) & ((TRUE:BOOL) => ((x : {TRUE}) <=> (y = TRUE) & (x = y) <=> (z = TRUE)) & x /= y <=> (z = TRUE)))"
2445		must_fail_det(11,[], b(exists([b(identifier(x),boolean,[do_not_optimize_away,nodeid(pos(7,1,4,3,4,3))]),b(identifier(y),boolean,[do_not_optimize_away,nodeid(pos(8,1,4,5,4,5))]),b(identifier(z),boolean,[do_not_optimize_away,nodeid(pos(9,1,4,7,4,7))])],b(implication(b(truth,pred,[nodeid(pos(19,1,4,29,4,34))]),b(conjunct(b(conjunct(b(equivalence(b(member(b(identifier(x),boolean,[nodeid(pos(26,1,4,40,4,40))]),b(set_extension([b(boolean_true,boolean,[nodeid(pos(28,1,4,43,4,46))])]),set(boolean),[nodeid(pos(27,1,4,42,4,47))])),pred,[nodeid(pos(25,1,4,40,4,47))]),b(equal(b(identifier(y),boolean,[nodeid(pos(30,1,4,53,4,53))]),b(boolean_true,boolean,[nodeid(pos(31,1,4,55,4,58))])),pred,[nodeid(pos(29,1,4,53,4,58))])),pred,[nodeid(pos(24,1,4,40,4,58))]),b(equivalence(b(equal(b(identifier(x),boolean,[nodeid(pos(34,1,4,64,4,64))]),b(identifier(y),boolean,[nodeid(pos(35,1,4,66,4,66))])),pred,[nodeid(pos(33,1,4,64,4,66))]),b(equal(b(identifier(z),boolean,[nodeid(pos(37,1,4,72,4,72))]),b(boolean_true,boolean,[nodeid(pos(38,1,4,74,4,77))])),pred,[nodeid(pos(36,1,4,72,4,77))])),pred,[nodeid(pos(32,1,4,64,4,77))])),pred,[nodeid(pos(23,1,4,40,4,77))]),b(equivalence(b(not_equal(b(identifier(x),boolean,[nodeid(pos(41,1,4,82,4,82))]),b(identifier(y),boolean,[nodeid(pos(42,1,4,85,4,85))])),pred,[nodeid(pos(40,1,4,82,4,85))]),b(equal(b(identifier(z),boolean,[nodeid(pos(44,1,4,90,4,90))]),b(boolean_true,boolean,[nodeid(pos(45,1,4,92,4,95))])),pred,[nodeid(pos(43,1,4,90,4,95))])),pred,[nodeid(pos(39,1,4,82,4,95))])),pred,[nodeid(pos(22,1,4,40,4,95))])),pred,[nodeid(pos(10,1,4,11,4,95))])),pred,[used_ids([]),nodeid(pos(6,1,4,1,4,97))])).
2446
2447
2448		must_fail_det(12,[], %"SIGMA(x,y).(x : 1 .. 10 & y : {1,2}|x) = 111",
2449		b(equal(b(general_sum([b(identifier(x),integer,[nodeid(pos(nan,1,1,7,1,7)),introduced_by(general_sum)]),b(identifier(y),integer,[nodeid(pos(nan,1,1,9,1,9)),introduced_by(general_sum)])],b(conjunct(b(member(b(identifier(x),integer,[nodeid(pos(nan,1,1,13,1,13)),introduced_by(general_sum)]),b(interval(b(integer(1),integer,[nodeid(pos(nan,1,1,17,1,17))]),b(integer(10),integer,[nodeid(pos(nan,1,1,22,1,22))])),set(integer),[nodeid(pos(nan,1,1,17,1,22))])),pred,[nodeid(pos(nan,1,1,13,1,22))]),b(member(b(identifier(y),integer,[nodeid(pos(nan,1,1,27,1,27)),introduced_by(general_sum)]),b(set_extension([b(integer(1),integer,[nodeid(pos(nan,1,1,32,1,32))]),b(integer(2),integer,[nodeid(pos(nan,1,1,34,1,34))])]),set(integer),[nodeid(pos(nan,1,1,31,1,35))])),pred,[nodeid(pos(nan,1,1,27,1,35))])),pred,[nodeid(pos(nan,1,1,13,1,35))]),b(identifier(x),integer,[nodeid(pos(nan,1,1,37,1,37)),introduced_by(general_sum)])),integer,[nodeid(pos(nan,1,1,1,1,38))]),b(integer(111),integer,[nodeid(pos(nan,1,1,42,1,42))])),pred,[nodeid(pos(nan,1,1,1,1,42))])).
2450
2451		must_fail_det(13,[], %"PI(x,y).(x : 1 .. 10 & y : {1,2}|x) = 111",
2452		b(equal(b(general_product([b(identifier(x),integer,[nodeid(pos(nan,1,1,4,1,4)),introduced_by(general_product)]),b(identifier(y),integer,[nodeid(pos(nan,1,1,6,1,6)),introduced_by(general_product)])],b(conjunct(b(member(b(identifier(x),integer,[nodeid(pos(nan,1,1,10,1,10)),introduced_by(general_product)]),b(interval(b(integer(1),integer,[nodeid(pos(nan,1,1,14,1,14))]),b(integer(10),integer,[nodeid(pos(nan,1,1,19,1,19))])),set(integer),[nodeid(pos(nan,1,1,14,1,19))])),pred,[nodeid(pos(nan,1,1,10,1,19))]),b(member(b(identifier(y),integer,[nodeid(pos(nan,1,1,24,1,24)),introduced_by(general_product)]),b(set_extension([b(integer(1),integer,[nodeid(pos(nan,1,1,29,1,29))]),b(integer(2),integer,[nodeid(pos(nan,1,1,31,1,31))])]),set(integer),[nodeid(pos(nan,1,1,28,1,32))])),pred,[nodeid(pos(nan,1,1,24,1,32))])),pred,[nodeid(pos(nan,1,1,10,1,32))]),b(identifier(x),integer,[nodeid(pos(nan,1,1,34,1,34)),introduced_by(general_product)])),integer,[nodeid(pos(nan,1,1,1,1,35))]),b(integer(111),integer,[nodeid(pos(nan,1,1,39,1,39))])),pred,[nodeid(pos(nan,1,1,1,1,39))])).
2453
2454		/*
2455		must_fail_det(16,"union(ran(%x.((x <: {1,2,3,4} & card(x) > 0) & min(x) = 2|x))) = {1,2,3,4}",
2456		b(equal(b(general_union(b(range(b(comprehension_set([b(identifier(x),set(integer),[nodeid(pos(0,0,0,0,0,0))]),b(identifier('_lambda_result_'),set(integer),[lambda_result])],b(conjunct(b(conjunct(b(conjunct(b(subset(b(identifier(x),set(integer),[nodeid(pos(0,0,0,0,0,0))]),b(set_extension([b(integer(1),integer,[nodeid(pos(0,0,0,0,0,0))]),b(integer(2),integer,[nodeid(pos(0,0,0,0,0,0))]),b(integer(3),integer,[nodeid(pos(0,0,0,0,0,0))]),b(integer(4),integer,[nodeid(pos(0,0,0,0,0,0))])]),set(integer),[nodeid(pos(0,0,0,0,0,0))])),pred,[nodeid(pos(0,0,0,0,0,0))]),b(greater(b(card(b(identifier(x),set(integer),[nodeid(pos(0,0,0,0,0,0))])),integer,[nodeid(pos(0,0,0,0,0,0))]),b(integer(0),integer,[nodeid(pos(0,0,0,0,0,0))])),pred,[nodeid(pos(0,0,0,0,0,0))])),pred,[nodeid(pos(0,0,0,0,0,0))]),b(equal(b(min(b(identifier(x),set(integer),[nodeid(pos(0,0,0,0,0,0))])),integer,[contains_wd_condition,nodeid(pos(0,0,0,0,0,0))]),b(integer(2),integer,[nodeid(pos(0,0,0,0,0,0))])),pred,[contains_wd_condition,nodeid(pos(0,0,0,0,0,0))])),pred,[contains_wd_condition,nodeid(pos(0,0,0,0,0,0))]),b(equal(b(identifier('_lambda_result_'),set(integer),[lambda_result]),b(identifier(x),set(integer),[nodeid(pos(0,0,0,0,0,0))])),pred,[])),pred,[contains_wd_condition])),set(couple(set(integer),set(integer))),[contains_wd_condition,was(lambda),generated(quantified_union)])),set(set(integer)),[contains_wd_condition,generated(quantified_union)])),set(integer),[contains_wd_condition,nodeid(pos(0,0,0,0,0,0))]),b(set_extension([b(integer(1),integer,[nodeid(pos(0,0,0,0,0,0))]),b(integer(2),integer,[nodeid(pos(0,0,0,0,0,0))]),b(integer(3),integer,[nodeid(pos(0,0,0,0,0,0))]),b(integer(4),integer,[nodeid(pos(0,0,0,0,0,0))])]),set(integer),[nodeid(pos(0,0,0,0,0,0))])),pred,[contains_wd_condition,nodeid(pos(0,0,0,0,0,0))])).
2457		*/
2458
2459
2460		% #(z,x,y).(((z : POW(POW(BOOL)) & x : POW(BOOL)) & y : INTEGER) & ((z = {{},{TRUE},{FALSE},{TRUE,FALSE}} & (x : z) <=> (y = 2)) & y > 3))
2461		% check that we detect that z is a complete set, hence x:z and hence y=2
2462		must_fail_det(14,[], %"z = {{},{TRUE},{FALSE},{TRUE,FALSE}} & (x:z <=> y=2) & y>3 ",
2463		b(exists([b(identifier(z),set(set(boolean)),[]),b(identifier(x),set(boolean),[]),b(identifier(y),integer,[])],b(conjunct(b(conjunct(b(equal(b(identifier(z),set(set(boolean)),[nodeid(pos(nan,1,1,1,1,1))]),b(set_extension([b(empty_set,set(boolean),[nodeid(pos(nan,1,1,6,1,6))]),b(set_extension([b(boolean_true,boolean,[nodeid(pos(nan,1,1,10,1,10))])]),set(boolean),[nodeid(pos(nan,1,1,9,1,14))]),b(set_extension([b(boolean_false,boolean,[nodeid(pos(nan,1,1,17,1,17))])]),set(boolean),[nodeid(pos(nan,1,1,16,1,22))]),b(set_extension([b(boolean_true,boolean,[nodeid(pos(nan,1,1,25,1,25))]),b(boolean_false,boolean,[nodeid(pos(nan,1,1,30,1,30))])]),set(boolean),[nodeid(pos(nan,1,1,24,1,35))])]),set(set(boolean)),[nodeid(pos(nan,1,1,5,1,36))])),pred,[nodeid(pos(nan,1,1,1,1,36))]),b(equivalence(b(member(b(identifier(x),set(boolean),[nodeid(pos(nan,1,1,41,1,41))]),b(identifier(z),set(set(boolean)),[nodeid(pos(nan,1,1,43,1,43))])),pred,[nodeid(pos(nan,1,1,41,1,43))]),b(equal(b(identifier(y),integer,[nodeid(pos(nan,1,1,49,1,49))]),b(integer(2),integer,[nodeid(pos(nan,1,1,51,1,51))])),pred,[nodeid(pos(nan,1,1,49,1,51))])),pred,[nodeid(pos(nan,1,1,41,1,51))])),pred,[nodeid(pos(nan,1,1,1,1,52))]),b(greater(b(identifier(y),integer,[nodeid(pos(nan,1,1,56,1,56))]),b(integer(3),integer,[nodeid(pos(nan,1,1,58,1,58))])),pred,[nodeid(pos(nan,1,1,56,1,58))])),pred,[nodeid(pos(nan,1,1,1,1,58))])),pred,[used_ids([x,y,z])])).
2464
2465		% #(z,x,y).(((z : POW(BOOL * BOOL) & x : BOOL * BOOL) & y : INTEGER) & ((z = {TRUE |-> FALSE,TRUE |-> TRUE,FALSE |-> FALSE,FALSE |-> TRUE} & (x : z) <=> (y = 2)) & y > 3))
2466		% check that we detect that z is a complete set, hence x:z and hence y=2
2467		must_fail_det(15,[], %" z = {(TRUE,FALSE),(TRUE,TRUE),(FALSE,FALSE),(FALSE,TRUE)} & (x:z <=> y=2) & y>3 ",
2468		b(exists([b(identifier(z),set(couple(boolean,boolean)),[]),b(identifier(x),couple(boolean,boolean),[]),b(identifier(y),integer,[])],b(conjunct(b(conjunct(b(equal(b(identifier(z),set(couple(boolean,boolean)),[nodeid(pos(nan,1,1,1,1,1))]),b(set_extension([b(couple(b(boolean_true,boolean,[nodeid(pos(nan,1,1,7,1,7))]),b(boolean_false,boolean,[nodeid(pos(nan,1,1,12,1,12))])),couple(boolean,boolean),[nodeid(pos(nan,1,1,6,1,17))]),b(couple(b(boolean_true,boolean,[nodeid(pos(nan,1,1,20,1,20))]),b(boolean_true,boolean,[nodeid(pos(nan,1,1,25,1,25))])),couple(boolean,boolean),[nodeid(pos(nan,1,1,19,1,29))]),b(couple(b(boolean_false,boolean,[nodeid(pos(nan,1,1,32,1,32))]),b(boolean_false,boolean,[nodeid(pos(nan,1,1,38,1,38))])),couple(boolean,boolean),[nodeid(pos(nan,1,1,31,1,43))]),b(couple(b(boolean_false,boolean,[nodeid(pos(nan,1,1,46,1,46))]),b(boolean_true,boolean,[nodeid(pos(nan,1,1,52,1,52))])),couple(boolean,boolean),[nodeid(pos(nan,1,1,45,1,56))])]),set(couple(boolean,boolean)),[nodeid(pos(nan,1,1,5,1,57))])),pred,[nodeid(pos(nan,1,1,1,1,57))]),b(equivalence(b(member(b(identifier(x),couple(boolean,boolean),[nodeid(pos(nan,1,1,62,1,62))]),b(identifier(z),set(couple(boolean,boolean)),[nodeid(pos(nan,1,1,64,1,64))])),pred,[nodeid(pos(nan,1,1,62,1,64))]),b(equal(b(identifier(y),integer,[nodeid(pos(nan,1,1,70,1,70))]),b(integer(2),integer,[nodeid(pos(nan,1,1,72,1,72))])),pred,[nodeid(pos(nan,1,1,70,1,72))])),pred,[nodeid(pos(nan,1,1,62,1,72))])),pred,[nodeid(pos(nan,1,1,1,1,73))]),b(greater(b(identifier(y),integer,[nodeid(pos(nan,1,1,77,1,77))]),b(integer(3),integer,[nodeid(pos(nan,1,1,79,1,79))])),pred,[nodeid(pos(nan,1,1,77,1,79))])),pred,[nodeid(pos(nan,1,1,1,1,79))])),pred,[used_ids([x,y,z])])).
2469
2470		% #(z,x,y).(((z : POW(POW(BOOL)) & x : POW(POW(BOOL))) & y : INTEGER) & ((z = {{},{TRUE},{FALSE},{TRUE,FALSE}} & x <: z <=> (y = 2)) & y > 3))
2471		must_fail_det(16,[],b(exists([b(identifier(z),set(set(boolean)),[]),b(identifier(x),set(set(boolean)),[]),b(identifier(y),integer,[])],b(conjunct(b(conjunct(b(equal(b(identifier(z),set(set(boolean)),[nodeid(pos(nan,1,1,1,1,1))]),b(set_extension([b(empty_set,set(boolean),[nodeid(pos(nan,1,1,6,1,6))]),b(set_extension([b(boolean_true,boolean,[nodeid(pos(nan,1,1,10,1,10))])]),set(boolean),[nodeid(pos(nan,1,1,9,1,14))]),b(set_extension([b(boolean_false,boolean,[nodeid(pos(nan,1,1,17,1,17))])]),set(boolean),[nodeid(pos(nan,1,1,16,1,22))]),b(set_extension([b(boolean_true,boolean,[nodeid(pos(nan,1,1,25,1,25))]),b(boolean_false,boolean,[nodeid(pos(nan,1,1,30,1,30))])]),set(boolean),[nodeid(pos(nan,1,1,24,1,35))])]),set(set(boolean)),[nodeid(pos(nan,1,1,5,1,36))])),pred,[nodeid(pos(nan,1,1,1,1,36))]),b(equivalence(b(subset(b(identifier(x),set(set(boolean)),[nodeid(pos(nan,1,1,41,1,41))]),b(identifier(z),set(set(boolean)),[nodeid(pos(nan,1,1,44,1,44))])),pred,[nodeid(pos(nan,1,1,41,1,44))]),b(equal(b(identifier(y),integer,[nodeid(pos(nan,1,1,50,1,50))]),b(integer(2),integer,[nodeid(pos(nan,1,1,52,1,52))])),pred,[nodeid(pos(nan,1,1,50,1,52))])),pred,[nodeid(pos(nan,1,1,41,1,52))])),pred,[nodeid(pos(nan,1,1,1,1,53))]),b(greater(b(identifier(y),integer,[nodeid(pos(nan,1,1,57,1,57))]),b(integer(3),integer,[nodeid(pos(nan,1,1,59,1,59))])),pred,[nodeid(pos(nan,1,1,57,1,59))])),pred,[nodeid(pos(nan,1,1,1,1,59))])),pred,[used_ids([x,y,z])])).
2472
2473		% Eval Time: 0 ms (0 ms walltime)
2474		% #(x).(x : INTEGER & ([111,222,333,444,555] |>> {x} = [111,222,333,444] & x > 555))
2475		must_fail_det(17,"#(x).(([111,222,333,444,555] |>> {x} = [111,222,333,444] & x > 555))", b(exists([b(identifier(x),integer,[do_not_optimize_away,nodeid(pos(3,-1,1,3,1,3)),introduced_by(exists)])],b(conjunct(b(equal(b(range_subtraction(b(value(avl_set(node((int(3),int(333)),true,0,node((int(1),int(111)),true,1,empty,node((int(2),int(222)),true,0,empty,empty)),node((int(4),int(444)),true,1,empty,node((int(5),int(555)),true,0,empty,empty))))),set(couple(integer,integer)),[nodeid(pos(7,-1,1,8,1,28))]),b(set_extension([b(identifier(x),integer,[nodeid(pos(14,-1,1,35,1,35)),introduced_by(exists)])]),set(integer),[nodeid(pos(13,-1,1,34,1,36))])),set(couple(integer,integer)),[nodeid(pos(6,-1,1,8,1,36))]),b(value(avl_set(node((int(2),int(222)),true,1,node((int(1),int(111)),true,0,empty,empty),node((int(3),int(333)),true,1,empty,node((int(4),int(444)),true,0,empty,empty))))),set(couple(integer,integer)),[nodeid(pos(15,-1,1,40,1,56))])),pred,[nodeid(pos(5,-1,1,8,1,56))]),b(greater(b(identifier(x),integer,[nodeid(pos(21,-1,1,60,1,60)),introduced_by(exists)]),b(integer(555),integer,[nodeid(pos(22,-1,1,64,1,66))])),pred,[nodeid(pos(20,-1,1,60,1,66))])),pred,[nodeid(pos(4,-1,1,8,1,66))])),pred,[used_ids([]),nodeid(pos(2,-1,1,1,1,68))])).
2476
2477
2478		% #(m,n).(m:30..100 & n:10..20 & m<n )
2479		must_fail_clpfd_det(101,b(exists([b(identifier(x),integer,[nodeid(pos(nan,1,1,3,1,3))])],b(conjunct(b(equal(b(range_subtraction(b(sequence_extension([b(integer(111),integer,[nodeid(pos(nan,1,1,9,1,9))]),b(integer(222),integer,[nodeid(pos(nan,1,1,13,1,13))]),b(integer(333),integer,[nodeid(pos(nan,1,1,17,1,17))]),b(integer(444),integer,[nodeid(pos(nan,1,1,21,1,21))]),b(integer(555),integer,[nodeid(pos(nan,1,1,25,1,25))])]),set(couple(integer,integer)),[nodeid(pos(nan,1,1,8,1,28))]),b(set_extension([b(identifier(x),integer,[nodeid(pos(nan,1,1,35,1,35)),introduced_by(exists)])]),set(integer),[nodeid(pos(nan,1,1,34,1,36))])),set(couple(integer,integer)),[nodeid(pos(nan,1,1,8,1,36))]),b(sequence_extension([b(integer(111),integer,[nodeid(pos(nan,1,1,41,1,41))]),b(integer(222),integer,[nodeid(pos(nan,1,1,45,1,45))]),b(integer(333),integer,[nodeid(pos(nan,1,1,49,1,49))]),b(integer(444),integer,[nodeid(pos(nan,1,1,53,1,53))])]),set(couple(integer,integer)),[nodeid(pos(nan,1,1,40,1,56))])),pred,[nodeid(pos(nan,1,1,8,1,56))]),b(greater(b(identifier(x),integer,[nodeid(pos(nan,1,1,60,1,60)),introduced_by(exists)]),b(integer(555),integer,[nodeid(pos(nan,1,1,64,1,64))])),pred,[nodeid(pos(nan,1,1,60,1,64))])),pred,[nodeid(pos(nan,1,1,8,1,64))])),pred,[used_ids([]),nodeid(pos(nan,1,1,1,1,68))])).
2480
2481		% #(m,n).(m:30..101 & n:10..20 & n*n=m & m/=100)
2482		must_fail_clpfd_det(102,b(exists([b(identifier(m),integer,[nodeid(pos(7,1,4,3,4,3))]),b(identifier(n),integer,[nodeid(pos(8,1,4,5,4,5))])],b(conjunct(b(conjunct(b(conjunct(b(member(b(identifier(m),integer,[nodeid(pos(13,1,4,9,4,9))]),b(interval(b(integer(30),integer,[nodeid(pos(15,1,4,11,4,12))]),b(integer(101),integer,[nodeid(pos(16,1,4,15,4,17))])),set(integer),[nodeid(pos(14,1,4,11,4,17))])),pred,[nodeid(pos(12,1,4,9,4,17))]),b(member(b(identifier(n),integer,[nodeid(pos(18,1,4,21,4,21))]),b(interval(b(integer(10),integer,[nodeid(pos(20,1,4,23,4,24))]),b(integer(20),integer,[nodeid(pos(21,1,4,27,4,28))])),set(integer),[nodeid(pos(19,1,4,23,4,28))])),pred,[nodeid(pos(17,1,4,21,4,28))])),pred,[nodeid(pos(11,1,4,9,4,28))]),b(equal(b(multiplication(b(identifier(n),integer,[nodeid(pos(24,1,4,32,4,32))]),b(identifier(n),integer,[nodeid(pos(25,1,4,34,4,34))])),integer,[nodeid(pos(23,1,4,32,4,34))]),b(identifier(m),integer,[nodeid(pos(26,1,4,36,4,36))])),pred,[nodeid(pos(22,1,4,32,4,36))])),pred,[nodeid(pos(10,1,4,9,4,36))]),b(not_equal(b(identifier(m),integer,[nodeid(pos(28,1,4,40,4,40))]),b(integer(100),integer,[nodeid(pos(29,1,4,43,4,45))])),pred,[nodeid(pos(27,1,4,40,4,45))])),pred,[nodeid(pos(9,1,4,9,4,45))])),pred,[used_ids([]),nodeid(pos(6,1,4,1,4,46))])).
2483
2484		% #(x,y).(y : BOOL & (x : NATURAL & (((x : {11}) <=> (y = TRUE) & x < 10) & (x : {12}) <=> (y = FALSE))))
2485		must_fail_clpfd_det(103,b(exists([b(identifier(x),integer,[nodeid(pos(7,1,4,3,4,3))]),b(identifier(y),boolean,[nodeid(pos(8,1,4,5,4,5))])],b(conjunct(b(member(b(identifier(x),integer,[nodeid(pos(12,1,4,9,4,9))]),b(integer_set('NATURAL'),set(integer),[nodeid(pos(13,1,4,11,4,17))])),pred,[nodeid(pos(11,1,4,9,4,17))]),b(conjunct(b(conjunct(b(equivalence(b(member(b(identifier(x),integer,[nodeid(pos(21,1,4,32,4,32))]),b(set_extension([b(integer(11),integer,[nodeid(pos(23,1,4,35,4,36))])]),set(integer),[nodeid(pos(22,1,4,34,4,37))])),pred,[nodeid(pos(20,1,4,32,4,37))]),b(equal(b(identifier(y),boolean,[nodeid(pos(25,1,4,43,4,43))]),b(boolean_true,boolean,[nodeid(pos(26,1,4,45,4,48))])),pred,[nodeid(pos(24,1,4,43,4,48))])),pred,[nodeid(pos(19,1,4,32,4,48))]),b(less(b(identifier(x),integer,[nodeid(pos(28,1,4,53,4,53))]),b(integer(10),integer,[nodeid(pos(29,1,4,55,4,56))])),pred,[nodeid(pos(27,1,4,53,4,56))])),pred,[nodeid(pos(18,1,4,32,4,56))]),b(equivalence(b(member(b(identifier(x),integer,[nodeid(pos(32,1,4,61,4,61))]),b(set_extension([b(integer(12),integer,[nodeid(pos(34,1,4,64,4,65))])]),set(integer),[nodeid(pos(33,1,4,63,4,66))])),pred,[nodeid(pos(31,1,4,61,4,66))]),b(equal(b(identifier(y),boolean,[nodeid(pos(36,1,4,72,4,72))]),b(boolean_false,boolean,[nodeid(pos(37,1,4,74,4,78))])),pred,[nodeid(pos(35,1,4,72,4,78))])),pred,[nodeid(pos(30,1,4,61,4,78))])),pred,[nodeid(pos(17,1,4,32,4,78))])),pred,[nodeid(pos(9,1,4,9,4,78))])),pred,[used_ids([]),nodeid(pos(6,1,4,1,4,81))])).
2486
2487
2488		% #(x,y).((x : INTEGER & y : INTEGER) & (({x} /<<: {11,12} <=> (y = 3) & x > 12) & y < 3))
2489		must_fail_clpfd_det(104,b(exists([b(identifier(x),integer,[]),b(identifier(y),integer,[])],b(conjunct(b(conjunct(b(equivalence(b(not_subset_strict(b(set_extension([b(identifier(x),integer,[nodeid(pos(nan,1,1,2,1,2))])]),set(integer),[nodeid(pos(nan,1,1,1,1,3))]),b(set_extension([b(integer(11),integer,[nodeid(pos(nan,1,1,11,1,11))]),b(integer(12),integer,[nodeid(pos(nan,1,1,14,1,14))])]),set(integer),[nodeid(pos(nan,1,1,10,1,16))])),pred,[nodeid(pos(nan,1,1,1,1,16))]),b(equal(b(identifier(y),integer,[nodeid(pos(nan,1,1,22,1,22))]),b(integer(3),integer,[nodeid(pos(nan,1,1,24,1,24))])),pred,[nodeid(pos(nan,1,1,22,1,24))])),pred,[nodeid(pos(nan,1,1,1,1,24))]),b(greater(b(identifier(x),integer,[nodeid(pos(nan,1,1,28,1,28))]),b(integer(12),integer,[nodeid(pos(nan,1,1,30,1,30))])),pred,[nodeid(pos(nan,1,1,28,1,30))])),pred,[nodeid(pos(nan,1,1,1,1,30))]),b(less(b(identifier(y),integer,[nodeid(pos(nan,1,1,35,1,35))]),b(integer(3),integer,[nodeid(pos(nan,1,1,37,1,37))])),pred,[nodeid(pos(nan,1,1,35,1,37))])),pred,[nodeid(pos(nan,1,1,1,1,37))])),pred,[used_ids([x,y])])).
2490
2491		% #(x,y).((x : 5 .. 10000 & x / y = 19000) & y : 1 .. 100)
2492		must_fail_clpfd_det(105,b(exists([b(identifier(x),integer,[]),b(identifier(y),integer,[])],b(conjunct(b(conjunct(b(member(b(identifier(x),integer,[nodeid(pos(nan,1,1,1,1,1))]),b(interval(b(integer(5),integer,[nodeid(pos(nan,1,1,3,1,3))]),b(integer(10000),integer,[nodeid(pos(nan,1,1,6,1,6))])),set(integer),[nodeid(pos(nan,1,1,3,1,6))])),pred,[nodeid(pos(nan,1,1,1,1,6))]),b(equal(b(div(b(identifier(x),integer,[nodeid(pos(nan,1,1,14,1,14))]),b(identifier(y),integer,[nodeid(pos(nan,1,1,16,1,16))])),integer,[contains_wd_condition,nodeid(pos(nan,1,1,14,1,16))]),b(integer(19000),integer,[nodeid(pos(nan,1,1,18,1,18))])),pred,[contains_wd_condition,nodeid(pos(nan,1,1,14,1,18))])),pred,[contains_wd_condition,nodeid(pos(nan,1,1,1,1,18))]),b(member(b(identifier(y),integer,[nodeid(pos(nan,1,1,26,1,26))]),b(interval(b(integer(1),integer,[nodeid(pos(nan,1,1,28,1,28))]),b(integer(100),integer,[nodeid(pos(nan,1,1,31,1,31))])),set(integer),[nodeid(pos(nan,1,1,28,1,31))])),pred,[nodeid(pos(nan,1,1,26,1,31))])),pred,[contains_wd_condition,nodeid(pos(nan,1,1,1,1,31))])),pred,[used_ids([x,y])])).
2493
2494		% #(x,y).((x : 500 .. 10000 & 499 / y = x) & y : 1 .. 100)
2495		must_fail_clpfd_det(106,b(exists([b(identifier(x),integer,[]),b(identifier(y),integer,[])],b(conjunct(b(conjunct(b(member(b(identifier(x),integer,[nodeid(pos(nan,1,1,1,1,1))]),b(interval(b(integer(500),integer,[nodeid(pos(nan,1,1,3,1,3))]),b(integer(10000),integer,[nodeid(pos(nan,1,1,8,1,8))])),set(integer),[nodeid(pos(nan,1,1,3,1,8))])),pred,[nodeid(pos(nan,1,1,1,1,8))]),b(equal(b(div(b(integer(499),integer,[nodeid(pos(nan,1,1,16,1,16))]),b(identifier(y),integer,[nodeid(pos(nan,1,1,20,1,20))])),integer,[contains_wd_condition,nodeid(pos(nan,1,1,16,1,20))]),b(identifier(x),integer,[nodeid(pos(nan,1,1,22,1,22))])),pred,[contains_wd_condition,nodeid(pos(nan,1,1,16,1,22))])),pred,[contains_wd_condition,nodeid(pos(nan,1,1,1,1,22))]),b(member(b(identifier(y),integer,[nodeid(pos(nan,1,1,26,1,26))]),b(interval(b(integer(1),integer,[nodeid(pos(nan,1,1,28,1,28))]),b(integer(100),integer,[nodeid(pos(nan,1,1,31,1,31))])),set(integer),[nodeid(pos(nan,1,1,28,1,31))])),pred,[nodeid(pos(nan,1,1,26,1,31))])),pred,[contains_wd_condition,nodeid(pos(nan,1,1,1,1,31))])),pred,[used_ids([x,y])])).
2496
2497		% #(y,f,x).((((y : 1 .. 1000001 & f : 100001 .. 100005 --> 1 .. 9000) & x : dom(f)) & x : 2 .. 100003) & (x > 5000 => y : 2000001 .. 2000002))
2498		must_fail_clpfd_det(107,b(exists([b(identifier(y),integer,[]),b(identifier(f),set(couple(integer,integer)),[]),b(identifier(x),integer,[])],b(conjunct(b(conjunct(b(conjunct(b(conjunct(b(member(b(identifier(y),integer,[nodeid(pos(nan,1,1,1,1,1))]),b(interval(b(integer(1),integer,[nodeid(pos(nan,1,1,3,1,3))]),b(integer(1000001),integer,[nodeid(pos(nan,1,1,6,1,6))])),set(integer),[nodeid(pos(nan,1,1,3,1,6))])),pred,[nodeid(pos(nan,1,1,1,1,6))]),b(member(b(identifier(f),set(couple(integer,integer)),[nodeid(pos(nan,1,1,16,1,16))]),b(total_function(b(interval(b(integer(100001),integer,[nodeid(pos(nan,1,1,18,1,18))]),b(integer(100005),integer,[nodeid(pos(nan,1,1,26,1,26))])),set(integer),[nodeid(pos(nan,1,1,18,1,26))]),b(interval(b(integer(1),integer,[nodeid(pos(nan,1,1,37,1,37))]),b(integer(9000),integer,[nodeid(pos(nan,1,1,40,1,40))])),set(integer),[nodeid(pos(nan,1,1,37,1,40))])),set(set(couple(integer,integer))),[nodeid(pos(nan,1,1,18,1,40))])),pred,[nodeid(pos(nan,1,1,16,1,40))])),pred,[nodeid(pos(nan,1,1,1,1,40))]),b(member(b(identifier(x),integer,[nodeid(pos(nan,1,1,48,1,48))]),b(domain(b(identifier(f),set(couple(integer,integer)),[nodeid(pos(nan,1,1,54,1,54))])),set(integer),[nodeid(pos(nan,1,1,50,1,55))])),pred,[nodeid(pos(nan,1,1,48,1,55))])),pred,[nodeid(pos(nan,1,1,1,1,55))]),b(member(b(identifier(x),integer,[nodeid(pos(nan,1,1,59,1,59))]),b(interval(b(integer(2),integer,[nodeid(pos(nan,1,1,61,1,61))]),b(integer(100003),integer,[nodeid(pos(nan,1,1,64,1,64))])),set(integer),[nodeid(pos(nan,1,1,61,1,64))])),pred,[nodeid(pos(nan,1,1,59,1,64))])),pred,[nodeid(pos(nan,1,1,1,1,64))]),b(implication(b(greater(b(identifier(x),integer,[nodeid(pos(nan,1,1,74,1,74))]),b(integer(5000),integer,[nodeid(pos(nan,1,1,76,1,76))])),pred,[nodeid(pos(nan,1,1,74,1,76))]),b(member(b(identifier(y),integer,[nodeid(pos(nan,1,1,84,1,84))]),b(interval(b(integer(2000001),integer,[nodeid(pos(nan,1,1,86,1,86))]),b(integer(2000002),integer,[nodeid(pos(nan,1,1,95,1,95))])),set(integer),[nodeid(pos(nan,1,1,86,1,95))])),pred,[nodeid(pos(nan,1,1,84,1,95))])),pred,[nodeid(pos(nan,1,1,74,1,95))])),pred,[nodeid(pos(nan,1,1,1,1,102))])),pred,[used_ids([f,x,y])])).
2499		% #(f,x).((f : (BOOL * (123456 .. 123459)) * BOOL --> 1 .. 100 & x : dom(f)) & #(b,y,b2).(((b : BOOL & y : INTEGER) & b2 : BOOL) & (x = (b |-> y) |-> b2 & (y > 123459 or y < 123456))))
2500		must_fail_clpfd_det(108,b(exists([b(identifier(f),set(couple(couple(couple(boolean,integer),boolean),integer)),[]),b(identifier(x),couple(couple(boolean,integer),boolean),[])],b(conjunct(b(conjunct(b(member(b(identifier(f),set(couple(couple(couple(boolean,integer),boolean),integer)),[nodeid(pos(nan,1,1,1,1,1))]),b(total_function(b(cartesian_product(b(cartesian_product(b(bool_set,set(boolean),[nodeid(pos(nan,1,1,5,1,5))]),b(interval(b(integer(123456),integer,[nodeid(pos(nan,1,1,11,1,11))]),b(integer(123459),integer,[nodeid(pos(nan,1,1,19,1,19))])),set(integer),[nodeid(pos(nan,1,1,11,1,19))])),set(couple(boolean,integer)),[nodeid(pos(nan,1,1,5,1,25))]),b(bool_set,set(boolean),[nodeid(pos(nan,1,1,27,1,27))])),set(couple(couple(boolean,integer),boolean)),[nodeid(pos(nan,1,1,5,1,27))]),b(interval(b(integer(1),integer,[nodeid(pos(nan,1,1,37,1,37))]),b(integer(100),integer,[nodeid(pos(nan,1,1,40,1,40))])),set(integer),[nodeid(pos(nan,1,1,37,1,40))])),set(set(couple(couple(couple(boolean,integer),boolean),integer))),[nodeid(pos(nan,1,1,4,1,40))])),pred,[nodeid(pos(nan,1,1,1,1,40))]),b(member(b(identifier(x),couple(couple(boolean,integer),boolean),[nodeid(pos(nan,1,1,46,1,46))]),b(domain(b(identifier(f),set(couple(couple(couple(boolean,integer),boolean),integer)),[nodeid(pos(nan,1,1,52,1,52))])),set(couple(couple(boolean,integer),boolean)),[nodeid(pos(nan,1,1,48,1,53))])),pred,[nodeid(pos(nan,1,1,46,1,53))])),pred,[nodeid(pos(nan,1,1,1,1,53))]),b(exists([b(identifier(b),boolean,[nodeid(pos(nan,1,1,59,1,59)),introduced_by(exists)]),b(identifier(y),integer,[nodeid(pos(nan,1,1,61,1,61)),introduced_by(exists)]),b(identifier(b2),boolean,[nodeid(pos(nan,1,1,63,1,63)),introduced_by(exists)])],b(conjunct(b(equal(b(identifier(x),couple(couple(boolean,integer),boolean),[nodeid(pos(nan,1,1,68,1,68))]),b(couple(b(couple(b(identifier(b),boolean,[nodeid(pos(nan,1,1,71,1,71)),introduced_by(exists)]),b(identifier(y),integer,[nodeid(pos(nan,1,1,73,1,73)),introduced_by(exists)])),couple(boolean,integer),[nodeid(pos(nan,1,1,70,1,77))]),b(identifier(b2),boolean,[nodeid(pos(nan,1,1,75,1,75)),introduced_by(exists)])),couple(couple(boolean,integer),boolean),[nodeid(pos(nan,1,1,70,1,77))])),pred,[nodeid(pos(nan,1,1,68,1,77))]),b(disjunct(b(greater(b(identifier(y),integer,[nodeid(pos(nan,1,1,82,1,82)),introduced_by(exists)]),b(integer(123459),integer,[nodeid(pos(nan,1,1,84,1,84))])),pred,[nodeid(pos(nan,1,1,82,1,84))]),b(less(b(identifier(y),integer,[nodeid(pos(nan,1,1,94,1,94)),introduced_by(exists)]),b(integer(123456),integer,[nodeid(pos(nan,1,1,96,1,96))])),pred,[nodeid(pos(nan,1,1,94,1,96))])),pred,[nodeid(pos(nan,1,1,82,1,96))])),pred,[nodeid(pos(nan,1,1,68,1,102))])),pred,[used_ids([x]),nodeid(pos(nan,1,1,57,1,103))])),pred,[nodeid(pos(nan,1,1,1,1,103))])),pred,[used_ids([f,x])])).
2501		% #(f,x,y).((x : INTEGER & y : INTEGER) & ((f : 10 .. 200 --> 1 .. 200000 & x |-> y : f) & (x > 200 or x < 10)))
2502		must_fail_clpfd_det(109,b(exists([b(identifier(f),set(couple(integer,integer)),[]),b(identifier(x),integer,[]),b(identifier(y),integer,[])],b(conjunct(b(conjunct(b(member(b(identifier(f),set(couple(integer,integer)),[nodeid(pos(nan,1,1,1,1,1))]),b(total_function(b(interval(b(integer(10),integer,[nodeid(pos(nan,1,1,4,1,4))]),b(integer(200),integer,[nodeid(pos(nan,1,1,8,1,8))])),set(integer),[nodeid(pos(nan,1,1,4,1,8))]),b(interval(b(integer(1),integer,[nodeid(pos(nan,1,1,16,1,16))]),b(integer(200000),integer,[nodeid(pos(nan,1,1,19,1,19))])),set(integer),[nodeid(pos(nan,1,1,16,1,19))])),set(set(couple(integer,integer))),[nodeid(pos(nan,1,1,4,1,19))])),pred,[nodeid(pos(nan,1,1,1,1,19))]),b(member(b(couple(b(identifier(x),integer,[nodeid(pos(nan,1,1,28,1,28))]),b(identifier(y),integer,[nodeid(pos(nan,1,1,32,1,32))])),couple(integer,integer),[nodeid(pos(nan,1,1,28,1,32))]),b(identifier(f),set(couple(integer,integer)),[nodeid(pos(nan,1,1,36,1,36))])),pred,[nodeid(pos(nan,1,1,28,1,36))])),pred,[nodeid(pos(nan,1,1,1,1,36))]),b(disjunct(b(greater(b(identifier(x),integer,[nodeid(pos(nan,1,1,41,1,41))]),b(integer(200),integer,[nodeid(pos(nan,1,1,43,1,43))])),pred,[nodeid(pos(nan,1,1,41,1,43))]),b(less(b(identifier(x),integer,[nodeid(pos(nan,1,1,50,1,50))]),b(integer(10),integer,[nodeid(pos(nan,1,1,52,1,52))])),pred,[nodeid(pos(nan,1,1,50,1,52))])),pred,[nodeid(pos(nan,1,1,41,1,52))])),pred,[nodeid(pos(nan,1,1,1,1,54))])),pred,[used_ids([f,x,y])])).
2503		% #(f,b,x).((b : BOOL * BOOL & x : INTEGER) & ((f : BOOL * BOOL --> 100 .. 200000 & b |-> x : f) & (x > 200000 or x < 100)))
2504		must_fail_clpfd_det(110,b(exists([b(identifier(f),set(couple(couple(boolean,boolean),integer)),[]),b(identifier(b),couple(boolean,boolean),[]),b(identifier(x),integer,[])],b(conjunct(b(conjunct(b(member(b(identifier(f),set(couple(couple(boolean,boolean),integer)),[nodeid(pos(nan,1,1,1,1,1))]),b(total_function(b(cartesian_product(b(bool_set,set(boolean),[nodeid(pos(nan,1,1,5,1,5))]),b(bool_set,set(boolean),[nodeid(pos(nan,1,1,10,1,10))])),set(couple(boolean,boolean)),[nodeid(pos(nan,1,1,5,1,10))]),b(interval(b(integer(100),integer,[nodeid(pos(nan,1,1,20,1,20))]),b(integer(200000),integer,[nodeid(pos(nan,1,1,25,1,25))])),set(integer),[nodeid(pos(nan,1,1,20,1,25))])),set(set(couple(couple(boolean,boolean),integer))),[nodeid(pos(nan,1,1,4,1,25))])),pred,[nodeid(pos(nan,1,1,1,1,25))]),b(member(b(couple(b(identifier(b),couple(boolean,boolean),[nodeid(pos(nan,1,1,34,1,34))]),b(identifier(x),integer,[nodeid(pos(nan,1,1,38,1,38))])),couple(couple(boolean,boolean),integer),[nodeid(pos(nan,1,1,34,1,38))]),b(identifier(f),set(couple(couple(boolean,boolean),integer)),[nodeid(pos(nan,1,1,42,1,42))])),pred,[nodeid(pos(nan,1,1,34,1,42))])),pred,[nodeid(pos(nan,1,1,1,1,42))]),b(disjunct(b(greater(b(identifier(x),integer,[nodeid(pos(nan,1,1,47,1,47))]),b(integer(200000),integer,[nodeid(pos(nan,1,1,49,1,49))])),pred,[nodeid(pos(nan,1,1,47,1,49))]),b(less(b(identifier(x),integer,[nodeid(pos(nan,1,1,59,1,59))]),b(integer(100),integer,[nodeid(pos(nan,1,1,61,1,61))])),pred,[nodeid(pos(nan,1,1,59,1,61))])),pred,[nodeid(pos(nan,1,1,47,1,61))])),pred,[nodeid(pos(nan,1,1,1,1,64))])),pred,[used_ids([b,f,x])])).
2505		% #(f,g).(((f : 10001 .. 10110 --> NATURAL & !(x).(x : dom(f) => f(x) : dom(f))) & g : 20010 .. 20020 --> BOOL) & !(x).(x : dom(f) => f(x) : dom(g)))
2506		must_fail_clpfd_det(111,b(exists([b(identifier(f),set(couple(integer,integer)),[]),b(identifier(g),set(couple(integer,boolean)),[])],b(conjunct(b(conjunct(b(conjunct(b(member(b(identifier(f),set(couple(integer,integer)),[nodeid(pos(nan,1,1,2,1,2))]),b(total_function(b(interval(b(integer(10001),integer,[nodeid(pos(nan,1,1,5,1,5))]),b(integer(10110),integer,[nodeid(pos(nan,1,1,12,1,12))])),set(integer),[nodeid(pos(nan,1,1,5,1,12))]),b(integer_set('NATURAL'),set(integer),[nodeid(pos(nan,1,1,22,1,22))])),set(set(couple(integer,integer))),[nodeid(pos(nan,1,1,5,1,22))])),pred,[nodeid(pos(nan,1,1,2,1,22))]),b(forall([b(identifier(x),integer,[nodeid(pos(nan,1,1,33,1,33)),introduced_by(forall)])],b(member(b(identifier(x),integer,[nodeid(pos(nan,1,1,36,1,36)),introduced_by(forall)]),b(domain(b(identifier(f),set(couple(integer,integer)),[nodeid(pos(nan,1,1,42,1,42))])),set(integer),[nodeid(pos(nan,1,1,38,1,43))])),pred,[nodeid(pos(nan,1,1,36,1,43))]),b(member(b(function(b(identifier(f),set(couple(integer,integer)),[nodeid(pos(nan,1,1,48,1,48))]),b(identifier(x),integer,[nodeid(pos(nan,1,1,50,1,50)),introduced_by(forall)])),integer,[contains_wd_condition,nodeid(pos(nan,1,1,48,1,51))]),b(domain(b(identifier(f),set(couple(integer,integer)),[nodeid(pos(nan,1,1,57,1,57))])),set(integer),[nodeid(pos(nan,1,1,53,1,58))])),pred,[contains_wd_condition,nodeid(pos(nan,1,1,48,1,58))])),pred,[used_ids([f]),nodeid(pos(nan,1,1,32,1,59))])),pred,[nodeid(pos(nan,1,1,2,1,59))]),b(member(b(identifier(g),set(couple(integer,boolean)),[nodeid(pos(nan,1,1,63,1,63))]),b(total_function(b(interval(b(integer(20010),integer,[nodeid(pos(nan,1,1,65,1,65))]),b(integer(20020),integer,[nodeid(pos(nan,1,1,72,1,72))])),set(integer),[nodeid(pos(nan,1,1,65,1,72))]),b(bool_set,set(boolean),[nodeid(pos(nan,1,1,82,1,82))])),set(set(couple(integer,boolean))),[nodeid(pos(nan,1,1,65,1,82))])),pred,[nodeid(pos(nan,1,1,63,1,82))])),pred,[nodeid(pos(nan,1,1,2,1,82))]),b(forall([b(identifier(x),integer,[nodeid(pos(nan,1,1,90,1,90)),introduced_by(forall)])],b(member(b(identifier(x),integer,[nodeid(pos(nan,1,1,93,1,93)),introduced_by(forall)]),b(domain(b(identifier(f),set(couple(integer,integer)),[nodeid(pos(nan,1,1,99,1,99))])),set(integer),[nodeid(pos(nan,1,1,95,1,100))])),pred,[nodeid(pos(nan,1,1,93,1,100))]),b(member(b(function(b(identifier(f),set(couple(integer,integer)),[nodeid(pos(nan,1,1,105,1,105))]),b(identifier(x),integer,[nodeid(pos(nan,1,1,107,1,107)),introduced_by(forall)])),integer,[contains_wd_condition,nodeid(pos(nan,1,1,105,1,108))]),b(domain(b(identifier(g),set(couple(integer,boolean)),[nodeid(pos(nan,1,1,114,1,114))])),set(integer),[nodeid(pos(nan,1,1,110,1,115))])),pred,[contains_wd_condition,nodeid(pos(nan,1,1,105,1,115))])),pred,[used_ids([f,g]),nodeid(pos(nan,1,1,89,1,116))])),pred,[nodeid(pos(nan,1,1,2,1,116))])),pred,[used_ids([f,g])])).
2507		% #(f,x,y).((x : INTEGER & y : INTEGER) & ((f : 1001 .. 2001 --> 1900 .. 3333 & x |-> y : f) & y + 101 < x))
2508		must_fail_clpfd_det(112,b(exists([b(identifier(f),set(couple(integer,integer)),[]),b(identifier(x),integer,[]),b(identifier(y),integer,[])],b(conjunct(b(conjunct(b(member(b(identifier(f),set(couple(integer,integer)),[nodeid(pos(nan,1,1,1,1,1))]),b(total_function(b(interval(b(integer(1001),integer,[nodeid(pos(nan,1,1,5,1,5))]),b(integer(2001),integer,[nodeid(pos(nan,1,1,11,1,11))])),set(integer),[nodeid(pos(nan,1,1,5,1,11))]),b(interval(b(integer(1900),integer,[nodeid(pos(nan,1,1,20,1,20))]),b(integer(3333),integer,[nodeid(pos(nan,1,1,26,1,26))])),set(integer),[nodeid(pos(nan,1,1,20,1,26))])),set(set(couple(integer,integer))),[nodeid(pos(nan,1,1,5,1,26))])),pred,[nodeid(pos(nan,1,1,1,1,26))]),b(member(b(couple(b(identifier(x),integer,[nodeid(pos(nan,1,1,33,1,33))]),b(identifier(y),integer,[nodeid(pos(nan,1,1,37,1,37))])),couple(integer,integer),[nodeid(pos(nan,1,1,33,1,37))]),b(identifier(f),set(couple(integer,integer)),[nodeid(pos(nan,1,1,41,1,41))])),pred,[nodeid(pos(nan,1,1,33,1,41))])),pred,[nodeid(pos(nan,1,1,1,1,41))]),b(less(b(add(b(identifier(y),integer,[nodeid(pos(nan,1,1,45,1,45))]),b(integer(101),integer,[nodeid(pos(nan,1,1,47,1,47))])),integer,[nodeid(pos(nan,1,1,45,1,47))]),b(identifier(x),integer,[nodeid(pos(nan,1,1,51,1,51))])),pred,[nodeid(pos(nan,1,1,45,1,51))])),pred,[nodeid(pos(nan,1,1,1,1,51))])),pred,[used_ids([f,x,y])])).
2509
2510		% #(r,x,y,v,w).((((x : INTEGER & y : INTEGER) & v : INTEGER) & w : INTEGER) & ((((r : 1001 .. 1005 <-> 1000 .. 1099 & x |-> y : r) & v |-> w : r) & x + y = (v + w) + 120) & card(r) = 3))
2511		must_fail_clpfd_det(113,b(exists([b(identifier(r),set(couple(integer,integer)),[]),b(identifier(x),integer,[]),b(identifier(y),integer,[]),b(identifier(v),integer,[]),b(identifier(w),integer,[])],b(conjunct(b(conjunct(b(conjunct(b(conjunct(b(member(b(identifier(r),set(couple(integer,integer)),[nodeid(pos(nan,1,1,1,1,1))]),b(relations(b(interval(b(integer(1001),integer,[nodeid(pos(nan,1,1,4,1,4))]),b(integer(1005),integer,[nodeid(pos(nan,1,1,10,1,10))])),set(integer),[nodeid(pos(nan,1,1,4,1,10))]),b(interval(b(integer(1000),integer,[nodeid(pos(nan,1,1,19,1,19))]),b(integer(1099),integer,[nodeid(pos(nan,1,1,25,1,25))])),set(integer),[nodeid(pos(nan,1,1,19,1,25))])),set(set(couple(integer,integer))),[nodeid(pos(nan,1,1,4,1,25))])),pred,[nodeid(pos(nan,1,1,1,1,25))]),b(member(b(couple(b(identifier(x),integer,[nodeid(pos(nan,1,1,32,1,32))]),b(identifier(y),integer,[nodeid(pos(nan,1,1,36,1,36))])),couple(integer,integer),[nodeid(pos(nan,1,1,32,1,36))]),b(identifier(r),set(couple(integer,integer)),[nodeid(pos(nan,1,1,40,1,40))])),pred,[nodeid(pos(nan,1,1,32,1,40))])),pred,[nodeid(pos(nan,1,1,1,1,40))]),b(member(b(couple(b(identifier(v),integer,[nodeid(pos(nan,1,1,44,1,44))]),b(identifier(w),integer,[nodeid(pos(nan,1,1,48,1,48))])),couple(integer,integer),[nodeid(pos(nan,1,1,44,1,48))]),b(identifier(r),set(couple(integer,integer)),[nodeid(pos(nan,1,1,52,1,52))])),pred,[nodeid(pos(nan,1,1,44,1,52))])),pred,[nodeid(pos(nan,1,1,1,1,52))]),b(equal(b(add(b(identifier(x),integer,[nodeid(pos(nan,1,1,57,1,57))]),b(identifier(y),integer,[nodeid(pos(nan,1,1,59,1,59))])),integer,[nodeid(pos(nan,1,1,57,1,59))]),b(add(b(add(b(identifier(v),integer,[nodeid(pos(nan,1,1,63,1,63))]),b(identifier(w),integer,[nodeid(pos(nan,1,1,65,1,65))])),integer,[nodeid(pos(nan,1,1,63,1,65))]),b(integer(120),integer,[nodeid(pos(nan,1,1,67,1,67))])),integer,[nodeid(pos(nan,1,1,63,1,67))])),pred,[nodeid(pos(nan,1,1,57,1,67))])),pred,[nodeid(pos(nan,1,1,1,1,67))]),b(equal(b(card(b(identifier(r),set(couple(integer,integer)),[nodeid(pos(nan,1,1,78,1,78))])),integer,[contains_wd_condition,nodeid(pos(nan,1,1,73,1,79))]),b(integer(3),integer,[nodeid(pos(nan,1,1,83,1,83))])),pred,[contains_wd_condition,nodeid(pos(nan,1,1,73,1,83))])),pred,[contains_wd_condition,nodeid(pos(nan,1,1,1,1,83))])),pred,[used_ids([r,v,w,x,y])])).
2512
2513		% #(r,x,y,v,w).((((x : INTEGER & y : INTEGER) & v : INTEGER) & w : INTEGER) & ((((r : 1001 .. 1005 +-> 1000 .. 1099 & x |-> y : r) & v |-> w : r) & x + y = (v + w) + 120) & card(r) = 3))
2514		must_fail_clpfd_det(114,b(exists([b(identifier(r),set(couple(integer,integer)),[]),b(identifier(x),integer,[]),b(identifier(y),integer,[]),b(identifier(v),integer,[]),b(identifier(w),integer,[])],b(conjunct(b(conjunct(b(conjunct(b(conjunct(b(member(b(identifier(r),set(couple(integer,integer)),[nodeid(pos(nan,1,1,1,1,1))]),b(partial_function(b(interval(b(integer(1001),integer,[nodeid(pos(nan,1,1,4,1,4))]),b(integer(1005),integer,[nodeid(pos(nan,1,1,10,1,10))])),set(integer),[nodeid(pos(nan,1,1,4,1,10))]),b(interval(b(integer(1000),integer,[nodeid(pos(nan,1,1,19,1,19))]),b(integer(1099),integer,[nodeid(pos(nan,1,1,25,1,25))])),set(integer),[nodeid(pos(nan,1,1,19,1,25))])),set(set(couple(integer,integer))),[nodeid(pos(nan,1,1,4,1,25))])),pred,[nodeid(pos(nan,1,1,1,1,25))]),b(member(b(couple(b(identifier(x),integer,[nodeid(pos(nan,1,1,32,1,32))]),b(identifier(y),integer,[nodeid(pos(nan,1,1,36,1,36))])),couple(integer,integer),[nodeid(pos(nan,1,1,32,1,36))]),b(identifier(r),set(couple(integer,integer)),[nodeid(pos(nan,1,1,40,1,40))])),pred,[nodeid(pos(nan,1,1,32,1,40))])),pred,[nodeid(pos(nan,1,1,1,1,40))]),b(member(b(couple(b(identifier(v),integer,[nodeid(pos(nan,1,1,44,1,44))]),b(identifier(w),integer,[nodeid(pos(nan,1,1,48,1,48))])),couple(integer,integer),[nodeid(pos(nan,1,1,44,1,48))]),b(identifier(r),set(couple(integer,integer)),[nodeid(pos(nan,1,1,52,1,52))])),pred,[nodeid(pos(nan,1,1,44,1,52))])),pred,[nodeid(pos(nan,1,1,1,1,52))]),b(equal(b(add(b(identifier(x),integer,[nodeid(pos(nan,1,1,57,1,57))]),b(identifier(y),integer,[nodeid(pos(nan,1,1,59,1,59))])),integer,[nodeid(pos(nan,1,1,57,1,59))]),b(add(b(add(b(identifier(v),integer,[nodeid(pos(nan,1,1,63,1,63))]),b(identifier(w),integer,[nodeid(pos(nan,1,1,65,1,65))])),integer,[nodeid(pos(nan,1,1,63,1,65))]),b(integer(120),integer,[nodeid(pos(nan,1,1,67,1,67))])),integer,[nodeid(pos(nan,1,1,63,1,67))])),pred,[nodeid(pos(nan,1,1,57,1,67))])),pred,[nodeid(pos(nan,1,1,1,1,67))]),b(equal(b(card(b(identifier(r),set(couple(integer,integer)),[nodeid(pos(nan,1,1,78,1,78))])),integer,[contains_wd_condition,nodeid(pos(nan,1,1,73,1,79))]),b(integer(3),integer,[nodeid(pos(nan,1,1,83,1,83))])),pred,[contains_wd_condition,nodeid(pos(nan,1,1,73,1,83))])),pred,[contains_wd_condition,nodeid(pos(nan,1,1,1,1,83))])),pred,[used_ids([r,v,w,x,y])])).
2515		% #(r,x,y,v,w).((((x : INTEGER & y : INTEGER) & v : INTEGER) & w : INTEGER) & ((((r : 1001 .. 1005 >+> 1000 .. 1099 & x |-> y : r) & v |-> w : r) & x + y = (v + w) + 104) & card(r) = 2))
2516		must_fail_clpfd_det(115,b(exists([b(identifier(r),set(couple(integer,integer)),[]),b(identifier(x),integer,[]),b(identifier(y),integer,[]),b(identifier(v),integer,[]),b(identifier(w),integer,[])],b(conjunct(b(conjunct(b(conjunct(b(conjunct(b(member(b(identifier(r),set(couple(integer,integer)),[nodeid(pos(nan,1,1,1,1,1))]),b(partial_injection(b(interval(b(integer(1001),integer,[nodeid(pos(nan,1,1,4,1,4))]),b(integer(1005),integer,[nodeid(pos(nan,1,1,10,1,10))])),set(integer),[nodeid(pos(nan,1,1,4,1,10))]),b(interval(b(integer(1000),integer,[nodeid(pos(nan,1,1,19,1,19))]),b(integer(1099),integer,[nodeid(pos(nan,1,1,25,1,25))])),set(integer),[nodeid(pos(nan,1,1,19,1,25))])),set(set(couple(integer,integer))),[nodeid(pos(nan,1,1,4,1,25))])),pred,[nodeid(pos(nan,1,1,1,1,25))]),b(member(b(couple(b(identifier(x),integer,[nodeid(pos(nan,1,1,32,1,32))]),b(identifier(y),integer,[nodeid(pos(nan,1,1,36,1,36))])),couple(integer,integer),[nodeid(pos(nan,1,1,32,1,36))]),b(identifier(r),set(couple(integer,integer)),[nodeid(pos(nan,1,1,40,1,40))])),pred,[nodeid(pos(nan,1,1,32,1,40))])),pred,[nodeid(pos(nan,1,1,1,1,40))]),b(member(b(couple(b(identifier(v),integer,[nodeid(pos(nan,1,1,44,1,44))]),b(identifier(w),integer,[nodeid(pos(nan,1,1,48,1,48))])),couple(integer,integer),[nodeid(pos(nan,1,1,44,1,48))]),b(identifier(r),set(couple(integer,integer)),[nodeid(pos(nan,1,1,52,1,52))])),pred,[nodeid(pos(nan,1,1,44,1,52))])),pred,[nodeid(pos(nan,1,1,1,1,52))]),b(equal(b(add(b(identifier(x),integer,[nodeid(pos(nan,1,1,57,1,57))]),b(identifier(y),integer,[nodeid(pos(nan,1,1,59,1,59))])),integer,[nodeid(pos(nan,1,1,57,1,59))]),b(add(b(add(b(identifier(v),integer,[nodeid(pos(nan,1,1,63,1,63))]),b(identifier(w),integer,[nodeid(pos(nan,1,1,65,1,65))])),integer,[nodeid(pos(nan,1,1,63,1,65))]),b(integer(104),integer,[nodeid(pos(nan,1,1,67,1,67))])),integer,[nodeid(pos(nan,1,1,63,1,67))])),pred,[nodeid(pos(nan,1,1,57,1,67))])),pred,[nodeid(pos(nan,1,1,1,1,67))]),b(equal(b(card(b(identifier(r),set(couple(integer,integer)),[nodeid(pos(nan,1,1,78,1,78))])),integer,[contains_wd_condition,nodeid(pos(nan,1,1,73,1,79))]),b(integer(2),integer,[nodeid(pos(nan,1,1,83,1,83))])),pred,[contains_wd_condition,nodeid(pos(nan,1,1,73,1,83))])),pred,[contains_wd_condition,nodeid(pos(nan,1,1,1,1,83))])),pred,[used_ids([r,v,w,x,y])])).
2517		% #(s,x,b,y,b2).(((((s : POW((INTEGER * STRING) * BOOL) & x : INTEGER) & b : BOOL) & y : INTEGER) & b2 : BOOL) & (((s = {((1|->"a")|->TRUE),((2|->"a")|->FALSE),((3|->"b")|->FALSE),((4|->"b")|->FALSE)} & (x |-> "a") |-> b : s) & (y |-> "b") |-> b2 : s) & x > y))
2518		must_fail_clpfd_det(116,b(exists([b(identifier(s),set(couple(couple(integer,string),boolean)),[]),b(identifier(x),integer,[]),b(identifier(b),boolean,[]),b(identifier(y),integer,[]),b(identifier(b2),boolean,[])],b(conjunct(b(conjunct(b(conjunct(b(equal(b(identifier(s),set(couple(couple(integer,string),boolean)),[nodeid(pos(nan,1,1,1,1,1))]),b(value(avl_set(node(((int(2),string(a)),pred_false),true,1,node(((int(1),string(a)),pred_true),true,0,empty,empty),node(((int(3),string(b)),pred_false),true,1,empty,node(((int(4),string(b)),pred_false),true,0,empty,empty))))),set(couple(couple(integer,string),boolean)),[nodeid(pos(nan,1,1,5,1,66))])),pred,[nodeid(pos(nan,1,1,1,1,66))]),b(member(b(couple(b(couple(b(identifier(x),integer,[nodeid(pos(nan,1,1,71,1,71))]),b(string(a),string,[nodeid(pos(nan,1,1,75,1,75))])),couple(integer,string),[nodeid(pos(nan,1,1,71,1,75))]),b(identifier(b),boolean,[nodeid(pos(nan,1,1,81,1,81))])),couple(couple(integer,string),boolean),[nodeid(pos(nan,1,1,71,1,81))]),b(identifier(s),set(couple(couple(integer,string),boolean)),[nodeid(pos(nan,1,1,85,1,85))])),pred,[nodeid(pos(nan,1,1,71,1,85))])),pred,[nodeid(pos(nan,1,1,1,1,85))]),b(member(b(couple(b(couple(b(identifier(y),integer,[nodeid(pos(nan,1,1,89,1,89))]),b(string(b),string,[nodeid(pos(nan,1,1,93,1,93))])),couple(integer,string),[nodeid(pos(nan,1,1,89,1,93))]),b(identifier(b2),boolean,[nodeid(pos(nan,1,1,99,1,99))])),couple(couple(integer,string),boolean),[nodeid(pos(nan,1,1,89,1,99))]),b(identifier(s),set(couple(couple(integer,string),boolean)),[nodeid(pos(nan,1,1,104,1,104))])),pred,[nodeid(pos(nan,1,1,89,1,104))])),pred,[nodeid(pos(nan,1,1,1,1,104))]),b(greater(b(identifier(x),integer,[nodeid(pos(nan,1,1,108,1,108))]),b(identifier(y),integer,[nodeid(pos(nan,1,1,110,1,110))])),pred,[nodeid(pos(nan,1,1,108,1,110))])),pred,[nodeid(pos(nan,1,1,1,1,110))])),pred,[used_ids([b,b2,s,x,y])])).
2519		% #(f,v,x).(((f : POW((INTEGER * BOOL) * INTEGER) & v : INTEGER) & x : INTEGER) & ((f = {(11 |-> TRUE) |-> 3,(10 |-> TRUE) |-> 4,(2 |-> FALSE) |-> 5,(3 |-> FALSE) |-> v} & x |-> FALSE : dom(f)) & x |-> TRUE : dom(f)))
2520		must_fail_clpfd_det(117,b(exists([b(identifier(f),set(couple(couple(integer,boolean),integer)),[]),b(identifier(v),integer,[]),b(identifier(x),integer,[])],b(conjunct(b(conjunct(b(equal(b(identifier(f),set(couple(couple(integer,boolean),integer)),[nodeid(pos(nan,1,1,1,1,1))]),b(set_extension([b(couple(b(couple(b(integer(11),integer,[nodeid(pos(nan,1,1,5,1,5))]),b(boolean_true,boolean,[nodeid(pos(nan,1,1,10,1,10))])),couple(integer,boolean),[nodeid(pos(nan,1,1,5,1,10))]),b(integer(3),integer,[nodeid(pos(nan,1,1,17,1,17))])),couple(couple(integer,boolean),integer),[nodeid(pos(nan,1,1,5,1,17))]),b(couple(b(couple(b(integer(10),integer,[nodeid(pos(nan,1,1,20,1,20))]),b(boolean_true,boolean,[nodeid(pos(nan,1,1,25,1,25))])),couple(integer,boolean),[nodeid(pos(nan,1,1,20,1,25))]),b(integer(4),integer,[nodeid(pos(nan,1,1,32,1,32))])),couple(couple(integer,boolean),integer),[nodeid(pos(nan,1,1,20,1,32))]),b(couple(b(couple(b(integer(2),integer,[nodeid(pos(nan,1,1,35,1,35))]),b(boolean_false,boolean,[nodeid(pos(nan,1,1,39,1,39))])),couple(integer,boolean),[nodeid(pos(nan,1,1,35,1,39))]),b(integer(5),integer,[nodeid(pos(nan,1,1,47,1,47))])),couple(couple(integer,boolean),integer),[nodeid(pos(nan,1,1,35,1,47))]),b(couple(b(couple(b(integer(3),integer,[nodeid(pos(nan,1,1,49,1,49))]),b(boolean_false,boolean,[nodeid(pos(nan,1,1,53,1,53))])),couple(integer,boolean),[nodeid(pos(nan,1,1,49,1,53))]),b(identifier(v),integer,[nodeid(pos(nan,1,1,61,1,61))])),couple(couple(integer,boolean),integer),[nodeid(pos(nan,1,1,49,1,61))])]),set(couple(couple(integer,boolean),integer)),[nodeid(pos(nan,1,1,4,1,62))])),pred,[nodeid(pos(nan,1,1,1,1,62))]),b(member(b(couple(b(identifier(x),integer,[nodeid(pos(nan,1,1,66,1,66))]),b(boolean_false,boolean,[nodeid(pos(nan,1,1,70,1,70))])),couple(integer,boolean),[nodeid(pos(nan,1,1,66,1,70))]),b(domain(b(identifier(f),set(couple(couple(integer,boolean),integer)),[nodeid(pos(nan,1,1,82,1,82))])),set(couple(integer,boolean)),[nodeid(pos(nan,1,1,78,1,83))])),pred,[nodeid(pos(nan,1,1,66,1,83))])),pred,[nodeid(pos(nan,1,1,1,1,83))]),b(member(b(couple(b(identifier(x),integer,[nodeid(pos(nan,1,1,87,1,87))]),b(boolean_true,boolean,[nodeid(pos(nan,1,1,91,1,91))])),couple(integer,boolean),[nodeid(pos(nan,1,1,87,1,91))]),b(domain(b(identifier(f),set(couple(couple(integer,boolean),integer)),[nodeid(pos(nan,1,1,102,1,102))])),set(couple(integer,boolean)),[nodeid(pos(nan,1,1,98,1,103))])),pred,[nodeid(pos(nan,1,1,87,1,103))])),pred,[nodeid(pos(nan,1,1,1,1,103))])),pred,[used_ids([f,v,x])])).
2521		% #(f,x).((f : POW((INTEGER * BOOL) * INTEGER) & x : INTEGER) & ((f = {((2|->FALSE)|->5),((3|->FALSE)|->77),((10|->TRUE)|->4),((11|->TRUE)|->3)} & x |-> FALSE : dom(f)) & x |-> TRUE : dom(f)))
2522		must_fail_clpfd_det(118,b(exists([b(identifier(f),set(couple(couple(integer,boolean),integer)),[]),b(identifier(x),integer,[])],b(conjunct(b(conjunct(b(equal(b(identifier(f),set(couple(couple(integer,boolean),integer)),[nodeid(pos(nan,1,1,1,1,1))]),b(value(avl_set(node(((int(3),pred_false),int(77)),true,1,node(((int(2),pred_false),int(5)),true,0,empty,empty),node(((int(10),pred_true),int(4)),true,1,empty,node(((int(11),pred_true),int(3)),true,0,empty,empty))))),set(couple(couple(integer,boolean),integer)),[nodeid(pos(nan,1,1,4,1,63))])),pred,[nodeid(pos(nan,1,1,1,1,63))]),b(member(b(couple(b(identifier(x),integer,[nodeid(pos(nan,1,1,67,1,67))]),b(boolean_false,boolean,[nodeid(pos(nan,1,1,71,1,71))])),couple(integer,boolean),[nodeid(pos(nan,1,1,67,1,71))]),b(domain(b(identifier(f),set(couple(couple(integer,boolean),integer)),[nodeid(pos(nan,1,1,83,1,83))])),set(couple(integer,boolean)),[nodeid(pos(nan,1,1,79,1,84))])),pred,[nodeid(pos(nan,1,1,67,1,84))])),pred,[nodeid(pos(nan,1,1,1,1,84))]),b(member(b(couple(b(identifier(x),integer,[nodeid(pos(nan,1,1,88,1,88))]),b(boolean_true,boolean,[nodeid(pos(nan,1,1,92,1,92))])),couple(integer,boolean),[nodeid(pos(nan,1,1,88,1,92))]),b(domain(b(identifier(f),set(couple(couple(integer,boolean),integer)),[nodeid(pos(nan,1,1,103,1,103))])),set(couple(integer,boolean)),[nodeid(pos(nan,1,1,99,1,104))])),pred,[nodeid(pos(nan,1,1,88,1,104))])),pred,[nodeid(pos(nan,1,1,1,1,104))])),pred,[used_ids([f,x])])).
2523		% #(a,v1,v2,w).((((a : POW(struct(x:INTEGER * INTEGER,y:INTEGER)) & v1 : INTEGER) & v2 : INTEGER) & w : INTEGER) & ((a = {rec(x:1 |-> 33,y:22),rec(x:2 |-> 34,y:44),rec(x:3 |-> 34,y:45)} & rec(x:v1 |-> v2,y:w) : a) & (v1 + v2) + w < 56))
2524		must_fail_clpfd_det(119,b(exists([b(identifier(a),set(record([field(x,couple(integer,integer)),field(y,integer)])),[]),b(identifier(v1),integer,[]),b(identifier(v2),integer,[]),b(identifier(w),integer,[])],b(conjunct(b(conjunct(b(equal(b(identifier(a),set(record([field(x,couple(integer,integer)),field(y,integer)])),[nodeid(pos(nan,1,1,1,1,1))]),b(set_extension([b(rec([field(x,b(couple(b(integer(1),integer,[nodeid(pos(nan,1,1,13,1,13))]),b(integer(33),integer,[nodeid(pos(nan,1,1,15,1,15))])),couple(integer,integer),[nodeid(pos(nan,1,1,12,1,17))])),field(y,b(integer(22),integer,[nodeid(pos(nan,1,1,21,1,21))]))]),record([field(x,couple(integer,integer)),field(y,integer)]),[nodeid(pos(nan,1,1,6,1,23))]),b(rec([field(x,b(couple(b(integer(2),integer,[nodeid(pos(nan,1,1,32,1,32))]),b(integer(34),integer,[nodeid(pos(nan,1,1,34,1,34))])),couple(integer,integer),[nodeid(pos(nan,1,1,31,1,36))])),field(y,b(integer(44),integer,[nodeid(pos(nan,1,1,40,1,40))]))]),record([field(x,couple(integer,integer)),field(y,integer)]),[nodeid(pos(nan,1,1,25,1,42))]),b(rec([field(x,b(couple(b(integer(3),integer,[nodeid(pos(nan,1,1,51,1,51))]),b(integer(34),integer,[nodeid(pos(nan,1,1,53,1,53))])),couple(integer,integer),[nodeid(pos(nan,1,1,50,1,55))])),field(y,b(integer(45),integer,[nodeid(pos(nan,1,1,59,1,59))]))]),record([field(x,couple(integer,integer)),field(y,integer)]),[nodeid(pos(nan,1,1,44,1,61))])]),set(record([field(x,couple(integer,integer)),field(y,integer)])),[nodeid(pos(nan,1,1,5,1,62))])),pred,[nodeid(pos(nan,1,1,1,1,62))]),b(member(b(rec([field(x,b(couple(b(identifier(v1),integer,[nodeid(pos(nan,1,1,73,1,73))]),b(identifier(v2),integer,[nodeid(pos(nan,1,1,76,1,76))])),couple(integer,integer),[nodeid(pos(nan,1,1,72,1,78))])),field(y,b(identifier(w),integer,[nodeid(pos(nan,1,1,82,1,82))]))]),record([field(x,couple(integer,integer)),field(y,integer)]),[nodeid(pos(nan,1,1,66,1,83))]),b(identifier(a),set(record([field(x,couple(integer,integer)),field(y,integer)])),[nodeid(pos(nan,1,1,85,1,85))])),pred,[nodeid(pos(nan,1,1,66,1,85))])),pred,[nodeid(pos(nan,1,1,1,1,85))]),b(less(b(add(b(add(b(identifier(v1),integer,[nodeid(pos(nan,1,1,89,1,89))]),b(identifier(v2),integer,[nodeid(pos(nan,1,1,92,1,92))])),integer,[nodeid(pos(nan,1,1,89,1,92))]),b(identifier(w),integer,[nodeid(pos(nan,1,1,95,1,95))])),integer,[nodeid(pos(nan,1,1,89,1,95))]),b(integer(56),integer,[nodeid(pos(nan,1,1,98,1,98))])),pred,[nodeid(pos(nan,1,1,89,1,98))])),pred,[nodeid(pos(nan,1,1,1,1,98))])),pred,[used_ids([a,v1,v2,w])])).
2525		% #(n,r1,a,b).((((n : INTEGER & r1 : POW(struct(x:INTEGER,y:INTEGER))) & a : INTEGER) & b : INTEGER) & ((({x|x : struct(x:INTEGER,y:INTEGER) & #(vv,ww).((x = rec(x:ww,y:vv) & vv : 1 .. n) & ww : 33 .. 34)} = r1 & n = 50) & rec(x:a,y:b) : r1) & rec(x:a + 2,y:b) : r1))
2526		must_fail_clpfd_det(120,b(exists([b(identifier(n),integer,[]),b(identifier(r1),set(record([field(x,integer),field(y,integer)])),[]),b(identifier(a),integer,[]),b(identifier(b),integer,[])],b(conjunct(b(conjunct(b(conjunct(b(equal(b(comprehension_set([b(identifier(x),record([field(x,integer),field(y,integer)]),[nodeid(pos(nan,1,1,12,1,12)),introduced_by(comprehension_set)])],b(exists([b(identifier(vv),integer,[nodeid(pos(nan,1,1,6,1,6)),introduced_by(comprehension_set)]),b(identifier(ww),integer,[nodeid(pos(nan,1,1,9,1,9)),introduced_by(comprehension_set)])],b(conjunct(b(conjunct(b(equal(b(identifier(x),record([field(x,integer),field(y,integer)]),[nodeid(pos(nan,1,1,14,1,14)),introduced_by(comprehension_set)]),b(rec([field(x,b(identifier(ww),integer,[nodeid(pos(nan,1,1,22,1,22)),introduced_by(comprehension_set)])),field(y,b(identifier(vv),integer,[nodeid(pos(nan,1,1,27,1,27)),introduced_by(comprehension_set)]))]),record([field(x,integer),field(y,integer)]),[nodeid(pos(nan,1,1,16,1,29))])),pred,[nodeid(pos(nan,1,1,14,1,29))]),b(member(b(identifier(vv),integer,[nodeid(pos(nan,1,1,33,1,33)),introduced_by(comprehension_set)]),b(interval(b(integer(1),integer,[nodeid(pos(nan,1,1,36,1,36))]),b(identifier(n),integer,[nodeid(pos(nan,1,1,39,1,39))])),set(integer),[nodeid(pos(nan,1,1,36,1,39))])),pred,[nodeid(pos(nan,1,1,33,1,39))])),pred,[nodeid(pos(nan,1,1,14,1,39))]),b(member(b(identifier(ww),integer,[nodeid(pos(nan,1,1,43,1,43)),introduced_by(comprehension_set)]),b(interval(b(integer(33),integer,[nodeid(pos(nan,1,1,46,1,46))]),b(integer(34),integer,[nodeid(pos(nan,1,1,50,1,50))])),set(integer),[nodeid(pos(nan,1,1,46,1,50))])),pred,[nodeid(pos(nan,1,1,43,1,50))])),pred,[nodeid(pos(nan,1,1,14,1,50))])),pred,[used_ids([n,vv,ww,x])])),set(record([field(x,integer),field(y,integer)])),[nodeid(pos(nan,1,1,1,1,53))]),b(identifier(r1),set(record([field(x,integer),field(y,integer)])),[nodeid(pos(nan,1,1,55,1,55))])),pred,[nodeid(pos(nan,1,1,1,1,55))]),b(equal(b(identifier(n),integer,[nodeid(pos(nan,1,1,60,1,60))]),b(integer(50),integer,[nodeid(pos(nan,1,1,62,1,62))])),pred,[nodeid(pos(nan,1,1,60,1,62))])),pred,[nodeid(pos(nan,1,1,1,1,62))]),b(member(b(rec([field(x,b(identifier(a),integer,[nodeid(pos(nan,1,1,74,1,74))])),field(y,b(identifier(b),integer,[nodeid(pos(nan,1,1,78,1,78))]))]),record([field(x,integer),field(y,integer)]),[nodeid(pos(nan,1,1,68,1,79))]),b(identifier(r1),set(record([field(x,integer),field(y,integer)])),[nodeid(pos(nan,1,1,81,1,81))])),pred,[nodeid(pos(nan,1,1,68,1,81))])),pred,[nodeid(pos(nan,1,1,1,1,81))]),b(member(b(rec([field(x,b(add(b(identifier(a),integer,[nodeid(pos(nan,1,1,92,1,92))]),b(integer(2),integer,[nodeid(pos(nan,1,1,94,1,94))])),integer,[nodeid(pos(nan,1,1,92,1,94))])),field(y,b(identifier(b),integer,[nodeid(pos(nan,1,1,98,1,98))]))]),record([field(x,integer),field(y,integer)]),[nodeid(pos(nan,1,1,86,1,99))]),b(identifier(r1),set(record([field(x,integer),field(y,integer)])),[nodeid(pos(nan,1,1,101,1,101))])),pred,[nodeid(pos(nan,1,1,86,1,101))])),pred,[nodeid(pos(nan,1,1,1,1,101))])),pred,[used_ids([a,b,n,r1])])).
2527		% #(x,y).(y : INTEGER & (((rec(f:x) /= rec(f:y) & x : 1 .. 2) & y = 2) & rec(f:x) /= rec(f:1)))
2528		must_fail_clpfd_det(121,b(exists([b(identifier(x),integer,[]),b(identifier(y),integer,[])],b(conjunct(b(conjunct(b(conjunct(b(not_equal(b(rec([field(f,b(identifier(x),integer,[nodeid(pos(nan,1,1,7,1,7))]))]),record([field(f,integer)]),[nodeid(pos(nan,1,1,1,1,8))]),b(rec([field(f,b(identifier(y),integer,[nodeid(pos(nan,1,1,19,1,19))]))]),record([field(f,integer)]),[nodeid(pos(nan,1,1,13,1,20))])),pred,[nodeid(pos(nan,1,1,1,1,20))]),b(member(b(identifier(x),integer,[nodeid(pos(nan,1,1,24,1,24))]),b(interval(b(integer(1),integer,[nodeid(pos(nan,1,1,26,1,26))]),b(integer(2),integer,[nodeid(pos(nan,1,1,29,1,29))])),set(integer),[nodeid(pos(nan,1,1,26,1,29))])),pred,[nodeid(pos(nan,1,1,24,1,29))])),pred,[nodeid(pos(nan,1,1,1,1,29))]),b(equal(b(identifier(y),integer,[nodeid(pos(nan,1,1,33,1,33))]),b(integer(2),integer,[nodeid(pos(nan,1,1,35,1,35))])),pred,[nodeid(pos(nan,1,1,33,1,35))])),pred,[nodeid(pos(nan,1,1,1,1,35))]),b(not_equal(b(rec([field(f,b(identifier(x),integer,[nodeid(pos(nan,1,1,45,1,45))]))]),record([field(f,integer)]),[nodeid(pos(nan,1,1,39,1,46))]),b(rec([field(f,b(integer(1),integer,[nodeid(pos(nan,1,1,57,1,57))]))]),record([field(f,integer)]),[nodeid(pos(nan,1,1,51,1,58))])),pred,[nodeid(pos(nan,1,1,39,1,58))])),pred,[nodeid(pos(nan,1,1,1,1,58))])),pred,[used_ids([x,y])])).
2529		% #(x,y).(y : INTEGER & ((((x |-> (1 |-> 2)) /= (y |-> (1 |-> 2)) & x : 1 .. 2) & y = 2) & (x |-> (1 |-> 2)) /= (1 |-> (1 |-> 2))))
2530		must_fail_clpfd_det(122,b(exists([b(identifier(x),integer,[]),b(identifier(y),integer,[])],b(conjunct(b(conjunct(b(conjunct(b(not_equal(b(couple(b(identifier(x),integer,[nodeid(pos(nan,1,1,2,1,2))]),b(couple(b(integer(1),integer,[nodeid(pos(nan,1,1,5,1,5))]),b(integer(2),integer,[nodeid(pos(nan,1,1,7,1,7))])),couple(integer,integer),[nodeid(pos(nan,1,1,4,1,8))])),couple(integer,couple(integer,integer)),[nodeid(pos(nan,1,1,1,1,9))]),b(couple(b(identifier(y),integer,[nodeid(pos(nan,1,1,15,1,15))]),b(couple(b(integer(1),integer,[nodeid(pos(nan,1,1,18,1,18))]),b(integer(2),integer,[nodeid(pos(nan,1,1,20,1,20))])),couple(integer,integer),[nodeid(pos(nan,1,1,17,1,21))])),couple(integer,couple(integer,integer)),[nodeid(pos(nan,1,1,14,1,22))])),pred,[nodeid(pos(nan,1,1,1,1,22))]),b(member(b(identifier(x),integer,[nodeid(pos(nan,1,1,26,1,26))]),b(interval(b(integer(1),integer,[nodeid(pos(nan,1,1,28,1,28))]),b(integer(2),integer,[nodeid(pos(nan,1,1,31,1,31))])),set(integer),[nodeid(pos(nan,1,1,28,1,31))])),pred,[nodeid(pos(nan,1,1,26,1,31))])),pred,[nodeid(pos(nan,1,1,1,1,31))]),b(equal(b(identifier(y),integer,[nodeid(pos(nan,1,1,35,1,35))]),b(integer(2),integer,[nodeid(pos(nan,1,1,37,1,37))])),pred,[nodeid(pos(nan,1,1,35,1,37))])),pred,[nodeid(pos(nan,1,1,1,1,37))]),b(not_equal(b(couple(b(identifier(x),integer,[nodeid(pos(nan,1,1,42,1,42))]),b(couple(b(integer(1),integer,[nodeid(pos(nan,1,1,45,1,45))]),b(integer(2),integer,[nodeid(pos(nan,1,1,47,1,47))])),couple(integer,integer),[nodeid(pos(nan,1,1,44,1,48))])),couple(integer,couple(integer,integer)),[nodeid(pos(nan,1,1,41,1,49))]),b(couple(b(integer(1),integer,[nodeid(pos(nan,1,1,55,1,55))]),b(couple(b(integer(1),integer,[nodeid(pos(nan,1,1,58,1,58))]),b(integer(2),integer,[nodeid(pos(nan,1,1,60,1,60))])),couple(integer,integer),[nodeid(pos(nan,1,1,57,1,61))])),couple(integer,couple(integer,integer)),[nodeid(pos(nan,1,1,54,1,62))])),pred,[nodeid(pos(nan,1,1,41,1,62))])),pred,[nodeid(pos(nan,1,1,1,1,62))])),pred,[used_ids([x,y])])).
2531		% #(y,v).(v : INTEGER & (((rec(a:y,b:1,c:1 |-> 2) /= rec(a:v,b:1,c:1 |-> 2) & y : 1 .. 2) & v = 1) & rec(a:1,b:y,c:1 |-> 2) /= rec(a:v,b:2,c:1 |-> 2)))
2532		must_fail_clpfd_det(123,b(exists([b(identifier(y),integer,[]),b(identifier(v),integer,[])],b(conjunct(b(conjunct(b(conjunct(b(not_equal(b(rec([field(a,b(identifier(y),integer,[nodeid(pos(nan,1,1,8,1,8))])),field(b,b(integer(1),integer,[nodeid(pos(nan,1,1,12,1,12))])),field(c,b(couple(b(integer(1),integer,[nodeid(pos(nan,1,1,17,1,17))]),b(integer(2),integer,[nodeid(pos(nan,1,1,19,1,19))])),couple(integer,integer),[nodeid(pos(nan,1,1,16,1,20))]))]),record([field(a,integer),field(b,integer),field(c,couple(integer,integer))]),[nodeid(pos(nan,1,1,2,1,21))]),b(rec([field(a,b(identifier(v),integer,[nodeid(pos(nan,1,1,30,1,30))])),field(b,b(integer(1),integer,[nodeid(pos(nan,1,1,34,1,34))])),field(c,b(couple(b(integer(1),integer,[nodeid(pos(nan,1,1,39,1,39))]),b(integer(2),integer,[nodeid(pos(nan,1,1,41,1,41))])),couple(integer,integer),[nodeid(pos(nan,1,1,38,1,42))]))]),record([field(a,integer),field(b,integer),field(c,couple(integer,integer))]),[nodeid(pos(nan,1,1,24,1,43))])),pred,[nodeid(pos(nan,1,1,2,1,43))]),b(member(b(identifier(y),integer,[nodeid(pos(nan,1,1,48,1,48))]),b(interval(b(integer(1),integer,[nodeid(pos(nan,1,1,50,1,50))]),b(integer(2),integer,[nodeid(pos(nan,1,1,53,1,53))])),set(integer),[nodeid(pos(nan,1,1,50,1,53))])),pred,[nodeid(pos(nan,1,1,48,1,53))])),pred,[nodeid(pos(nan,1,1,1,1,53))]),b(equal(b(identifier(v),integer,[nodeid(pos(nan,1,1,57,1,57))]),b(integer(1),integer,[nodeid(pos(nan,1,1,59,1,59))])),pred,[nodeid(pos(nan,1,1,57,1,59))])),pred,[nodeid(pos(nan,1,1,1,1,59))]),b(not_equal(b(rec([field(a,b(integer(1),integer,[nodeid(pos(nan,1,1,70,1,70))])),field(b,b(identifier(y),integer,[nodeid(pos(nan,1,1,74,1,74))])),field(c,b(couple(b(integer(1),integer,[nodeid(pos(nan,1,1,79,1,79))]),b(integer(2),integer,[nodeid(pos(nan,1,1,81,1,81))])),couple(integer,integer),[nodeid(pos(nan,1,1,78,1,82))]))]),record([field(a,integer),field(b,integer),field(c,couple(integer,integer))]),[nodeid(pos(nan,1,1,64,1,83))]),b(rec([field(a,b(identifier(v),integer,[nodeid(pos(nan,1,1,92,1,92))])),field(b,b(integer(2),integer,[nodeid(pos(nan,1,1,96,1,96))])),field(c,b(couple(b(integer(1),integer,[nodeid(pos(nan,1,1,101,1,101))]),b(integer(2),integer,[nodeid(pos(nan,1,1,103,1,103))])),couple(integer,integer),[nodeid(pos(nan,1,1,100,1,104))]))]),record([field(a,integer),field(b,integer),field(c,couple(integer,integer))]),[nodeid(pos(nan,1,1,86,1,105))])),pred,[nodeid(pos(nan,1,1,64,1,105))])),pred,[nodeid(pos(nan,1,1,1,1,106))])),pred,[used_ids([v,y])])).
2533		% #(b,y,v).((b : BOOL & v : INTEGER) & ((((b = bool(rec(a:y,b:1,c:1 |-> 2) /= rec(a:v,b:1,c:1 |-> 2)) & y : 1 .. 2) & v = 1) & rec(a:1,b:y,c:1 |-> 2) /= rec(a:v,b:2,c:1 |-> 2)) & b = TRUE))
2534		must_fail_clpfd_det(124,b(exists([b(identifier(b),boolean,[]),b(identifier(y),integer,[]),b(identifier(v),integer,[])],b(conjunct(b(conjunct(b(conjunct(b(conjunct(b(equal(b(identifier(b),boolean,[nodeid(pos(nan,1,1,1,1,1))]),b(convert_bool(b(not_equal(b(rec([field(a,b(identifier(y),integer,[nodeid(pos(nan,1,1,14,1,14))])),field(b,b(integer(1),integer,[nodeid(pos(nan,1,1,18,1,18))])),field(c,b(couple(b(integer(1),integer,[nodeid(pos(nan,1,1,23,1,23))]),b(integer(2),integer,[nodeid(pos(nan,1,1,25,1,25))])),couple(integer,integer),[nodeid(pos(nan,1,1,22,1,26))]))]),record([field(a,integer),field(b,integer),field(c,couple(integer,integer))]),[nodeid(pos(nan,1,1,8,1,27))]),b(rec([field(a,b(identifier(v),integer,[nodeid(pos(nan,1,1,36,1,36))])),field(b,b(integer(1),integer,[nodeid(pos(nan,1,1,40,1,40))])),field(c,b(couple(b(integer(1),integer,[nodeid(pos(nan,1,1,45,1,45))]),b(integer(2),integer,[nodeid(pos(nan,1,1,47,1,47))])),couple(integer,integer),[nodeid(pos(nan,1,1,44,1,48))]))]),record([field(a,integer),field(b,integer),field(c,couple(integer,integer))]),[nodeid(pos(nan,1,1,30,1,49))])),pred,[nodeid(pos(nan,1,1,8,1,49))])),boolean,[nodeid(pos(nan,1,1,3,1,50))])),pred,[nodeid(pos(nan,1,1,1,1,50))]),b(member(b(identifier(y),integer,[nodeid(pos(nan,1,1,54,1,54))]),b(interval(b(integer(1),integer,[nodeid(pos(nan,1,1,56,1,56))]),b(integer(2),integer,[nodeid(pos(nan,1,1,59,1,59))])),set(integer),[nodeid(pos(nan,1,1,56,1,59))])),pred,[nodeid(pos(nan,1,1,54,1,59))])),pred,[nodeid(pos(nan,1,1,1,1,59))]),b(equal(b(identifier(v),integer,[nodeid(pos(nan,1,1,63,1,63))]),b(integer(1),integer,[nodeid(pos(nan,1,1,65,1,65))])),pred,[nodeid(pos(nan,1,1,63,1,65))])),pred,[nodeid(pos(nan,1,1,1,1,65))]),b(not_equal(b(rec([field(a,b(integer(1),integer,[nodeid(pos(nan,1,1,76,1,76))])),field(b,b(identifier(y),integer,[nodeid(pos(nan,1,1,80,1,80))])),field(c,b(couple(b(integer(1),integer,[nodeid(pos(nan,1,1,85,1,85))]),b(integer(2),integer,[nodeid(pos(nan,1,1,87,1,87))])),couple(integer,integer),[nodeid(pos(nan,1,1,84,1,88))]))]),record([field(a,integer),field(b,integer),field(c,couple(integer,integer))]),[nodeid(pos(nan,1,1,70,1,89))]),b(rec([field(a,b(identifier(v),integer,[nodeid(pos(nan,1,1,98,1,98))])),field(b,b(integer(2),integer,[nodeid(pos(nan,1,1,102,1,102))])),field(c,b(couple(b(integer(1),integer,[nodeid(pos(nan,1,1,107,1,107))]),b(integer(2),integer,[nodeid(pos(nan,1,1,109,1,109))])),couple(integer,integer),[nodeid(pos(nan,1,1,106,1,110))]))]),record([field(a,integer),field(b,integer),field(c,couple(integer,integer))]),[nodeid(pos(nan,1,1,92,1,111))])),pred,[nodeid(pos(nan,1,1,70,1,111))])),pred,[nodeid(pos(nan,1,1,1,1,112))]),b(equal(b(identifier(b),boolean,[nodeid(pos(nan,1,1,116,1,116))]),b(boolean_true,boolean,[nodeid(pos(nan,1,1,118,1,118))])),pred,[nodeid(pos(nan,1,1,116,1,118))])),pred,[nodeid(pos(nan,1,1,1,1,118))])),pred,[used_ids([b,v,y])])).
2535		% #(a,v1,v2,w).((((a : POW(struct(x:INTEGER * INTEGER,y:INTEGER,z:BOOL)) & v1 : INTEGER) & v2 : INTEGER) & w : INTEGER) & ((a = {rec(x:1 |-> 33,y:22,z:FALSE),rec(x:2 |-> 34,y:44,z:TRUE),rec(x:3 |-> 34,y:45,z:TRUE)} & rec(x:v1 |-> v2,y:w,z:TRUE) : a) & (v1 + v2) + w < 57))
2536		must_fail_clpfd_det(125,b(exists([b(identifier(a),set(record([field(x,couple(integer,integer)),field(y,integer),field(z,boolean)])),[]),b(identifier(v1),integer,[]),b(identifier(v2),integer,[]),b(identifier(w),integer,[])],b(conjunct(b(conjunct(b(equal(b(identifier(a),set(record([field(x,couple(integer,integer)),field(y,integer),field(z,boolean)])),[nodeid(pos(nan,1,1,1,1,1))]),b(set_extension([b(rec([field(x,b(couple(b(integer(1),integer,[nodeid(pos(nan,1,1,13,1,13))]),b(integer(33),integer,[nodeid(pos(nan,1,1,15,1,15))])),couple(integer,integer),[nodeid(pos(nan,1,1,12,1,17))])),field(y,b(integer(22),integer,[nodeid(pos(nan,1,1,21,1,21))])),field(z,b(boolean_false,boolean,[nodeid(pos(nan,1,1,26,1,26))]))]),record([field(x,couple(integer,integer)),field(y,integer),field(z,boolean)]),[nodeid(pos(nan,1,1,6,1,31))]),b(rec([field(x,b(couple(b(integer(2),integer,[nodeid(pos(nan,1,1,40,1,40))]),b(integer(34),integer,[nodeid(pos(nan,1,1,42,1,42))])),couple(integer,integer),[nodeid(pos(nan,1,1,39,1,44))])),field(y,b(integer(44),integer,[nodeid(pos(nan,1,1,48,1,48))])),field(z,b(boolean_true,boolean,[nodeid(pos(nan,1,1,53,1,53))]))]),record([field(x,couple(integer,integer)),field(y,integer),field(z,boolean)]),[nodeid(pos(nan,1,1,33,1,57))]),b(rec([field(x,b(couple(b(integer(3),integer,[nodeid(pos(nan,1,1,66,1,66))]),b(integer(34),integer,[nodeid(pos(nan,1,1,68,1,68))])),couple(integer,integer),[nodeid(pos(nan,1,1,65,1,70))])),field(y,b(integer(45),integer,[nodeid(pos(nan,1,1,74,1,74))])),field(z,b(boolean_true,boolean,[nodeid(pos(nan,1,1,79,1,79))]))]),record([field(x,couple(integer,integer)),field(y,integer),field(z,boolean)]),[nodeid(pos(nan,1,1,59,1,83))])]),set(record([field(x,couple(integer,integer)),field(y,integer),field(z,boolean)])),[nodeid(pos(nan,1,1,5,1,84))])),pred,[nodeid(pos(nan,1,1,1,1,84))]),b(member(b(rec([field(x,b(couple(b(identifier(v1),integer,[nodeid(pos(nan,1,1,95,1,95))]),b(identifier(v2),integer,[nodeid(pos(nan,1,1,98,1,98))])),couple(integer,integer),[nodeid(pos(nan,1,1,94,1,100))])),field(y,b(identifier(w),integer,[nodeid(pos(nan,1,1,104,1,104))])),field(z,b(boolean_true,boolean,[nodeid(pos(nan,1,1,108,1,108))]))]),record([field(x,couple(integer,integer)),field(y,integer),field(z,boolean)]),[nodeid(pos(nan,1,1,88,1,112))]),b(identifier(a),set(record([field(x,couple(integer,integer)),field(y,integer),field(z,boolean)])),[nodeid(pos(nan,1,1,114,1,114))])),pred,[nodeid(pos(nan,1,1,88,1,114))])),pred,[nodeid(pos(nan,1,1,1,1,114))]),b(less(b(add(b(add(b(identifier(v1),integer,[nodeid(pos(nan,1,1,118,1,118))]),b(identifier(v2),integer,[nodeid(pos(nan,1,1,121,1,121))])),integer,[nodeid(pos(nan,1,1,118,1,121))]),b(identifier(w),integer,[nodeid(pos(nan,1,1,124,1,124))])),integer,[nodeid(pos(nan,1,1,118,1,124))]),b(integer(57),integer,[nodeid(pos(nan,1,1,127,1,127))])),pred,[nodeid(pos(nan,1,1,118,1,127))])),pred,[nodeid(pos(nan,1,1,1,1,127))])),pred,[used_ids([a,v1,v2,w])])).
2537		% #(x).(x : INTEGER & ((((x > 0 & x mod 50 = 0) & x mod 61 = 0) & x mod 23 = 0) & x < 70150))
2538		must_fail_clpfd_det(126,b(exists([b(identifier(x),integer,[])],b(conjunct(b(conjunct(b(conjunct(b(conjunct(b(greater(b(identifier(x),integer,[nodeid(pos(nan,1,1,1,1,1))]),b(integer(0),integer,[nodeid(pos(nan,1,1,5,1,5))])),pred,[nodeid(pos(nan,1,1,1,1,5))]),b(equal(b(modulo(b(identifier(x),integer,[nodeid(pos(nan,1,1,10,1,10))]),b(integer(50),integer,[nodeid(pos(nan,1,1,16,1,16))])),integer,[contains_wd_condition,nodeid(pos(nan,1,1,10,1,16))]),b(integer(0),integer,[nodeid(pos(nan,1,1,20,1,20))])),pred,[contains_wd_condition,nodeid(pos(nan,1,1,10,1,20))])),pred,[contains_wd_condition,nodeid(pos(nan,1,1,1,1,20))]),b(equal(b(modulo(b(identifier(x),integer,[nodeid(pos(nan,1,1,24,1,24))]),b(integer(61),integer,[nodeid(pos(nan,1,1,30,1,30))])),integer,[contains_wd_condition,nodeid(pos(nan,1,1,24,1,30))]),b(integer(0),integer,[nodeid(pos(nan,1,1,35,1,35))])),pred,[contains_wd_condition,nodeid(pos(nan,1,1,24,1,35))])),pred,[contains_wd_condition,nodeid(pos(nan,1,1,1,1,35))]),b(equal(b(modulo(b(identifier(x),integer,[nodeid(pos(nan,1,1,39,1,39))]),b(integer(23),integer,[nodeid(pos(nan,1,1,45,1,45))])),integer,[contains_wd_condition,nodeid(pos(nan,1,1,39,1,45))]),b(integer(0),integer,[nodeid(pos(nan,1,1,50,1,50))])),pred,[contains_wd_condition,nodeid(pos(nan,1,1,39,1,50))])),pred,[contains_wd_condition,nodeid(pos(nan,1,1,1,1,50))]),b(less(b(identifier(x),integer,[nodeid(pos(nan,1,1,54,1,54))]),b(integer(70150),integer,[nodeid(pos(nan,1,1,56,1,56))])),pred,[nodeid(pos(nan,1,1,54,1,56))])),pred,[contains_wd_condition,nodeid(pos(nan,1,1,1,1,56))])),pred,[used_ids([x])])).
2539		% #(x,B,C).(((x : INTEGER & B : INTEGER) & C : BOOL) & (((((({x} : POW({101,102})) <=> B < 20 & x > 103) & B > 0) & B < 100) & (B = 19) <=> (C = TRUE)) & (C = FALSE => B < 20)))
2540		must_fail_clpfd_det(127,b(exists([b(identifier(x),integer,[]),b(identifier('B'),integer,[]),b(identifier('C'),boolean,[])],b(conjunct(b(conjunct(b(conjunct(b(conjunct(b(conjunct(b(equivalence(b(member(b(set_extension([b(identifier(x),integer,[nodeid(pos(nan,1,1,3,1,3))])]),set(integer),[nodeid(pos(nan,1,1,2,1,4))]),b(pow_subset(b(value(avl_set(node(int(101),true,1,empty,node(int(102),true,0,empty,empty)))),set(integer),[nodeid(pos(nan,1,1,10,1,18))])),set(set(integer)),[nodeid(pos(nan,1,1,6,1,19))])),pred,[nodeid(pos(nan,1,1,2,1,19))]),b(less(b(identifier('B'),integer,[nodeid(pos(nan,1,1,25,1,25))]),b(integer(20),integer,[nodeid(pos(nan,1,1,27,1,27))])),pred,[nodeid(pos(nan,1,1,25,1,27))])),pred,[nodeid(pos(nan,1,1,2,1,27))]),b(greater(b(identifier(x),integer,[nodeid(pos(nan,1,1,33,1,33))]),b(integer(103),integer,[nodeid(pos(nan,1,1,35,1,35))])),pred,[nodeid(pos(nan,1,1,33,1,35))])),pred,[nodeid(pos(nan,1,1,1,1,35))]),b(greater(b(identifier('B'),integer,[nodeid(pos(nan,1,1,40,1,40))]),b(integer(0),integer,[nodeid(pos(nan,1,1,42,1,42))])),pred,[nodeid(pos(nan,1,1,40,1,42))])),pred,[nodeid(pos(nan,1,1,1,1,42))]),b(less(b(identifier('B'),integer,[nodeid(pos(nan,1,1,46,1,46))]),b(integer(100),integer,[nodeid(pos(nan,1,1,48,1,48))])),pred,[nodeid(pos(nan,1,1,46,1,48))])),pred,[nodeid(pos(nan,1,1,1,1,48))]),b(equivalence(b(equal(b(identifier('B'),integer,[nodeid(pos(nan,1,1,55,1,55))]),b(integer(19),integer,[nodeid(pos(nan,1,1,57,1,57))])),pred,[nodeid(pos(nan,1,1,55,1,57))]),b(equal(b(identifier('C'),boolean,[nodeid(pos(nan,1,1,64,1,64))]),b(boolean_true,boolean,[nodeid(pos(nan,1,1,66,1,66))])),pred,[nodeid(pos(nan,1,1,64,1,66))])),pred,[nodeid(pos(nan,1,1,55,1,66))])),pred,[nodeid(pos(nan,1,1,1,1,70))]),b(implication(b(equal(b(identifier('C'),boolean,[nodeid(pos(nan,1,1,75,1,75))]),b(boolean_false,boolean,[nodeid(pos(nan,1,1,77,1,77))])),pred,[nodeid(pos(nan,1,1,75,1,77))]),b(less(b(identifier('B'),integer,[nodeid(pos(nan,1,1,86,1,86))]),b(integer(20),integer,[nodeid(pos(nan,1,1,88,1,88))])),pred,[nodeid(pos(nan,1,1,86,1,88))])),pred,[nodeid(pos(nan,1,1,75,1,88))])),pred,[nodeid(pos(nan,1,1,1,1,90))])),pred,[used_ids(['B','C',x])])).
2541
2542		% Eval Time: 10 ms (0 ms walltime)
2543		% #(r,x,y,z).(((r : POW((INTEGER * INTEGER) * INTEGER) & x : INTEGER) & z : INTEGER) & (((r = {((1|->2)|->3),((3|->4)|->5),((6|->7)|->8),((9|->10)|->11),((12|->13)|->14)} & (x |-> y) |-> z : r) & y : 10 .. 13) & z < 11))
2544		must_fail_clpfd_det(128,b(let_predicate([b(identifier(r),set(couple(couple(integer,integer),integer)),[do_not_optimize_away,nodeid(pos(3,-1,1,3,1,3)),introduced_by(exists)])],[b(value(avl_set(node(((int(6),int(7)),int(8)),true,0,node(((int(1),int(2)),int(3)),true,1,empty,node(((int(3),int(4)),int(5)),true,0,empty,empty)),node(((int(9),int(10)),int(11)),true,1,empty,node(((int(12),int(13)),int(14)),true,0,empty,empty))))),set(couple(couple(integer,integer),integer)),[nodeid(pos(29,-1,1,93,1,168))])],b(exists([b(identifier(x),integer,[do_not_optimize_away,nodeid(pos(4,-1,1,5,1,5)),introduced_by(exists)]),b(identifier(y),integer,[do_not_optimize_away,nodeid(pos(5,-1,1,7,1,7)),introduced_by(exists)]),b(identifier(z),integer,[do_not_optimize_away,nodeid(pos(6,-1,1,9,1,9)),introduced_by(exists)])],b(conjunct(b(conjunct(b(member(b(couple(b(couple(b(identifier(x),integer,[nodeid(pos(58,-1,1,173,1,173)),introduced_by(exists)]),b(identifier(y),integer,[nodeid(pos(59,-1,1,179,1,179)),introduced_by(exists)])),couple(integer,integer),[nodeid(pos(57,-1,1,173,1,179))]),b(identifier(z),integer,[nodeid(pos(60,-1,1,186,1,186)),introduced_by(exists)])),couple(couple(integer,integer),integer),[nodeid(pos(56,-1,1,173,1,186))]),b(identifier(r),set(couple(couple(integer,integer),integer)),[nodeid(pos(61,-1,1,190,1,190)),introduced_by(exists)])),pred,[nodeid(pos(55,-1,1,173,1,190))]),b(member(b(identifier(y),integer,[nodeid(pos(63,-1,1,195,1,195)),introduced_by(exists)]),b(interval(b(integer(10),integer,[nodeid(pos(65,-1,1,199,1,200))]),b(integer(13),integer,[nodeid(pos(66,-1,1,205,1,206))])),set(integer),[nodeid(pos(64,-1,1,199,1,206))])),pred,[nodeid(pos(62,-1,1,195,1,206))])),pred,[]),b(less(b(identifier(z),integer,[nodeid(pos(68,-1,1,211,1,211)),introduced_by(exists)]),b(integer(11),integer,[nodeid(pos(69,-1,1,215,1,216))])),pred,[nodeid(pos(67,-1,1,211,1,216))])),pred,[])),pred,[used_ids([r])])),pred,[nodeid(pos(2,-1,1,1,1,218))])).
2545
2546		% Eval Time: 0 ms (0 ms walltime)
2547		% #(f,a,b,c,x,r).(((((a : INTEGER & b : INTEGER) & c : INTEGER) & x : INTEGER) & r : INTEGER) & ((((((((f : 11 .. 23 +-> 1 .. 10 & f = {a |-> 2,b |-> 3,c |-> 4}) & card({a,b,c}) = 3) & f(x) = r) & a > b) & b > c) & x /= a) & /* falsity */ x /= x) & r /= b))
2548		must_fail_clpfd_det(129,b(exists([b(identifier(f),set(couple(integer,integer)),[]),b(identifier(a),integer,[]),b(identifier(b),integer,[]),b(identifier(c),integer,[]),b(identifier(x),integer,[]),b(identifier(r),integer,[])],b(conjunct(b(conjunct(b(conjunct(b(conjunct(b(conjunct(b(conjunct(b(conjunct(b(conjunct(b(member(b(identifier(f),set(couple(integer,integer)),[nodeid(pos(11,-1,1,1,1,1))]),b(partial_function(b(interval(b(integer(11),integer,[nodeid(pos(14,-1,1,5,1,6))]),b(integer(23),integer,[nodeid(pos(15,-1,1,9,1,10))])),set(integer),[nodeid(pos(13,-1,1,5,1,10))]),b(interval(b(integer(1),integer,[nodeid(pos(17,-1,1,16,1,16))]),b(integer(10),integer,[nodeid(pos(18,-1,1,19,1,20))])),set(integer),[nodeid(pos(16,-1,1,16,1,20))])),set(set(couple(integer,integer))),[nodeid(pos(12,-1,1,5,1,20))])),pred,[nodeid(pos(10,-1,1,1,1,20))]),b(equal(b(identifier(f),set(couple(integer,integer)),[nodeid(pos(20,-1,1,24,1,24))]),b(set_extension([b(couple(b(identifier(a),integer,[nodeid(pos(23,-1,1,29,1,29))]),b(integer(2),integer,[nodeid(pos(24,-1,1,33,1,33))])),couple(integer,integer),[nodeid(pos(22,-1,1,29,1,33))]),b(couple(b(identifier(b),integer,[nodeid(pos(26,-1,1,36,1,36))]),b(integer(3),integer,[nodeid(pos(27,-1,1,40,1,40))])),couple(integer,integer),[nodeid(pos(25,-1,1,36,1,40))]),b(couple(b(identifier(c),integer,[nodeid(pos(29,-1,1,43,1,43))]),b(integer(4),integer,[nodeid(pos(30,-1,1,47,1,47))])),couple(integer,integer),[nodeid(pos(28,-1,1,43,1,47))])]),set(couple(integer,integer)),[nodeid(pos(21,-1,1,28,1,48))])),pred,[nodeid(pos(19,-1,1,24,1,48))])),pred,[nodeid(pos(9,-1,1,1,1,48))]),b(equal(b(card(b(set_extension([b(identifier(a),integer,[nodeid(pos(34,-1,1,58,1,58))]),b(identifier(b),integer,[nodeid(pos(35,-1,1,60,1,60))]),b(identifier(c),integer,[nodeid(pos(36,-1,1,62,1,62))])]),set(integer),[nodeid(pos(33,-1,1,57,1,63))])),integer,[nodeid(pos(32,-1,1,52,1,64))]),b(integer(3),integer,[nodeid(pos(37,-1,1,66,1,66))])),pred,[nodeid(pos(31,-1,1,52,1,66))])),pred,[nodeid(pos(8,-1,1,1,1,66))]),b(equal(b(function(b(identifier(f),set(couple(integer,integer)),[nodeid(pos(40,-1,1,70,1,70))]),b(identifier(x),integer,[nodeid(pos(41,-1,1,72,1,72))])),integer,[contains_wd_condition,nodeid(pos(39,-1,1,70,1,73))]),b(identifier(r),integer,[nodeid(pos(42,-1,1,75,1,75))])),pred,[contains_wd_condition,nodeid(pos(38,-1,1,70,1,75))])),pred,[contains_wd_condition,nodeid(pos(7,-1,1,1,1,75))]),b(greater(b(identifier(a),integer,[nodeid(pos(44,-1,1,79,1,79))]),b(identifier(b),integer,[nodeid(pos(45,-1,1,81,1,81))])),pred,[nodeid(pos(43,-1,1,79,1,81))])),pred,[contains_wd_condition,nodeid(pos(6,-1,1,1,1,81))]),b(greater(b(identifier(b),integer,[nodeid(pos(47,-1,1,85,1,85))]),b(identifier(c),integer,[nodeid(pos(48,-1,1,87,1,87))])),pred,[nodeid(pos(46,-1,1,85,1,87))])),pred,[contains_wd_condition,nodeid(pos(5,-1,1,1,1,87))]),b(not_equal(b(identifier(x),integer,[nodeid(pos(50,-1,1,91,1,91))]),b(identifier(a),integer,[nodeid(pos(51,-1,1,94,1,94))])),pred,[nodeid(pos(49,-1,1,91,1,94))])),pred,[contains_wd_condition,nodeid(pos(4,-1,1,1,1,94))]),b(falsity,pred,[was(not_equal(b(identifier(x),integer,[nodeid(pos(53,-1,1,98,1,98))]),b(identifier(x),integer,[nodeid(pos(54,-1,1,101,1,101))]))),nodeid(pos(52,-1,1,98,1,101))])),pred,[contains_wd_condition,nodeid(pos(3,-1,1,1,1,101))]),b(not_equal(b(identifier(r),integer,[nodeid(pos(56,-1,1,105,1,105))]),b(identifier(b),integer,[nodeid(pos(57,-1,1,108,1,108))])),pred,[nodeid(pos(55,-1,1,105,1,108))])),pred,[contains_wd_condition,nodeid(pos(2,-1,1,1,1,108))])),pred,[used_ids([]),contains_wd_condition])).
2549
2550		% Eval Time: 10 ms (0 ms walltime)
2551		% #(f,aa,x,y,r,v).((f : POW(INTEGER * (INTEGER * INTEGER)) & r : INTEGER * INTEGER) & ((((((f = {aa |-> (1 |-> aa),x |-> (2 |-> x + 1),y |-> (3 |-> y + 1)} & x : 1 .. 2) & aa : 0 .. 1) & y : 3 .. 5) & r = f(v)) & v : 2 .. 4) & prj1(INTEGER,INTEGER)(r) /: 2 .. 3))
2552		% REQUIRES TRY_FIND_ABORT=FALSE
2553		must_fail_clpfd_det(130,b(exists([b(identifier(f),set(couple(integer,couple(integer,integer))),[]),b(identifier(aa),integer,[]),b(identifier(x),integer,[]),b(identifier(y),integer,[]),b(identifier(r),couple(integer,integer),[]),b(identifier(v),integer,[])],b(conjunct(b(conjunct(b(conjunct(b(conjunct(b(conjunct(b(conjunct(b(equal(b(identifier(f),set(couple(integer,couple(integer,integer))),[nodeid(pos(9,-1,1,1,1,1))]),b(set_extension([b(couple(b(identifier(aa),integer,[nodeid(pos(12,-1,1,6,1,7))]),b(couple(b(integer(1),integer,[nodeid(pos(14,-1,1,12,1,12))]),b(identifier(aa),integer,[nodeid(pos(15,-1,1,14,1,15))])),couple(integer,integer),[nodeid(pos(13,-1,1,11,1,16))])),couple(integer,couple(integer,integer)),[nodeid(pos(11,-1,1,6,1,16))]),b(couple(b(identifier(x),integer,[nodeid(pos(17,-1,1,19,1,19))]),b(couple(b(integer(2),integer,[nodeid(pos(19,-1,1,24,1,24))]),b(add(b(identifier(x),integer,[nodeid(pos(21,-1,1,26,1,26))]),b(integer(1),integer,[nodeid(pos(22,-1,1,28,1,28))])),integer,[nodeid(pos(20,-1,1,26,1,28))])),couple(integer,integer),[nodeid(pos(18,-1,1,23,1,29))])),couple(integer,couple(integer,integer)),[nodeid(pos(16,-1,1,19,1,29))]),b(couple(b(identifier(y),integer,[nodeid(pos(24,-1,1,32,1,32))]),b(couple(b(integer(3),integer,[nodeid(pos(26,-1,1,37,1,37))]),b(add(b(identifier(y),integer,[nodeid(pos(28,-1,1,39,1,39))]),b(integer(1),integer,[nodeid(pos(29,-1,1,41,1,41))])),integer,[nodeid(pos(27,-1,1,39,1,41))])),couple(integer,integer),[nodeid(pos(25,-1,1,36,1,42))])),couple(integer,couple(integer,integer)),[nodeid(pos(23,-1,1,32,1,42))])]),set(couple(integer,couple(integer,integer))),[nodeid(pos(10,-1,1,5,1,43))])),pred,[nodeid(pos(8,-1,1,1,1,43))]),b(member(b(identifier(x),integer,[nodeid(pos(31,-1,1,47,1,47))]),b(interval(b(integer(1),integer,[nodeid(pos(33,-1,1,49,1,49))]),b(integer(2),integer,[nodeid(pos(34,-1,1,52,1,52))])),set(integer),[nodeid(pos(32,-1,1,49,1,52))])),pred,[nodeid(pos(30,-1,1,47,1,52))])),pred,[nodeid(pos(7,-1,1,1,1,52))]),b(member(b(identifier(aa),integer,[nodeid(pos(36,-1,1,56,1,57))]),b(interval(b(integer(0),integer,[nodeid(pos(38,-1,1,59,1,59))]),b(integer(1),integer,[nodeid(pos(39,-1,1,62,1,62))])),set(integer),[nodeid(pos(37,-1,1,59,1,62))])),pred,[nodeid(pos(35,-1,1,56,1,62))])),pred,[nodeid(pos(6,-1,1,1,1,62))]),b(member(b(identifier(y),integer,[nodeid(pos(41,-1,1,66,1,66))]),b(interval(b(integer(3),integer,[nodeid(pos(43,-1,1,68,1,68))]),b(integer(5),integer,[nodeid(pos(44,-1,1,71,1,71))])),set(integer),[nodeid(pos(42,-1,1,68,1,71))])),pred,[nodeid(pos(40,-1,1,66,1,71))])),pred,[nodeid(pos(5,-1,1,1,1,71))]),b(equal(b(identifier(r),couple(integer,integer),[nodeid(pos(46,-1,1,75,1,75))]),b(function(b(identifier(f),set(couple(integer,couple(integer,integer))),[nodeid(pos(48,-1,1,79,1,79))]),b(identifier(v),integer,[nodeid(pos(49,-1,1,81,1,81))])),couple(integer,integer),[contains_wd_condition,nodeid(pos(47,-1,1,79,1,82))])),pred,[contains_wd_condition,nodeid(pos(45,-1,1,75,1,82))])),pred,[contains_wd_condition,nodeid(pos(4,-1,1,1,1,82))]),b(member(b(identifier(v),integer,[nodeid(pos(51,-1,1,86,1,86))]),b(interval(b(integer(2),integer,[nodeid(pos(53,-1,1,88,1,88))]),b(integer(4),integer,[nodeid(pos(54,-1,1,91,1,91))])),set(integer),[nodeid(pos(52,-1,1,88,1,91))])),pred,[nodeid(pos(50,-1,1,86,1,91))])),pred,[contains_wd_condition,nodeid(pos(3,-1,1,1,1,91))]),b(not_member(b(first_of_pair(b(identifier(r),couple(integer,integer),[nodeid(pos(60,-1,1,117,1,117))])),integer,[nodeid(pos(56,-1,1,95,1,118))]),b(interval(b(integer(2),integer,[nodeid(pos(62,-1,1,123,1,123))]),b(integer(3),integer,[nodeid(pos(63,-1,1,126,1,126))])),set(integer),[nodeid(pos(61,-1,1,123,1,126))])),pred,[nodeid(pos(55,-1,1,95,1,126))])),pred,[contains_wd_condition,nodeid(pos(2,-1,1,1,1,126))])),pred,[used_ids([]),contains_wd_condition])).
2554
2555		% Eval Time: 0 ms (0 ms walltime)
2556		% #(f,aa,x,y,r,v).((f : POW(INTEGER * struct(p1:INTEGER,p2:INTEGER)) & r : struct(p1:INTEGER,p2:INTEGER)) & ((((((f = {aa |-> rec(p1:1,p2:aa),x |-> rec(p1:2,p2:x + 1),y |-> rec(p1:3,p2:y + 1)} & x : 1 .. 2) & aa : 0 .. 1) & y : 3 .. 5) & r = f(v)) & v : 2 .. 4) & r'p1 /: 2 .. 3))
2557		% REQUIRES TRY_FIND_ABORT=FALSE
2558		must_fail_clpfd_det(131,b(exists([b(identifier(f),set(couple(integer,record([field(p1,integer),field(p2,integer)]))),[]),b(identifier(aa),integer,[]),b(identifier(x),integer,[]),b(identifier(y),integer,[]),b(identifier(r),record([field(p1,integer),field(p2,integer)]),[]),b(identifier(v),integer,[])],b(conjunct(b(conjunct(b(conjunct(b(conjunct(b(conjunct(b(conjunct(b(equal(b(identifier(f),set(couple(integer,record([field(p1,integer),field(p2,integer)]))),[nodeid(pos(9,-1,1,1,1,1))]),b(set_extension([b(couple(b(identifier(aa),integer,[nodeid(pos(12,-1,1,6,1,7))]),b(rec([field(p1,b(integer(1),integer,[nodeid(pos(16,-1,1,18,1,18))])),field(p2,b(identifier(aa),integer,[nodeid(pos(19,-1,1,23,1,24))]))]),record([field(p1,integer),field(p2,integer)]),[nodeid(pos(13,-1,1,11,1,25))])),couple(integer,record([field(p1,integer),field(p2,integer)])),[nodeid(pos(11,-1,1,6,1,25))]),b(couple(b(identifier(x),integer,[nodeid(pos(21,-1,1,28,1,28))]),b(rec([field(p1,b(integer(2),integer,[nodeid(pos(25,-1,1,39,1,39))])),field(p2,b(add(b(identifier(x),integer,[nodeid(pos(29,-1,1,44,1,44))]),b(integer(1),integer,[nodeid(pos(30,-1,1,46,1,46))])),integer,[nodeid(pos(28,-1,1,44,1,46))]))]),record([field(p1,integer),field(p2,integer)]),[nodeid(pos(22,-1,1,32,1,47))])),couple(integer,record([field(p1,integer),field(p2,integer)])),[nodeid(pos(20,-1,1,28,1,47))]),b(couple(b(identifier(y),integer,[nodeid(pos(32,-1,1,50,1,50))]),b(rec([field(p1,b(integer(3),integer,[nodeid(pos(36,-1,1,61,1,61))])),field(p2,b(add(b(identifier(y),integer,[nodeid(pos(40,-1,1,66,1,66))]),b(integer(1),integer,[nodeid(pos(41,-1,1,68,1,68))])),integer,[nodeid(pos(39,-1,1,66,1,68))]))]),record([field(p1,integer),field(p2,integer)]),[nodeid(pos(33,-1,1,54,1,69))])),couple(integer,record([field(p1,integer),field(p2,integer)])),[nodeid(pos(31,-1,1,50,1,69))])]),set(couple(integer,record([field(p1,integer),field(p2,integer)]))),[nodeid(pos(10,-1,1,5,1,70))])),pred,[nodeid(pos(8,-1,1,1,1,70))]),b(member(b(identifier(x),integer,[nodeid(pos(43,-1,1,74,1,74))]),b(interval(b(integer(1),integer,[nodeid(pos(45,-1,1,76,1,76))]),b(integer(2),integer,[nodeid(pos(46,-1,1,79,1,79))])),set(integer),[nodeid(pos(44,-1,1,76,1,79))])),pred,[nodeid(pos(42,-1,1,74,1,79))])),pred,[nodeid(pos(7,-1,1,1,1,79))]),b(member(b(identifier(aa),integer,[nodeid(pos(48,-1,1,83,1,84))]),b(interval(b(integer(0),integer,[nodeid(pos(50,-1,1,86,1,86))]),b(integer(1),integer,[nodeid(pos(51,-1,1,89,1,89))])),set(integer),[nodeid(pos(49,-1,1,86,1,89))])),pred,[nodeid(pos(47,-1,1,83,1,89))])),pred,[nodeid(pos(6,-1,1,1,1,89))]),b(member(b(identifier(y),integer,[nodeid(pos(53,-1,1,93,1,93))]),b(interval(b(integer(3),integer,[nodeid(pos(55,-1,1,95,1,95))]),b(integer(5),integer,[nodeid(pos(56,-1,1,98,1,98))])),set(integer),[nodeid(pos(54,-1,1,95,1,98))])),pred,[nodeid(pos(52,-1,1,93,1,98))])),pred,[nodeid(pos(5,-1,1,1,1,98))]),b(equal(b(identifier(r),record([field(p1,integer),field(p2,integer)]),[nodeid(pos(58,-1,1,102,1,102))]),b(function(b(identifier(f),set(couple(integer,record([field(p1,integer),field(p2,integer)]))),[nodeid(pos(60,-1,1,106,1,106))]),b(identifier(v),integer,[nodeid(pos(61,-1,1,108,1,108))])),record([field(p1,integer),field(p2,integer)]),[contains_wd_condition,nodeid(pos(59,-1,1,106,1,109))])),pred,[contains_wd_condition,nodeid(pos(57,-1,1,102,1,109))])),pred,[contains_wd_condition,nodeid(pos(4,-1,1,1,1,109))]),b(member(b(identifier(v),integer,[nodeid(pos(63,-1,1,113,1,113))]),b(interval(b(integer(2),integer,[nodeid(pos(65,-1,1,115,1,115))]),b(integer(4),integer,[nodeid(pos(66,-1,1,118,1,118))])),set(integer),[nodeid(pos(64,-1,1,115,1,118))])),pred,[nodeid(pos(62,-1,1,113,1,118))])),pred,[contains_wd_condition,nodeid(pos(3,-1,1,1,1,118))]),b(not_member(b(record_field(b(identifier(r),record([field(p1,integer),field(p2,integer)]),[nodeid(pos(69,-1,1,122,1,122))]),p1),integer,[nodeid(pos(68,-1,1,122,1,125))]),b(interval(b(integer(2),integer,[nodeid(pos(72,-1,1,130,1,130))]),b(integer(3),integer,[nodeid(pos(73,-1,1,133,1,133))])),set(integer),[nodeid(pos(71,-1,1,130,1,133))])),pred,[nodeid(pos(67,-1,1,122,1,133))])),pred,[contains_wd_condition,nodeid(pos(2,-1,1,1,1,133))])),pred,[used_ids([]),contains_wd_condition])).
2559
2560		% Eval Time: 0 ms (0 ms walltime)
2561		% #(x,a).((x = (IF a < 10 THEN 0 ELSE 5 END ) & x : 6 .. 10) & a : 1 .. 23)
2562		must_fail_clpfd_det(132,b(exists([b(identifier(x),integer,[]),b(identifier(a),integer,[])],b(conjunct(b(conjunct(b(equal(b(identifier(x),integer,[nodeid(pos(5,-1,1,1,1,1))]),b(if_then_else(b(less(b(identifier(a),integer,[nodeid(pos(8,-1,1,8,1,8))]),b(integer(10),integer,[nodeid(pos(9,-1,1,10,1,11))])),pred,[nodeid(pos(7,-1,1,8,1,11))]),b(integer(0),integer,[nodeid(pos(10,-1,1,18,1,18))]),b(integer(5),integer,[nodeid(pos(11,-1,1,25,1,25))])),integer,[nodeid(pos(6,-1,1,5,1,29))])),pred,[nodeid(pos(4,-1,1,1,1,29))]),b(member(b(identifier(x),integer,[nodeid(pos(13,-1,1,33,1,33))]),b(interval(b(integer(6),integer,[nodeid(pos(15,-1,1,35,1,35))]),b(integer(10),integer,[nodeid(pos(16,-1,1,38,1,39))])),set(integer),[nodeid(pos(14,-1,1,35,1,39))])),pred,[nodeid(pos(12,-1,1,33,1,39))])),pred,[nodeid(pos(3,-1,1,1,1,39))]),b(member(b(identifier(a),integer,[nodeid(pos(18,-1,1,43,1,43))]),b(interval(b(integer(1),integer,[nodeid(pos(20,-1,1,45,1,45))]),b(integer(23),integer,[nodeid(pos(21,-1,1,48,1,49))])),set(integer),[nodeid(pos(19,-1,1,45,1,49))])),pred,[nodeid(pos(17,-1,1,43,1,49))])),pred,[nodeid(pos(2,-1,1,1,1,49))])),pred,[used_ids([])])).
2563
2564		% Eval Time: 0 ms (0 ms walltime)
2565		% #(x,bb).((x : INTEGER & bb : BOOL) & (((IF x < 10 THEN TRUE ELSE bb END ) = FALSE & x < 20) & (IF x < 12 THEN FALSE ELSE bb END ) = TRUE))
2566		must_fail_clpfd_det(133,b(exists([b(identifier(x),integer,[]),b(identifier(bb),boolean,[])],b(conjunct(b(conjunct(b(equal(b(if_then_else(b(less(b(identifier(x),integer,[nodeid(pos(7,-1,1,4,1,4))]),b(integer(10),integer,[nodeid(pos(8,-1,1,6,1,7))])),pred,[nodeid(pos(6,-1,1,4,1,7))]),b(boolean_true,boolean,[nodeid(pos(9,-1,1,14,1,17))]),b(identifier(bb),boolean,[nodeid(pos(10,-1,1,24,1,25))])),boolean,[nodeid(pos(5,-1,1,1,1,29))]),b(boolean_false,boolean,[nodeid(pos(11,-1,1,33,1,37))])),pred,[nodeid(pos(4,-1,1,1,1,37))]),b(less(b(identifier(x),integer,[nodeid(pos(13,-1,1,41,1,41))]),b(integer(20),integer,[nodeid(pos(14,-1,1,43,1,44))])),pred,[nodeid(pos(12,-1,1,41,1,44))])),pred,[nodeid(pos(3,-1,1,1,1,44))]),b(equal(b(if_then_else(b(less(b(identifier(x),integer,[nodeid(pos(18,-1,1,51,1,51))]),b(integer(12),integer,[nodeid(pos(19,-1,1,53,1,54))])),pred,[nodeid(pos(17,-1,1,51,1,54))]),b(boolean_false,boolean,[nodeid(pos(20,-1,1,61,1,65))]),b(identifier(bb),boolean,[nodeid(pos(21,-1,1,72,1,73))])),boolean,[nodeid(pos(16,-1,1,48,1,77))]),b(boolean_true,boolean,[nodeid(pos(22,-1,1,81,1,84))])),pred,[nodeid(pos(15,-1,1,48,1,84))])),pred,[nodeid(pos(2,-1,1,1,1,84))])),pred,[used_ids([])])).
2567
2568		:- endif.
2569
2570		test_enabled(130) :- get_preference(find_abort_values,false).
2571		test_enabled(131) :- get_preference(find_abort_values,false).