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(b_interpreter_check,[imply_test_boolean_expression/7,
6		equiv_test_boolean_expression/7,
7		equiv_bidrectional_test_boolean_expression/7,
8		get_priority_of_boolean_expression/2, get_priority_of_boolean_expression2/2,
9		b_check_boolean_expression/5,b_check_boolean_expression/7,
10		b_force_check_boolean_expression/5,
11
12		/* some lower-level propagation predicates */
13		imply/3, imply_true/2,
14		b_check_forall_wf/8, b_check_exists_wf/7,
15
16		reify_closure_with_small_cardinality/5,
17
18		register_predicate/6,
19		norm_pred_check/2, norm_expr_check/2, norm_check/2,
20
21		conjoin/6, disjoin/6,
22		check_less_than_equal/3
23		]).
24
25		/* A version for checking the truth value of boolean-expressions,
26		the result is instantiated with pred_true/pred_false as soon as the result is known */
27		/* Warning: does not cover all expressions */
28		/* It provides SMT-like performance, for predicates involving arithmetic comparisons (<,...),
29		equality, disequality and membership/not_membership
30		It is not restricted to CNF
31		*/
32
33		:- meta_predicate wd_delay(0,-,-,-).
34		:- meta_predicate wd_delay_block(0,-,-,-,-,-).
35		:- meta_predicate wd_delay_until_needed(-,0).
36		:- meta_predicate wd_delay_until_needed_block(-,-,0).
37
38		:- use_module(debug).
39		:- use_module(self_check).
40		:- use_module(error_manager).
41		:- use_module(b_interpreter,[b_compute_expression/5, b_not_test_boolean_expression/6, b_test_boolean_expression/6, b_test_boolean_expression/4]).
42		:- use_module(kernel_waitflags).
43		:- use_module(performance_messages).
44		:- use_module(translate,[print_bexpr/1, convert_and_ajoin_ids/2]).
45
46
47		:- use_module(kernel_objects,[less_than_direct/2, less_than_equal_direct/2]).
48
49		:- use_module(kernel_equality).
50
51		:- use_module(tools).
52
53		:- use_module(module_information,[module_info/2]).
54		:- module_info(group,interpreter).
55		:- module_info(description,'This module provides a reified interpreter for certain predicates.').
56
57
58
59
60		:- block imply_test_boolean_expression(-, ?,?,?,?,?,?). % TO DO: pass at least Ai to it
61		imply_test_boolean_expression(PredRes1,PredRes2, RHS,LocalState,State,WF,Ai) :-
62		(PredRes1=PredRes2
63	?	-> b_test_boolean_expression(RHS,LocalState,State,WF,Ai,_)
64		; true
65		).
66
67		:- block equiv_test_boolean_expression(-, ?,?,?,?,?,?).
68		equiv_test_boolean_expression(PredRes,PredRes, RHS,LocalState,State,WF,Ai) :- !,
69	?	b_test_boolean_expression(RHS,LocalState,State,WF,Ai,_).
70		equiv_test_boolean_expression(_PredRes,_, RHS,LocalState,State,WF,Ai) :-
71	?	b_not_test_boolean_expression(RHS,LocalState,State,WF,Ai,_).
72
73		equiv_bidrectional_test_boolean_expression(PredResLHS,PredResRHS, _LHS,_RHS,_LocalState,_State,WF) :-
74		PredResLHS=PredResRHS,
75	?	(var(PredResLHS)
76		-> % create a choice point to enumerate two possible solutions
77		% important, e.g., for not((y > 0 & y * y > 20) <=> (y * y > 25 & y > 0))
78		get_last_wait_flag(equivalence,WF,LWF),
79		enum_bool(PredResLHS,LWF)
80		; true).
81		:- block enum_bool(-,-).
82		enum_bool(pred_true,_).
83		enum_bool(pred_false,_).
84		/*
85		:- block equiv_bidrectional_test_boolean_expression(-,-, ?,?,?,?,?).
86		equiv_bidrectional_test_boolean_expression(PredResLHS,PredResRHS, LHS,RHS,LocalState,State,WF) :-
87		( PredResLHS == pred_true -> b_test_boolean_expression(RHS,LocalState,State,WF)
88		; PredResLHS == pred_false -> b_not_test_boolean_expression(RHS,LocalState,State,WF)
89		; PredResRHS == pred_true -> b_test_boolean_expression(LHS,LocalState,State,WF)
90		; PredResRHS == pred_false -> b_not_test_boolean_expression(LHS,LocalState,State,WF)
91		; add_error_fail(equiv,'Illegal values: ',equiv_bidrectional_test_boolean_expression(PredResLHS,PredResRHS))
92		).
93		*/
94
95		% return starting priority for binary choice points; should be power of 2
96		get_priority_of_boolean_expression(priority(P),Prio) :- !,
97		% case generated for disjoin by contains_fd_element, and not_in_difference_set_wf,not_in_intersection_set_wf,in_union_set_wf
98		Prio=P.
99		get_priority_of_boolean_expression(b(Expr,_,_Infos),Prio) :- !,
100		% try to estimate a priority for performing a case split upon a predicate
101		% i.e., forcing a predicate Expr to be true/false
102		get_priority_of_boolean_expression2(Expr,Prio).
103		get_priority_of_boolean_expression(E,Prio) :-
104		add_internal_error('Boolean expression not properly wrapped: ',get_priority_of_boolean_expression(E,Prio)),
105		get_priority_of_boolean_expression2(E,Prio).
106
107		:- use_module(bsyntaxtree).
108		get_priority_of_boolean_expression2(truth,1) :- !. %, nl,nl,print('TRUTH in disjunct/conjunct'),nl.
109		get_priority_of_boolean_expression2(falsity,1) :- !. %, nl,nl,print('FALSITY in disjunct/conjunct'),nl.
110		get_priority_of_boolean_expression2(_,R) :-
111		preferences:preference(data_validation_mode,true), % in data validation mode we want to drive enumeration from data values only
112		!, R=4096.
113		get_priority_of_boolean_expression2(_,R) :- !, R=4. % force SMT style case-splitting; was 3 before using get_binary_choice_wait_flag_exp_backoff; raising this to 4 makes test 1358, 49 behave better (baload_R07 recognised possible)
114
115
116
117
118		count_number_of_conjuncts(b(Expr,_,_Infos),Prio) :- !,
119		count_number_of_conjuncts2(Expr,Prio).
120		count_number_of_conjuncts(priority(_),Prio) :- !, Prio=1.
121		count_number_of_conjuncts(B,Prio) :-
122		add_internal_error('Expression not wrapped: ',count_number_of_conjuncts(B,Prio)),Prio=1.
123		count_number_of_conjuncts2(conjunct(A,B),Nr) :- !, count_number_of_conjuncts(A,NA),
124		count_number_of_conjuncts(B,NB), Nr is NA+NB.
125		count_number_of_conjuncts2(norm_conjunct(_,RHS),Res) :- length(RHS,Len),!,
126		Res is Len+1.
127		count_number_of_conjuncts2(negation(A),Nr) :- !, count_number_of_disjuncts(A,Nr).
128		count_number_of_conjuncts2(_,1).
129
130		:- public count_number_of_disjuncts/2. %currently commented out above
131		count_number_of_disjuncts(b(Expr,_,_Infos),Prio) :- !,
132		count_number_of_disjuncts2(Expr,Prio).
133		count_number_of_disjuncts(priority(_),Prio) :- !, Prio=1.
134		count_number_of_disjuncts(B,Prio) :-
135		add_internal_error('Expression not wrapped: ',count_number_of_disjuncts(B,Prio)),Prio=1.
136		count_number_of_disjuncts2(disjunct(A,B),Nr) :- !, count_number_of_disjuncts(A,NA),
137		count_number_of_disjuncts(B,NB), Nr is NA+NB.
138		count_number_of_disjuncts2(norm_disjunct(_,RHS),Res) :- length(RHS,Len),!,
139		Res is Len+1.
140		count_number_of_disjuncts2(negation(A),Nr) :- !, count_number_of_conjuncts(A,Nr).
141		count_number_of_disjuncts2(_,1).
142
143
144
145		% we need to ensure that b_check_boolean_expression does not create a choice point on its own
146
147		b_check_boolean_expression(b(Expr,_,Infos),LS,S,WF,Res) :-
148		(composed(Expr) -> empty_avl(Ai)
149		; Ai = no_avl), % simple expression: no sharing is possible: no need to register expressions
150		create_wfwd_needed(WF,WFD),
151	?	b_check_boolean_expression2(Expr,Infos,LS,S,WFD,Res,Ai,_).
152
153		composed(negation(_)).
154		composed(conjunct(_,_)).
155		composed(disjunct(_,_)).
156		composed(implication(_,_)).
157		composed(equivalence(_,_)).
158		composed(if_predicate(_,_,_)).
159		composed(let_predicate(_,_,_)).
160		composed(lazy_let_pred(_,_,_)).
161
162		b_check_boolean_expression(E,LS,S,WF,Res,Ai,Ao) :-
163		% WFD adds information about WD context: wfwd(WF_store, ExpectedVal, Val,Infos)
164		% when Val becomes nonvar: if Val==ExpectedVal we need the value of E, otherwise it should be discarded
165		create_wfwd_needed(WF,WFD),
166	?	b_check_boolean_expression1(E,LS,S,WFD,Res,Ai,Ao).
167
168		b_check_boolean_expression0(WDE,WDV,Expr,LS,S,WF,Res,Ai,Ao) :-
169		create_wfwd(WF,WDE,WDV,WFD),
170	?	b_check_boolean_expression1(Expr,LS,S,WFD,Res,Ai,Ao).
171
172
173		b_check_boolean_expression1(b(Expr,_,Infos),LS,S,WFD,Res,Ai,Ao) :- get_wd(WFD,WDE,WDV),!,
174		% print('check : '), translate:print_bexpr(b(Expr,pred,Infos)),nl,
175		(nonvar(WDV),WDE \= WDV % the expression Expr is not needed
176		-> Ai=Ao,
177		(var(Res)
178		-> Res=pred_false % set it to false, value does not matter; note: predicate is not reused
179		; true)
180	?	; b_check_boolean_expression2(Expr,Infos,LS,S,WFD,Res,Ai,Ao)).
181		b_check_boolean_expression1(already_reified(X),_,_,_WFD,Res,Ai,Ao) :- !,Res=X, Ai=Ao.
182		b_check_boolean_expression1(E,LS,S,WFD,Res,Ai,Ao) :-
183		add_internal_error('Boolean expression not properly wrapped: ',b_check_boolean_expression1(E,LS,S,WFD,Res,Ai,Ao)),
184		b_check_boolean_expression2(E,[],LS,S,WFD,Res,Ai,Ao).
185
186		% normalise conjunction into flat list of conjuncts
187		normalise_conjunct(b(E,_,Info)) --> normalise_conjunct2(E,Info).
188		normalise_conjunct2(conjunct(A,B),_) --> !,normalise_conjunct(A),normalise_conjunct(B).
189		normalise_conjunct2(F,Info) --> [b(F,pred,Info)].
190
191		construct_norm_conjunct(A,b(B,pred,Info)) :- construct_norm_conjunct2(A,B,Info).
192		construct_norm_conjunct2([],truth,[]).
193		construct_norm_conjunct2([H|T],Res,Info) :-
194		(T==[] -> H=b(Res,pred,Info) ; Res=norm_conjunct(H,T),Info=[]).
195		% TO DO: build up member(contains_wd_condition,Infos)
196
197
198		% normalise disjunction into flat list of disjuncts
199		normalise_disjunct(b(E,_,Info)) --> normalise_disjunct2(E,Info).
200		normalise_disjunct2(disjunct(A,B),_) --> !,normalise_disjunct(A),normalise_disjunct(B).
201		normalise_disjunct2(F,Info) --> [b(F,pred,Info)].
202
203		construct_norm_disjunct(A,b(B,pred,Info)) :- construct_norm_disjunct2(A,B,Info).
204		construct_norm_disjunct2([],falsity,[]).
205		construct_norm_disjunct2([H|T],Res,Info) :-
206		(T==[] -> H=b(Res,pred,Info) ; Res=norm_disjunct(H,T),Info=[]).
207
208		can_negate_expression(b(Expr,pred,I),b(NExpr,pred,I)) :- can_negate2(Expr,NExpr).
209		can_negate2(equal(A,B),not_equal(A,B)).
210		can_negate2(not_equal(A,B),equal(A,B)).
211		can_negate2(member(A,B),not_member(A,B)).
212		can_negate2(not_member(A,B),member(A,B)).
213		can_negate2(subset(A,B),not_subset(A,B)).
214		can_negate2(not_subset(A,B),subset(A,B)).
215		can_negate2(subset_strict(A,B),not_subset_strict(A,B)).
216		can_negate2(not_subset_strict(A,B),subset_strict(A,B)).
217		can_negate2(greater_equal(A,B),less(A,B)).
218		can_negate2(less(A,B),greater_equal(A,B)).
219		can_negate2(less_equal(A,B),greater(A,B)).
220		can_negate2(greater(A,B),less_equal(A,B)).
221		can_negate2(less_real(A,B),less_equal_real(B,A)).
222		can_negate2(less_equal_real(A,B),less_real(B,A)).
223
224		b_check_boolean_expression2(truth,_,_,_,_WFD,Res,Ai,Ao) :- !,Res=pred_true, Ai=Ao.
225		b_check_boolean_expression2(falsity,_,_,_,_WFD,Res,Ai,Ao) :- !,Res=pred_false, Ai=Ao.
226		b_check_boolean_expression2(negation(BExpr),_,LocalState,State,WFD,Res,Ai,Ao) :- !,
227		(can_negate_expression(BExpr,NBExpr)
228		-> /* avoid introducing negate propagator; maybe not necessary */
229		b_check_boolean_expression1(NBExpr,LocalState,State,WFD,Res,Ai,Ao)
230		; negate(NR,Res),
231		b_check_boolean_expression1(BExpr,LocalState,State,WFD,NR,Ai,Ao)).
232		b_check_boolean_expression2(conjunct(LHS,RHS),CInfo,LocalState,State,WFD,Res,Ai,Ao) :- !,
233		normalise_conjunct2(conjunct(LHS,RHS),CInfo,NormRes,[]),
234		construct_norm_conjunct2(NormRes,NC,Info),
235	?	b_check_boolean_expression2(NC,Info,LocalState,State,WFD,Res,Ai,Ao).
236		b_check_boolean_expression2(norm_conjunct(LHS,RHS),_,LocalState,State,wfwd(WF,WDE,WDV,_),Res,Ai,Ao) :- !,
237		construct_norm_conjunct(RHS,NC),
238		conjoin(LR,RR,Res,LHS,NC,WF),
239		create_wfwd(WF,WDE,WDV,WFD),
240	?	b_check_boolean_expression1(LHS,LocalState,State,WFD,LR,Ai,Aii),
241		propagagate_wfwd(WDE,WDV,GuardFlag,LR,pred_false), % if WDE/=WDV then set GuardFlag to pred_false; indicating to RHS that it is not needed also
242	?	b_check_boolean_expression0(pred_true,GuardFlag,NC,LocalState,State,WF,RR,Aii,Ao).
243		b_check_boolean_expression2(implication(LHS,RHS),_,LocalState,State,wfwd(WF,WDE,WDV,_),Res,Ai,Ao) :- !,
244		imply(LR,RR,Res),
245		create_wfwd(WF,WDE,WDV,WFD),
246		b_check_boolean_expression1(LHS,LocalState,State,WFD,LR,Ai,Aii),
247		propagagate_wfwd(WDE,WDV,GuardFlag,LR,pred_false), % if WDE/=WDV then set GuardFlag to pred_false
248	?	b_check_boolean_expression0(pred_true,GuardFlag,RHS,LocalState,State,WF,RR,Aii,Ao).
249		b_check_boolean_expression2(if_predicate(Test,LHS,RHS),_,LocalState,State,wfwd(WF,WDE,WDV,_),Res,Ai,Ao) :- !,
250		if_pred(TestR,LR,RR,Res,WF),
251		create_wfwd(WF,WDE,WDV,WFD),
252		b_check_boolean_expression1(Test,LocalState,State,WFD,TestR,Ai,Aii),
253		propagagate_wfwd(WDE,WDV,GuardFlag1,TestR,pred_false), % value of LHS ignored with GuardFlag1=pred_false
254		b_check_boolean_expression0(pred_true,GuardFlag1,LHS,LocalState,State,WF,LR,Aii,Aiii),
255		propagagate_wfwd(WDE,WDV,GuardFlag2,TestR,pred_true), % value of RHS ignored with GuardFlag2=pred_true
256		b_check_boolean_expression0(pred_false,GuardFlag2,RHS,LocalState,State,WF,RR,Aiii,Ao).
257		b_check_boolean_expression2(equivalence(LHS,RHS),_,LocalState,State,WFD,Res,Ai,Ao) :- !, equiv(LR,RR,Res),
258		b_check_boolean_expression1(LHS,LocalState,State,WFD,LR,Ai,Aii),
259	?	b_check_boolean_expression1(RHS,LocalState,State,WFD,RR,Aii,Ao).
260		b_check_boolean_expression2(disjunct(LHS,RHS),CInfo,LocalState,State,WFD,Res,Ai,Ao) :- !,
261		normalise_disjunct2(disjunct(LHS,RHS),CInfo,NormRes,[]),
262		construct_norm_disjunct2(NormRes,NC,Info),
263	?	b_check_boolean_expression2(NC,Info,LocalState,State,WFD,Res,Ai,Ao).
264		b_check_boolean_expression2(norm_disjunct(LHS,RHS),_,LocalState,State,wfwd(WF,WDE,WDV,_),Res,Ai,Ao) :- !,
265		construct_norm_disjunct(RHS,NC),
266		disjoin(LR,RR,Res,LHS,NC,WF),
267		create_wfwd(WF,WDE,WDV,WFD),
268	?	b_check_boolean_expression1(LHS,LocalState,State,WFD,LR,Ai,Aii),
269		propagagate_wfwd(WDE,WDV,GuardFlag,LR,pred_true),
270	?	b_check_boolean_expression0(pred_false,GuardFlag,NC,LocalState,State,WF,RR,Aii,Ao).
271		b_check_boolean_expression2(let_predicate(Ids,AssignmentExprs,Pred),_Info,LocalState,State,WFD,Res,Ai,Ao) :- !,
272		wd_set_up_localstate_for_let(Ids,AssignmentExprs,LocalState,State,LetState,WFD),
273		Ao=Ai, % anything cached inside the LET may depend on Ids and should not be reused outside of LET, see test 2397
274		empty_avl(InnerAi), % we can only reuse predicates inside if Ids are fresh, see test 2398
275		b_check_boolean_expression1(Pred,LetState,State,WFD,Res,InnerAi,_).
276		b_check_boolean_expression2(lazy_let_pred(Id,AssignmentExpr,Pred),_I,LocalState,State,wfwd(WF,WDE,WDV,_),Res,Ai,Ao) :- !,
277		set_up_localstate([Id],[(Trigger,IdValue)],LocalState,LetState),
278		b_interpreter:lazy_compute_expression(Trigger,AssignmentExpr,LocalState,State,IdValue,WF,Ai),
279		create_wfwd(WF,WDE,WDV,WFD),
280		b_check_boolean_expression1(Pred,LetState,State,WFD,Res,Ai,Ao). % Lazy lets always unique, we can pass Ai
281		b_check_boolean_expression2(lazy_lookup_pred(Id),Info,LocalState,_State,WFD,Res,Ai,Ao) :- !, Ai=Ao,
282		store:lookup_value_for_existing_id(Id,LocalState,(Trigger,Value)), % should normally only occur in LocalState; value introduced by lazy_let
283		wd_delay(((Trigger,Value) = (pred_true,Res)),
284		Res,b(lazy_lookup_pred(Id),pred,Info),WFD).
285		b_check_boolean_expression2(value(V),_Info,_LocalState,_State,_WFD,Res,Ai,Ao) :- !, % this can occur when lazy_lookup_pred gets compiled by b_compiler
286		Res=V,Ai=Ao.
287		b_check_boolean_expression2(not_equal(LHS,RHS),Info,LocalState,State,WFD,Res,Ai,Ao) :- !,
288		(negate_equal_false(LHS,RHS,LHS1,RHS1)
289		-> /* X/=FALSE equivalent to X=TRUE */
290		b_check_boolean_expression3_pos(equal(LHS1,RHS1),Info,LocalState,State,WFD,Res,Ai,Ao)
291	?	; b_check_boolean_expression3_neg(equal(LHS,RHS),Info,LocalState,State,WFD,Res,Ai,Ao)
292		).
293		b_check_boolean_expression2(equal(LHS,RHS),Info,LocalState,State,WFD,Res,Ai,Ao) :- !,
294	?	(negate_equal_false(LHS,RHS,LHS1,RHS1)
295		-> RHS1=b(boolean_true,boolean,[]), /* X/=FALSE equivalent to X=TRUE */
296		b_check_boolean_expression3_neg(equal(LHS1,RHS1),Info,LocalState,State,WFD,Res,Ai,Ao)
297	?	; b_check_boolean_expression3_pos(equal(LHS,RHS),Info,LocalState,State,WFD,Res,Ai,Ao)
298		).
299		b_check_boolean_expression2(not_member(LHS,RHS),Info,LocalState,State,WFD,Res,Ai,Ao) :- !,
300		b_check_boolean_expression3_neg(member(LHS,RHS),Info,LocalState,State,WFD,Res,Ai,Ao).
301		b_check_boolean_expression2(not_subset(LHS,RHS),Info,LocalState,State,WFD,Res,Ai,Ao) :- !,
302		b_check_boolean_expression3_neg(subset(LHS,RHS),Info,LocalState,State,WFD,Res,Ai,Ao).
303		b_check_boolean_expression2(not_subset_strict(LHS,RHS),Info,LocalState,State,WFD,Res,Ai,Ao) :- !,
304		b_check_boolean_expression3_neg(subset_strict(LHS,RHS),Info,LocalState,State,WFD,Res,Ai,Ao).
305		b_check_boolean_expression2(greater(LHS,RHS),Info,LocalState,State,WFD,Res,Ai,Ao) :- !,
306		b_check_boolean_expression3_pos(less(RHS,LHS),Info,LocalState,State,WFD,Res,Ai,Ao).
307		b_check_boolean_expression2(greater_equal(LHS,RHS),Info,LocalState,State,WFD,Res,Ai,Ao) :- !,
308		b_check_boolean_expression3_neg(less(LHS,RHS),Info,LocalState,State,WFD,Res,Ai,Ao).
309		b_check_boolean_expression2(less_equal(LHS,RHS),Info,LocalState,State,WFD,Res,Ai,Ao) :- !,
310	?	b_check_boolean_expression3_neg(less(RHS,LHS),Info,LocalState,State,WFD,Res,Ai,Ao).
311		b_check_boolean_expression2(Pred,Infos,LocalState,State,WFD,Res,Ai,Ao) :-
312	?	b_check_boolean_expression3_pos(Pred,Infos,LocalState,State,WFD,Res,Ai,Ao).
313
314
315		% check whether one of the two arguments is FALSE
316		% translate X/=FALSE -> X=TRUE for normalisation purposes
317		negate_equal_false(b(boolean_false,boolean,_),E,E,b(boolean_true,boolean,[])).
318		negate_equal_false(E,b(boolean_false,boolean,_),E,b(boolean_true,boolean,[])).
319
320		b_check_boolean_expression3_pos(Pred,Infos,LocalState,State,WFD,Res,Ai,Ao) :-
321		%print(register_predicate(WFD)),nl,portray_avl(Ai),nl,
322		register_predicate_wfd(WFD,Pred,Infos,Res,Reused,Ai,Ai2),
323		(Reused=true
324		-> Ao=Ai2 % , print(reused_pred(Res,WFD,Infos)),nl
325	?	; b_check_boolean_expression4(Pred,Infos,LocalState,State,WFD,Ok,Res),
326		(Ok=ok_to_store -> Ao=Ai2 ; Ao=Ai)
327		).
328
329		b_check_boolean_expression3_neg(Pred,Infos,LocalState,State,WFD,NegRes,Ai,Ao) :-
330		%print(register_neg_predicate(WFD,Infos,Pred)),nl,
331		register_predicate_wfd(WFD,Pred,Infos,Res,Reused,Ai,Ai2), negate(Res,NegRes),
332		(Reused=true
333		-> Ao=Ai2
334	?	; b_check_boolean_expression4(Pred,Infos,LocalState,State,WFD,Ok,Res),
335		(Ok=ok_to_store -> Ao=Ai2 ; Ao=Ai)
336		).
337
338		% Register a new predicate in the AVL tree if either forced or non-WD condition inside
339		register_predicate_wfd(_,_,_,_,false,Ai,Ao) :- Ai = no_avl,!, Ai=Ao.
340		register_predicate_wfd(_,_Pred,_Infos,_,false,Ai,Ao) :-
341		preferences:preference(use_common_subexpression_elimination,true),
342		preferences:preference(use_common_subexpression_also_for_predicates,true),
343		preferences:preference(disprover_mode,false), % there are still a few things detected here that CSE does not detect (=FALSE,=TRUE,...)
344		!, % CSE already statically detects these ( all of the time !?)
345		Ai=Ao.
346		register_predicate_wfd(WFWD,Pred,Infos,PredTruthVar,Reused,Ai,Ao) :-
347		get_wd(WFWD,A,B),
348		(A==B -> register_predicate_aux(Pred,PredTruthVar,Reused,Ai,Ao) % it will be evaluated; we can share it
349		; nonmember(contains_wd_condition,Infos) -> register_predicate_aux(Pred,PredTruthVar,Reused,Ai,Ao)
350		% Pred is not guaranteed to be evaluated: WD-condition + not in forced WFD context (beware of exists!)
351		; register_predicate_aux(Pred,PredTruthVar,true,Ai,Ao) -> Reused=true % the predicate is already stored
352		% Note: as predicate is already stored; no problem with WD; relevant for test 1959
353		; Ai=Ao, Reused=false % not guaranteed to be evaluated: WD-condition + not in forced WFD context
354		% ,print('NOT REGISTERING: '), translate:print_bexpr(Pred),nl
355		).
356
357		:- assert_must_succeed((E=empty, %avl:empty_avl(E),
358		A=b(value(_VAR),integer,[]),
359		b_interpreter_check:register_predicate(equal(A,A),[],pred_true,Reused,E,A1),
360		Reused==false, A1==empty)). % ensure we do not store non-var expressions
361		:- assert_must_succeed((E=empty, %avl:empty_avl(E),
362		A=b(value(int(1)),integer,[]),
363		b_interpreter_check:register_predicate(equal(A,A),[],pred_true,Reused,E,A1),
364		Reused==false, A1 \= empty, B=b(value(_),integer,[]),
365		b_interpreter_check:register_predicate(equal(B,B),[],pred_true,Reuse2,A1,A2),
366		Reuse2==false, A2==A1)). % ensure we do not look up non-var expressions
367		:- assert_must_succeed((E=empty, %avl:empty_avl(E),
368		A=b(value(int(1)),integer,[]),
369		b_interpreter_check:register_predicate(equal(A,A),[info1],pred_true,Reused,E,A1),
370		Reused==false,
371		b_interpreter_check:register_predicate(equal(A,A),[info2],pred_true,Reuse2,A1,A2),
372		Reuse2==true, A2==A1)). % ensure registering works
373
374		% Register a new predicate in the AVL tree (for outside callers like b_interpreter.pl)
375	?	register_predicate(Pred,_Infos,NegPredTruthVar,Reused,Ai,Ao) :- negate_pred(Pred,NegPred),!,
376		%print(negating),nl,
377		negate(PredTruthVar,NegPredTruthVar),
378		register_predicate_aux(NegPred,PredTruthVar,Reused,Ai,Ao).
379		register_predicate(Pred,_Infos,PredTruthVar,Reused,Ai,Ao) :-
380	?	register_predicate_aux(Pred,PredTruthVar,Reused,Ai,Ao).
381
382	?	negate_typed_pred(b(A,pred,_),NegA) :- negate_pred(A,NegA).
383	?	negate_pred(equal(A,B),equal(AA,TRUE)) :- negate_equal_false(A,B,AA,TRUE).
384		negate_pred(not_equal(A,B),equal(A,B)). % TO DO: we should check negate_equal_false
385		negate_pred(not_member(A,B),member(A,B)).
386		negate_pred(not_subset(A,B),subset(A,B)).
387		negate_pred(not_subset_strict(A,B),subset_strict(A,B)).
388		negate_pred(greater_equal(A,B),less(A,B)).
389		negate_pred(less_equal(A,B),less(B,A)).
390		negate_pred(negation(b(A,pred,_)),A).
391
392		% to do: detect convert_bool(Pred) = X and register Pred?
393		register_predicate_aux(Pred,_PredTruthVar,Reused,Ai,Ao) :- do_not_store_pred(Pred),
394		!,
395		Ai=Ao, Reused=false.
396		register_predicate_aux(Pred,PredTruthVar,Reused,Ai,Ao) :- check_pred_truth_var(PredTruthVar),
397		norm_pred_check(Pred,NPred), % We could store this information in the info field computed by ast_cleanup ?
398		(%too_simple(NPred) -> Reused=false, Ao=Ai ; %% even for simple equalities it actually pays off !
399		reuse_predicate(NPred,Var,Ai)
400		-> % nl,print(reusing(NPred,Var)),nl, %%
401		PredTruthVar=Var,Ao=Ai, Reused=true
402		; add_predicate(NPred,PredTruthVar,Ai,Ao), Reused=false
403		%,nl,print(not_reusing(NPred)),nl
404		).
405
406		check_pred_truth_var(X) :- var(X),!.
407		check_pred_truth_var(pred_true) :- !.
408		check_pred_truth_var(pred_false) :- !.
409		check_pred_truth_var(X) :- add_internal_error('Illegal Predicate Truth Value: ',check_pred_truth_var(X)).
410
411		:- use_module(kernel_tools,[ground_bexpr/1]).
412		do_not_store_pred(external_pred_call(_P,_)) :- !. % expcept maybe LESS, CHOOSE,... we could check performs_io
413		do_not_store_pred(B) :-
414		(ground_bexpr(b(B,pred,[]))
415		% TO DO: improve performance: marking bexpr with potential non-ground value(.) terms inside
416		% maybe avoid registering predicates with very large values inside
417		% avoid registering predicate if it is the only one in a closure
418		-> fail
419		; true %print('-> Not storing: '),translate:print_bexpr(b(B,pred,[])),nl
420		).
421
422
423		% Quantifier Expansion
424
425		b_check_forall_wf(Parameters,LHS,RHS,Info,LocalState,State,WF,PredRes) :-
426		create_wfwd_needed(WF,WFD), % we expect it to be in a context where the value will be needed
427		b_check_forall_wfwd(Parameters,LHS,RHS,Info,LocalState,State,WFD,PredRes).
428		b_check_forall_wfwd(_Parameters,LHS,RHS,_Info,_LocalState,_State,_WFD,PredRes) :-
429		(is_falsity(LHS) ; is_truth(RHS)),!, % quantifier always true
430		PredRes = pred_true.
431		b_check_forall_wfwd(Parameters,LHS,RHS,Info,LocalState,State,WFD,PredRes) :-
432	?	small_quantifier_cardinality(Parameters,LHS,LHS1,LHSRest),
433		%print(expand(forall(Parameters))),nl,
434		expand_quantifier(Parameters,LHS1,List,forall,Info), %print(List),nl,
435		Body = b(implication(LHSRest,RHS),pred,Info),% translate:print_bexpr(Body),nl,
436		get_wf(WFD,WF),
437		check_expanded_forall_quantifier(List,Body, LocalState, State,WF,WFD,PredRes).
438		% TO DO: if not small_quantifier_cardinality: b_check_boolean_expression4_delay
439
440
441		b_check_exists_wf(Parameters,Body,Info,LocalState,State,WF,PredRes) :-
442		create_wfwd_needed(WF,WFD), % we expect it to be in a context where the value will be needed
443		b_check_exists_wfwd(Parameters,Body,Info,LocalState,State,WFD,_,PredRes).
444		b_check_exists_wfwd(Parameters,Body,Info,LocalState,State,WFD,ok_to_store,PredRes) :-
445		% could be generalised to take into consideration domain as restricted by Body
446	?	small_quantifier_cardinality(Parameters,Body,LHS,RHS),!,
447		% print(expanding_check_exists(_Card,Parameters)),nl, % portray_waitflags(WF),
448		expand_quantifier(Parameters,LHS,List,exists,Info),
449		% now compute a priority for the disjunction based on the number of case splits
450		% relevant for tests 1358, 1746
451		length(List,Len), % Note: if Len=1: the body must be true; no disjoin will be set up
452		get_pow2_binary_choice_priority(Len,Prio),
453		% if Len=2 -> we actually have just two possibilities T,_ and F,T; but we want Prio to start at 4 ?
454		% if Len=3 -> we have T,_,_ ; F,T,_ ; F,F,T less possibilites if disjoin enumerated from left-to-right; TO DO: should we lower the priority taking this into account ?
455		% TO DO: maybe we could directly set up an n-ary disjoin predicate;
456		% if one disjunct true; remove case-splits on other disjuncts
457		get_wf(WFD,WF),
458		check_expanded_exists_quantifier(List,Prio,RHS, LocalState, State,WF,WFD,PredRes).
459		b_check_exists_wfwd(Parameters,Body,Infos,LocalState,State,wfwd(WF,WDE,WDV,ContextInfo),do_not_store,PredRes) :-
460		% the above reification has not worked; we now "pretend" that reification worked
461		% and introduce a delayed choice point
462		% do_not_store means that the predicate result should not be re-used somewhere else, because
463		% as the predicate evaluation is delayed it may later not be needed and not evaluated, cf test 2404
464		ContextInfo \= outer_wfwd_context, % at the outer-level interpreter expects reification succeeds only if
465		% at least top-level operator was reified deterministically,
466		% important for tests 1074, 1338, 1358, 1915 with this clause enabled
467		% test 305 #x.(x + x = 1000) now works, but not 1739 (timeout)
468		reify_inner_exists_non_deterministically, % hence we currently only use it in data validation mode
469		% here we enumerate reification variables with a much lower priority (data driven enumeration)
470		% (see get_binary_choice_wait_flag_exp_backoff)
471		% this clause relevant for 0323/CCSL/TYPES_AUTORISES_RVF3_GEN__MRGA.mch
472		Pred = exists(Parameters,Body),
473		perfmessage(reify,reifiying_inner_exists_non_deterministically(Parameters),Infos),
474		b_check_boolean_expression4_delay(WDE,WDV,Pred,Infos,LocalState,State,WF,PredRes).
475
476		% true if we allow reification of exists which cannot be expanded
477		% by delayed non-det enumeration (of pred_false, pred_true) if exists is not at top-level
478		reify_inner_exists_non_deterministically :- preferences:preference(data_validation_mode,true).
479
480
481		:- use_module(b_enumerate, [b_tighter_enumerate_values_in_ctxt/3]).
482		expand_quantifier(Parameters,Pred,ListOfNewLocalStates,QuantKind,Span) :-
483		% at the moment LS,State not really needed; only necessary if non-compiled Pred can be used
484		% also: feeding in any non-bound variables in LocalState or State would cause problems in findall !
485		findall(ParLocalState,
486		(b_interpreter:set_up_typed_localstate(Parameters,ParaValues,ParamTypedVals,
487		[],ParLocalState,all_solutions),
488		kernel_waitflags:init_wait_flags_with_call_stack(WF,
489		[quantifier_call(QuantKind,Parameters,ParaValues,Span)]),
490		b_test_boolean_expression(Pred,[],ParLocalState,WF),
491		b_tighter_enumerate_values_in_ctxt(ParamTypedVals,Pred,WF),
492		kernel_waitflags:ground_wait_flags(WF)),
493		ListOfNewLocalStates).
494
495		% a version which ensures that we have unique solutions of the bindings
496		expand_quantifier_normalised(Parameters,Pred,ListOfNewLocalStates,QuantKind,Span) :-
497		expand_quantifier(Parameters,Pred,List,QuantKind,Span),
498		normalise_local_states(List,NList),
499		sort(NList,ListOfNewLocalStates). % will remove duplicates
500
501		normalise_local_states([],[]).
502		normalise_local_states([State|T],[NS|NT]) :-
503		convert_bindings_to_avl(State,NS),
504		normalise_local_states(T,NT).
505
506		:- use_module(custom_explicit_sets,[convert_to_avl/2]).
507		convert_bindings_to_avl([],[]).
508		convert_bindings_to_avl([bind(Var,Val)|T],[bind(Var,NVal)|NT]) :-
509		(convert_to_avl(Val,NVal) -> true ; add_internal_error('Cannot normalise:',Val),fail),
510		convert_bindings_to_avl(T,NT).
511
512		check_expanded_forall_quantifier([], _Body, _LS, _State,_WF,_WFD,Res) :-
513		Res=pred_true.
514		check_expanded_forall_quantifier([LS1|TLS], Body, LS, State,WF,WFD,Res) :-
515		conjoin(Res1,TRes,Res,Body,Body,WF),
516		empty_avl(InnerAi), % TO DO: maybe use no_avl ?
517		append(LS1,LS,InnerLS),
518		% Note: we do not need to guard against wd-definition from other instances inside a quantified expression
519		% either all conjuncts can be evaluated or none
520		% print(expand_forall(WFD)), translate:print_bexpr(Body),nl,
521		b_check_boolean_expression1(Body,InnerLS,State,WFD,Res1,InnerAi,_Aii),
522		%instantiate_wfwd_result(WDE,WDV,Res1),
523		check_expanded_forall_quantifier(TLS,Body,LS,State,WF,WFD,TRes).
524
525		/*
526		:- block instantiate_wfwd_result(?,-,-).
527		% instantiate a boolean variable in case it is no longer needed and not set by something else
528		instantiate_wfwd_result(WDE,WDV,Res) :-
529		(nonvar(Res) -> true
530		; WDE==WDV -> true
531		; Res = pred_false). */
532
533		check_expanded_exists_quantifier([], _, _Body, _LS, _State,_WF,_WFD,Res) :-
534		Res=pred_false.
535		check_expanded_exists_quantifier([LS1|TLS], Priority, Body, LS, State,WF,WFD,Res) :-
536		(TLS = [] -> Res=Res1
537		; disjoin(Res1,TRes,Res,priority(Priority),priority(Priority),WF)), % was using Body instead of priority(Priority)
538		empty_avl(InnerAi), % TO DO: maybe use no_avl ?
539		append(LS1,LS,InnerLS),
540		b_check_boolean_expression1(Body,InnerLS,State,WFD,Res1,InnerAi,_Aii),
541		% Note: we do not need to guard against wd-definition from other instances inside a quantified expression
542		check_expanded_exists_quantifier(TLS,Priority,Body,LS,State,WF,WFD,TRes).
543
544
545		% try and convert a closure into a list of 0/1 variables for each potential element
546		reify_closure_with_small_cardinality(P,T,Body, WF,ReifiedList) :- %print(try(P)),nl,
547		create_typed_ids(P,T,Parameters),
548		small_quantifier_cardinality(Parameters,Body,LHS,RHS,350,25000), % TO DO: how to choose these parameters ?
549		% for card({x|x:1..n & x mod 3=0})=c & n=24000 -> 340 ms with reification; 320 ms without; n=74000 : 1020 ms without, 1160 with reification
550		% but there is a big difference for card({x|x:1..n & x mod 3=0 & x<10}) with n=74000 : 0 ms without reification, 1580 with; n=500: 20 ms with reification; n=250: 10 ms with reification
551		expand_quantifier_normalised(Parameters,LHS,List,comprehension_set,Body),
552		% important to normalise and have unique solutions for cardinality reification,
553		% see tests 639, 640 for card(POW(SS)-{{}}) with SS full set
554		create_wfwd_needed(WF,WFD), % is this ok ??
555	?	reifiy_list(List,RHS,WFD,ReifiedList).
556
557
558
559		reifiy_list([], _Body,_WFD,[]).
560		reifiy_list([LS1|TLS], Body,WFD,[Res_01|TRes]) :-
561		empty_avl(InnerAi),
562	?	b_check_boolean_expression1(Body,LS1,[],WFD,Res1_pred,InnerAi,_Aii),
563		prop_pred_01(Res1_pred,Res_01),
564		%format(' reify ~w : ~w~n',[Res_01,LS1]),
565		% Note: we do not need to guard against wd-definition from other instances inside a quantified expression
566	?	reifiy_list(TLS,Body,WFD,TRes).
567
568
569
570		:- use_module(library(lists),[select/3]).
571
572		% check if Body produces a small cardinality for the paramters Par
573		% if yes: the predicates constraining Par are put into LHS, the rest into RHS
574		% also: LHS must ensure that ground values are produced for Par and that we can enumerate with a separate WF (in expand_quantifier)
575		small_quantifier_cardinality(Par,Body,LHS,RHS) :-
576		%preferences:preference(solver_strength,SS), NL is 10+SS, SMTL is 40+SS,
577		NL=10,SMTL=40,
578	?	small_quantifier_cardinality(Par,Body,LHS,RHS,NL,SMTL). % was 10,35; raising it to 10,41 makes tests 1441, 1442 fail due to expansion of exists; raising it to 16,50 makes test 1112 fail; TO DO: investigate
579		small_quantifier_cardinality(Par,Body,LHS,RHS,NormalLimit,SMTLimit) :-
580		conjunction_to_list(Body,BodyList),
581		def_get_texpr_ids(Par,AllParas),
582	?	small_quantifier_cardinality_aux(Par,AllParas,BodyList,_UpBoundOnSize,LLHS,LRHS,NormalLimit,SMTLimit),
583		conjunct_predicates_with_pos_info(LLHS,LHS),
584		conjunct_predicates_with_pos_info(LRHS,RHS).
585
586		is_membership_or_eq(b(P,pred,Info),TLHS,RHS,Info) :- is_mem_aux(P,TLHS,RHS).
587		is_mem_aux(member(TLHS,b(RHS,_,_)),TLHS,RHS).
588		%is_mem_aux(subset(SONE,b(RHS,_,_)),TLHS,RHS) :- singleton_set_extension(SONE,TLHS).
589		is_mem_aux(equal(TLHS,b(value(V),_,_)),TLHS,value([V])). % x = V is the same as x:{V}
590		%TODO: use :- use_module(bsyntaxtree,[is_membership_or_equality/3]). % will create set_extension
591
592		% do not rely on size for anything: it is just an upper bound on the size; the actual size could be smaller
593		small_quantifier_cardinality_aux([],_,Body,Size,LHS,RHS,_,_) :- !,
594		LHS=[],RHS=Body,Size=1.
595		small_quantifier_cardinality_aux(Parameters,AllParas,[LHS|TBody],FullSize,FullLHS,FullRHS,NormalLimit,SMTLimit) :-
596		is_membership_or_eq(LHS,SID,MemRHS,Info),
597	?	constrains_ID(SID,AllParas,Parameters,RestParameters,SkelVal,SkelToUnify,BindList), % we could check RestParameters /= Parameters
598		% TO DO: we could also allow parameter to be constrained twice x: 1..100 & x: {...} ?
599		(is_small_set(MemRHS,Size,NormalLimit,SMTLimit,Info) % we have a small set of ground values: we can evaluate LHS to expand the quantifier/set_comprehension for the parameters occuring in LHS
600		-> FullLHS = [LHS|RestLHS],FullRHS = RestRHS
601	?	; infer_ground_membership(MemRHS,SID,SkelVal,SkelToUnify,BindList,NormalLimit,SMTLimit, Size,InferredLHS) ->
602		% we have inferred a superset InferredLHS of MemRHS which is small and known
603		FullLHS = [InferredLHS|RestLHS], % we have added an inferred membership constraint
604		FullRHS = [LHS|RestRHS]), % the original membership LHS still needs to be checked later, after expansion of the quantifier
605		!,
606		% we select LHS to be included in FullLHS and mark parameter ID as constrained
607		small_quantifier_cardinality_aux(RestParameters,AllParas,TBody,RestSize,RestLHS,RestRHS,NormalLimit,SMTLimit),
608		FullSize is Size*RestSize,
609		is_small_size(FullSize,NormalLimit,SMTLimit, Parameters).
610		small_quantifier_cardinality_aux(Parameters,AllParas,[H|Rest],FullSize,RestLHS,[H|RestRHS],NormalLimit,SMTLimit) :- !,
611		% skip the conjunct H
612	?	small_quantifier_cardinality_aux(Parameters,AllParas,Rest,FullSize,RestLHS,RestRHS,NormalLimit,SMTLimit).
613		small_quantifier_cardinality_aux(Parameters,_AllParas,Body,ParCard,[],Body,NormalLimit,SMTLimit) :-
614		% if the remaining parameter type cardinality is small: just use "truth" as body; will instantiate parameters
615	?	b_interpreter:parameter_list_cardinality(Parameters,ParCard),
616		is_small_size(ParCard,NormalLimit,SMTLimit, Parameters).
617
618		% try and extract a ground superset (InferredLHS) of the RHS (ID:RHS) which constrains ID
619		infer_ground_membership(value(List),SID,SkelVal,SkelToUnify,BindList,NormalLimit,SMTLimit, Size,InferredLHS) :-
620		!,
621		% the List is probably not ground; let's try and see if we can extract ground matches for the parameters at least; see test 1627 (s=1..20 & x: s-->BOOL & card({t|t|->TRUE:x}):18..19)
622		extract_bind_list(BindList,LHSTerm,RHSValue),
623		has_bounded_ground_matches(List,SkelVal,SkelToUnify,RHSValue,MatchedValues,1,NrMatches), % TO DO: provide SMTLimit as upper limit
624		NrMatches = Size,
625		is_small_size(Size,NormalLimit,SMTLimit, SID),
626		get_texpr_type(LHSTerm,LHSTermType),
627		InferredLHS = b(member(LHSTerm,b(value(MatchedValues),set(LHSTermType),[])),pred,[generated]).
628		infer_ground_membership(Set,SID,SkelVal,SkelToUnify,BindList,NormalLimit,SMTLimit,Size,InferredLHS) :-
629	?	superset(Set,SuperSet),
630		% e.g., if ID: {1} /\ x -> InferredLHS = {1} and we will add ID : {1} to the LHS of the quantifier and keep ID : {1} /\ x as the RHS
631		infer_ground_mem_aux(SuperSet,SID,SkelVal,SkelToUnify,BindList,NormalLimit,SMTLimit,Size,InferredLHS).
632
633
634		superset(intersection(A,B),Set) :- (Set=A ; Set=B). % Set /\ X <: Set
635		superset(set_subtraction(Set,_),Set). % Set \ X <: Set
636		superset(domain_restriction(_,Set),Set). % X <| Set <: Set
637		superset(domain_subtraction(_,Set),Set). % X <<| Set <: Set
638		superset(range_subtraction(Set,_),Set). % Set |> X <: Set
639		superset(range_restriction(Set,_),Set). % Set |>> X <: Set
640
641		infer_ground_mem_aux(b(Set,T,I),SID,SkelVal,SkelToUnify,BindList,NormalLimit,SMTLimit, Size,InferredLHS) :-
642		(is_small_set(Set,Size,NormalLimit,SMTLimit,I)
643		-> InferredLHS = b(member(SID,b(Set,T,I)),pred,[generated])
644		; infer_ground_membership(Set,SID,SkelVal,SkelToUnify,BindList,NormalLimit,SMTLimit, Size,InferredLHS)).
645
646		:- use_module(bsyntaxtree, [create_couple/3]).
647		% extract result of constrains_ID BindList into an Expression-Tuple for new membership constraint and a value that will be put into a value(List)
648		extract_bind_list([TID/Val],TID,Val) :- !.
649		extract_bind_list([TID/Val|BList],Couple,(Val,RestVal)) :-
650		create_couple(TID,RestExpr,Couple),
651		extract_bind_list(BList,RestExpr,RestVal).
652
653		:- use_module(kernel_tools,[can_match/2]).
654		% check if we can find a bounded / fixed number of ground matches for Skeleton Value in List
655		has_bounded_ground_matches(Var,_,_,_, _,_,_) :- var(Var),!.
656		has_bounded_ground_matches([],_SkelVal,_SkelToUnify,_,[],LenAcc,LenAcc).
657		has_bounded_ground_matches([H|T],SkelVal,SkelToUnify,ValueToStore,Matches,LenAcc,LenRes) :-
658		(can_match(H,SkelVal) -> copy_term((SkelToUnify,ValueToStore),(H,HValueToStore)),
659		ground_value(HValueToStore),
660		Matches = [HValueToStore|MT],
661		A1 is LenAcc+1 ; Matches=MT,A1=LenAcc),
662		has_bounded_ground_matches(T,SkelVal,SkelToUnify,ValueToStore,MT,A1,LenRes).
663
664		% check if the Expr contains ID, i.e., matching Expr with an element of a set will also instantiate and determine TID
665		% TO DO: also accept other patterns: records, sets?,....
666
667		% SkeletonToUnify: a skeleton that can be used to unify with any value and extracts value in BindList
668		constrains_ID(b(E,_,_),AllParas,Parameters,RestParameters,SkeletonValue,SkeletonToUnify,BindList) :-
669	?	constrains_ID_aux(E,AllParas,Parameters,RestParameters,SkeletonValue,SkeletonToUnify,BindList).
670		constrains_ID_aux(couple(A,B),AllParas,Parameters,RestParameters,(V1,V2),(Skel1,Skel2),Bind) :-
671	?	constrains_ID(A,AllParas,Parameters,Rest1,V1,Skel1,Bind1),
672	?	constrains_ID(B,AllParas,Rest1,RestParameters,V2,Skel2,Bind2),
673		append(Bind1,Bind2,Bind). % TO DO: use DCGs
674		constrains_ID_aux(rec(F),AllParas,Parameters,RestParameters,record(SkelV),record(SkelU),Bind) :-
675	?	constrains_ID_fields(F,AllParas,Parameters,RestParameters,SkelV,SkelU,Bind).
676		constrains_ID_aux(identifier(ID),AllParas,Parameters,RestParameters,_SkelV,SkelU,Bind) :-
677		% TO DO: allow same id to appear multiple times in expression + allow to re-use parameters in another conjunct
678	?	(select(TID,Parameters,RestParameters), get_texpr_id(TID,ID)
679		-> Bind = [TID/SkelU]
680	?	; member(ID,AllParas), % we have already used/bound ID; we will use first occurence for skeleton/bind; this one is simply ignored
681		% TO DO: we could try and see whether using the second occurence gives a better result
682		RestParameters=Parameters, Bind=[]
683		).
684		constrains_ID_aux(value(V),_AllParas,P,P,V,_,[]) :- ground_value(V).% if not ground value we may not be able to compute all possible values for ID
685		constrains_ID_aux(boolean_true,_AllParas,P,P,pred_true,pred_true,[]). % needed ?? everything is compiled anway ?
686		constrains_ID_aux(boolean_false,_AllParas,P,P,pred_false,pred_false,[]). % needed ?? everything is compiled anway ?
687		% Below: allow any other expression as long as it only uses AllParas
688		% e.g. x+1 in : s: 1..20 --> (BOOL*(1..20)) & card({x|x|->(TRUE|->x):s})=10 & card({x|x|->(FALSE|->x+1):s})=10
689		constrains_ID_aux(add(A,B),AllParas,P,P,_,_,[]) :- % basically allow other Parameters or ground values
690	?	constrains_ID(A,AllParas,[],[],_,_,_), constrains_ID(B,AllParas,[],[],_,_,_).
691		constrains_ID_aux(minus(A,B),AllParas,P,P,_,_,[]) :- % TO DO: allow other binary/unary operators ?
692		constrains_ID(A,AllParas,[],[],_,_,_), constrains_ID(B,AllParas,[],[],_,_,_).
693		%constrains_ID_aux(Other,All,P,P,_,_,[]) :- print(other(Other)),nl,fail.
694
695		constrains_ID_fields([],_AllParas,P,P,[],[],[]).
696		constrains_ID_fields([field(Field,Val)|TF],AllParas,Parameters,RestParameters,
697		[field(Field,SkelVal)|TSkelV],[field(Field,SkelUnify)|TSkelU],Bind) :-
698	?	constrains_ID(Val,AllParas,Parameters,Rest1,SkelVal,SkelUnify,Bind1),
699	?	constrains_ID_fields(TF,AllParas,Rest1,RestParameters,TSkelV,TSkelU,Bind2),
700		append(Bind1,Bind2,Bind). % TO DO: use DCGs
701
702		:- use_module(custom_explicit_sets,[efficient_card_for_set/3]).
703
704
705		is_small_set(Val,Size,NormalLimit,SMTLimit,SrcLoc) :-
706		get_small_set_size(Val,Size),
707		is_small_size(Size,NormalLimit,SMTLimit,SrcLoc).
708
709		:- use_module(kernel_card_arithmetic,[safe_mul/3]).
710		:- use_module(kernel_tools,[ground_value/1]).
711		get_small_set_size(value(S),Size) :- !,
712		ground_value(S), % otherwise we could have S=[X] and expand_quantifier will erroneously create multiple solutions for parameter=X
713		efficient_card_for_set(S,Size,C),
714		call(C).
715		get_small_set_size(interval(From,To),Size) :- !,
716		custom_explicit_sets:is_interval_with_integer_bounds(interval(From,To),Low,Up),
717		number(Low), number(Up),
718		(Low > Up -> Size = 1 ; Size is 1+Up-Low).
719		% we provide dom/ran here explicitly as this is often used {i|i:dom(f) ...}
720		get_small_set_size(bool_set,Size) :- !, Size=2.
721		get_small_set_size(domain(b(Val,_,_)),Size) :- !,
722		get_small_domain_set_size(Val,Size). % this is only an upper bound on the size !!
723		get_small_set_size(range(b(Val,_,_)),Size) :- !,
724		get_small_set_size(Val,Size). % this is only an upper bound on the size !!
725		get_small_set_size(cartesian_product(b(A,_,_),b(B,_,_)),Size) :- !,
726		get_small_set_size(A,SizeA), number(SizeA),
727		get_small_set_size(B,SizeB), number(SizeB),
728		safe_mul(SizeA,SizeB,Size), number(Size).
729
730		%get_small_set_size(set_extension(L),Size,_,_,_) :- !, length(L,Size), is_small_size(Size). what if elements itself notknown ?? probably the case as otherwise this would have been compiled into a value
731		%get_small_set_size(sequence_extension(L),Size,_,_,_) :- !, length(L,Size), is_small_size(Size). ditto
732		%get_small_set_size(interval...
733		%get_small_set_size(domain(value([....]))...
734		% for this to work efficiently one should call b_compiler:compile on the predicates before sending them
735		% to b_interpreter_check; otherwise the sets will not yet be in value(_) form
736
737		% TO DO: the same for range or find more principled solution
738		%get_small_domain_set_size(value(S),Size) :- var(S), frozen(S,Frozen), print(var_value(S,Frozen)),nl,fail.
739		get_small_domain_set_size(value(Val),Size) :- nonvar(Val), Val=[H|T],!,
740		efficient_card_for_set([H|T],Size,C),
741		ground_domain([H|T]), % rather than requiring ground of entire list; we only require ground for domain (see test 1272)
742		call(C).
743		get_small_domain_set_size(Val,Size) :-
744		get_small_set_size(Val,Size).
745		ground_domain(V) :- var(V),!,fail.
746		ground_domain([]).
747		ground_domain([H|T]) :-
748		nonvar(H), H=(D,_),
749		ground_value(D), ground_domain(T).
750
751		is_small_size(Size,NormalLimit,SMTLimit,SrcLoc) :- number(Size), %Size \= inf,
752		(Size < NormalLimit -> true
753		; preferences:preference(use_smt_mode,true)
754		-> preference(solver_strength,SS),
755		(Size < SMTLimit + SS
756		-> true
757		; perfmessage(reify,'Not reifiying quantifier, try increasing SOLVER_STRENGTH: ','>'(Size,'+'(SMTLimit,SS)),SrcLoc),
758		fail
759		)
760		; perfmessage(reify,'Not reifiying quantifier, try setting SMT preference: ','>'(Size,limit(NormalLimit)),SrcLoc),
761		fail
762		).
763
764		% -------------------------------------
765		% EXPRESSIONS
766
767		:- use_module(store,[set_up_localstate/4]).
768
769		wd_set_up_localstate_for_let(Ids,Exprs,LocalState,State,LetState,WFD) :-
770		set_up_localstate(Ids,Vars,LocalState,LetState),
771		wd_compute_let_expressions(Exprs,Vars,LetState,State,WFD).
772		wd_compute_let_expressions([],[],_,_,_).
773		wd_compute_let_expressions([Expr|RestExprs],[Var|RestVars],LocalState,State,WFD) :-
774		b_wd_compute_expression(Expr,LocalState,State,Value,WFD),
775		kernel_objects:equal_object_optimized(Var,Value,compute_let_expressions),
776		wd_compute_let_expressions(RestExprs,RestVars,LocalState,State,WFD).
777
778
779		% compute a Prolog list of expressions:
780		b_wd_compute_expressions([], _, _, [],_WFD).
781		b_wd_compute_expressions([EXPRsHd|EXPRsTl],LocalState,State,[ValHd|ValTl],WFD) :-
782	?	b_wd_compute_expression(EXPRsHd,LocalState,State,ValHd,WFD),
783	?	b_wd_compute_expressions(EXPRsTl,LocalState,State,ValTl,WFD).
784
785		% we have to avoid trying to compute certain expressions: evaluation can fail if not well-defined !
786		b_wd_compute_expression(Expr,LocalState,State,Value,wfwd(WF,WDE,WDV,_)) :- !,
787		(nonvar(WDV)
788		-> (WDE==WDV
789		-> % print('REQUIRED: '), translate:print_bexpr(Expr),nl,
790	?	if(b_compute_expression(Expr,LocalState,State,Value,WF), % TO DO: we could use fresh variable for Value
791		true,
792		(kernel_objects:unbound_value(Value), % we have a WD error, if nonvar it could be because we expect a wrong value
793		add_wd_error_span('Well-definedness error evaluating expression: ',Expr,span_predicate(Expr,LocalState,State),WF)
794		%Value = term(undefined),
795		)
796		)
797		; instantiate_to_any_value(Value,Expr,WF))
798		; always_wd_no_fail_nor_error(Expr)
799		-> % print('ALWAYS WD: '), translate:print_bexpr(Expr),nl, %
800	?	b_compute_expression(Expr,LocalState,State,Value,WF)
801	?	; b_compiler:b_optimize(Expr,[],LocalState,State,CExpr,WF),
802		% try compiling; this will inline values and may make the expression well_defined; relevant for test 2013
803		(always_wd_no_fail_nor_error(CExpr)
804		% it is important that this computation cannot fail and cannot raise any errors
805		% an example showing this is :wde f=[2,4] & xx:1..3 & (xx=1 or f(xx-1)=4) with -p TRY_FIND_ABORT TRUE
806		% even though the whole expression is well-defined, the function call f(xx-1) does lead
807		% to an error with xx=1
808		-> b_compute_expression(CExpr,LocalState,State,Value,WF)
809		; % print('DELAYING DUE TO WD: '), translate:print_bexpr(CExpr),nl, %%
810		b_compute_expression_delay(WDE,WDV, CExpr,LocalState,State,Value,WF)
811		)
812		).
813		b_wd_compute_expression(Expr,LocalState,State,Value,WFD) :-
814		add_internal_error('Illegal WFD value: ', b_wd_compute_expression(Expr,LocalState,State,Value,WFD)),fail.
815
816
817		always_wd_no_fail_nor_error(Expr) :-
818		always_well_defined(Expr).
819		% should not use always_well_defined_or_disprover_mode or WD discharged information!
820
821		:- block b_compute_expression_delay(?,-, ?,?,?,?,?).
822		b_compute_expression_delay(WDE,WDV,Expr,LocalState,State,Value,WF) :-
823		(WDE==WDV
824		-> % write('WD Evaluation: '), print(WDE),write(' =?= '), print(WDV), write(' '),translate:print_bexpr(Expr),nl,
825	?	b_compute_expression(Expr,LocalState,State,Value,WF)
826		; %print(instantiate_to_any_value(Value,Expr)),nl,
827		instantiate_to_any_value(Value,Expr,WF) % does not matter anyway; but there can be pending co-routines :-(
828		).
829
830		% WARNING: the variable could be used in another context, where it is relevant !
831
832
833		wd_delay(WDCall,Res, Expr,wfwd(WF,WDExpected,WDV,_)) :-
834		(WDExpected==WDV -> call(WDCall) % WDV truth value on left is ok: we can evaluate
835		; nonvar(WDV) -> instantiate_to_any_value(Res,Expr,WF) % truth value not ok; we do not need the value
836		; always_wd_no_fail_nor_error(Expr) -> call(WDCall)
837		; wd_delay_block(WDCall,Res,Expr,WDExpected,WDV,WF)).
838		:- block wd_delay_block(?,?,?,?,-,?).
839		wd_delay_block(WDCall,Res,Expr,WDExpected,WDV,WF) :-
840		(WDExpected==WDV -> call(WDCall)
841		; instantiate_to_any_value(Res,Expr,WF)).
842
843
844		:- use_module(typing_tools,[any_value_for_type/2]).
845		:- use_module(kernel_tools,[ground_value_check/2]).
846		%instantiate_to_any_value(V,E,_) :- print(instantiate_to_any_value(V)),nl,translate:print_bexpr(E),nl,nl,fail.
847		instantiate_to_any_value(V,_,_) :- ground_value(V),!.
848		instantiate_to_any_value(V,b(_B,TYPE,_I),WF) :-
849		get_enumeration_finished_wait_flag(WF,EWF),
850		ground_value_check(V,GV),
851		blocking_any_value_for_type(EWF,GV,TYPE,V).
852
853		:- block blocking_any_value_for_type(-,-,?,?).
854		blocking_any_value_for_type(_,_,TYPE,V) :- any_value_for_type(TYPE,V). % , print(inst2(TYPE,V)),translate:print_bexpr(b(_B,TYPE,_I)),nl.
855
856
857		:- block propagagate_wfwd(-,?,?,-,?), propagagate_wfwd(?,-,?,-,?).
858		% propagate expected and actual value guarding left with actual predicate value obtained for left
859		propagagate_wfwd(WDE,WDV,Res,F1,F2) :-
860		(F1==F2 -> Res=F1 % then value of WDE does not matter at all; Res always the same
861	?	; propagagate_wfwd2(WDE,WDV,Res,F1,F2)).
862
863		:- block propagagate_wfwd2(-,?,?,?,?), propagagate_wfwd2(?,-,?,?,?).
864		propagagate_wfwd2(WDE,WDV,Res,F1,F2) :- (WDE==WDV -> Res=F1 ; Res=F2).
865
866		:- use_module(external_functions,[external_fun_has_wd_condition/1]).
867		:- use_module(preferences).
868		b_check_boolean_expression4(exists(Parameters,Body),Info,LocalState,State,WFD,OkToStore,Res) :- !,
869		if(b_check_exists_wfwd(Parameters,Body,Info,LocalState,State,WFD,OkToStore,Res),true,
870		(perfmessagecall(reify,cannot_reify_exists(Parameters),translate:print_bexpr(Body),Body),
871		fail)).
872		b_check_boolean_expression4(Pred,Infos,LocalState,State,WFD,ok_to_store,Res) :-
873	?	b_check_boolean_expression4_ok(Pred,Infos,LocalState,State,WFD,Res).
874
875		b_check_boolean_expression4_ok(equal(LHS,RHS),_,LocalState,State,WFD,EqRes) :- !,
876	?	b_wd_compute_expression(LHS,LocalState,State,LHValue,WFD),
877	?	b_wd_compute_expression(RHS,LocalState,State,RHValue,WFD),
878		get_texpr_type(LHS,Type), get_wf(WFD,WF),
879		equality_objects_with_type_wf(Type,LHValue,RHValue,EqRes,WF).
880		% we may need to improve not_member for closure to invert symbolic operators
881		b_check_boolean_expression4_ok(member(LHS,RHS),Info,LocalState,State,WFD,Res) :-
882		%member_check_should_be_reified(LHS,RHS), % no longer need this: symbolic operators will be kept as closures if large ?!
883		!,
884		get_texpr_expr(RHS,ERHS),
885	?	b_check_member_expression(ERHS,RHS,LHS,Info,LocalState,State,WFD,Res).
886		% TO DO: compile forall, exists + setup choice point if expansion fails + remove compile calls in b_interpreter
887		b_check_boolean_expression4_ok(forall(Parameters,LHS,RHS),Info,LocalState,State,WFD,Res) :- !,
888	?	if(b_check_forall_wfwd(Parameters,LHS,RHS,Info,LocalState,State,WFD,Res),true,
889		(perfmessages_bexpr_call(reify,['Cannot reify forall over ', Pids, ': '],LHS,
890		convert_and_ajoin_ids(Parameters,Pids)),
891		fail)).
892		b_check_boolean_expression4_ok(subset(LHS,RHS),_,LocalState,State,WFD,Res) :- !, get_wf(WFD,WF),
893	?	b_wd_compute_expression(LHS,LocalState,State,LHValue,WFD),
894	?	b_wd_compute_expression(RHS,LocalState,State,RHValue,WFD),
895		subset_test(LHValue,RHValue,Res,WF).
896		b_check_boolean_expression4_ok(subset_strict(LHS,RHS),_,LocalState,State,WFD,Res) :- !, get_wf(WFD,WF),
897		b_wd_compute_expression(LHS,LocalState,State,LHValue,WFD),
898		b_wd_compute_expression(RHS,LocalState,State,RHValue,WFD),
899		subset_strict_test(LHValue,RHValue,Res,WF).
900		b_check_boolean_expression4_ok(external_pred_call(FunName,Args),Info,LocalState,State,WFD,Res) :-
901		!,
902		(external_fun_has_wd_condition(FunName)
903		-> wd_delay_until_needed(WFD,b_check_external_pred_call(FunName,Args,Info,LocalState,State,WFD,Res))
904		; b_check_external_pred_call(FunName,Args,Info,LocalState,State,WFD,Res)).
905		b_check_boolean_expression4_ok(freetype_case(FT,IsCase,Expr),_Infos,LocalState,State,WFD,Res) :- !,
906		b_wd_compute_expression(Expr,LocalState,State,freeval(FT,ActualCase,_A),WFD),
907		eq_atomic(IsCase,ActualCase,freeval_case,Res).
908		b_check_boolean_expression4_ok(finite(Expr),_Infos,LocalState,State,WFD,Res) :- !, get_wf(WFD,WF),
909		b_wd_compute_expression(Expr,LocalState,State,ExprVal,WFD),
910		kernel_objects:test_finite_set_wf(ExprVal,Res,WF).
911		b_check_boolean_expression4_ok(partition(Expr,ListOfSets),_Infos,LocalState,State,WFD,Res) :- !, get_wf(WFD,WF),
912		b_wd_compute_expression(Expr,LocalState,State,ExprVal,WFD),
913		b_wd_compute_expressions(ListOfSets,LocalState,State,PartitionList,WFD), % arg is a Prolog list, not a set
914	?	kernel_objects:test_partition_wf(ExprVal,PartitionList,Res,WF).
915		b_check_boolean_expression4_ok(Pred,_,LocalState,State,WFD,Res) :-
916		arithmetic_op(Pred,Op,LHS,RHS),!,
917	?	b_wd_compute_expression(LHS,LocalState,State,int(LHValue),WFD),
918	?	b_wd_compute_expression(RHS,LocalState,State,int(RHValue),WFD),
919		check_arithmetic_operator(Op,LHValue,RHValue,Res).
920		b_check_boolean_expression4_ok(Pred,_,LocalState,State,WFD,Res) :-
921		real_arithmetic_op(Pred,Op,LHS,RHS),!,
922		b_wd_compute_expression(LHS,LocalState,State,LHValue,WFD),
923		b_wd_compute_expression(RHS,LocalState,State,RHValue,WFD),
924		get_wf(WFD,WF),
925		real_comp_wf(Op,LHValue,RHValue,Res,WF).
926		% TO DO ???: use idea of b_artihmetic_expression to avoid intermediate CLPFD variables
927		% TO DO: add other operators, ...
928		/* use_smt_mode = full is never set; at some point we should enable the following clause by default
929		b_check_boolean_expression4_ok(Pred,Infos,LocalState,State,wfwd(WF,WDE,WDV,ContextInfos),Res) :-
930		% preferences:preference(use_smt_mode,full), %% comment out to enable check testing of complicated predicates inside;
931		% caused slowdowns of cbtc/actions_cbtc.mch (test 1751); but no longer the case
932		functor(Pred,F,N),format('~n Cannot reify ~w/~w~n~n',[F,N]),fail,
933		%ContextInfo \= outer_wfwd_context,
934		b_check_boolean_expression4_delay(WDE,WDV,Pred,Infos,LocalState,State,WF,Res).
935		*/
936
937		:- use_module(library(lists),[maplist/3]).
938		% TO DO: add member(,pow_subset, fin_subset) --> subset_test
939		% we could distribute RHS=union -> disjunction, LHS=intersection -> conjunction ,... ?
940		%b_check_member_expression(EHRS,_RHS,_LHS,_,_LocalState,_State,_WFD,_Res) :-
941		% print('member : '), print(EHRS),nl,fail.
942		%b_check_member_expression(union(A,B),LHS,_,LocalState,State,WFD,Res) :-
943		b_check_member_expression(pow_subset(RHS),_,LHS,_Info,LocalState,State,WFD,Res) :- !,
944		b_check_boolean_expression4_ok(subset(LHS,RHS),[],LocalState,State,WFD,Res).
945		%b_check_member_expression(NotContainingEmptySet,_TRHS,LHS,LocalState,State,WFD,Res) :-
946		% non_empty_set_version_of(NotContainingEmptySet,RHS_With_EmptySet),
947		% % translate x:seq1(RHS) -> x /= {} & x:seq(RHS), ...
948		% % this improves propagation, in particular in light of WD issues
949		% % TO DO: avoid computing LHS twice !
950		% !,
951		% get_texpr_type(LHS,LType),
952		% EMPTYVERSION = b(member(LHS,b(RHS_With_EmptySet,set(LType),[])),pred,[]),
953		% NOTEMPTYPRED = b(not_equal(LHS,b(empty_set,LType,[])),pred,[]),
954		% print('Translating : '), translate:print_bexpr(EMPTYVERSION), print(' & '), translate:print_bexpr(NOTEMPTYPRED),nl,
955		% empty_avl(Ai), Infos=[], % Infos not important for conjunction
956		% b_check_boolean_expression2(conjunct(EMPTYVERSION,NOTEMPTYPRED),Infos,LocalState,State,WFD,Res,Ai,_).
957		b_check_member_expression(interval(Low,Up),_,LHS,_Info,LocalState,State,WFD,Res) :- !, get_wf(WFD,WF),
958		% to do: should we also match interval value closure
959		b_wd_compute_expression(LHS,LocalState,State,LHValue,WFD),
960		b_wd_compute_expression(Low,LocalState,State,LowValue,WFD),
961		b_wd_compute_expression(Up,LocalState,State,UpValue,WFD),
962		kernel_objects:test_in_nat_range_wf(LHValue,LowValue,UpValue,Res,WF).
963		b_check_member_expression(set_extension(SetExt),_RHS,LHS,_Info,LocalState,State,WFD,Res) :- !, get_wf(WFD,WF),
964		% rewrite x:{a,b,c} into x=a or x=b or x=c (is the opposite of rewrite_disjunct_to_member)
965		% The rewrite_disjunct_to_member is good when we know a membership to be true; the disjunct is better for reification
966		% Note: the problem is in particular when the result of the membership is not needed and an uninstantiated
967		% variable is used in the set extension, example y:dom(f) => (x:{f(y),0} or f(y)=0)
968		% print(mem_check_set_extension),print(' '),translate:print_bexpr(b(member(LHS,_RHS),pred,[])),nl,
969	?	b_wd_compute_expressions(SetExt,LocalState,State,SetExtValues,WFD),
970		b_wd_compute_expression(LHS,LocalState,State,LHValue,WFD),
971		get_texpr_type(LHS,Type),
972		NewLHS = b(value(LHValue),Type,[]),
973		(ground_value(SetExtValues)
974		-> % better to use normal treatment, we can compute the entire set and translate it into an AVL tree
975		maplist(construct_value(Type),SetExtValues,Vals),
976		b_wd_compute_expression(b(set_extension(Vals),set(Type),[]),LocalState,State,RHValue,WFD),
977		membership_test_wf(RHValue,LHValue,Res,WF),
978		force_membership_test(Res,LHValue,RHValue,WF)
979		; maplist(construct_equality(NewLHS,Type),SetExtValues,Disjuncts),
980		construct_norm_disjunct2(Disjuncts,NC,InfoNC),
981		empty_avl(Ai),
982		b_check_boolean_expression2(NC,InfoNC,LocalState,State,WFD,Res,Ai,_)
983		).
984		b_check_member_expression(closure(Relation),_RHS,LHS,Info,LocalState,State,WFD,Res) :- !, get_wf(WFD,WF),
985		b_wd_compute_expression(LHS,LocalState,State,LHValue,WFD),
986		b_wd_compute_expression(Relation,LocalState,State,RelValue,WFD),
987		opt_push_wait_flag_call_stack_info(WF,b_operator_call(member,
988		[LHValue,b_operator(closure,[RelValue])],Info),WF2), % this is closure1
989	?	bsets_clp:in_closure1_membership_test_wf(LHValue,RelValue,Res,WF2).
990		b_check_member_expression(partial_function(Dom,Range),_RHS,LHS,Info,LocalState,State,WFD,Res) :- !, get_wf(WFD,WF),
991		b_wd_compute_expression(LHS,LocalState,State,LHValue,WFD),
992		b_wd_compute_expression(Dom,LocalState,State,DomValue,WFD),
993		b_wd_compute_expression(Range,LocalState,State,RangeValue,WFD),
994		opt_push_wait_flag_call_stack_info(WF,b_operator_call(member,
995		[LHValue,b_operator(partial_function,[DomValue,RangeValue])],Info),WF2),
996		bsets_clp:partial_function_test_wf(LHValue,DomValue,RangeValue,Res,WF2).
997		b_check_member_expression(total_function(Dom,Range),_RHS,LHS,Info,LocalState,State,WFD,Res) :- !, get_wf(WFD,WF),
998		b_wd_compute_expression(LHS,LocalState,State,LHValue,WFD),
999		b_wd_compute_expression(Dom,LocalState,State,DomValue,WFD),
1000		b_wd_compute_expression(Range,LocalState,State,RangeValue,WFD),
1001		opt_push_wait_flag_call_stack_info(WF,b_operator_call(member,
1002		[LHValue,b_operator(total_function,[DomValue,RangeValue])],Info),WF2),
1003		bsets_clp:total_function_test_wf(LHValue,DomValue,RangeValue,Res,WF2).
1004		b_check_member_expression(partial_surjection(Dom,Range),_RHS,LHS,Info,LocalState,State,WFD,Res) :- !, get_wf(WFD,WF),
1005		b_wd_compute_expression(LHS,LocalState,State,LHValue,WFD),
1006		b_wd_compute_expression(Dom,LocalState,State,DomValue,WFD),
1007		b_wd_compute_expression(Range,LocalState,State,RangeValue,WFD),
1008		opt_push_wait_flag_call_stack_info(WF,b_operator_call(member,
1009		[LHValue,b_operator(partial_surjection,[DomValue,RangeValue])],Info),WF2),
1010		bsets_clp:partial_surjection_test_wf(LHValue,DomValue,RangeValue,Res,WF2).
1011		b_check_member_expression(seq1(SeqType),_RHS,LHS,Info,LocalState,State,WFD,Res) :- !, get_wf(WFD,WF),
1012	?	b_wd_compute_expression(LHS,LocalState,State,LHValue,WFD),
1013		b_wd_compute_expression(SeqType,LocalState,State,SeqTValue,WFD),
1014		opt_push_wait_flag_call_stack_info(WF,b_operator_call(member,
1015		[LHValue,b_operator(seq1,[SeqTValue])],Info),WF2),
1016		bsets_clp:test_finite_non_empty_sequence(LHValue,SeqTValue,Res,WF2).
1017		% TODO: more sequence checks seq()
1018		b_check_member_expression(_Arg,RHS,LHS,_Info,LocalState,State,WFD,Res) :- get_wf(WFD,WF),
1019	?	b_wd_compute_expression(LHS,LocalState,State,LHValue,WFD),
1020	?	b_wd_compute_expression(RHS,LocalState,State,RHValue,WFD),
1021		membership_test_wf(RHValue,LHValue,Res,WF),
1022		%(var(Res) -> add_message(reify,member,LHS,_Info) ; true),
1023	?	force_membership_test(Res,LHValue,RHValue,WF).
1024
1025		% -------------------------
1026
1027		% wfwd/4 add information about WD context to a WF store: wfwd(WF_store, ExpectedVal, Val,Infos)
1028		% when Val becomes nonvar: if Val==ExpectedVal we need the value of E, otherwise it should be discarded
1029
1030		% get WF store from WFD record
1031		get_wf(wfwd(WF,_,_,_),Res) :- !, Res=WF.
1032		get_wf(WFD,WF) :- add_internal_error('Illegal WFD store: ',get_wf(WFD,WF)),
1033		WF = no_wf_available.
1034
1035		% get expected PredicateResult and actual value; if both identical the associated expression is needed
1036		get_wd(wfwd(_,WDExpected,WDVal,_),WDE,WDV) :- !, (WDExpected,WDVal)=(WDE,WDV).
1037		get_wd(WFWD,WDE,WDV) :- add_internal_error('Illegal WFWD info:',get_wd(WFWD,WDE,WDV)), WDE=pred_true,WDV=pred_true.
1038
1039		% create a WFWF construct for an expression that is needed and where reification should only succeed
1040		% if the top-level construct at least can be fully reified (without non-determinism)
1041		create_wfwd_needed(WF,wfwd(WF,pred_true,pred_true,outer_wfwd_context)).
1042
1043		create_wfwd(WF,WDExpected,WDVal,wfwd(WF,WDExpected,WDVal,inner_wfwd_context)).
1044
1045		:- public portray_wfwd/1.
1046		portray_wfwd(wfwd(_,WDExpected,WDVal,Ctxt)) :-
1047		format('Sub-formula required if ~w is expected ~w (ctxt: ~w)~n',[WDVal,WDExpected,Ctxt]).
1048
1049		% ----------------------
1050
1051		construct_value(Type,Val,b(value(Val),Type,[])).
1052
1053		:- use_module(bsyntaxtree, [safe_create_texpr/3]).
1054		construct_equality(NewLHS,Type,ElementV,Equality) :-
1055		Element = b(value(ElementV),Type,[]),
1056		safe_create_texpr(equal(NewLHS,Element),pred,Equality). %, translate:print_bexpr(Equality),nl.
1057
1058		%non_empty_set_version_of(seq1(RHS),seq(RHS)).
1059		%non_empty_set_version_of(iseq1(RHS),iseq(RHS)).
1060		%non_empty_set_version_of(fin1_subset(RHS),fin_subset(RHS)).
1061		%non_empty_set_version_of(pow1_subset(RHS),pow_subset(RHS)).
1062
1063		% check a boolean expression without reification attempt: wait until result is known or waitflag triggered
1064		% can be useful for predicates which we know cannot be reified
1065		b_force_check_boolean_expression(b(Pred,pred,Infos),LocalState,State,WF,Res) :-
1066		b_check_boolean_expression4_delay(pred_true,pred_true,Pred,Infos,LocalState,State,WF,Res).
1067
1068		:- block b_check_boolean_expression4_delay(?,-,?,?,?,?,?,?).
1069		% currently only used for existential quantified predicates in data_validation_mode
1070		b_check_boolean_expression4_delay(WDE,WDV,_Pred,_Infos,_,_,_WF,Res) :- WDE \= WDV,
1071		% no need to check reify_inner_exists_non_deterministically, as we have marked _Pred as do_not_store
1072		% ignoring (not evaluating) predicate
1073		!,
1074		Res=pred_false. % does not matter here (but Res could have been in another context, see above and test 2404)
1075		b_check_boolean_expression4_delay(_WDE,_WDV,Pred,Infos,LocalState,State,WF,Res) :-
1076		% we currently have not yet implemented a way to check the Pred; wait until Result is known
1077		(preferences:preference(use_smt_mode,false)
1078		-> get_last_wait_flag(b_check_test_boolean_expression,WF,WF2)
1079		; get_binary_choice_wait_flag(b_check_test_boolean_expression,WF,WF2)
1080		),
1081		(debug_level_active_for(19) -> print(' Check Testing: '),translate:print_bexpr(Pred),nl ; true),
1082		b_check_test_boolean_expression(Res,WF2,b(Pred,pred,Infos),LocalState,State,WF).
1083
1084		:- block b_check_test_boolean_expression(-,-,?,?,?,?).
1085		%b_check_test_boolean_expression(P,LWF,Pred,LocalState,State,WF) :- write(check_test4(P,LWF)),nl,fail.
1086		b_check_test_boolean_expression(pred_true,_,Pred,LocalState,State,WF) :-
1087		b_test_boolean_expression(Pred,LocalState,State,WF).
1088		b_check_test_boolean_expression(pred_false,_,Pred,LocalState,State,WF) :-
1089	?	b_interpreter:b_not_test_boolean_expression(Pred,LocalState,State,WF).
1090
1091
1092		/*
1093		:- use_module(kernel_mappings).
1094		member_check_should_be_reified(_,b(RHS,_,_)) :- functor(RHS,BOP,Arity), print(check(BOP,Arity)),nl,!.
1095		member_check_should_be_reified(_,_) :- \+ preferences:preference(use_smt_mode,false),!.
1096		member_check_should_be_reified(_LHS,b(RHS,_,_)) :- functor(RHS,BOP,Arity),
1097		% check if we have optimized treatments available, for which we do not yet have reified versions
1098		(Arity=1 -> \+ kernel_mappings:unary_in_boolean_type(BOP,_)
1099		; Arity=2 -> \+ kernel_mappings:binary_in_boolean_type(BOP,_)
1100		; Arity=0 -> \+ kernel_mappings:cst_in_boolean_type(BOP,_)
1101		; true).
1102		*/
1103
1104
1105		:- block force_membership_test(-,?,?,?).
1106		% currently required for ensuring that following fails:
1107		% kernel_objects:union(closure(['_zzzz_unit_tests'],[integer],b(member(b(identifier('_zzzz_unit_tests'),integer,[generated]),b(value([int(3),int(4)]),set(integer),[])),pred,[])),closure(['_zzzz_unit_tests'],[integer],b(member(b(identifier('_zzzz_unit_tests'),integer,[generated]),b(value([int(2),int(1)]),set(integer),[])),pred,[])),[int(1),int(3),int(2)])
1108		% Reason: membership_test does not on its own enumerate
1109		force_membership_test(pred_true,X,Set,WF) :-
1110		Set \= [],
1111		(ground_value(X) -> true
1112		; nonvar(Set),no_use_forcing(Set) -> true % no use in forcing membership, will call same element_of_avl_set_wf
1113	?	; kernel_objects:check_element_of_wf(X,Set,WF)
1114		).
1115		force_membership_test(pred_false,_X,_Set,_WF).
1116
1117		% forcing is sometimes useful because we can transmit a WF, currently some of the reification predicates
1118		% do not have a WF-Store and can thus do limited enumeration ! in particular true for CLPFD = FALSE mode
1119		no_use_forcing(avl_set(_)) :- preferences:preference(use_clpfd_solver,true).
1120		no_use_forcing(global_set(_)).
1121		%no_use_forcing(closure(_,_,B)) :- preferences:preference(use_clpfd_solver,true).
1122
1123
1124
1125		:- use_module(external_functions,[call_external_predicate/8, do_not_evaluate_args/1]).
1126		b_check_external_pred_call(FunName,Args,Info,LocalState,State,WFD,Res) :-
1127		get_wf(WFD,WF),
1128		(do_not_evaluate_args(FunName) -> EvaluatedArgs=[]
1129		; b_wd_compute_expressions(Args, LocalState,State, EvaluatedArgs, WFD)),
1130		push_wait_flag_call_stack_info(WF,external_call(FunName,EvaluatedArgs,Info),WF2),
1131		call_external_predicate(FunName,Args,EvaluatedArgs,LocalState,State,Res,Info,WF2).
1132
1133		wd_delay_until_needed(WFWD,Call) :-
1134		get_wd(WFWD,WDExpected,WDV),
1135		wd_delay_until_needed_block(WDExpected,WDV,Call).
1136		:- block wd_delay_until_needed_block(-,?,?), wd_delay_until_needed_block(?,-,?).
1137		wd_delay_until_needed_block(WDExpected,WDV,Call) :- WDExpected==WDV,!,
1138		call(Call).
1139		wd_delay_until_needed_block(_,_,_). % first call not needed
1140
1141
1142		:- use_module(library(avl)).
1143		reuse_predicate(_,_,no_avl) :- !,fail.
1144		reuse_predicate(Pred,Var,AVL) :-
1145		avl_fetch(Pred,AVL,Var),!. %pred_var(Var)).
1146		reuse_predicate(Pred,Var,AVL) :- %print(check(Pred)),nl, portray_avl(AVL),nl,
1147		preferences:preference(use_smt_mode,true), % it does not seem very expensive; we could always enable it
1148	?	implied_by(Pred,Val,OtherPred,OVal),
1149		avl_fetch(OtherPred,AVL,OVar), OVar==OVal,!,
1150		%print(reused_due_to_implication(Pred)),nl,nl,
1151		Var=Val.
1152
1153		add_predicate(_Pred,_Var,no_avl,NewAVL) :- !, NewAVL=no_avl.
1154		add_predicate(Pred,Var,AVL,NewAVL) :-
1155		% we could compute terms:term_hash(Pred,H) and add pred(H,Pred) to AVL to avoid comparing terms during avl_fetch
1156		(avl_store(Pred,AVL,Var,NewAVL) -> true ; NewAVL=no_avl). %pred_var(Var),NewAVL).
1157
1158		% detect whether predicate implied by some registered predicate
1159		% detects inconsistency in x:INTEGER & x>y & y>x
1160		% very lightweight propagation also achieved by CHR for less
1161		implied_by(less(A,B),pred_false,less(B,A),pred_true). % A>B => not( A<B ) <=> A>=B
1162		implied_by(subset_strict(A,B),pred_false,subset_strict(B,A),pred_true). % B <<: A => not( A<<:B )
1163		implied_by(subset_strict(A,B),pred_false,subset(B,A),pred_true). % B <: A => not( A<<:B )
1164		implied_by(subset(A,B),pred_false,subset_strict(B,A),pred_true). % B <<: A => not( A<:B )
1165		% TO DO: add more rules; e.g., less(x,10) implied by less(x,9)
1166
1167		% normalises a typed predicate by removing position information and ordering commutative operators in a canonical way
1168		norm_pred_check(B,Res) :-
1169		( norm_pred(B,Res)
1170		-> true
1171		; bget_functor(B,F,N),
1172		print(norm_pred_failed(F/N)), nl,
1173		print_bexpr(B), nl,
1174		Res=B
1175		).
1176
1177		bget_functor(b(B,_,_),F,N) :- functor(B,F,N).
1178		bget_functor(B,F,N) :- functor(B,F,N).
1179
1180		%% :-(+List, -UntypedConj).
1181		conjunct_untyped([], Res) :- !, Res=truth.
1182		conjunct_untyped([P|Rest],Result) :- conjunct2(Rest,P,Result).
1183		conjunct2([],P,P).
1184		conjunct2([Q|Rest],P,Result) :- conjunct2(Rest,conjunct(P,Q),Result).
1185
1186		%% disjunct_untyped(+List, -UntypedDisj).
1187		disjunct_untyped([], Res) :- !, Res=falsity.
1188		disjunct_untyped([P|Rest],Result) :- disjunct2(Rest,P,Result).
1189		disjunct2([],P,P).
1190		disjunct2([Q|Rest],P,Result) :- disjunct2(Rest,disjunct(P,Q),Result).
1191
1192		:- assert_must_succeed((I=b(identifier(i),integer,[]),P1=b(greater_equal(I,I),pred,[]),norm_pred(P1,N1),
1193		P2=b(greater_equal(I,I),pred,[info]),norm_pred(P2,N2), N2==N1)). % info ignored
1194		:- assert_must_succeed((I1=b(identifier(i1),integer,[]),I2=b(identifier(i2),integer,[]),
1195		P1=b(equal(I1,I2),pred,[]),norm_pred(P1,N1),
1196		P2=b(equal(I2,I1),pred,[info]),norm_pred(P2,N2), N2==N1)). % equal re-ordered
1197		:- assert_must_succeed((I1=b(identifier(i1),integer,[]),I2=b(identifier(i2),integer,[]),
1198		P1=b(greater_equal(I1,I2),pred,[]),norm_pred(P1,N1),
1199		P2=b(less_equal(I2,I1),pred,[info]),norm_pred(P2,N2), N2==N1)). % <= and >= re-ordered
1200		:- assert_must_succeed((I1=b(identifier(i1),integer,[]),I2=b(identifier(i2),integer,[]),
1201		P1=b(greater(I1,I2),pred,[]),norm_pred(P1,N1),
1202		P2=b(less(I2,I1),pred,[info]),norm_pred(P2,N2), N2==N1)). % < and > re-ordered
1203		:- assert_must_succeed((I1=b(identifier(i1),integer,[]),I2=b(identifier(i2),integer,[]),
1204		P1=b(greater(I1,I2),pred,[]),norm_pred(P1,N1),
1205		P2=b(less_equal(I2,I1),pred,[]),norm_pred(P2,N2), N2 \= N1)). % > and <= not made equal
1206		:- assert_must_succeed((I=b(identifier(i),integer,[]),P1=b(greater_equal(I,I),pred,[was(test1)]),
1207		P2=b(not_equal(I,I),pred,[was(test2)]),
1208		conjunct_predicates_with_pos_info([P1,P2],C1),norm_pred(C1,N1),
1209		conjunct_predicates_with_pos_info([P2,P1],C2),norm_pred(C2,N2), N2==N1)). % conjunct re-ordered
1210		:- assert_must_succeed((I=b(identifier(i),integer,[]),P1=b(greater_equal(I,I),pred,[was(test1)]),
1211		P2=b(not_equal(I,I),pred,[was(test2)]), P3=b(equal(I,I),pred,[was(test3)]),
1212		conjunct_predicates_with_pos_info([P1,P2,P3],C1),norm_pred(C1,N1),
1213		conjunct_predicates_with_pos_info([P2,P3,P1],C2),norm_pred(C2,N2), N2==N1)).
1214
1215		%% norm_pred(+AstOrExpr, -Norm).
1216		norm_pred(X,Res) :- var(X),!,Res=X.
1217		norm_pred(b(B,_,_),Res) :- !, norm_pred(B,Res).
1218		norm_pred(falsity,Res) :- !, Res=falsity.
1219		norm_pred(truth,Res) :- !, Res=truth.
1220		norm_pred(conjunct(A,B),Res) :-
1221		!,
1222		flatten_conjunctions([A,B],CList),
1223		% sort nested conjunctions and disjunctions instead of only single ones
1224		% e.g., difference for '#i.(i : NATURAL & (i > `max`(self) & num′ = num <+ {self |-> i}))' if removing nested parentheses
1225		l_norm_pred(CList, NormedList),
1226		sort(NormedList,SortedList), % better to sort after normalisation
1227		conjunct_untyped(SortedList, Res).
1228		norm_pred(disjunct(A,B),Res) :-
1229		!,
1230		disjunction_to_list(b(disjunct(A,B),pred,[]), CList), % it would be more efficient not to re-construct the b/3 term
1231		l_norm_pred(CList, NormedList),
1232		sort(NormedList,SortedList),
1233		disjunct_untyped(SortedList, Res).
1234		norm_pred(equal(A,B),Res) :- !,norm_expr(A,AA),norm_expr(B,BB),
1235		(BB @< AA -> Res = equal(AA,BB) ; Res= equal(BB,AA)).
1236		norm_pred(equivalence(A,B),Res) :- !, norm_pred(A,AA), norm_pred(B,BB),
1237		(BB @< AA -> Res = equivalence(AA,BB) ; Res= equivalence(BB,AA)).
1238		norm_pred(exists(A,B),Res) :- !, Res=exists(AA,BB),l_norm_expr(A,AA), norm_pred(B,BB).
1239		norm_pred(finite(A),finite(AA)) :- !,norm_expr(A,AA).
1240		norm_pred(forall(A,B,C),Res) :- !, Res=forall(AA,BB,CC),l_norm_expr(A,AA), norm_pred(B,BB), norm_pred(C,CC).
1241		norm_pred(greater(A,B),Less) :- !,norm_expr(A,AA),norm_expr(B,BB), norm_less(BB,AA,Less).
1242		norm_pred(greater_equal(A,B),Leq) :- !,norm_expr(A,AA),norm_expr(B,BB), norm_less_equal(BB,AA,Leq).
1243		norm_pred(if_predicate(A,B,C),Res) :- !, % we could rewrite this to implications but check ok for WD prover
1244		Res=if_predicate(AA,BB,CC), norm_pred(A,AA), norm_pred(B,BB), norm_pred(C,CC).
1245		norm_pred(implication(A,B),Res) :- !, % we could rewrite this to disjunct(not(A),B); but check ok for WD prover
1246		Res=implication(AA,BB),norm_pred(A,AA), norm_pred(B,BB).
1247		norm_pred(less(A,B),Less) :- !,norm_expr(A,AA),norm_expr(B,BB), norm_less(AA,BB,Less).
1248		norm_pred(less_real(A,B),less_real(AA,BB)) :- !,norm_expr(A,AA),norm_expr(B,BB).
1249		norm_pred(less_equal(A,B),Leq) :- !,norm_expr(A,AA),norm_expr(B,BB), norm_less_equal(AA,BB,Leq).
1250		norm_pred(less_equal_real(A,B),less_equal_real(AA,BB)) :- !,norm_expr(A,AA),norm_expr(B,BB).
1251		norm_pred(let_predicate(A,B,C),Res) :- !,
1252		Res=let_predicate(AA,BB,CC),
1253		l_norm_expr(A,AA), l_norm_expr(B,BB),norm_pred(C,CC).
1254		norm_pred(lazy_let_pred(A,B,C),Res) :- !,
1255		Res = lazy_let_pred(AA,BB,CC),
1256		norm_expr(A,AA),
1257		norm_pred_or_expr(B,BB),norm_pred(C,CC).
1258		norm_pred(lazy_lookup_pred(A),Res) :- !, Res = lazy_lookup_pred(A).
1259		norm_pred(member(A,B),member(AA,BB)) :- !,norm_expr(A,AA),norm_expr(B,BB).
1260		norm_pred(negation(A),Res) :- !,
1261	?	(negate_typed_pred(A,NegA) -> norm_pred(NegA,Res)
1262		; Res=negation(AA), norm_pred(A,AA)).
1263		norm_pred(not_equal(A,B),Res) :- !,norm_expr(A,AA),norm_expr(B,BB),
1264		(BB @< AA -> Res = not_equal(AA,BB) ; Res= not_equal(BB,AA)).
1265		norm_pred(not_member(A,B),not_member(AA,BB)) :- !,norm_expr(A,AA),norm_expr(B,BB).
1266		norm_pred(not_subset(A,B),not_subset(AA,BB)) :- !,norm_expr(A,AA),norm_expr(B,BB).
1267		norm_pred(not_subset_strict(A,B),not_subset_strict(AA,BB)) :- !,norm_expr(A,AA),norm_expr(B,BB).
1268		norm_pred(partition(A,L),partition(AA,LL)) :- !,norm_expr(A,AA),l_norm_expr(L,LL).
1269		norm_pred(subset(A,B),subset(AA,BB)) :- !,norm_expr(A,AA),norm_expr(B,BB).
1270		norm_pred(subset_strict(A,B),subset_strict(AA,BB)) :- !,norm_expr(A,AA),norm_expr(B,BB).
1271		norm_pred(freetype_case(Type,Case,A),freetype_case(Type,Case,AA)) :- !,norm_expr(A,AA).
1272		norm_pred(X,X). % :- print(norm_pred(X)),nl.
1273
1274
1275		l_norm_pred([],[]).
1276		l_norm_pred([H|T],[NH|NT]) :- norm_pred(H,NH), l_norm_pred(T,NT).
1277
1278		norm_pred_or_expr(b(B,pred,_),Res) :- norm_pred(B,Res).
1279		norm_pred_or_expr(B,Res) :- norm_expr(B,Res).
1280
1281	?	norm_less(unary_minus(A),MB,Res) :- apply_unary_minus(MB,B), !,norm_less(B,A,Res). % -A < -B => A > B
1282		% we could also move unary_minus to B if not present
1283		norm_less(MA,unary_minus(B),Res) :- apply_unary_minus(MA,A), !,norm_less(B,A,Res).
1284		norm_less(A,B,less(A,B)).
1285
1286		apply_unary_minus(unary_minus(A),A).
1287		apply_unary_minus(Nr,MNr) :- number(Nr), MNr is -Nr.
1288
1289	?	norm_less_equal(unary_minus(A),MB,Res) :- apply_unary_minus(MB,B), !,norm_less_equal(B,A,Res). % -A <= -B => A >= B
1290		norm_less_equal(MA,unary_minus(B),Res) :- apply_unary_minus(MA,A), !,norm_less_equal(B,A,Res).
1291		norm_less_equal(A,B,less_equal(A,B)).
1292
1293		% ---------------------
1294
1295		% generic normalisation predicate
1296		norm_check(BExpr,Res) :- BExpr = b(_,pred,_),!, norm_pred_check(BExpr,Res).
1297		norm_check(BExpr,Res) :- norm_expr_check(BExpr,Res).
1298
1299		% normalise expressions and check for failure
1300		norm_expr_check(X,Res) :- var(X),!,Res=X.
1301		norm_expr_check(b(B,_,_),Res) :- !, norm_expr_check2(B,Res).
1302		norm_expr_check(X,X).
1303
1304		norm_expr_check2(B,Res) :-
1305		(norm_expr2(B,Res) -> true
1306		; functor(B,F,N),print(norm_expr2_failed(F/N)),nl,
1307		Res=B).
1308
1309		norm_expr(X,Res) :- var(X),!,Res=X.
1310		norm_expr(b(B,_,_),Res) :- !, norm_expr2(B,Res).
1311		%norm_expr_check2(B,Res). %% comment in to obtain details about failed normalisation for expressions
1312		norm_expr(X,X). % :- add_internal_error('Expr not wrapped:',norm_expr(X,X)).
1313
1314		:- use_module(kernel_reals,[construct_real_number/2]).
1315		norm_expr2(assertion_expression(Cond,E,Expr),assertion_expression(AA,E,BB)) :- norm_pred(Cond,AA),norm_expr(Expr,BB).
1316		norm_expr2(add(A,B),Res) :- norm_expr(A,AA), norm_expr(B,BB), (BB @< AA -> Res = add(AA,BB) ; Res= add(BB,AA)).
1317		norm_expr2(add_real(A,B),add_real(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1318		norm_expr2(bag_items(A),bag_items(AA)) :- norm_expr(A,AA).
1319		norm_expr2(boolean_false,boolean_false).
1320		norm_expr2(boolean_true,boolean_true).
1321		norm_expr2(bool_set,bool_set).
1322		norm_expr2(card(A),card(AA)) :- norm_expr(A,AA).
1323		norm_expr2(cartesian_product(A,B),cartesian_product(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1324		norm_expr2(closure(A),closure(AA)) :- norm_expr(A,AA). % this is closure1
1325		norm_expr2(compaction(A),compaction(AA)) :- norm_expr(A,AA).
1326		norm_expr2(composition(A,B),composition(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1327		norm_expr2(comprehension_set(A,B),comprehension_set(AA,BB)) :- l_norm_expr(A,AA), norm_pred(B,BB).
1328		norm_expr2(concat(A,B),concat(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1329		norm_expr2(convert_bool(A),convert_bool(AA)) :- norm_pred_check(A,AA).
1330		norm_expr2(convert_real(A),convert_real(AA)) :- norm_expr(A,AA).
1331		norm_expr2(convert_int_floor(A),convert_int_floor(AA)) :- norm_expr(A,AA).
1332		norm_expr2(convert_int_ceiling(A),convert_int_ceiling(AA)) :- norm_expr(A,AA).
1333		norm_expr2(couple(A,B),couple(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1334		norm_expr2(direct_product(A,B),direct_product(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1335		norm_expr2(div(A,B),div(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1336		norm_expr2(div_real(A,B),div_real(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1337		norm_expr2(floored_div(A,B),floored_div(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1338		norm_expr2(domain_restriction(A,B),domain_restriction(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1339		norm_expr2(domain_subtraction(A,B),domain_subtraction(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1340		norm_expr2(domain(A),domain(AA)) :- norm_expr(A,AA).
1341		norm_expr2(empty_sequence,empty_sequence).
1342		norm_expr2(empty_set,empty_set).
1343		norm_expr2(event_b_identity,event_b_identity).
1344		norm_expr2(external_function_call(A,B),external_function_call(A,BB)) :- l_norm_expr(B,BB).
1345		norm_expr2(fin_subset(A),fin_subset(AA)) :- norm_expr(A,AA).
1346		norm_expr2(fin1_subset(A),fin1_subset(AA)) :- norm_expr(A,AA).
1347		norm_expr2(first(A),first(AA)) :- norm_expr(A,AA).
1348		norm_expr2(first_of_pair(A),first_of_pair(AA)) :- norm_expr(A,AA).
1349		norm_expr2(first_projection(A,B),first_projection(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1350		norm_expr2(float_set,float_set).
1351		norm_expr2(front(A),front(AA)) :- norm_expr(A,AA).
1352		norm_expr2(function(A,B),function(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1353		norm_expr2(general_concat(A),general_concat(AA)) :- norm_expr(A,AA).
1354		norm_expr2(general_intersection(A),general_intersection(AA)) :- norm_expr(A,AA).
1355		norm_expr2(general_product(A,B,C),Res) :- !,
1356		Res=general_product(AA,BB,CC),l_norm_expr(A,AA), norm_pred(B,BB), norm_expr(C,CC).
1357		norm_expr2(general_sum(A,B,C),Res) :- !,
1358		Res=general_sum(AA,BB,CC),l_norm_expr(A,AA), norm_pred(B,BB), norm_expr(C,CC).
1359		norm_expr2(general_union(A),general_union(AA)) :- norm_expr(A,AA).
1360		norm_expr2(identifier(A),'$'(A)). % need wrapper to avoid confusion with other terms !
1361		norm_expr2(identity(A),identity(AA)) :- norm_expr(A,AA).
1362		norm_expr2(if_then_else(P,A,B),if_then_else(PP,AA,BB)) :- norm_pred(P,PP),norm_expr(A,AA), norm_expr(B,BB).
1363		norm_expr2(image(A,B),image(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1364		norm_expr2(insert_front(A,B),insert_front(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1365		norm_expr2(insert_tail(A,B),insert_tail(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1366		norm_expr2(integer_set(A),A).
1367		norm_expr2(integer(A),A). % integer represented as number
1368		norm_expr2(intersection(A,B),Res) :- norm_expr(A,AA), norm_expr(B,BB),
1369		(BB @< AA -> Res = intersection(AA,BB) ; Res= intersection(BB,AA)).
1370		norm_expr2(interval(A,B),interval(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1371		norm_expr2(iseq(A),iseq(AA)) :- norm_expr(A,AA).
1372		norm_expr2(iseq1(A),iseq1(AA)) :- norm_expr(A,AA).
1373		norm_expr2(iteration(A,B),iteration(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1374		norm_expr2(last(A),last(AA)) :- norm_expr(A,AA).
1375		norm_expr2(lazy_let_expr(A,B,C),lazy_let_expr(AA,BB,CC)) :-
1376		norm_expr(A,AA),norm_pred_or_expr(B,BB),norm_expr(C,CC).
1377		norm_expr2(lazy_lookup_expr(A),lazy_lookup_expr(A)) :- !.
1378		norm_expr2(let_expression(A,B,C),let_expression(AA,BB,CC)) :- l_norm_expr(A,AA), l_norm_expr(B,BB),norm_expr(C,CC).
1379		norm_expr2(let_expression_global(A,B,C),let_expression_global(AA,BB,CC)) :- l_norm_expr(A,AA), l_norm_expr(B,BB),norm_pred(C,CC).
1380		norm_expr2(max(A),max(AA)) :- norm_expr(A,AA).
1381		norm_expr2(max_real(A),max_real(AA)) :- norm_expr(A,AA).
1382		norm_expr2(max_int,max_int).
1383		norm_expr2(min(A),min(AA)) :- norm_expr(A,AA).
1384		norm_expr2(min_real(A),min_real(AA)) :- norm_expr(A,AA).
1385		norm_expr2(min_int,min_int).
1386		norm_expr2(minus(A,B),minus(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1387		norm_expr2(minus_or_set_subtract(A,B),minus_or_set_subtract(AA,BB)) :- write(cannot_normalise_minus_or_set_subtract),nl,
1388		norm_expr(A,AA), norm_expr(B,BB). % should have been removed by cleanup_pre !!
1389		norm_expr2(minus_real(A,B),minus_real(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1390		norm_expr2(modulo(A,B),modulo(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1391		norm_expr2(mu(A),mu(AA)) :- norm_expr(A,AA).
1392		norm_expr2(multiplication(A,B),Res) :-
1393		norm_expr(A,AA), norm_expr(B,BB), (BB @< AA -> Res = multiplication(AA,BB) ; Res= multiplication(BB,AA)).
1394		norm_expr2(mult_or_cart(A,B),mult_or_cart(AA,BB)) :- write(cannot_normalise_mult_or_cart),nl,
1395		norm_expr(A,AA), norm_expr(B,BB). % should have been removed by cleanup_pre !!
1396		norm_expr2(multiplication_real(A,B),multiplication_real(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1397		norm_expr2(operation_call_in_expr(A,B),operation_call_in_expr(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1398		norm_expr2(overwrite(A,B),overwrite(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1399		norm_expr2(parallel_product(A,B),parallel_product(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1400		norm_expr2(partial_bijection(A,B),partial_bijection(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1401		norm_expr2(partial_function(A,B),partial_function(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1402		norm_expr2(partial_injection(A,B),partial_injection(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1403		norm_expr2(partial_surjection(A,B),partial_surjection(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1404		norm_expr2(perm(A),perm(AA)) :- norm_expr(A,AA).
1405		norm_expr2(power_of(A,B),power_of(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1406		norm_expr2(power_of_real(A,B),power_of_real(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1407		norm_expr2(pow_subset(A),pow_subset(AA)) :- norm_expr(A,AA).
1408		norm_expr2(pow1_subset(A),pow1_subset(AA)) :- norm_expr(A,AA).
1409		norm_expr2(predecessor,predecessor).
1410		% quantified_intersection, quantified_union : should be removed by ast_cleanup
1411		norm_expr2(range_restriction(A,B),range_restriction(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1412		norm_expr2(range_subtraction(A,B),range_subtraction(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1413		norm_expr2(range(A),range(AA)) :- norm_expr(A,AA).
1414		norm_expr2(real(Atom),Nr) :- construct_real_number(Atom,Nr).
1415		norm_expr2(real_set,real_set).
1416		norm_expr2(rec(A),rec(AA)) :- norm_fields(A,AA).
1417		norm_expr2(record_field(A,Field),record_field(AA,Field)) :- norm_expr(A,AA).
1418		norm_expr2(relations(A,B),relations(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1419		norm_expr2(restrict_front(A,B),restrict_front(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1420		norm_expr2(restrict_tail(A,B),restrict_tail(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1421		norm_expr2(reflexive_closure(A),reflexive_closure(AA)) :- norm_expr(A,AA). % this is rewritten in ast_cleanup
1422		norm_expr2(rev(A),rev(AA)) :- norm_expr(A,AA).
1423		norm_expr2(reverse(A),reverse(AA)) :- norm_expr(A,AA).
1424		norm_expr2(second_of_pair(A),second_of_pair(AA)) :- norm_expr(A,AA).
1425		norm_expr2(second_projection(A,B),second_projection(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1426		norm_expr2(seq(A),seq(AA)) :- norm_expr(A,AA).
1427		norm_expr2(seq1(A),seq1(AA)) :- norm_expr(A,AA).
1428		norm_expr2(sequence_extension(L),sequence_extension(NL)) :- l_norm_expr(L,NL).
1429		norm_expr2(set_extension(L),set_extension(NL)) :- l_norm_expr(L,NL).
1430		norm_expr2(set_subtraction(A,B),set_subtraction(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB). % set difference
1431		norm_expr2(size(A),size(AA)) :- norm_expr(A,AA).
1432		norm_expr2(string(A),string(A)). % need wrapper to avoid confusion with other terms !
1433		norm_expr2(string_set,string_set).
1434		norm_expr2(struct(A),struct(AA)) :- norm_expr(A,AA).
1435		norm_expr2(successor,successor).
1436		norm_expr2(surjection_relation(A,B),surjection_relation(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1437		norm_expr2(tail(A),tail(AA)) :- norm_expr(A,AA).
1438		norm_expr2(total_bijection(A,B),total_bijection(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1439		norm_expr2(total_function(A,B),total_function(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1440		norm_expr2(total_injection(A,B),total_injection(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1441		norm_expr2(total_relation(A,B),total_relation(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1442		norm_expr2(total_surjection(A,B),total_surjection(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1443		norm_expr2(total_surjection_relation(A,B),total_surjection_relation(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1444		norm_expr2(typeof(A,B),Res) :- norm_expr(A,AA),
1445		(wrap_with_typeof(AA) -> (norm_expr(B,BB), Res = typeof(AA,BB)) ; Res = AA).
1446		norm_expr2(typeset,typeset).
1447
1448		norm_expr2(unary_minus(A),unary_minus(AA)) :- norm_expr(A,AA).
1449		norm_expr2(unary_minus_real(A),unary_minus_real(AA)) :- norm_expr(A,AA).
1450		norm_expr2(union(A,B),Res) :- norm_expr(A,AA), norm_expr(B,BB), (BB @< AA -> Res = union(AA,BB) ; Res= union(BB,AA)).
1451		norm_expr2(value(A),NA) :- norm_value(A,NA).
1452
1453		norm_expr2(freetype_set(T),freetype_set(T)).
1454		norm_expr2(freetype_constructor(FT,Case,A), freetype_constructor(FT,Case,AA)) :- norm_expr(A,AA).
1455		norm_expr2(freetype_destructor(FT,Case,A),freetype_destructor(FT,Case,AA)) :- norm_expr(A,AA).
1456		norm_expr2(recursive_let(A,B),recursive_let(AA,BB)) :- norm_expr(A,AA),norm_expr(B,BB).
1457
1458		% needed if ast_cleanup and replacements were not performed
1459		norm_expr2(event_b_comprehension_set(A,B,C),event_b_comprehension_set(AA,BB,CC)) :- l_norm_expr(A,AA), norm_expr(B,BB), norm_pred(C,CC).
1460		norm_expr2(event_b_first_projection_v2,event_b_first_projection_v2).
1461		norm_expr2(event_b_second_projection_v2,event_b_second_projection_v2).
1462		norm_expr2(quantified_intersection(A,B,C),quantified_intersection(AA,BB,CC)) :- l_norm_expr(A,AA), norm_pred(B,BB), norm_expr(C,CC).
1463		norm_expr2(quantified_union(A,B,C),quantified_union(AA,BB,CC)) :- l_norm_expr(A,AA), norm_pred(B,BB), norm_expr(C,CC).
1464		norm_expr2(ring(A,B),ring(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1465
1466		wrap_with_typeof(event_b_first_projection_v2).
1467		wrap_with_typeof(event_b_identity).
1468		wrap_with_typeof(event_b_second_projection_v2).
1469
1470		norm_fields([],[]).
1471		norm_fields([field(Name,H)|T],[field(Name,NH)|NT]) :- norm_expr(H,NH), norm_fields(T,NT).
1472
1473		l_norm_expr([],[]).
1474		l_norm_expr([H|T],[NH|NT]) :- norm_expr(H,NH), l_norm_expr(T,NT).
1475
1476		:- use_module(closures,[is_member_closure/5]).
1477		norm_value(V,R) :- var(V),!,R=value(V).
1478		norm_value(int(Nr),R) :- integer(Nr),!,R=Nr.
1479		norm_value(term(F),R) :- nonvar(F),F=floating(Nr),number(Nr),!,R=Nr.
1480		norm_value([],R) :- !, R=empty_set.
1481		norm_value(pred_false,R) :- !, R=boolean_false.
1482		norm_value(pred_true,R) :- !, R=boolean_true.
1483		norm_value(closure(P,T,B),R) :-
1484		(is_member_closure(P,T,B,_,Set) % peel useless member closure wrapper, see test 2483
1485		-> !, norm_expr_check2(Set,R)
1486		; norm_pred_check(B,NB)
1487		-> !, % normalising relevant for test 1544 with position info added by construct_member_closure
1488		R=value(closure(P,T,NB))
1489		).
1490		norm_value((A,B),R) :- !, R=(NA,NB), norm_value(A,NA), norm_value(B,NB).
1491		norm_value(rec(Fields),rec(NFields)) :- !, norm_field_values(Fields,NFields).
1492		norm_value(V,value(V)). % we could normalise AVL, or pairs
1493
1494		norm_field_values([],[]).
1495		norm_field_values([field(Name,H)|T],[field(Name,NH)|NT]) :- norm_inner_value(H,NH), norm_field_values(T,NT).
1496
1497		% norm inside values; e.g., getting rid of info fields of closures, see test 2483
1498		norm_inner_value((A,B),R) :- !, R=(NA,NB), norm_inner_value(A,NA), norm_inner_value(B,NB).
1499		norm_inner_value(rec(Fields),rec(NFields)) :- !, norm_field_values(Fields,NFields).
1500		norm_inner_value(closure(P,T,B),R) :- norm_pred_check(B,NB),!,
1501		R=closure(P,T,NB).
1502		% TODO: inside sets ? but AVL sets contain no closures
1503		norm_inner_value(V,V).
1504
1505
1506		arithmetic_op(less(LHS,RHS),'<',LHS,RHS).
1507		arithmetic_op(less_equal(LHS,RHS),'<=',LHS,RHS).
1508		arithmetic_op(greater(LHS,RHS),'<',RHS,LHS).
1509		arithmetic_op(greater_equal(LHS,RHS),'<=',RHS,LHS).
1510
1511		:- use_module(probsrc(kernel_reals),[real_comp_wf/5]).
1512		% these two predicates can be checked by real_comp_wf:
1513		real_arithmetic_op(less_real(LHS,RHS),'<',LHS,RHS).
1514		real_arithmetic_op(less_equal_real(LHS,RHS),'=<',LHS,RHS).
1515
1516		:- use_module(clpfd_interface).
1517		:- use_module(library(clpfd), [(#<=>)/2]).
1518		check_arithmetic_operator('<',X,Y,Res) :- check_less(X,Y,Res),
1519		(nonvar(Res) -> true
1520		; clpfd_interface:try_post_constraint((X#<Y) #<=> R01), prop_pred_01(Res,R01)).
1521		check_arithmetic_operator('<=',X,Y,Res) :- check_less_than_equal(X,Y,Res),
1522		(nonvar(Res) -> true
1523		; clpfd_interface:try_post_constraint((X#=<Y) #<=> R01), prop_pred_01(Res,R01)).
1524
1525
1526		:- block prop_pred_01(-,-).
1527		prop_pred_01(A,B) :- B==1,!,A=pred_true. % cut ok: either pred_true or 1 set
1528		prop_pred_01(pred_true,1).
1529		prop_pred_01(pred_false,0).
1530
1531		:- block check_less(-,?,-), check_less(?,-,-).
1532		check_less(X,Y,Res) :- nonvar(Res),!, /* truth value known: enforce it */
1533	?	(Res=pred_true -> less_than_direct(X,Y) ; less_than_equal_direct(Y,X)).
1534		check_less(X,Y,Res) :-
1535		X < Y,!,/* we could call safe_less_than(X,Y), */
1536		Res=pred_true.
1537		check_less(_,_,pred_false).
1538		:- block check_less_than_equal(-,?,-), check_less_than_equal(?,-,-).
1539		check_less_than_equal(X,Y,Res) :- nonvar(Res),!, /* truth value known: enforce it */
1540	?	(Res=pred_true -> less_than_equal_direct(X,Y) ; less_than_direct(Y,X)).
1541		check_less_than_equal(X,Y,Res) :- X =< Y,!,Res=pred_true.
1542		check_less_than_equal(_,_,pred_false).
1543
1544
1545
1546		:- use_module(bool_pred).
1547
1548		:- use_module(kernel_objects,[exhaustive_kernel_check_wf/2,
1549		exhaustive_kernel_check/1, exhaustive_kernel_check/2, exhaustive_kernel_fail_check/1]).
1550
1551		:- assert_must_succeed(exhaustive_kernel_check_wf(b_interpreter_check:conjoin(pred_false,pred_false,pred_false,b(truth,pred,[]),b(truth,pred,[]),WF),WF)).
1552		:- assert_must_succeed(exhaustive_kernel_check_wf(b_interpreter_check:conjoin(pred_false,pred_true,pred_false,b(truth,pred,[]),b(truth,pred,[]),WF),WF)).
1553		:- assert_must_succeed(exhaustive_kernel_check_wf(b_interpreter_check:conjoin(pred_true,pred_false,pred_false,b(truth,pred,[]),b(truth,pred,[]),WF),WF)).
1554		:- assert_must_succeed(exhaustive_kernel_check_wf(b_interpreter_check:conjoin(pred_true,pred_true,pred_true,b(truth,pred,[]),b(truth,pred,[]),WF),WF)).
1555		:- assert_must_fail(b_interpreter_check:conjoin(pred_true,pred_false,pred_true,b(truth,pred,[]),b(truth,pred,[]),_WF)).
1556		:- assert_must_fail(b_interpreter_check:conjoin(pred_true,pred_true,pred_false,b(truth,pred,[]),b(truth,pred,[]),_WF)).
1557
1558
1559		% same as and_equality/3 but for pred_false/pred_true rather than eq_obj/pred_false
1560		:- block conjoin(-,-,-,?,?,?).
1561		conjoin(X,Y,Res,LHS,RHS,WF) :- % print(conjoin(X,Y,Res)),nl, translate:print_bexpr(LHS),nl,%
1562		( Res==pred_true -> X=pred_true,Y=pred_true % on SWI these propagations happen one after the other, see test 2202
1563		; X==pred_true -> Res=Y
1564		; X==pred_false -> Res=pred_false
1565		; Y==pred_true -> Res=X
1566		; Y==pred_false -> Res=pred_false
1567	?	; Res==pred_false -> conjoin_false0(X,Y,LHS,RHS,WF)
1568		; add_error_fail(conjoin,'Illegal values: ', conjoin(X,Y,Res,LHS,RHS,WF))
1569		).
1570		conjoin_false0(X,Y,_LHS,_RHS,_WF) :- X==Y,!,
1571		%print(conjoin_false_eqeq(X,Y)),nl, translate:print_bexpr(_LHS),nl,
1572		X=pred_false.
1573		conjoin_false0(X,Y,_LHS,_RHS,_WF) :- % X & not(X) -> always false
1574		bool_negate_check(X,Y),!
1575		. %,print(conjoin_false_neqeq(X,Y)),nl,translate:print_bexpr(_LHS),nl.
1576		conjoin_false0(X,Y,LHS,RHS,WF) :-
1577		%%Prio=1, %%
1578		%%(preferences:preference(use_smt_mode,full) -> FullPrio=1.5 ;
1579		get_priority_of_boolean_expression(LHS,Prio),
1580		(preferences:preference(use_clpfd_solver,true) ->
1581		% relevant for tests 349, 362:
1582		count_number_of_conjuncts(RHS,NrC),
1583		FullPrio is Prio+(NrC-1)/10,
1584		get_wait_flag(FullPrio,conjoin,WF,LWF) %%
1585		; % in non-clpfd mode: much less propagation going on, avoid explosion of choice points
1586		% tests 349, 362 fail with the following for CLPFD: TO DO investigate and use this also in CLPFD mode
1587		get_binary_choice_wait_flag_exp_backoff(Prio,not_conjunct,WF,LWF)
1588		),
1589	?	conjoin_false(X,Y,LHS,RHS,LWF).
1590		% missing rule: if X==Y -> X=pred_true
1591		:- block conjoin_false(-,-,?,?,-).
1592		conjoin_false(X,Y,LHS,_RHS,_LWF) :-
1593		( X==pred_true -> pred_false=Y
1594		; X==pred_false -> true
1595		; Y==pred_true -> pred_false=X
1596		; Y==pred_false -> true
1597		; useless_to_force(LHS) ->
1598		( % print(forcing_conjoin_rhs_false(X,Y,_LWF)), translate:print_bexpr(_RHS), print(' == FALSE '),nl,
1599		Y=pred_false
1600		;
1601		(Y,X)=(pred_true,pred_false)
1602		)
1603		; ( % print(forcing_conjoin_lhs_false(X,Y,_LWF)), translate:print_bexpr(LHS), print(' == FALSE '),nl,
1604		X=pred_false
1605		; % print(forcing_conjoin_rhs_false(X,Y,_LWF)), translate:print_bexpr(LHS), print(' == TRUE ; '), nl,
1606		(X,Y)=(pred_true,pred_false)
1607		)
1608		).
1609
1610		% determine when forcing a predicate to true/false does not really help; better choose something else
1611		useless_to_force(b(B,T,I)) :- useless_to_force3(B,T,I).
1612		useless_to_force3(finite(_),_,_). % forcing finite to be false usually not a good idea; we cannot propagate this
1613		% what are other predicates useless to force: some foralls/exists ? some external_pred_call
1614		% in principle a conjunction of useless predicates is also useless: but could be more expensive to check
1615
1616		:- assert_must_succeed(exhaustive_kernel_check(b_interpreter_check:disjoin(pred_false,pred_false,pred_false,_,_,_WF))).
1617		:- assert_must_succeed(exhaustive_kernel_check([commutative],b_interpreter_check:disjoin(pred_false,pred_true,pred_true,_,_,_WF))).
1618		:- assert_must_succeed(exhaustive_kernel_check(b_interpreter_check:disjoin(pred_true,pred_true,pred_true,_,_,_WF))).
1619		:- assert_must_succeed(exhaustive_kernel_fail_check(b_interpreter_check:disjoin(pred_true,pred_true,pred_false,_,_,_WF))).
1620		:- assert_must_succeed(exhaustive_kernel_fail_check(b_interpreter_check:disjoin(pred_true,pred_false,pred_false,_,_,_WF))).
1621		:- assert_must_succeed(exhaustive_kernel_fail_check(b_interpreter_check:disjoin(pred_false,pred_true,pred_false,_,_,_WF))).
1622		:- assert_must_succeed(exhaustive_kernel_fail_check(b_interpreter_check:disjoin(pred_false,pred_false,pred_true,_,_,_WF))).
1623
1624		:- block disjoin(-,-,-,?,?,?).
1625		disjoin(X,Y,Res,LHS,RHS,WF) :-
1626		%print(disjoin(X,Y,Res,WF)),nl, %% translate:print_bexpr(LHS),print(' or '),translate:print_bexpr(RHS),nl,%%
1627		( Res==pred_false -> X=pred_false,Y=pred_false
1628		; X==pred_true -> Res=pred_true
1629		; X==pred_false -> Res=Y
1630		; Y==pred_true -> Res=pred_true
1631		; Y==pred_false -> Res=X
1632	?	; Res==pred_true -> disjoin_true0(X,Y,LHS,RHS,WF)
1633		; add_error_fail(disjoin,'Illegal values: ',disjoin(X,Y,Res,LHS,RHS,WF))
1634		).
1635		disjoin_true0(X,Y,_LHS,_RHS,_WF) :- X==Y,!,
1636		X=pred_true.
1637		%disjoin_true0(X,Y,LHS,_,WF) :- !, disjoin_true(X,Y,_).
1638		disjoin_true0(X,Y,_LHS,_RHS,_WF) :- % X or not(X) -> always true
1639		bool_negate_check(X,Y),!.
1640
1641		disjoin_true0(X,Y,LHS,_RHS,WF) :-
1642		%%(preferences:preference(use_smt_mode,full) -> FullPrio=2.5 ;
1643		% poses problem for test 1096:
1644		% count_number_of_disjuncts(RHS,NrC),
1645		%FullPrio is Prio+(NrC-1)/10,
1646		%get_wait_flag(FullPrio,disjoin,WF,LWF), %%
1647		get_priority_of_boolean_expression(LHS,StartPrio),
1648		get_binary_choice_wait_flag_exp_backoff(StartPrio,disjunct,WF,LWF),
1649		% TO DO: extract FD information from LHS and RHS and assert, e.g. x:1..2 or x:4..5
1650	?	disjoin_true(X,Y,LHS,LWF).
1651		% missing rule: if X==Y -> X=pred_true ; if X==~Y -> no need to setup choice point
1652		:- block disjoin_true(-,-,?,-).
1653		disjoin_true(X,Y,LHS,_LWF) :-
1654		( X==pred_true -> true
1655		; X==pred_false -> pred_true=Y
1656		; Y==pred_true -> true
1657		; Y==pred_false -> pred_true=X
1658		; useless_to_force(LHS) ->
1659		( %% print(forcing_disjoin_true(X,Y,_LWF)),nl, %%
1660		Y=pred_true
1661		;
1662		%%print(forcing_disjoin_false(X,Y,_LWF)),nl,
1663		(Y,X) = (pred_false,pred_true) % these two unifications will happen atomically !
1664		)
1665		; ( %% print(forcing_disjoin_true(X,Y,_LWF)),nl, %%
1666		X=pred_true
1667		;
1668		%%print(forcing_disjoin_false(X,Y,_LWF)),nl,
1669		(X,Y) = (pred_false,pred_true) % these two unifications will happen atomically !
1670		)
1671		%add_error_fail(disjoin_true,'Illegal values: ',disjoin_true(X,Y))
1672		).
1673
1674		:- assert_must_succeed(exhaustive_kernel_check(b_interpreter_check:imply(pred_false,pred_false,pred_true))).
1675		:- assert_must_succeed(exhaustive_kernel_check(b_interpreter_check:imply(pred_false,pred_true,pred_true))).
1676		:- assert_must_succeed(exhaustive_kernel_check(b_interpreter_check:imply(pred_true,pred_false,pred_false))).
1677		:- assert_must_succeed(exhaustive_kernel_check(b_interpreter_check:imply(pred_true,pred_true,pred_true))).
1678		:- assert_must_succeed(exhaustive_kernel_fail_check(b_interpreter_check:imply(pred_false,pred_false,pred_false))).
1679		:- assert_must_succeed(exhaustive_kernel_fail_check(b_interpreter_check:imply(pred_false,pred_true,pred_false))).
1680		:- assert_must_succeed(exhaustive_kernel_fail_check(b_interpreter_check:imply(pred_true,pred_false,pred_true))).
1681		:- assert_must_succeed(exhaustive_kernel_fail_check(b_interpreter_check:imply(pred_true,pred_true,pred_false))).
1682
1683		imply(X,Y,Res) :-
1684		(var(X),var(Y),var(Res) -> bool_equality(X,Y,EqXY) ; true /* impl4 will not block anyway */),
1685		impl4(X,Y,EqXY,Res).
1686		:- block impl4(-,-,-,-).
1687		impl4(X,Y,EqXY,Res) :-
1688		( Res==pred_false -> X=pred_true,Y=pred_false
1689		; Res==pred_true -> imply_true3(X,Y,EqXY)
1690		; X==pred_false -> Res=pred_true
1691		; X==pred_true -> Res=Y
1692		; Y==pred_true -> Res=pred_true
1693		; Y==pred_false -> negate(X,Res)
1694		; EqXY==pred_true -> Res=pred_true % X => X is always true
1695		; EqXY==pred_false -> Y=Res % not(Y) => Y is true iff Y is true
1696		; add_error_fail(impl,'Illegal values: ',imply(X,Y,EqXY,Res))
1697		).
1698
1699		% assert X=pred_true => Y=pred_true
1700		imply_true(X,Y) :-
1701		(var(X),var(Y) -> bool_equality(X,Y,EqXY) ; true /* imply_true will not block anyway */),
1702	?	imply_true3(X,Y,EqXY).
1703		:- block imply_true3(-,-,-).
1704		imply_true3(X,Y,EqXY) :-
1705		( X==pred_false -> true
1706		; X==pred_true -> Y=pred_true
1707		; Y==pred_true -> true
1708		; Y==pred_false -> X=pred_false
1709		; EqXY==pred_true -> true
1710		; EqXY==pred_false -> X=pred_false % X => not(X) ===> X=pred_false
1711		; add_error_fail(imply_true,'Illegal values: ',imply_true3(X,Y,EqXY))
1712		).
1713
1714
1715		:- assert_must_succeed(exhaustive_kernel_check(b_interpreter_check:equiv(pred_false,pred_false,pred_true))).
1716		:- assert_must_succeed(exhaustive_kernel_check(b_interpreter_check:equiv(pred_false,pred_true,pred_false))).
1717		:- assert_must_succeed(exhaustive_kernel_check(b_interpreter_check:equiv(pred_true,pred_false,pred_false))).
1718		:- assert_must_succeed(exhaustive_kernel_check(b_interpreter_check:equiv(pred_true,pred_true,pred_true))).
1719		:- assert_must_succeed(exhaustive_kernel_fail_check(b_interpreter_check:equiv(pred_false,pred_false,pred_false))).
1720		:- assert_must_succeed(exhaustive_kernel_fail_check(b_interpreter_check:equiv(pred_false,pred_true,pred_true))).
1721		:- assert_must_succeed(exhaustive_kernel_fail_check(b_interpreter_check:equiv(pred_true,pred_false,pred_true))).
1722		:- assert_must_succeed(exhaustive_kernel_fail_check(b_interpreter_check:equiv(pred_true,pred_true,pred_false))).
1723
1724		% b_interpreter_check:equiv(X,Y,Res),X=Y, Res==pred_true
1725		equiv(X,Y,Res) :-
1726		bool_equality(X,Y,Res).
1727
1728
1729		:- assert_must_succeed(exhaustive_kernel_check(b_interpreter_check:if_pred(pred_false,pred_false,pred_true,pred_true,no_wf_available))).
1730		:- assert_must_succeed(exhaustive_kernel_check(b_interpreter_check:if_pred(pred_true,pred_false,pred_true,pred_false,no_wf_available))).
1731		:- assert_must_succeed(exhaustive_kernel_check(b_interpreter_check:if_pred(pred_true,pred_false,pred_true,pred_false,no_wf_available))).
1732
1733		/*
1734		Here is the truth-table of the IF-THEN-ELSE predicate generated in the ProB repl:
1735		>>> {test,lhs,rhs,res|(IF test=TRUE THEN lhs=TRUE ELSE rhs=TRUE END)<=> res=TRUE}
1736		Expression Value =
1737		{(FALSE|->FALSE|->FALSE|->FALSE),(FALSE|->FALSE|->TRUE|->TRUE),(FALSE|->TRUE|->FALSE|->FALSE),(FALSE|->TRUE|->TRUE|->TRUE),(TRUE|->FALSE|->FALSE|->FALSE),(TRUE|->FALSE|->TRUE|->FALSE),(TRUE|->TRUE|->FALSE|->TRUE),(TRUE|->TRUE|->TRUE|->TRUE)}
1738		>>> :show
1739		Nr test lhs rhs res
1740		1 FALSE FALSE FALSE FALSE
1741		2 FALSE FALSE TRUE TRUE
1742		3 FALSE TRUE FALSE FALSE
1743		4 FALSE TRUE TRUE TRUE
1744		5 TRUE FALSE FALSE FALSE
1745		6 TRUE FALSE TRUE FALSE
1746		7 TRUE TRUE FALSE TRUE
1747		8 TRUE TRUE TRUE TRUE
1748		*/
1749
1750		% propagate reified version of IF-THEN-ELSE predicate
1751		% Note: IF pt THEN qt ELSE rt END <=> ((pt => qt) & (not(pt) => rt))
1752		:- block if_pred(-,-,-,-,?).
1753		if_pred(Test,LHS,RHS,Res,WF) :-
1754		( Test == pred_true -> LHS=Res
1755		; Test == pred_false -> RHS=Res
1756		; LHS == pred_true -> negate(Test,NegTest), imply(NegTest,RHS,Res)
1757	?	; LHS == pred_false -> negate(Test,NegTest), conjoin(NegTest,RHS,Res,priority(1),priority(1),WF)
1758		; RHS == pred_true -> imply(Test,LHS,Res)
1759		; RHS == pred_false -> conjoin(Test,LHS,Res,lhs,rhs,WF)
1760		; Res == pred_true -> imply_true(Test,LHS), negate(Test,NegTest), imply_true(NegTest,RHS)
1761		; Res == pred_false -> if_pred_false(Test,LHS,RHS)
1762		; add_internal_error('Illegal call: ',if_pred(Test,LHS,RHS,Res,WF))
1763		).
1764
1765		% as facts the truth table for if_pred_false would be:
1766		%if_pred_false(pred_true,pred_false,_).
1767		%if_pred_false(pred_false,_,pred_false).
1768		% but we provide a deterministic propagator:
1769		:- block if_pred_false(-,-,-).
1770		if_pred_false(Test,LHS,RHS) :-
1771		( Test==pred_true -> LHS=pred_false
1772		; Test==pred_false -> RHS=pred_false
1773		; LHS == pred_true -> Test = pred_false, RHS = pred_false
1774		; RHS == pred_true -> Test = pred_true, LHS = pred_false
1775		; LHS == pred_false -> if_false_lhs(Test,RHS)
1776		; RHS == pred_false -> if_false_rhs(Test,LHS)
1777		).
1778
1779		:- block if_false_lhs(-,-).
1780		if_false_lhs(Test,RHS) :- var(Test), RHS==pred_false,!. % Test value does not matter, both lhs/rhs false
1781		if_false_lhs(pred_false,pred_false). % we choose RHS which must be false for the if_predicate to be false
1782		if_false_lhs(pred_true,_). % we choose the lhs which is false, RHS does not matter
1783
1784		:- block if_false_rhs(-,-).
1785		if_false_rhs(Test,LHS) :- var(Test), LHS==pred_false,!. % Test value does not matter, both lhs/rhs false
1786		if_false_rhs(pred_true,pred_false).
1787		if_false_rhs(pred_false,_). % we choose the rhs which is false, LHS does not matter