1		% (c) 2009-2019 Lehrstuhl fuer Softwaretechnik und Programmiersprachen,
2		% Heinrich Heine Universitaet Duesseldorf
3		% This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html)
4
5		:- module(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
11		/* some lower-level propagation predicates */
12		imply_true/2,
13		b_check_forall_wf/8, b_check_exists_wf/7,
14
15		reify_closure_with_small_cardinality/5,
16
17		register_predicate/6,
18
19		conjoin/6, disjoin/6
20		]).
21
22		/* A version for checking the truth value of boolean-expressions,
23		the result is instantiated with pred_true/pred_false as soon as the result is known */
24		/* Warning: does not cover all expressions */
25		/* It provides SMT-like performance, for predicates involving arithmetic comparisons (<,...),
26		equality, disequality and membership/not_membership
27		It is not restricted to CNF
28		*/
29
30		:- use_module(debug).
31		:- use_module(self_check).
32		:- use_module(error_manager).
33		:- use_module(b_interpreter,[b_compute_expression/5, b_not_test_boolean_expression/6, b_test_boolean_expression/6, b_test_boolean_expression/4]).
34		:- use_module(kernel_waitflags).
35
36
37		:- use_module(kernel_objects,[less_than_direct/2, less_than_equal_direct/2]).
38
39		:- use_module(kernel_equality).
40
41		:- use_module(tools).
42
43		:- use_module(module_information,[module_info/2]).
44		:- module_info(group,interpreter).
45		:- module_info(description,'This module provides a reified interpreter for certain predicates.').
46
47
48
49		:- meta_predicate wd_delay(0,-,-,-).
50		:- meta_predicate wd_delay_block(0,-,-,-,-,-).
51		:- meta_predicate wd_delay_until_needed(-,0).
52		:- meta_predicate wd_delay_until_needed_block(-,-,0,0).
53
54		:- block imply_test_boolean_expression(-, ?,?,?,?,?,?). % TO DO: pass at least Ai to it
55		imply_test_boolean_expression(PredRes1,PredRes2, RHS,LocalState,State,WF,Ai) :-
56	?	(PredRes1=PredRes2
57		-> % print('enforcing RHS '),print(PredRes), print(' : '), translate:print_bexpr(RHS),nl, %%
58		% print(LocalState),nl,
59	?	b_test_boolean_expression(RHS,LocalState,State,WF,Ai,_)
60		; true %,print(not_checking_rhs(_PRes)), print(' : '), print_bexpr(_RHS),nl, print(_State),nl
61		).
62
63		:- block equiv_test_boolean_expression(-, ?,?,?,?,?,?).
64		equiv_test_boolean_expression(PredRes,PredRes, RHS,LocalState,State,WF,Ai) :- !,
65		%print('enforcing RHS '),print(PredRes), print(' : '), print_bexpr(RHS),nl,
66		b_test_boolean_expression(RHS,LocalState,State,WF,Ai,_).
67		equiv_test_boolean_expression(_PredRes,_, RHS,LocalState,State,WF,Ai) :-
68		%print('enforcing negation of RHS '),print(_PredRes), print(' : '), print_bexpr(RHS),nl,
69		b_not_test_boolean_expression(RHS,LocalState,State,WF,Ai,_).
70
71		equiv_bidrectional_test_boolean_expression(PredResLHS,PredResRHS, _LHS,_RHS,_LocalState,_State,WF) :-
72		PredResLHS=PredResRHS,
73		(var(PredResLHS)
74		-> % create a choice point to enumerate two possible solutions
75		% important, e.g., for not((y > 0 & y * y > 20) <=> (y * y > 25 & y > 0))
76		get_last_wait_flag(equivalence,WF,LWF),
77		enum_bool(PredResLHS,LWF)
78		; true).
79		:- block enum_bool(-,-).
80		enum_bool(pred_true,_).
81		enum_bool(pred_false,_).
82		/*
83		:- block equiv_bidrectional_test_boolean_expression(-,-, ?,?,?,?,?).
84		equiv_bidrectional_test_boolean_expression(PredResLHS,PredResRHS, LHS,RHS,LocalState,State,WF) :-
85		( PredResLHS == pred_true -> b_test_boolean_expression(RHS,LocalState,State,WF)
86		; PredResLHS == pred_false -> b_not_test_boolean_expression(RHS,LocalState,State,WF)
87		; PredResRHS == pred_true -> b_test_boolean_expression(LHS,LocalState,State,WF)
88		; PredResRHS == pred_false -> b_not_test_boolean_expression(LHS,LocalState,State,WF)
89		; add_error_fail(equiv,'Illegal values: ',equiv_bidrectional_test_boolean_expression(PredResLHS,PredResRHS))
90		).
91		*/
92
93		% return starting priority for binary choice points; should be power of 2
94		get_priority_of_boolean_expression(priority(P),Prio) :- !,
95		% case generated for disjoin by contains_fd_element, and not_in_difference_set_wf,not_in_intersection_set_wf,in_union_set_wf
96		Prio=P.
97		get_priority_of_boolean_expression(b(Expr,_,_Infos),Prio) :- !,
98		% try to estimate a priority for performing a case split upon a predicate
99		% i.e., forcing a predicate Expr to be true/false
100		get_priority_of_boolean_expression2(Expr,Prio).
101		get_priority_of_boolean_expression(E,Prio) :-
102		add_internal_error('Boolean expression not properly wrapped: ',get_priority_of_boolean_expression(E,Prio)),
103		get_priority_of_boolean_expression2(E,Prio).
104
105		:- use_module(bsyntaxtree).
106		get_priority_of_boolean_expression2(truth,0) :- !. %, nl,nl,print('TRUTH in disjunct/conjunct'),nl.
107		get_priority_of_boolean_expression2(falsity,0) :- !. %, nl,nl,print('FALSITY in disjunct/conjunct'),nl.
108		get_priority_of_boolean_expression2(_,R) :-
109		preferences:preference(data_validation_mode,true), % in data validation mode we want to drive enumeration from data values only
110		!, R=4096.
111		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)
112
113
114
115
116		count_number_of_conjuncts(b(Expr,_,_Infos),Prio) :- !,
117		count_number_of_conjuncts2(Expr,Prio).
118		count_number_of_conjuncts(priority(_),Prio) :- !, Prio=1.
119		count_number_of_conjuncts(B,Prio) :-
120		add_internal_error('Expression not wrapped: ',count_number_of_conjuncts(B,Prio)),Prio=1.
121		count_number_of_conjuncts2(conjunct(A,B),Nr) :- !, count_number_of_conjuncts(A,NA),
122		count_number_of_conjuncts(B,NB), Nr is NA+NB.
123		count_number_of_conjuncts2(norm_conjunct(_,RHS),Res) :- length(RHS,Len),!,
124		Res is Len+1.
125		count_number_of_conjuncts2(negation(A),Nr) :- !, count_number_of_disjuncts(A,Nr).
126		count_number_of_conjuncts2(_,1).
127
128		:- public count_number_of_disjuncts/2. %currently commented out above
129		count_number_of_disjuncts(b(Expr,_,_Infos),Prio) :- !,
130		count_number_of_disjuncts2(Expr,Prio).
131		count_number_of_disjuncts(priority(_),Prio) :- !, Prio=1.
132		count_number_of_disjuncts(B,Prio) :-
133		add_internal_error('Expression not wrapped: ',count_number_of_disjuncts(B,Prio)),Prio=1.
134		count_number_of_disjuncts2(disjunct(A,B),Nr) :- !, count_number_of_disjuncts(A,NA),
135		count_number_of_disjuncts(B,NB), Nr is NA+NB.
136		count_number_of_disjuncts2(norm_disjunct(_,RHS),Res) :- length(RHS,Len),!,
137		Res is Len+1.
138		count_number_of_disjuncts2(negation(A),Nr) :- !, count_number_of_conjuncts(A,Nr).
139		count_number_of_disjuncts2(_,1).
140
141
142
143		% we need to ensure that b_check_boolean_expression does not create a choice point on its own
144
145		b_check_boolean_expression(b(Expr,_,Infos),LS,S,WF,Res) :-
146		(composed(Expr) -> empty_avl(Ai)
147		; Ai = no_avl), % simple expression: no sharing is possible: no need to register expressions
148		b_check_boolean_expression2(Expr,Infos,LS,S,wfwd(WF,pred_true,pred_true),Res,Ai,_).
149
150		composed(negation(_)).
151		composed(conjunct(_,_)).
152		composed(disjunct(_,_)).
153		composed(implication(_,_)).
154		composed(equivalence(_,_)).
155		composed(let_predicate(_,_,_)).
156		composed(lazy_let_pred(_,_,_)).
157
158		b_check_boolean_expression(E,LS,S,WF,Res,Ai,Ao) :-
159		% add information about WD context: wfwd(WF_store, ExpectedVal, Val)
160		% when Val becomes nonvar: if Val==ExpectedVal we need the value of E, otherwise it should be discarded
161		b_check_boolean_expression1(E,LS,S,wfwd(WF,pred_true,pred_true),Res,Ai,Ao).
162
163		b_check_boolean_expression0(WDE,WDV,Expr,LS,S,WF,Res,Ai,Ao) :-
164		b_check_boolean_expression1(Expr,LS,S,wfwd(WF,WDE,WDV),Res,Ai,Ao).
165		% ((nonvar(WDV),WDE \= WDV) -> Ai=Ao, Res=pred_false
166		% ; b_check_boolean_expression1(Expr,LS,S,wfwd(WF,WDE,WDV),Res,Ai,Ao)).
167
168		b_check_boolean_expression1(b(Expr,_,Infos),LS,S,WFD,Res,Ai,Ao) :- WFD=wfwd(_WF,WDE,WDV),!,
169		% print('check : '), translate:print_bexpr(b(Expr,pred,Infos)),nl,
170		%when(nonvar(Res), (print(Res), print(' <--> '),translate:print_bexpr(b(Expr,pred,Infos)),nl)),
171		(nonvar(WDV),WDE \= WDV
172		-> Ai=Ao,
173		(var(Res) -> Res=pred_false ; true)
174		; b_check_boolean_expression2(Expr,Infos,LS,S,WFD,Res,Ai,Ao)).
175		b_check_boolean_expression1(b(Expr,T,Infos),LS,S,WFD,Res,Ai,Ao) :- !,
176		add_internal_error('Illegal WFWD info: ',b_check_boolean_expression1(b(Expr,T,Infos),LS,S,WFD,Res,Ai,Ao)),
177		b_check_boolean_expression2(Expr,Infos,LS,S,wfwd(WFD,pred_true,pred_true),Res,Ai,Ao).
178		b_check_boolean_expression1(E,LS,S,WFD,Res,Ai,Ao) :-
179		add_internal_error('Boolean expression not properly wrapped: ',b_check_boolean_expression1(E,LS,S,WFD,Res,Ai,Ao)),
180		b_check_boolean_expression2(E,[],LS,S,WFD,Res,Ai,Ao).
181
182		% normalise conjunction into flat list of conjuncts
183		normalise_conjunct(b(E,_,Info)) --> normalise_conjunct2(E,Info).
184		normalise_conjunct2(conjunct(A,B),_) --> !,normalise_conjunct(A),normalise_conjunct(B).
185		normalise_conjunct2(F,Info) --> [b(F,pred,Info)].
186
187		construct_norm_conjunct(A,b(B,pred,Info)) :- construct_norm_conjunct2(A,B,Info).
188		construct_norm_conjunct2([],truth,[]).
189		construct_norm_conjunct2([H|T],Res,Info) :-
190		(T==[] -> H=b(Res,pred,Info) ; Res=norm_conjunct(H,T),Info=[]).
191		% TO DO: build up member(contains_wd_condition,Infos)
192
193
194		% normalise disjunction into flat list of disjuncts
195		normalise_disjunct(b(E,_,Info)) --> normalise_disjunct2(E,Info).
196		normalise_disjunct2(disjunct(A,B),_) --> !,normalise_disjunct(A),normalise_disjunct(B).
197		normalise_disjunct2(F,Info) --> [b(F,pred,Info)].
198
199		construct_norm_disjunct(A,b(B,pred,Info)) :- construct_norm_disjunct2(A,B,Info).
200		construct_norm_disjunct2([],falsity,[]).
201		construct_norm_disjunct2([H|T],Res,Info) :-
202		(T==[] -> H=b(Res,pred,Info) ; Res=norm_disjunct(H,T),Info=[]).
203
204		can_negate_expression(b(Expr,pred,I),b(NExpr,pred,I)) :- can_negate2(Expr,NExpr).
205		can_negate2(equal(A,B),not_equal(A,B)).
206		can_negate2(not_equal(A,B),equal(A,B)).
207		can_negate2(member(A,B),not_member(A,B)).
208		can_negate2(not_member(A,B),member(A,B)).
209		can_negate2(subset(A,B),not_subset(A,B)).
210		can_negate2(not_subset(A,B),subset(A,B)).
211		can_negate2(subset_strict(A,B),not_subset_strict(A,B)).
212		can_negate2(not_subset_strict(A,B),subset_strict(A,B)).
213		can_negate2(greater_equal(A,B),less(A,B)).
214		can_negate2(less(A,B),greater_equal(A,B)).
215		can_negate2(less_equal(A,B),greater(A,B)).
216		can_negate2(greater(A,B),less_equal(A,B)).
217
218		b_check_boolean_expression2(truth,_,_,_,_WFD,Res,Ai,Ao) :- !,Res=pred_true, Ai=Ao.
219		b_check_boolean_expression2(falsity,_,_,_,_WFD,Res,Ai,Ao) :- !,Res=pred_false, Ai=Ao.
220		b_check_boolean_expression2(negation(BExpr),_,LocalState,State,WFD,Res,Ai,Ao) :- !,
221		(can_negate_expression(BExpr,NBExpr)
222		-> /* avoid introducing negate propagator; maybe not necessary */
223		b_check_boolean_expression1(NBExpr,LocalState,State,WFD,Res,Ai,Ao)
224		; negate(NR,Res),
225		b_check_boolean_expression1(BExpr,LocalState,State,WFD,NR,Ai,Ao)).
226		b_check_boolean_expression2(conjunct(LHS,RHS),CInfo,LocalState,State,WFD,Res,Ai,Ao) :- !,
227		normalise_conjunct2(conjunct(LHS,RHS),CInfo,NormRes,[]),
228		construct_norm_conjunct2(NormRes,NC,Info), % print(normalised(NC)),nl,
229		b_check_boolean_expression2(NC,Info,LocalState,State,WFD,Res,Ai,Ao).
230		b_check_boolean_expression2(norm_conjunct(LHS,RHS),_,LocalState,State,wfwd(WF,WDE,WDV),Res,Ai,Ao) :- !,
231		construct_norm_conjunct(RHS,NC),
232		conjoin(LR,RR,Res,LHS,NC,WF),
233		b_check_boolean_expression1(LHS,LocalState,State,wfwd(WF,WDE,WDV),LR,Ai,Aii),
234		% when(nonvar(LR),(print(LR), print(' && : '), translate:print_bexpr(LHS),nl)),
235		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
236		b_check_boolean_expression0(pred_true,GuardFlag,NC,LocalState,State,WF,RR,Aii,Ao).
237		b_check_boolean_expression2(implication(LHS,RHS),_,LocalState,State,wfwd(WF,WDE,WDV),Res,Ai,Ao) :- !, impl(LR,RR,Res),
238		b_check_boolean_expression1(LHS,LocalState,State,wfwd(WF,WDE,WDV),LR,Ai,Aii),
239		% when(nonvar(LR),(LR=pred_true -> print(' => : '), translate:print_bexpr(RHS),nl ; true)),
240		propagagate_wfwd(WDE,WDV,GuardFlag,LR,pred_false),
241		b_check_boolean_expression0(pred_true,GuardFlag,RHS,LocalState,State,WF,RR,Aii,Ao).
242		b_check_boolean_expression2(equivalence(LHS,RHS),_,LocalState,State,WFD,Res,Ai,Ao) :- !, equiv(LR,RR,Res),
243		b_check_boolean_expression1(LHS,LocalState,State,WFD,LR,Ai,Aii),
244		b_check_boolean_expression1(RHS,LocalState,State,WFD,RR,Aii,Ao).
245		b_check_boolean_expression2(disjunct(LHS,RHS),CInfo,LocalState,State,WFD,Res,Ai,Ao) :- !,
246		normalise_disjunct2(disjunct(LHS,RHS),CInfo,NormRes,[]),
247		construct_norm_disjunct2(NormRes,NC,Info), % print(normalised_disj(NC)),nl,
248		b_check_boolean_expression2(NC,Info,LocalState,State,WFD,Res,Ai,Ao).
249		b_check_boolean_expression2(norm_disjunct(LHS,RHS),_,LocalState,State,wfwd(WF,WDE,WDV),Res,Ai,Ao) :- !,
250		construct_norm_disjunct(RHS,NC),
251		disjoin(LR,RR,Res,LHS,NC,WF),
252		%print(disjoin(WDE,WDV)), translate:print_bexpr(LHS),nl,
253		b_check_boolean_expression1(LHS,LocalState,State,wfwd(WF,WDE,WDV),LR,Ai,Aii),
254		propagagate_wfwd(WDE,WDV,GuardFlag,LR,pred_true),
255		b_check_boolean_expression0(pred_false,GuardFlag,NC,LocalState,State,WF,RR,Aii,Ao).
256		b_check_boolean_expression2(let_predicate(Ids,AssignmentExprs,Pred),_Info,LocalState,State,WFD,Res,Ai,Ao) :-
257		% nl,print(check_let_predicate(Ids)),nl, translate:print_bexpr(Pred),nl,
258		!,
259		wd_set_up_localstate_for_let(Ids,AssignmentExprs,LocalState,State,LetState,WFD),
260		b_check_boolean_expression1(Pred,LetState,State,WFD,Res,Ai,Ao).
261		b_check_boolean_expression2(lazy_let_pred(Id,AssignmentExpr,Pred),_I,LocalState,State,wfwd(WF,WDE,WDV),Res,Ai,Ao) :- !,
262		store:set_up_localstate([Id],[(Trigger,IdValue)],LocalState,LetState),
263		% print(setting_up_lazy_let_pred(Id)),nl,
264		b_interpreter:lazy_compute_expression(Trigger,AssignmentExpr,LocalState,State,IdValue,WF,Ai),
265		b_check_boolean_expression1(Pred,LetState,State,wfwd(WF,WDE,WDV),Res,Ai,Ao).
266		b_check_boolean_expression2(lazy_lookup_pred(Id),Info,LocalState,_State,WFD,Res,Ai,Ao) :- !, Ai=Ao,
267		% print(lazy_lookup_pred_check(Id,Info)),nl,
268		store:lookup_value_for_existing_id(Id,LocalState,(Trigger,Value)), % should normally only occur in LocalState; value introduced by lazy_let
269		%(Trigger,Value) = (pred_true,Res). % ,print(res(Res)),nl. % force evaluation
270		wd_delay(((Trigger,Value) = (pred_true,Res)),
271		Res,b(lazy_lookup_pred(Id),pred,Info),WFD).
272		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
273		Res=V,Ai=Ao.
274		b_check_boolean_expression2(not_equal(LHS,RHS),Info,LocalState,State,WFD,Res,Ai,Ao) :- !,
275		(negate_equal_false(LHS,RHS,LHS1,RHS1)
276		-> /* X/=FALSE equivalent to X=TRUE */
277		b_check_boolean_expression3_pos(equal(LHS1,RHS1),Info,LocalState,State,WFD,Res,Ai,Ao)
278		; b_check_boolean_expression3_neg(equal(LHS,RHS),Info,LocalState,State,WFD,Res,Ai,Ao)
279		).
280		b_check_boolean_expression2(equal(LHS,RHS),Info,LocalState,State,WFD,Res,Ai,Ao) :- !,
281		(negate_equal_false(LHS,RHS,LHS1,RHS1)
282		-> RHS1=b(boolean_true,boolean,[]), /* X/=FALSE equivalent to X=TRUE */
283		b_check_boolean_expression3_neg(equal(LHS1,RHS1),Info,LocalState,State,WFD,Res,Ai,Ao)
284		; b_check_boolean_expression3_pos(equal(LHS,RHS),Info,LocalState,State,WFD,Res,Ai,Ao)
285		).
286		b_check_boolean_expression2(not_member(LHS,RHS),Info,LocalState,State,WFD,Res,Ai,Ao) :- !,
287		b_check_boolean_expression3_neg(member(LHS,RHS),Info,LocalState,State,WFD,Res,Ai,Ao).
288		b_check_boolean_expression2(not_subset(LHS,RHS),Info,LocalState,State,WFD,Res,Ai,Ao) :- !,
289		b_check_boolean_expression3_neg(subset(LHS,RHS),Info,LocalState,State,WFD,Res,Ai,Ao).
290		b_check_boolean_expression2(not_subset_strict(LHS,RHS),Info,LocalState,State,WFD,Res,Ai,Ao) :- !,
291		b_check_boolean_expression3_neg(subset_strict(LHS,RHS),Info,LocalState,State,WFD,Res,Ai,Ao).
292		b_check_boolean_expression2(greater(LHS,RHS),Info,LocalState,State,WFD,Res,Ai,Ao) :- !,
293		b_check_boolean_expression3_pos(less(RHS,LHS),Info,LocalState,State,WFD,Res,Ai,Ao).
294		b_check_boolean_expression2(greater_equal(LHS,RHS),Info,LocalState,State,WFD,Res,Ai,Ao) :- !,
295		b_check_boolean_expression3_neg(less(LHS,RHS),Info,LocalState,State,WFD,Res,Ai,Ao).
296		b_check_boolean_expression2(less_equal(LHS,RHS),Info,LocalState,State,WFD,Res,Ai,Ao) :- !,
297		b_check_boolean_expression3_neg(less(RHS,LHS),Info,LocalState,State,WFD,Res,Ai,Ao).
298		b_check_boolean_expression2(Pred,Infos,LocalState,State,WFD,Res,Ai,Ao) :-
299		b_check_boolean_expression3_pos(Pred,Infos,LocalState,State,WFD,Res,Ai,Ao).
300
301
302		% check whether one of the two arguments is FALSE
303		% translate X/=FALSE -> X=TRUE for normalisation purposes
304		negate_equal_false(b(boolean_false,boolean,_),E,E,b(boolean_true,boolean,[])).
305		negate_equal_false(E,b(boolean_false,boolean,_),E,b(boolean_true,boolean,[])).
306
307		b_check_boolean_expression3_pos(Pred,Infos,LocalState,State,WFD,Res,Ai,Ao) :-
308		%print(register_predicate(WFD,Infos,Pred)),nl,portray_avl(Ai),nl,
309		register_predicate_wfd(WFD,Pred,Infos,Res,Reused,Ai,Ao),
310		(Reused=true
311		-> true % , print(reused_pred(WFD,Infos)),nl, translate:print_bexpr(Pred),nl
312		; b_check_boolean_expression4(Pred,Infos,LocalState,State,WFD,Res)
313		).
314
315		b_check_boolean_expression3_neg(Pred,Infos,LocalState,State,WFD,NegRes,Ai,Ao) :-
316		%print(register_neg_predicate(WFD,Infos,Pred)),nl,
317		register_predicate_wfd(WFD,Pred,Infos,Res,Reused,Ai,Ao), negate(Res,NegRes),
318		(Reused=true
319		-> true
320		; b_check_boolean_expression4(Pred,Infos,LocalState,State,WFD,Res)
321		).
322
323		% Register a new predicate in the AVL tree if either forced or non-WD condition inside
324		register_predicate_wfd(_,_,_,_,false,Ai,Ao) :- Ai = no_avl,!, Ai=Ao.
325		register_predicate_wfd(_,_Pred,_Infos,_,false,Ai,Ao) :-
326		preferences:preference(use_common_subexpression_elimination,true),
327		preferences:preference(use_common_subexpression_also_for_predicates,true),
328		preferences:preference(disprover_mode,false), % there are still a few things detected here that CSE does not detect (=FALSE,=TRUE,...)
329		!, % CSE already statically detects these ( all of the time !?)
330		Ai=Ao.
331		register_predicate_wfd(wfwd(_,A,B),Pred,Infos,PredTruthVar,Reused,Ai,Ao) :-
332		(A==B -> register_predicate_aux(Pred,PredTruthVar,Reused,Ai,Ao) % it will be evaluated; we can share it
333		; nonmember(contains_wd_condition,Infos) -> register_predicate_aux(Pred,PredTruthVar,Reused,Ai,Ao)
334		; Ai=Ao, Reused=false % not guaranteed to be evaluated: WD-condition + not in forced WFD context
335		% ,print('NOT REGISTERING: '), translate:print_bexpr(Pred),nl
336		).
337
338		% Register a new predicate in the AVL tree (for outside callers like b_interpreter.pl)
339		register_predicate(Pred,_Infos,NegPredTruthVar,Reused,Ai,Ao) :- negate_pred(Pred,NegPred),!,
340		%print(negating),nl,
341		negate(PredTruthVar,NegPredTruthVar),
342		register_predicate_aux(NegPred,PredTruthVar,Reused,Ai,Ao).
343		register_predicate(Pred,_Infos,PredTruthVar,Reused,Ai,Ao) :-
344		register_predicate_aux(Pred,PredTruthVar,Reused,Ai,Ao).
345
346		negate_pred(equal(A,B),not_equal(AA,TRUE)) :- negate_equal_false(A,B,AA,TRUE).
347		negate_pred(not_equal(A,B),equal(A,B)). % TO DO: we should check negate_equal_false
348		negate_pred(not_member(A,B),member(A,B)).
349		negate_pred(not_subset(A,B),subset(A,B)).
350		negate_pred(not_subset_strict(A,B),subset_strict(A,B)).
351		negate_pred(greater_equal(A,B),less(A,B)).
352		negate_pred(less_equal(A,B),less(B,A)).
353
354		register_predicate_aux(Pred,_PredTruthVar,Reused,Ai,Ao) :- do_not_store_pred(Pred),!,
355		Ai=Ao, Reused=false.
356		register_predicate_aux(Pred,PredTruthVar,Reused,Ai,Ao) :- check_pred_truth_var(PredTruthVar),
357		norm_pred_check(Pred,NPred), % We could store this information in the info field computed by ast_cleanup ?
358		(%too_simple(NPred) -> Reused=false, Ao=Ai ; %% even for simple equalities it actually pays off !
359		reuse_predicate(NPred,Var,Ai)
360		-> % nl,print(reusing(NPred,Var)),nl, %%
361		PredTruthVar=Var,Ao=Ai, Reused=true
362		; add_predicate(NPred,PredTruthVar,Ai,Ao), Reused=false
363		%,nl,print(not_reusing(NPred)),nl
364		).
365
366		check_pred_truth_var(X) :- var(X),!.
367		check_pred_truth_var(pred_true) :- !.
368		check_pred_truth_var(pred_false) :- !.
369		check_pred_truth_var(X) :- add_internal_error('Illegal Predicate Truth Value: ',check_pred_truth_var(X)).
370
371		:- use_module(kernel_tools,[ground_bexpr/1]).
372		%do_not_store_pred(b(P,_,_)) :- do_not_store_pred_aux(P),!.
373		do_not_store_pred(external_pred_call(_P,_)) :- !. % expcept maybe LESS, CHOOSE,... we could check performs_io
374		do_not_store_pred(B) :-
375		(ground_bexpr(b(B,pred,[]))
376		% TO DO: improve performance: marking bexpr with potential non-ground value(.) terms inside
377		-> fail
378		; true %print('-> Not storing: '),translate:print_bexpr(b(B,pred,[])),nl
379		).
380		do_not_store_pred_aux(external_pred_call(_P,_)). % expcept maybe LESS, CHOOSE,... we could check performs_io
381
382
383		% Quantifier Expansion
384
385		b_check_forall_wf(Parameters,LHS,RHS,Info,LocalState,State,WF,PredRes) :-
386		WFD=wfwd(WF,pred_true,pred_true), % we expect it to be in a context where the value will be needed
387		b_check_forall_wfwd(Parameters,LHS,RHS,Info,LocalState,State,WFD,PredRes).
388		b_check_forall_wfwd(_Parameters,LHS,RHS,_Info,_LocalState,_State,_WFD,PredRes) :-
389		(is_falsity(LHS) ; is_truth(RHS)),!, % quantifier always true
390		PredRes = pred_true.
391		b_check_forall_wfwd(Parameters,LHS,RHS,Info,LocalState,State,WFD,PredRes) :-
392		small_quantifier_cardinality(Parameters,LHS,LHS1,LHSRest),
393		%print(expand(forall(Parameters))),nl,
394		expand_quantifier(Parameters,LHS1,List), %print(List),nl,
395		Body = b(implication(LHSRest,RHS),pred,Info),% translate:print_bexpr(Body),nl,
396		WFD=wfwd(WF,_,_),
397		check_expanded_forall_quantifier(List,Body, LocalState, State,WF,WFD,PredRes).
398		% TO DO: if not small_quantifier_cardinality: b_check_boolean_expression4_delay
399
400
401		b_check_exists_wf(Parameters,Body,Info,LocalState,State,WF,PredRes) :-
402		WFD=wfwd(WF,pred_true,pred_true), % we expect it to be in a context where the value will be needed
403		b_check_exists_wfwd(Parameters,Body,Info,LocalState,State,WFD,PredRes).
404		b_check_exists_wfwd(Parameters,Body,_Info,LocalState,State,WFD,PredRes) :-
405		% could be generalised to take into consideration domain as restricted by Body
406		small_quantifier_cardinality(Parameters,Body,LHS,RHS),
407		% print(expanding_check_exists(_Card,Parameters)),nl, % portray_waitflags(WF),
408		expand_quantifier(Parameters,LHS,List),
409		% print(List),nl, translate:print_bexpr(Body),nl,nl,
410		% now compute a priority for the disjunction based on the number of case splits
411		% relevant for tests 1358, 1746
412		length(List,Len), % Note: if Len=1: the body must be true; no disjoin will be set up
413		get_pow2_binary_choice_priority(Len,Prio),
414		% if Len=2 -> we actually have just two possibilities T,_ and F,T; but we want Prio to start at 4 ?
415		% 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 ?
416		% TO DO: maybe we could directly set up an n-ary disjoin predicate ? if one disjunct true; remove case-splits on other disjuncts
417		WFD=wfwd(WF,_,_),
418		check_expanded_exists_quantifier(List,Prio,RHS, LocalState, State,WF,WFD,PredRes).
419		% TO DO: if not small_quantifier_cardinality: b_check_boolean_expression4_delay
420
421
422		:- use_module(b_enumerate, [b_tighter_enumerate_values/2]).
423		expand_quantifier(Parameters,Pred,ListOfNewLocalStates) :-
424		% at the moment LS,State not really needed; only necessary if non-compiled Pred can be used
425		% also: feeding in any non-bound variables in LocalState or State would cause problems in findall !
426		findall(ParLocalState,
427		(b_interpreter:set_up_typed_localstate(Parameters,_ParaValues,ParamTypedVals,[],ParLocalState,all_solutions),
428		kernel_waitflags:init_wait_flags(WF),
429		b_test_boolean_expression(Pred,[],ParLocalState,WF),
430		b_tighter_enumerate_values(ParamTypedVals,WF),
431		kernel_waitflags:ground_wait_flags(WF)),
432		ListOfNewLocalStates).
433
434		check_expanded_forall_quantifier([], _Body, _LS, _State,_WF,_WFD,Res) :-
435		Res=pred_true.
436		check_expanded_forall_quantifier([LS1|TLS], Body, LS, State,WF,WFD,Res) :-
437		conjoin(Res1,TRes,Res,Body,Body,WF),
438		empty_avl(InnerAi), % TO DO: maybe use no_avl ?
439		append(LS1,LS,InnerLS),
440		% Note: we do not need to guard against wd-definition from other instances inside a quantified expression
441		% either all conjuncts can be evaluated or none
442		% print(expand_forall(WFD)), translate:print_bexpr(Body),nl,
443		b_check_boolean_expression1(Body,InnerLS,State,WFD,Res1,InnerAi,_Aii),
444		%instantiate_wfwd_result(WDE,WDV,Res1),
445		check_expanded_forall_quantifier(TLS,Body,LS,State,WF,WFD,TRes).
446
447		/*
448		:- block instantiate_wfwd_result(?,-,-).
449		% instantiate a boolean variable in case it is no longer needed and not set by something else
450		instantiate_wfwd_result(WDE,WDV,Res) :-
451		(nonvar(Res) -> true
452		; WDE==WDV -> true
453		; Res = pred_false). */
454
455		check_expanded_exists_quantifier([], _, _Body, _LS, _State,_WF,_WFD,Res) :-
456		Res=pred_false.
457		check_expanded_exists_quantifier([LS1|TLS], Priority, Body, LS, State,WF,WFD,Res) :-
458		(TLS = [] -> Res=Res1
459		; disjoin(Res1,TRes,Res,priority(Priority),priority(Priority),WF)), % was using Body instead of priority(Priority)
460		empty_avl(InnerAi), % TO DO: maybe use no_avl ?
461		append(LS1,LS,InnerLS),
462		b_check_boolean_expression1(Body,InnerLS,State,WFD,Res1,InnerAi,_Aii),
463		% Note: we do not need to guard against wd-definition from other instances inside a quantified expression
464		check_expanded_exists_quantifier(TLS,Priority,Body,LS,State,WF,WFD,TRes).
465
466
467		:- use_module(library(lists),[maplist/4]).
468		% try and convert a closure into a list of 0/1 variables for each potential element
469		reify_closure_with_small_cardinality(P,T,Body, WF,ReifiedList) :- %print(try(P)),nl,
470		maplist(create_typed_id,P,T,Parameters),
471		small_quantifier_cardinality(Parameters,Body,LHS,RHS,350,25000), % TO DO: how to choose these parameters ?
472		% 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
473		% 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
474		%print(clos_card(Card,LHS,RHS)),nl,
475		expand_quantifier(Parameters,LHS,List),
476		% print(list_of_local_states(List)),nl,
477		WFD=wfwd(WF,pred_true,pred_true), % is this ok ??
478		reifiy_list(List,RHS,WFD,ReifiedList).
479
480		reifiy_list([], _Body,_WFD,[]).
481		reifiy_list([LS1|TLS], Body,WFD,[Res_01|TRes]) :-
482		empty_avl(InnerAi),
483		b_check_boolean_expression1(Body,LS1,[],WFD,Res1_pred,InnerAi,_Aii),
484		%print(reified(Res1_pred,LS1)),nl,
485		prop_pred_01(Res1_pred,Res_01),
486		% Note: we do not need to guard against wd-definition from other instances inside a quantified expression
487		reifiy_list(TLS,Body,WFD,TRes).
488
489
490
491		:- use_module(library(lists),[select/3]).
492
493		% check if Body produces a small cardinality for the paramters Par
494		% if yes: the predicates constraining Par are put into LHS, the rest into RHS
495		% also: LHS must ensure that ground values are produced for Par and that we can enumerate with a separate WF (in expand_quantifier)
496		small_quantifier_cardinality(Par,Body,LHS,RHS) :-
497		%preferences:preference(solver_strength,SS), NL is 10+SS, SMTL is 40+SS,
498		NL=10,SMTL=40,
499		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
500		small_quantifier_cardinality(Par,Body,LHS,RHS,NormalLimit,SMTLimit) :-
501		conjunction_to_list(Body,BodyList),
502		def_get_texpr_ids(Par,AllParas),
503		small_quantifier_cardinality_aux(Par,AllParas,BodyList,_UpBoundOnSize,LLHS,LRHS,NormalLimit,SMTLimit),
504		conjunct_predicates(LLHS,LHS),
505		conjunct_predicates(LRHS,RHS).
506
507		is_membership(b(P,pred,_),TLHS,RHS) :- is_mem_aux(P,TLHS,RHS).
508		is_mem_aux(member(TLHS,b(RHS,_,_)),TLHS,RHS).
509		is_mem_aux(equal(TLHS,b(value(V),_,_)),TLHS,value([V])). % x = V is the same as x:{V}
510
511		% do not rely on size for anything: it is just an upper bound on the size; the actual size could be smaller
512		small_quantifier_cardinality_aux([],_,Body,Size,LHS,RHS,_,_) :- !,
513		LHS=[],RHS=Body,Size=1.
514		small_quantifier_cardinality_aux(Parameters,AllParas,[LHS|TBody],FullSize,FullLHS,FullRHS,NormalLimit,SMTLimit) :-
515		%LHS = b(member(SID,b(MemRHS,_,_)),pred,_),
516		is_membership(LHS,SID,MemRHS),
517		%print(try_small(SID,MemRHS)),nl,
518	?	constrains_ID(SID,AllParas,Parameters,RestParameters,SkelVal,SkelToUnify,BindList), % we could check RestParameters /= Parameters
519		% TO DO: we could also allow parameter to be constrained twice x: 1..100 & x: {...} ?
520		%print(check_is_small(MemRHS,SkelToUnify,BindList)),nl,
521		(is_small_set(MemRHS,Size,NormalLimit,SMTLimit) % we have a small set of ground values: we can evaluate LHS to expand the quantifier/set_comprehension for the parameters occuring in LHS
522		-> FullLHS = [LHS|RestLHS],FullRHS = RestRHS
523		; infer_ground_membership(MemRHS,SID,SkelVal,SkelToUnify,BindList,NormalLimit,SMTLimit, Size,InferredLHS) ->
524		% we have inferred a superset InferredLHS of MemRHS which is small and known
525		FullLHS = [InferredLHS|RestLHS], % we have added an inferred membership constraint
526		FullRHS = [LHS|RestRHS]), % the original membership LHS still needs to be checked later, after expansion of the quantifier
527		!,
528		% we select LHS to be included in FullLHS and mark parameter ID as constrained
529		small_quantifier_cardinality_aux(RestParameters,AllParas,TBody,RestSize,RestLHS,RestRHS,NormalLimit,SMTLimit),
530		FullSize is Size*RestSize,
531		is_small_size(FullSize,NormalLimit,SMTLimit, Parameters).
532		small_quantifier_cardinality_aux(Parameters,AllParas,[H|Rest],FullSize,RestLHS,[H|RestRHS],NormalLimit,SMTLimit) :- !,
533		% skip the conjunct H
534		small_quantifier_cardinality_aux(Parameters,AllParas,Rest,FullSize,RestLHS,RestRHS,NormalLimit,SMTLimit).
535		small_quantifier_cardinality_aux(Parameters,_AllParas,Body,ParCard,[],Body,NormalLimit,SMTLimit) :-
536		% if the remaining parameter type cardinality is small: just use "truth" as body; will instantiate parameters
537		b_interpreter:parameter_list_cardinality(Parameters,ParCard),
538		is_small_size(ParCard,NormalLimit,SMTLimit, Parameters).
539
540		% try and extract a ground superset (InferredLHS) of the RHS (ID:RHS) which constrains ID
541		infer_ground_membership(value(List),_,SkelVal,SkelToUnify,BindList,NormalLimit,SMTLimit, Size,InferredLHS) :-
542		!,
543		% 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)
544		extract_bind_list(BindList,LHSTerm,RHSValue),
545		has_bounded_ground_matches(List,SkelVal,SkelToUnify,RHSValue,MatchedValues,1,NrMatches), % TO DO: provide SMTLimit as upper limit
546		NrMatches = Size,
547		is_small_size(Size,NormalLimit,SMTLimit, unknown),
548		get_texpr_type(LHSTerm,LHSTermType),
549		InferredLHS = b(member(LHSTerm,b(value(MatchedValues),set(LHSTermType),[])),pred,[generated]).
550		%print(matches(NrMatches,MatchedValues)),nl, translate:print_bexpr(InferredLHS),nl,
551		infer_ground_membership(Set,SID,SkelVal,SkelToUnify,BindList,NormalLimit,SMTLimit,Size,InferredLHS) :-
552		superset(Set,SuperSet),
553		% 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
554		infer_ground_mem_aux(SuperSet,SID,SkelVal,SkelToUnify,BindList,NormalLimit,SMTLimit,Size,InferredLHS).
555
556
557		superset(intersection(A,B),Set) :- (Set=A ; Set=B). % Set /\ X <: Set
558		superset(set_subtraction(Set,_),Set). % Set \ X <: Set
559		superset(domain_restriction(_,Set),Set). % X <| Set <: Set
560		superset(domain_subtraction(_,Set),Set). % X <<| Set <: Set
561		superset(range_subtraction(Set,_),Set). % Set |> X <: Set
562		superset(range_restriction(Set,_),Set). % Set |>> X <: Set
563
564		infer_ground_mem_aux(b(Set,T,I),SID,SkelVal,SkelToUnify,BindList,NormalLimit,SMTLimit, Size,InferredLHS) :-
565		(is_small_set(Set,Size,NormalLimit,SMTLimit) -> InferredLHS = b(member(SID,b(Set,T,I)),pred,[generated])
566		; infer_ground_membership(Set,SID,SkelVal,SkelToUnify,BindList,NormalLimit,SMTLimit, Size,InferredLHS)).
567
568		:- use_module(bsyntaxtree, [create_couple/3]).
569		% 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)
570		extract_bind_list([TID/Val],TID,Val) :- !.
571		extract_bind_list([TID/Val|BList],Couple,(Val,RestVal)) :-
572		create_couple(TID,RestExpr,Couple),
573		extract_bind_list(BList,RestExpr,RestVal).
574
575		:- use_module(kernel_tools,[can_match/2]).
576		% check if we can find a bounded / fixed number of ground matches for Skeleton Value in List
577		has_bounded_ground_matches(Var,_,_,_, _,_,_) :- var(Var),!.
578		has_bounded_ground_matches([],_SkelVal,_SkelToUnify,_,[],LenAcc,LenAcc).
579		has_bounded_ground_matches([H|T],SkelVal,SkelToUnify,ValueToStore,Matches,LenAcc,LenRes) :-
580		(can_match(H,SkelVal) -> copy_term((SkelToUnify,ValueToStore),(H,HValueToStore)),
581		ground_value(HValueToStore),
582		Matches = [HValueToStore|MT],
583		A1 is LenAcc+1 ; Matches=MT,A1=LenAcc),
584		has_bounded_ground_matches(T,SkelVal,SkelToUnify,ValueToStore,MT,A1,LenRes).
585
586		% check if the Expr contains ID, i.e., matching Expr with an element of a set will also instantiate and determine TID
587		% TO DO: also accept other patterns: records, sets?,....
588
589		% SkeletonToUnify: a skeleton that can be used to unify with any value and extracts value in BindList
590		constrains_ID(b(E,_,_),AllParas,Parameters,RestParameters,SkeletonValue,SkeletonToUnify,BindList) :-
591	?	constrains_ID_aux(E,AllParas,Parameters,RestParameters,SkeletonValue,SkeletonToUnify,BindList).
592		constrains_ID_aux(couple(A,B),AllParas,Parameters,RestParameters,(V1,V2),(Skel1,Skel2),Bind) :-
593	?	constrains_ID(A,AllParas,Parameters,Rest1,V1,Skel1,Bind1),
594	?	constrains_ID(B,AllParas,Rest1,RestParameters,V2,Skel2,Bind2),
595		append(Bind1,Bind2,Bind). % TO DO: use DCGs
596		constrains_ID_aux(rec(F),AllParas,Parameters,RestParameters,record(SkelV),record(SkelU),Bind) :-
597		constrains_ID_fields(F,AllParas,Parameters,RestParameters,SkelV,SkelU,Bind).
598		constrains_ID_aux(identifier(ID),AllParas,Parameters,RestParameters,_SkelV,SkelU,Bind) :-
599		% TO DO: allow same id to appear multiple times in expression + allow to re-use parameters in another conjunct
600	?	(select(TID,Parameters,RestParameters), get_texpr_id(TID,ID)
601		-> Bind = [TID/SkelU]
602	?	; member(ID,AllParas), % we have already used/bound ID; we will use first occurence for skeleton/bind; this one is simply ignored
603		% TO DO: we could try and see whether using the second occurence gives a better result
604		% print(double_match(ID)),nl,
605		RestParameters=Parameters, Bind=[]
606		).
607		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
608		constrains_ID_aux(boolean_true,_AllParas,P,P,pred_true,pred_true,[]). % needed ?? everything is compiled anway ?
609		constrains_ID_aux(boolean_false,_AllParas,P,P,pred_false,pred_false,[]). % needed ?? everything is compiled anway ?
610		% Below: allow any other expression as long as it only uses AllParas
611		% 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
612		constrains_ID_aux(add(A,B),AllParas,P,P,_,_,[]) :- % basically allow other Parameters or ground values
613		constrains_ID(A,AllParas,[],[],_,_,_), constrains_ID(B,AllParas,[],[],_,_,_).
614		constrains_ID_aux(minus(A,B),AllParas,P,P,_,_,[]) :- % TO DO: allow other binary/unary operators ?
615		constrains_ID(A,AllParas,[],[],_,_,_), constrains_ID(B,AllParas,[],[],_,_,_).
616		%constrains_ID_aux(Other,All,P,P,_,_,[]) :- print(other(Other)),nl,fail.
617
618		constrains_ID_fields([],_AllParas,P,P,[],[],[]).
619		constrains_ID_fields([field(Field,Val)|TF],AllParas,Parameters,RestParameters,
620		[field(Field,SkelVal)|TSkelV],[field(Field,SkelUnify)|TSkelU],Bind) :-
621		constrains_ID(Val,AllParas,Parameters,Rest1,SkelVal,SkelUnify,Bind1),
622		constrains_ID_fields(TF,AllParas,Rest1,RestParameters,TSkelV,TSkelU,Bind2),
623		append(Bind1,Bind2,Bind). % TO DO: use DCGs
624
625		:- use_module(custom_explicit_sets,[efficient_card_for_set/3]).
626
627		%is_small_set(S,_,LocalState,State) :- print(is_small_set(S,LocalState,State)),nl,fail.
628
629		is_small_set(Val,Size,NormalLimit,SMTLimit) :-
630		get_small_set_size(Val,Size),
631		is_small_size(Size,NormalLimit,SMTLimit,unknown).
632
633		:- use_module(kernel_tools,[ground_value/1]).
634		get_small_set_size(value(S),Size) :- !,
635		ground_value(S), % otherwise we could have S=[X] and expand_quantifier will erroneously create multiple solutions for parameter=X
636		efficient_card_for_set(S,Size,C),
637		call(C).
638		get_small_set_size(interval(From,To),Size) :- !,
639		custom_explicit_sets:is_interval_with_integer_bounds(interval(From,To),Low,Up),
640		number(Low), number(Up),
641		(Low > Up -> Size = 1 ; Size is 1+Up-Low).
642		% we provide dom/ran here explicitly as this is often used {i|i:dom(f) ...}
643		get_small_set_size(bool_set,Size) :- !, Size=2.
644		get_small_set_size(domain(b(Val,_,_)),Size) :- !, get_small_domain_set_size(Val,Size). % this is only an upper bound on the size !!
645		get_small_set_size(range(b(Val,_,_)),Size) :- !, get_small_set_size(Val,Size). % this is only an upper bound on the size !!
646		get_small_set_size(cartesian_product(b(A,_,_),b(B,_,_)),Size) :- !,
647		get_small_set_size(A,SizeA), number(SizeA),
648		get_small_set_size(B,SizeB), number(SizeB),
649		kernel_objects:safe_mul(SizeA,SizeB,Size), number(Size).
650
651		%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
652		%get_small_set_size(sequence_extension(L),Size,_,_,_) :- !, length(L,Size), is_small_size(Size). ditto
653		%get_small_set_size(interval...
654		%get_small_set_size(domain(value([....]))...
655		% for this to work efficiently one should call b_compiler:compile on the predicates before sending them
656		% to b_interpreter_check; otherwise the sets will not yet be in value(_) form
657
658		% TO DO: the same for range or find more principled solution
659		%get_small_domain_set_size(value(S),Size) :- var(S), frozen(S,Frozen), print(var_value(S,Frozen)),nl,fail.
660		get_small_domain_set_size(value(Val),Size) :- nonvar(Val), Val=[H|T],!,
661		efficient_card_for_set([H|T],Size,C),
662		ground_domain([H|T]), % rather than requiring ground of entire list; we only require ground for domain (see test 1272)
663		call(C).
664		get_small_domain_set_size(Val,Size) :- get_small_set_size(Val,Size).
665		ground_domain(V) :- var(V),!,fail.
666		ground_domain([]).
667		ground_domain([H|T]) :- nonvar(H), H=(D,_), ground_value(D), ground_domain(T).
668
669		% maybe in other cases try b_compiler:compile ?
670		%is_small_set(EXPR,Size,Parameters,LocalState,State) :-
671		% print('check is_small_set: '),translate:print_bexpr(EXPR),nl,
672		% def_get_texpr_ids(Parameters,PN),
673		% print(parameters(PN)),nl,
674		% b_compiler:b_compile(b(EXPR,pred,[]),PN,LocalState,State,CLHS,WF),
675		% print('compiled: '), print(CLHS),nl,
676		% CLHS = value(S),efficient_card_for_set(S,Size,C),call(C), is_small_size(Size).
677
678		:- use_module(performance_messages).
679		is_small_size(Size,NormalLimit,SMTLimit,SrcLocation) :- Size \= inf,
680		(Size < NormalLimit -> true
681		; Size < SMTLimit
682		-> (preferences:preference(use_smt_mode,true) -> true
683		; perfmessage(not_reifiying_size_too_large_try_SMT_mode(Size,limits(NormalLimit,SMTLimit)),SrcLocation),fail)
684		; perfmessage(not_reifiying_size_too_large(Size,limits(NormalLimit,SMTLimit)),SrcLocation),fail).
685
686		% -------------------------------------
687		% EXPRESSIONS
688
689		:- use_module(store,[set_up_localstate/4]).
690
691		wd_set_up_localstate_for_let(Ids,Exprs,LocalState,State,LetState,WFD) :-
692		set_up_localstate(Ids,Vars,LocalState,LetState),
693		wd_compute_let_expressions(Exprs,Vars,LetState,State,WFD).
694		wd_compute_let_expressions([],[],_,_,_).
695		wd_compute_let_expressions([Expr|RestExprs],[Var|RestVars],LocalState,State,WFD) :-
696		b_wd_compute_expression(Expr,LocalState,State,Value,WFD),
697		kernel_objects:equal_object_optimized(Var,Value,compute_let_expressions),
698		wd_compute_let_expressions(RestExprs,RestVars,LocalState,State,WFD).
699
700
701		b_wd_compute_expressions([], _, _, [],_WFD).
702		b_wd_compute_expressions([EXPRsHd|EXPRsTl],LocalState,State,[ValHd|ValTl],WFD) :-
703		b_wd_compute_expression(EXPRsHd,LocalState,State,ValHd,WFD),
704		b_wd_compute_expressions(EXPRsTl,LocalState,State,ValTl,WFD).
705
706		% we have to avoid trying to compute certain expressions: evaluation can fail if not well-defined !
707		b_wd_compute_expression(Expr,LocalState,State,Value,wfwd(WF,WDE,WDV)) :-
708		(nonvar(WDV)
709		-> (WDE==WDV
710		-> %print('REQUIRED: '), translate:print_bexpr(Expr),nl,
711		if(b_compute_expression(Expr,LocalState,State,Value,WF), % TO DO: we could use fresh variable for Value
712		true,
713		(kernel_objects:unbound_value(Value), % we have a WD error, if nonvar it could be because we expect a wrong value
714		translate:translate_bexpression_with_limit(Expr,TS),
715		add_wd_error_span('Well-definedness error evaluating expression: ',TS,span_predicate(Expr,LocalState,State),WF)
716		%Value = term(undefined),
717		)
718		)
719		; instantiate_to_any_value(Value,Expr,WF))
720		; always_well_defined(Expr) % should we use always_well_defined_or_disprover_mode ?; probably not because of failure of the entire computation!
721		-> % print('ALWAYS WD: '), translate:print_bexpr(Expr),nl, %
722		b_compute_expression(Expr,LocalState,State,Value,WF)
723		% ; \+ preferences:preference(use_smt_mode,_____false) %,\+ may_instantiate(Expr)
724		% ->
725		% % Necessary for tests 323, 324 : but dangerous inside set comprehensions ,... !!
726		% print('NOT DELAYING WD in SMT MODE: '), translate:print_bexpr(Expr),nl,
727		% b_compute_expression(Expr,LocalState,State,Value,WF)
728		; % print('DELAYING DUE TO WD: '), translate:print_bexpr(Expr),nl, %%
729		b_compute_expression_delay(WDE,WDV, Expr,LocalState,State,Value,WF)
730		% TO DO: allow further partial instantiation
731		).
732
733		/*
734		% what if function is used inside Expr ??
735		may_instantiate(b(E,_,_Infos)) :- !,may_instantiate_aux(E).
736		% Warning: function application can force a variable to be bound to non-empty set !
737		may_instantiate_aux(function(_,_)).
738		*/
739
740		:- block b_compute_expression_delay(?,-, ?,?,?,?,?).
741		b_compute_expression_delay(WDE,WDV,Expr,LocalState,State,Value,WF) :-
742	?	(WDE==WDV
743		-> % print('WD Evaluation: '), print(WDE),print(' =?= '), print(WDV), print(' '),translate:print_bexpr(Expr),nl,
744	?	b_compute_expression(Expr,LocalState,State,Value,WF)
745		% ,print(' Value: '), print(Value),nl
746		; %print(instantiate_to_any_value(Value,Expr)),nl,
747		instantiate_to_any_value(Value,Expr,WF) % does not matter anyway; but there can be pending co-routines :-(
748		).
749
750		% WARNING: the variable could be used in another context, where it is relevant !
751
752
753		wd_delay(WDCall,Res, Expr,wfwd(WF,WDExpected,WDV)) :- %print(wd_delay(WDExpected,WDV)),nl,
754		(WDExpected==WDV -> call(WDCall) % WDV truth value on left is ok: we can evaluate
755		; nonvar(WDV) -> instantiate_to_any_value(Res,Expr,WF) % truth value not ok; we do not need the value
756		; always_well_defined(Expr) -> call(WDCall)
757		; wd_delay_block(WDCall,Res,Expr,WDExpected,WDV,WF)).
758		:- block wd_delay_block(?,?,?,?,-,?).
759		wd_delay_block(WDCall,Res,Expr,WDExpected,WDV,WF) :-
760		(WDExpected==WDV -> call(WDCall)
761		; instantiate_to_any_value(Res,Expr,WF)).
762
763
764		:- use_module(typing_tools,[any_value_for_type/2]).
765		%instantiate_to_any_value(V,_) :- print(inst(V)),nl,nonvar(V),!.
766		instantiate_to_any_value(V,_,_) :- ground_value(V),!.
767		instantiate_to_any_value(V,b(_B,TYPE,_I),WF) :-
768		get_enumeration_finished_wait_flag(WF,EWF),
769		% TO DO: use ground value check
770		when((nonvar(EWF);ground(V)),any_value_for_type(TYPE,V)). % , print(inst2(TYPE,V)),translate:print_bexpr(b(_B,TYPE,_I)),nl.
771
772
773		:- block propagagate_wfwd(-,?,?,-,?), propagagate_wfwd(?,-,?,-,?).
774		% propagate expected and actual value guarding left with actual predicate value obtained for left
775		propagagate_wfwd(WDE,WDV,Res,F1,F2) :-
776	?	(F1==F2 -> Res=F1 % then value of WDE does not matter at all; Res always the same
777	?	; propagagate_wfwd2(WDE,WDV,Res,F1,F2)).
778
779		:- block propagagate_wfwd2(-,?,?,?,?), propagagate_wfwd2(?,-,?,?,?).
780	?	propagagate_wfwd2(WDE,WDV,Res,F1,F2) :- (WDE==WDV -> Res=F1 ; Res=F2).
781
782		:- use_module(external_functions,[external_fun_has_wd_condition/1]).
783		:- use_module(preferences).
784		b_check_boolean_expression4(equal(LHS,RHS),_,LocalState,State,WFD,EqRes) :- !,
785		b_wd_compute_expression(LHS,LocalState,State,LHValue,WFD),
786		b_wd_compute_expression(RHS,LocalState,State,RHValue,WFD),
787		get_texpr_type(LHS,Type),
788		%translate:translate_bexpression(b(equal(LHS,RHS),pred,[]),SSS),preq(EqRes,SSS),
789		% was translate_eq(Eq,Res),
790		%when(nonvar(EqRes),(print(EqRes),print(' : '),translate:print_bexpr(b(equal(LHS,RHS),pred,[])),nl)),
791		%print(equality(Type,LHValue,RHValue,WFD)), translate:print_bexpr(b(equal(LHS,RHS),pred,[])),nl,
792		equality_objects_with_type(Type,LHValue,RHValue,EqRes).
793		%:- block preq(-,?).
794		%preq(Res,Expr) :- print('Equality determined '), print(Res), print(' '),print(Expr),nl.
795		% we may need to improve not_member for closure to invert symbolic operators
796		% we may want to add things like partial_function_check, subset_check, ...
797		b_check_boolean_expression4(member(LHS,RHS),Info,LocalState,State,WFD,Res) :-
798		%member_check_should_be_reified(LHS,RHS), % no longer need this: symbolic operators will be kept as closures if large ?!
799		!,
800		get_texpr_expr(RHS,ERHS),
801		b_check_member_expression(ERHS,RHS,LHS,Info,LocalState,State,WFD,Res).
802		% TO DO: add member(,pow_subset, fin_subset) --> subset_test
803		% TO DO: compile forall, exists + setup choice point if expansion fails + remove compile calls in b_interpreter
804		b_check_boolean_expression4(forall(Parameters,LHS,RHS),Info,LocalState,State,WFD,Res) :- !,
805		if(b_check_forall_wfwd(Parameters,LHS,RHS,Info,LocalState,State,WFD,Res),true,
806		(perfmessagecall(cannot_reify_forall(Parameters),translate:print_bexpr(LHS),LHS),fail)).
807		b_check_boolean_expression4(exists(Parameters,Body),Info,LocalState,State,WFD,Res) :- !,
808		if(b_check_exists_wfwd(Parameters,Body,Info,LocalState,State,WFD,Res),true,
809		(perfmessagecall(cannot_reify_exists(Parameters),translate:print_bexpr(Body),Body),fail)).
810		b_check_boolean_expression4(subset(LHS,RHS),_,LocalState,State,WFD,Res) :- !, WFD=wfwd(WF,_,_),
811		b_wd_compute_expression(LHS,LocalState,State,LHValue,WFD),
812		b_wd_compute_expression(RHS,LocalState,State,RHValue,WFD),
813		% print(subset_check),print(' '),translate:print_bexpr(b(subset(LHS,RHS),pred,[])),nl, %%
814		subset_test(LHValue,RHValue,Res,WF).
815		b_check_boolean_expression4(subset_strict(LHS,RHS),_,LocalState,State,WFD,Res) :- !, WFD=wfwd(WF,_,_),
816		b_wd_compute_expression(LHS,LocalState,State,LHValue,WFD),
817		b_wd_compute_expression(RHS,LocalState,State,RHValue,WFD),
818		% print(subset_strict_check),print(' '),translate:print_bexpr(b(subset_strict(LHS,RHS),pred,[])),nl, %%
819		subset_strict_test(LHValue,RHValue,Res,WF).
820		b_check_boolean_expression4(external_pred_call(FunName,Args),Info,LocalState,State,WFD,Res) :-
821		!,
822		(external_fun_has_wd_condition(FunName)
823		-> wd_delay_until_needed(WFD,b_check_external_pred_call(FunName,Args,Info,LocalState,State,WFD,Res))
824		; b_check_external_pred_call(FunName,Args,Info,LocalState,State,WFD,Res)).
825		b_check_boolean_expression4(freetype_case(FT,IsCase,Expr),_Infos,LocalState,State,WFD,Res) :- !,
826		b_wd_compute_expression(Expr,LocalState,State,freeval(FT,ActualCase,_A),WFD),
827		%print(eq_atomic(IsCase,ActualCase,FT,_A,Res,WFD)),nl,translate:print_bexpr(Expr),nl,
828		eq_atomic(IsCase,ActualCase,freeval_case,Res).
829		b_check_boolean_expression4(finite(Expr),_Infos,LocalState,State,WFD,Res) :- !, WFD=wfwd(WF,_,_),
830		b_wd_compute_expression(Expr,LocalState,State,ExprVal,WFD),
831		% print(test_finite),nl,translate:print_bexpr(Expr),nl,
832		kernel_objects:test_finite_set_wf(ExprVal,Res,WF).
833		b_check_boolean_expression4(Pred,_,LocalState,State,WFD,Res) :-
834		arithmetic_op(Pred,Op,LHS,RHS),!,
835		% print('checking arith: '), print(op(Op,Res)),nl,translate:print_bexpr(Pred),nl, %
836		b_wd_compute_expression(LHS,LocalState,State,int(LHValue),WFD),
837		% kernel_objects:basic_type2(integer,int(LHValue)), %
838		b_wd_compute_expression(RHS,LocalState,State,int(RHValue),WFD),
839		% kernel_objects:basic_type2(integer,int(RHValue)), %
840		check_arithmetic_operator(Op,LHValue,RHValue,Res). %
841		% TO DO ???: use idea of b_artihmetic_expression to avoid intermediate CLPFD variables
842		% TO DO: add other operators, ...
843		/* use_smt_mode = full is never set; at some point we should enable the following clause by default
844		b_check_boolean_expression4(Pred,Infos,LocalState,State,wfwd(WF,WDE,WDV),Res) :-
845		preferences:preference(use_smt_mode,full), %% comment out to enable check testing of complicated predicates inside;
846		% causes slowdowns of cbtc/actions_cbtc.mch; TO DO: investigate why
847		b_check_boolean_expression4_delay(WDE,WDV,Pred,Infos,LocalState,State,WF,Res).
848		*/
849
850		:- use_module(library(lists),[maplist/3]).
851		% TO DO: add member(,pow_subset, fin_subset) --> subset_test
852		% we could distribute RHS=union -> disjunction, LHS=intersection -> conjunction ,... ?
853		%b_check_member_expression(EHRS,_RHS,_LHS,_,_LocalState,_State,_WFD,_Res) :-
854		% print('member : '), print(EHRS),nl,fail.
855		%b_check_member_expression(union(A,B),LHS,_,LocalState,State,WFD,Res) :-
856		b_check_member_expression(pow_subset(RHS),_,LHS,_Info,LocalState,State,WFD,Res) :- !,
857		b_check_boolean_expression4(subset(LHS,RHS),[],LocalState,State,WFD,Res).
858		%b_check_member_expression(NotContainingEmptySet,_TRHS,LHS,LocalState,State,WFD,Res) :-
859		% non_empty_set_version_of(NotContainingEmptySet,RHS_With_EmptySet),
860		% % translate x:seq1(RHS) -> x /= {} & x:seq(RHS), ...
861		% % this improves propagation, in particular in light of WD issues
862		% % TO DO: avoid computing LHS twice !
863		% !,
864		% get_texpr_type(LHS,LType),
865		% EMPTYVERSION = b(member(LHS,b(RHS_With_EmptySet,set(LType),[])),pred,[]),
866		% NOTEMPTYPRED = b(not_equal(LHS,b(empty_set,LType,[])),pred,[]),
867		% print('Translating : '), translate:print_bexpr(EMPTYVERSION), print(' & '), translate:print_bexpr(NOTEMPTYPRED),nl,
868		% empty_avl(Ai), Infos=[], % Infos not important for conjunction
869		% b_check_boolean_expression2(conjunct(EMPTYVERSION,NOTEMPTYPRED),Infos,LocalState,State,WFD,Res,Ai,_).
870		b_check_member_expression(interval(Low,Up),_,LHS,_Info,LocalState,State,WFD,Res) :- !, WFD=wfwd(WF,_,_),
871		% to do: should we also match interval value closure
872		b_wd_compute_expression(LHS,LocalState,State,LHValue,WFD),
873		b_wd_compute_expression(Low,LocalState,State,LowValue,WFD),
874		b_wd_compute_expression(Up,LocalState,State,UpValue,WFD),
875		% print(mem_check_in_interval),print(' '),translate:print_bexpr(b(interval(Low,Up),set(integer),[])),nl,
876		kernel_objects:test_in_nat_range_wf(LHValue,LowValue,UpValue,Res,WF).
877		b_check_member_expression(set_extension(SetExt),_RHS,LHS,Info,LocalState,State,WFD,Res) :- !, WFD=wfwd(WF,_,_),
878		% rewrite x:{a,b,c} into x=a or x=b or x=c (is the opposite of rewrite_disjunct_to_member)
879		% The rewrite_disjunct_to_member is good when we know a membership to be true; the disjunct is better for reification
880		% Note: the problem is in particular when the result of the membership is not needed and an uninstantiated
881		% variable is used in the set extension, example y:dom(f) => (x:{f(y),0} or f(y)=0)
882		% print(mem_check_set_extension),print(' '),translate:print_bexpr(b(member(LHS,_RHS),pred,[])),nl,
883		b_wd_compute_expressions(SetExt,LocalState,State,SetExtValues,WFD),
884		b_wd_compute_expression(LHS,LocalState,State,LHValue,WFD),
885		get_texpr_type(LHS,Type),
886		NewLHS = b(value(LHValue),Type,[]),
887		(ground(SetExtValues)
888		-> % better to use normal treatment, we can compute the entire set and translate it into an AVL tree
889		maplist(construct_value(Type),SetExtValues,Vals),
890		b_wd_compute_expression(b(set_extension(Vals),set(Type),[]),LocalState,State,RHValue,WFD),
891		%print(rhval(RHValue)),nl,
892		membership_test_wf(RHValue,LHValue,Res,WF),
893		force_membership_test(Res,LHValue,RHValue,WF)
894		; maplist(construct_equality(NewLHS,Type),SetExtValues,Disjuncts),
895		construct_norm_disjunct2(Disjuncts,NC,Info), % print(normalised_disj(NC)),nl,
896		empty_avl(Ai),
897		b_check_boolean_expression2(NC,Info,LocalState,State,WFD,Res,Ai,_)
898		).
899		b_check_member_expression(closure(Relation),_RHS,LHS,_Info,LocalState,State,WFD,Res) :- !, WFD=wfwd(WF,_,_),
900		b_wd_compute_expression(LHS,LocalState,State,LHValue,WFD),
901		b_wd_compute_expression(Relation,LocalState,State,RelValue,WFD),
902		%print(reify_in_closure(LHValue,RelValue)),nl,
903		bsets_clp:in_closure1_membership_test_wf(LHValue,RelValue,Res,WF).
904		b_check_member_expression(_,RHS,LHS,_Info,LocalState,State,WFD,Res) :- WFD=wfwd(WF,_,_),
905		b_wd_compute_expression(LHS,LocalState,State,LHValue,WFD),
906		b_wd_compute_expression(RHS,LocalState,State,RHValue,WFD),
907		% print(mem_check),print(' '),translate:print_bexpr(b(member(LHS,RHS),pred,[])),nl,
908		% print(mem_test(RHValue,LHValue,Res)),nl, trace,
909		membership_test_wf(RHValue,LHValue,Res,WF),
910		force_membership_test(Res,LHValue,RHValue,WF).
911
912		construct_value(Type,Val,b(value(Val),Type,[])).
913
914		:- use_module(bsyntaxtree, [safe_create_texpr/3]).
915		construct_equality(NewLHS,Type,ElementV,Equality) :-
916		Element = b(value(ElementV),Type,[]),
917		safe_create_texpr(equal(NewLHS,Element),pred,Equality). %, translate:print_bexpr(Equality),nl.
918
919		%non_empty_set_version_of(seq1(RHS),seq(RHS)).
920		%non_empty_set_version_of(iseq1(RHS),iseq(RHS)).
921		%non_empty_set_version_of(fin1_subset(RHS),fin_subset(RHS)).
922		%non_empty_set_version_of(pow1_subset(RHS),pow_subset(RHS)).
923
924		/*
925		:- block b_check_boolean_expression4_delay(?,-,?,?,?,?,?,?).
926		b_check_boolean_expression4_delay(WDE,WDV,_,_,_,_,_,Res) :- WDE \= WDV,!,
927		Res=pred_false. % does not matter
928		b_check_boolean_expression4_delay(_WDE,_WDV,Pred,Infos,LocalState,State,WF,Res) :-
929		% we currently have not yet implemented a way to check the Pred; wait until Result is known
930		(preferences:preference(use_smt_mode,false)
931		->
932		get_last_wait_flag(b_check_test_boolean_expression,WF,WF2)
933		%Prio=10000,get_wait_flag(Prio,b_check_test_boolean_expression,WF,WF2)
934		; get_binary_choice_wait_flag(b_check_test_boolean_expression,WF,WF2)
935		),
936		(debug:debug_mode(on) -> print(' Check Testing: '),translate:print_bexpr(Pred),nl ; true),
937		b_check_test_boolean_expression(Res,WF2,b(Pred,pred,Infos),LocalState,State,WF).
938
939		:- block b_check_test_boolean_expression(-,-,?,?,?,?).
940		b_check_test_boolean_expression(pred_true,_,Pred,LocalState,State,WF) :-
941		b_test_boolean_expression(Pred,LocalState,State,WF).
942		b_check_test_boolean_expression(pred_false,_,Pred,LocalState,State,WF) :-
943		b_not_test_boolean_expression(Pred,LocalState,State,WF).
944		*/
945
946		/*
947		:- use_module(kernel_mappings).
948		member_check_should_be_reified(_,b(RHS,_,_)) :- functor(RHS,BOP,Arity), print(check(BOP,Arity)),nl,!.
949		member_check_should_be_reified(_,_) :- \+ preferences:preference(use_smt_mode,false),!.
950		member_check_should_be_reified(_LHS,b(RHS,_,_)) :- functor(RHS,BOP,Arity),
951		% check if we have optimized treatments available, for which we do not yet have reified versions
952		(Arity=1 -> \+ kernel_mappings:unary_in_boolean_type(BOP,_)
953		; Arity=2 -> \+ kernel_mappings:binary_in_boolean_type(BOP,_)
954		; Arity=0 -> \+ kernel_mappings:cst_in_boolean_type(BOP,_)
955		; true).
956		*/
957
958
959		:- block force_membership_test(-,?,?,?).
960		% currently required for ensuring that following fails:
961		% 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)])
962		% Reason: membership_test does not on its own enumerate
963		force_membership_test(pred_true,X,Set,WF) :- % print(forcing_element_true(X,Set)),nl,%
964		Set \= [],
965		(ground_value(X) -> true
966		; (nonvar(Set),no_use_forcing(Set)) -> true % no use in forcing membership, will call same element_of_avl_set_wf
967		%, tools_printing:print_term_summary(not_forcing(X,Set)),nl
968		; kernel_objects:check_element_of_wf(X,Set,WF)
969		)
970		%, tools:bt_trace(force_membership)
971		%, print(forced(X)),nl
972		.
973		force_membership_test(pred_false,_X,_Set,_WF).
974
975		% forcing is sometimes useful because we can transmit a WF, currently some of the reification predicates
976		% do not have a WF-Store and can thus do limited enumeration ! in particular true for CLPFD = FALSE mode
977		no_use_forcing(avl_set(_)) :- preferences:preference(use_clpfd_solver,true).
978		no_use_forcing(global_set(_)).
979		%no_use_forcing(closure(_,_,B)) :- preferences:preference(use_clpfd_solver,true).
980
981
982
983		:- use_module(external_functions,[call_external_predicate/8, do_not_evaluate_args/1]).
984		b_check_external_pred_call(FunName,Args,Info,LocalState,State,WFD,Res) :-
985		WFD=wfwd(WF,_,_),
986		(do_not_evaluate_args(FunName) -> EvaluatedArgs=[]
987		; b_wd_compute_expressions(Args, LocalState,State, EvaluatedArgs, WFD)),
988		%% print(external_pred_check),print(FunName),nl,%%
989		call_external_predicate(FunName,Args,EvaluatedArgs,LocalState,State,Res,Info,WF).
990
991		wd_delay_until_needed(wfwd(_,WDExpected,WDV),Call) :- !,
992		wd_delay_until_needed_block(WDExpected,WDV,Call,true).
993		wd_delay_until_needed(WFD,Call) :- add_internal_error('Illegal WFWD info:',wd_delay_until_needed(WFD,Call)),
994		call(Call).
995		:- block wd_delay_until_needed_block(-,?,?,?), wd_delay_until_needed_block(?,-,?,?).
996		wd_delay_until_needed_block(WDExpected,WDV,Call,_) :- WDExpected==WDV,!,
997		call(Call).
998		wd_delay_until_needed_block(_,_,_,Call) :- call(Call). % first call not needed
999
1000
1001		:- use_module(library(avl)).
1002		reuse_predicate(_,_,no_avl) :- !,fail.
1003		reuse_predicate(Pred,Var,AVL) :- avl_fetch(Pred,AVL,Var). %pred_var(Var)).
1004		add_predicate(_Pred,_Var,no_avl,NewAVL) :- !, NewAVL=no_avl.
1005		add_predicate(Pred,Var,AVL,NewAVL) :- (avl_store(Pred,AVL,Var,NewAVL) -> true ; NewAVL=no_avl). %pred_var(Var),NewAVL).
1006
1007
1008		:- use_module(translate,[print_bexpr/1]).
1009		% normalises a typed predicate by removing position information and ordering commutative operators in a canonical way
1010		norm_pred_check(B,Res) :-
1011		(norm_pred(B,Res) -> true
1012		; bget_functor(B,F,N),print(norm_pred_failed(F/N)),nl, print_bexpr(B),nl, % print(B),nl,
1013		Res=B).
1014		bget_functor(b(B,_,_),F,N) :- functor(B,F,N).
1015		bget_functor(B,F,N) :- functor(B,F,N).
1016
1017		norm_pred(X,Res) :- var(X),!,Res=X.
1018		norm_pred(b(B,_,_),Res) :- !, norm_pred(B,Res).
1019		norm_pred(conjunct(A,B),Res) :- !, norm_pred(A,AA), norm_pred(B,BB),
1020		(BB @< AA -> Res = conjunct(AA,BB) ; Res= conjunct(BB,AA)).
1021		norm_pred(disjunct(A,B),Res) :- !, norm_pred(A,AA), norm_pred(B,BB),
1022		(BB @< AA -> Res = disjunct(AA,BB) ; Res= disjunct(BB,AA)).
1023		norm_pred(equal(A,B),Res) :- !,norm_expr(A,AA),norm_expr(B,BB),
1024		(BB @< AA -> Res = equal(AA,BB) ; Res= equal(BB,AA)).
1025		norm_pred(equivalence(A,B),Res) :- !, norm_pred(A,AA), norm_pred(B,BB),
1026		(BB @< AA -> Res = equivalence(AA,BB) ; Res= equivalence(BB,AA)).
1027		norm_pred(exists(A,B),Res) :- !, Res=exists(AA,BB),l_norm_expr(A,AA), norm_pred(B,BB).
1028		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).
1029		norm_pred(greater(A,B),less(BB,AA)) :- !,norm_expr(A,AA),norm_expr(B,BB).
1030		norm_pred(greater_equal(A,B),less_equal(BB,AA)) :- !,norm_expr(A,AA),norm_expr(B,BB).
1031		norm_pred(implication(A,B),Res) :- !, Res=implication(AA,BB),norm_pred(A,AA), norm_pred(B,BB).
1032		norm_pred(less(A,B),less(AA,BB)) :- !,norm_expr(A,AA),norm_expr(B,BB).
1033		norm_pred(less_equal(A,B),less_equal(AA,BB)) :- !,norm_expr(A,AA),norm_expr(B,BB).
1034		norm_pred(let_predicate(A,B,C),Res) :- !,
1035		Res=let_predicate(AA,BB,CC),
1036		l_norm_expr(A,AA), l_norm_expr(B,BB),norm_pred(C,CC).
1037		norm_pred(lazy_let_pred(A,B,C),Res) :- !,
1038		Res = lazy_let_pred(AA,BB,CC),
1039		norm_expr(A,AA),
1040		norm_pred_or_expr(B,BB),norm_pred(C,CC).
1041		norm_pred(lazy_lookup_pred(A),Res) :- !, Res = lazy_lookup_pred(A).
1042		norm_pred(member(A,B),member(AA,BB)) :- !,norm_expr(A,AA),norm_expr(B,BB).
1043		norm_pred(negation(A),Res) :- !, Res=negation(AA), norm_pred(A,AA).
1044		norm_pred(not_equal(A,B),Res) :- !,norm_expr(A,AA),norm_expr(B,BB),
1045		(BB @< AA -> Res = not_equal(AA,BB) ; Res= not_equal(BB,AA)).
1046		norm_pred(not_member(A,B),not_member(AA,BB)) :- !,norm_expr(A,AA),norm_expr(B,BB).
1047		norm_pred(not_subset(A,B),not_subset(AA,BB)) :- !,norm_expr(A,AA),norm_expr(B,BB).
1048		norm_pred(not_subset_strict(A,B),not_subset_strict(AA,BB)) :- !,norm_expr(A,AA),norm_expr(B,BB).
1049		norm_pred(subset(A,B),subset(AA,BB)) :- !,norm_expr(A,AA),norm_expr(B,BB).
1050		norm_pred(subset_strict(A,B),subset_strict(AA,BB)) :- !,norm_expr(A,AA),norm_expr(B,BB).
1051		norm_pred(freetype_case(Type,Case,A),freetype_case(Type,Case,AA)) :- !,norm_expr(A,AA).
1052		norm_pred(X,X). % :- print(norm_pred(X)),nl.
1053
1054		norm_pred_or_expr(b(B,pred,_),Res) :- norm_pred(B,Res).
1055		norm_pred_or_expr(B,Res) :- norm_expr(B,Res).
1056
1057		:- public norm_expr_check/2.
1058		norm_expr_check(X,Res) :- var(X),!,Res=X.
1059		norm_expr_check(b(B,_,_),Res) :- !, norm_expr_check2(B,Res).
1060		norm_expr_check(X,X).
1061
1062		norm_expr_check2(B,Res) :-
1063		(norm_expr2(B,Res) -> true
1064		; functor(B,F,N),print(norm_expr2_failed(F/N)),nl,
1065		Res=B).
1066
1067		norm_expr(X,Res) :- var(X),!,Res=X.
1068		norm_expr(b(B,_,_),Res) :- !, norm_expr2(B,Res).
1069		%norm_expr_check2(B,Res). %% comment in to obtain details about failed normalisation for expressions
1070		norm_expr(X,X).
1071
1072		norm_expr2(assertion_expression(Cond,E,Expr),assertion_expression(AA,E,BB)) :- norm_pred(Cond,AA),norm_expr(Expr,BB).
1073		norm_expr2(add(A,B),Res) :- norm_expr(A,AA), norm_expr(B,BB), (BB @< AA -> Res = add(AA,BB) ; Res= add(BB,AA)).
1074		norm_expr2(bag_items(A),bag_items(AA)) :- norm_expr(A,AA).
1075		norm_expr2(boolean_false,boolean_false).
1076		norm_expr2(boolean_true,boolean_true).
1077		norm_expr2(bool_set,bool_set).
1078		norm_expr2(card(A),card(AA)) :- norm_expr(A,AA).
1079		norm_expr2(cartesian_product(A,B),cartesian_product(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1080		norm_expr2(closure(A),closure(AA)) :- norm_expr(A,AA). % this is closure1
1081		norm_expr2(compaction(A),compaction(AA)) :- norm_expr(A,AA).
1082		norm_expr2(composition(A,B),composition(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1083		norm_expr2(comprehension_set(A,B),comprehension_set(AA,BB)) :- norm_expr(A,AA), norm_pred(B,BB).
1084		norm_expr2(concat(A,B),concat(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1085		norm_expr2(convert_bool(A),convert_bool(AA)) :- norm_pred_check(A,AA).
1086		norm_expr2(couple(A,B),couple(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1087		norm_expr2(direct_product(A,B),direct_product(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1088		norm_expr2(div(A,B),div(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1089		norm_expr2(floored_div(A,B),floored_div(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1090		norm_expr2(domain_restriction(A,B),domain_restriction(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1091		norm_expr2(domain_subtraction(A,B),domain_subtraction(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1092		norm_expr2(domain(A),domain(AA)) :- norm_expr(A,AA).
1093		norm_expr2(empty_sequence,empty_sequence).
1094		norm_expr2(empty_set,empty_set).
1095		norm_expr2(event_b_identity,event_b_identity).
1096		norm_expr2(external_function_call(A,B),external_function_call(A,BB)) :- l_norm_expr(B,BB).
1097		norm_expr2(fin_subset(A),fin_subset(AA)) :- norm_expr(A,AA).
1098		norm_expr2(fin1_subset(A),fin1_subset(AA)) :- norm_expr(A,AA).
1099		norm_expr2(first(A),first(AA)) :- norm_expr(A,AA).
1100		norm_expr2(first_of_pair(A),first_of_pair(AA)) :- norm_expr(A,AA).
1101		norm_expr2(front(A),front(AA)) :- norm_expr(A,AA).
1102		norm_expr2(function(A,B),function(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1103		norm_expr2(general_concat(A),general_concat(AA)) :- norm_expr(A,AA).
1104		norm_expr2(general_intersection(A),general_intersection(AA)) :- norm_expr(A,AA).
1105		norm_expr2(general_product(A,B,C),Res) :- !, Res=general_sum(AA,BB,CC),l_norm_expr(A,AA), norm_pred(B,BB), norm_expr(C,CC).
1106		norm_expr2(general_sum(A,B,C),Res) :- !, Res=general_sum(AA,BB,CC),l_norm_expr(A,AA), norm_pred(B,BB), norm_expr(C,CC).
1107		norm_expr2(general_union(A),general_union(AA)) :- norm_expr(A,AA).
1108		norm_expr2(identifier(A),'$'(A)). % need wrapper to avoid confusion with other terms !
1109		norm_expr2(identity(A),identity(AA)) :- norm_expr(A,AA).
1110		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).
1111		norm_expr2(image(A,B),image(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1112		norm_expr2(insert_front(A,B),insert_front(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1113		norm_expr2(insert_tail(A,B),insert_tail(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1114		norm_expr2(integer_set(A),A).
1115		norm_expr2(integer(A),A).
1116		norm_expr2(intersection(A,B),Res) :- norm_expr(A,AA), norm_expr(B,BB),
1117		(BB @< AA -> Res = intersection(AA,BB) ; Res= intersection(BB,AA)).
1118		norm_expr2(interval(A,B),interval(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1119		norm_expr2(iseq(A),iseq(AA)) :- norm_expr(A,AA).
1120		norm_expr2(iseq1(A),iseq1(AA)) :- norm_expr(A,AA).
1121		norm_expr2(iteration(A,B),iteration(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1122		norm_expr2(last(A),last(AA)) :- norm_expr(A,AA).
1123		norm_expr2(lazy_let_expr(A,B,C),lazy_let_expr(AA,BB,CC)) :-
1124		norm_expr(A,AA),norm_pred_or_expr(B,BB),norm_expr(C,CC).
1125		norm_expr2(lazy_lookup_expr(A),lazy_lookup_expr(A)) :- !.
1126		norm_expr2(let_expression(A,B,C),let_expression(AA,BB,CC)) :- l_norm_expr(A,AA), l_norm_expr(B,BB),norm_pred(C,CC).
1127		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).
1128		norm_expr2(max(A),max(AA)) :- norm_expr(A,AA).
1129		norm_expr2(max_int,max_int).
1130		norm_expr2(min(A),min(AA)) :- norm_expr(A,AA).
1131		norm_expr2(min_int,min_int).
1132		norm_expr2(minus(A,B),minus(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1133		norm_expr2(modulo(A,B),modulo(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1134		norm_expr2(mu(A),mu(AA)) :- norm_expr(A,AA).
1135		norm_expr2(multiplication(A,B),Res) :- norm_expr(A,AA), norm_expr(B,BB), (BB @< AA -> Res = multiplication(AA,BB) ; Res= multiplication(BB,AA)).
1136		norm_expr2(operation_call_in_expr(A,B),overwrite(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1137		norm_expr2(overwrite(A,B),overwrite(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1138		norm_expr2(parallel_product(A,B),parallel_product(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1139		norm_expr2(partial_bijection(A,B),partial_bijection(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1140		norm_expr2(partial_function(A,B),partial_function(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1141		norm_expr2(partial_injection(A,B),partial_injection(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1142		norm_expr2(partial_surjection(A,B),partial_surjection(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1143		norm_expr2(perm(A),perm(AA)) :- norm_expr(A,AA).
1144		norm_expr2(power_of(A,B),power_of(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1145		norm_expr2(pow_subset(A),pow_subset(AA)) :- norm_expr(A,AA).
1146		norm_expr2(pow1_subset(A),pow1_subset(AA)) :- norm_expr(A,AA).
1147		norm_expr2(range_restriction(A,B),range_restriction(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1148		norm_expr2(range_subtraction(A,B),range_subtraction(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1149		norm_expr2(range(A),range(AA)) :- norm_expr(A,AA).
1150		norm_expr2(rec(A),rec(A)). % should we do norm_fields here ?
1151		norm_expr2(record_field(A,B),record_field(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1152		norm_expr2(relations(A,B),relations(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1153		norm_expr2(restrict_front(A,B),restrict_front(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1154		norm_expr2(restrict_tail(A,B),restrict_tail(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1155		norm_expr2(reflexive_closure(A),reflexive_closure(AA)) :- norm_expr(A,AA). % this is rewritten in ast_cleanup
1156		norm_expr2(rev(A),rev(AA)) :- norm_expr(A,AA).
1157		norm_expr2(reverse(A),reverse(AA)) :- norm_expr(A,AA).
1158		norm_expr2(second_of_pair(A),second_of_pair(AA)) :- norm_expr(A,AA).
1159		norm_expr2(seq(A),seq(AA)) :- norm_expr(A,AA).
1160		norm_expr2(seq1(A),seq1(AA)) :- norm_expr(A,AA).
1161		norm_expr2(sequence_extension(L),sequence_extension(NL)) :- l_norm_expr(L,NL).
1162		norm_expr2(set_extension(L),set_extension(NL)) :- l_norm_expr(L,NL).
1163		norm_expr2(set_subtraction(A,B),set_subtraction(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1164		norm_expr2(size(A),size(AA)) :- norm_expr(A,AA).
1165		norm_expr2(string(A),string(A)). % need wrapper to avoid confusion with other terms !
1166		norm_expr2(string_set,string_set).
1167		norm_expr2(struct(A),struct(A)). % should we do norm_fields here ?
1168		norm_expr2(surjection_relation(A,B),surjection_relation(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1169		norm_expr2(tail(A),tail(AA)) :- norm_expr(A,AA).
1170		norm_expr2(total_bijection(A,B),total_bijection(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1171		norm_expr2(total_function(A,B),total_function(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1172		norm_expr2(total_injection(A,B),total_injection(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1173		norm_expr2(total_relation(A,B),total_relation(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1174		norm_expr2(total_surjection(A,B),total_surjection(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1175		norm_expr2(total_surjection_relation(A,B),total_surjection_relation(AA,BB)) :- norm_expr(A,AA), norm_expr(B,BB).
1176
1177		norm_expr2(unary_minus(A),unary_minus(AA)) :- norm_expr(A,AA).
1178		norm_expr2(union(A,B),Res) :- norm_expr(A,AA), norm_expr(B,BB), (BB @< AA -> Res = union(AA,BB) ; Res= union(BB,AA)).
1179		norm_expr2(value(A),value(NA)) :- norm_value(A,NA).
1180
1181		norm_expr2(freetype_set(T),freetype_set(T)).
1182		norm_expr2(freetype_constructor(FT,Case,A), freetype_constructor(FT,Case,AA)) :- norm_expr(A,AA).
1183		norm_expr2(freetype_destructor(FT,Case,A),freetype_destructor(FT,Case,AA)) :- norm_expr(A,AA).
1184		norm_expr2(recursive_let(A,B),recursive_let(AA,BB)) :- norm_expr(A,AA),norm_expr(B,BB).
1185
1186		l_norm_expr([],[]).
1187		l_norm_expr([H|T],[NH|NT]) :- norm_expr(H,NH), l_norm_expr(T,NT).
1188
1189		norm_value(V,R) :- var(V),!,R=V.
1190		norm_value(closure(P,T,B),R) :- norm_pred(B,NB),
1191		!, % normalising relevant for test 1544 with position info aded by construct_member_closure
1192		R=closure(P,T,NB).
1193		norm_value(V,V). % we could normalise AVL
1194
1195		arithmetic_op(less(LHS,RHS),'<',LHS,RHS).
1196		arithmetic_op(less_equal(LHS,RHS),'<=',LHS,RHS).
1197		arithmetic_op(greater(LHS,RHS),'<',RHS,LHS).
1198		arithmetic_op(greater_equal(LHS,RHS),'<=',RHS,LHS).
1199
1200		:- use_module(clpfd_interface).
1201		check_arithmetic_operator('<',X,Y,Res) :- check_less(X,Y,Res),
1202		(nonvar(Res) -> true
1203		; clpfd_interface:try_post_constraint(clpfd:'#<=>'((X#<Y) , R01)), prop_pred_01(Res,R01)).
1204		check_arithmetic_operator('<=',X,Y,Res) :- check_less_than_equal(X,Y,Res),
1205		(nonvar(Res) -> true
1206		; clpfd_interface:try_post_constraint(clpfd:'#<=>'( (X#=<Y) , R01)), prop_pred_01(Res,R01)).
1207
1208		:- block prop_pred_01(-,-).
1209		% prop_pred_01(A,B) :- print(prop(A,B)),nl,fail.
1210		prop_pred_01(A,B) :- B==1,!,A=pred_true. % cut ok: either pred_true or 1 set
1211		prop_pred_01(pred_true,1).
1212		prop_pred_01(pred_false,0).
1213
1214		:- block check_less(-,?,-), check_less(?,-,-).
1215		check_less(X,Y,Res) :- nonvar(Res),!, /* truth value known: enforce it */
1216		%% print(forcing_less(X,Y,Res)),nl, %%
1217		(Res=pred_true -> less_than_direct(X,Y) ; less_than_equal_direct(Y,X)).
1218		check_less(X,Y,Res) :- % print(check_less(X,Y)),nl,%%
1219		X < Y,!,/* we could call safe_less_than(X,Y), */
1220		Res=pred_true.
1221		check_less(_,_,pred_false).
1222		:- block check_less_than_equal(-,?,-), check_less_than_equal(?,-,-).
1223		check_less_than_equal(X,Y,Res) :- nonvar(Res),!, /* truth value known: enforce it */
1224		%% print(forcing_less_than_equal(X,Y,Res)),nl,%%
1225		(Res=pred_true -> less_than_equal_direct(X,Y) ; less_than_direct(Y,X)).
1226		check_less_than_equal(X,Y,Res) :- X =< Y,!,Res=pred_true.
1227		check_less_than_equal(_,_,pred_false).
1228
1229
1230
1231		:- use_module(bool_pred).
1232
1233		:- use_module(kernel_objects,[exhaustive_kernel_check_wf/2,
1234		exhaustive_kernel_check/1, exhaustive_kernel_check/2, exhaustive_kernel_fail_check/1]).
1235
1236		:- 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)).
1237		:- 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)).
1238		:- 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)).
1239		:- 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)).
1240		:- assert_must_fail(b_interpreter_check:conjoin(pred_true,pred_false,pred_true,b(truth,pred,[]),b(truth,pred,[]),_WF)).
1241		:- assert_must_fail(b_interpreter_check:conjoin(pred_true,pred_true,pred_false,b(truth,pred,[]),b(truth,pred,[]),_WF)).
1242
1243
1244		% same as and_equality/3 but for pred_false/pred_true rather than eq_obj/pred_false
1245		:- block conjoin(-,-,-,?,?,?).
1246		conjoin(X,Y,Res,LHS,RHS,WF) :- % print(conjoin(X,Y,Res)),nl, translate:print_bexpr(LHS),nl,%
1247	?	( Res==pred_true -> X=pred_true,Y=pred_true
1248		; X==pred_true -> Res=Y
1249		; X==pred_false -> Res=pred_false
1250		; Y==pred_true -> Res=X
1251		; Y==pred_false -> Res=pred_false
1252		; Res==pred_false -> conjoin_false0(X,Y,LHS,RHS,WF)
1253		; add_error_fail(conjoin,'Illegal values: ', conjoin(X,Y,Res,LHS,RHS,WF))
1254		).
1255		conjoin_false0(X,Y,_LHS,_RHS,_WF) :- X==Y,!,
1256		%print(conjoin_false_eqeq(X,Y)),nl, translate:print_bexpr(_LHS),nl,
1257		X=pred_false.
1258		conjoin_false0(X,Y,_LHS,_RHS,_WF) :- % X & not(X) -> always false
1259		bool_negate_check(X,Y),!
1260		. %,print(conjoin_false_neqeq(X,Y)),nl,translate:print_bexpr(_LHS),nl.
1261		conjoin_false0(X,Y,LHS,RHS,WF) :-
1262		%%Prio=1, %%
1263		%%(preferences:preference(use_smt_mode,full) -> FullPrio=1.5 ;
1264		get_priority_of_boolean_expression(LHS,Prio),
1265		(preferences:preference(use_clpfd_solver,true) ->
1266		% relevant for tests 349, 362:
1267		count_number_of_conjuncts(RHS,NrC),
1268		FullPrio is Prio+(NrC-1)/10,
1269		get_wait_flag(FullPrio,conjoin,WF,LWF) %%
1270		; % in non-clpfd mode: much less propagation going on, avoid explosion of choice points
1271		% tests 349, 362 fail with the following for CLPFD: TO DO investigate and use this also in CLPFD mode
1272		get_binary_choice_wait_flag_exp_backoff(Prio,not_conjunct,WF,LWF)
1273		),
1274		% print('SETUP conjoin_false: '), print(FullPrio), print(' '), print(NrC), print(' '), translate:print_bexpr(LHS),nl, % kernel_waitflags:portray_waitflags(WF),
1275		conjoin_false(X,Y,LHS,RHS,LWF).
1276		% missing rule: if X==Y -> X=pred_true
1277		:- block conjoin_false(-,-,?,?,-).
1278		conjoin_false(X,Y,LHS,_RHS,_LWF) :- % print(conjoin_false(X,Y)),nl, translate:print_bexpr(LHS),nl,%
1279	?	( X==pred_true -> % print('TRUE: '), translate:print_bexpr(LHS),nl,
1280		% print(' FORCING FALSE: '), translate:print_bexpr(_RHS),nl,
1281		pred_false=Y
1282	?	; X==pred_false -> true % , print('FALSE: '), translate:print_bexpr(LHS),nl
1283	?	; Y==pred_true -> pred_false=X
1284	?	; Y==pred_false -> true %, print('FALSE: '), translate:print_bexpr(_RHS),nl
1285	?	; useless_to_force(LHS) ->
1286		( % print(forcing_conjoin_rhs_false(X,Y,_LWF)), translate:print_bexpr(_RHS), print(' == FALSE '),nl,
1287		Y=pred_false
1288		;
1289		(Y,X)=(pred_true,pred_false)
1290		)
1291		; ( % print(forcing_conjoin_lhs_false(X,Y,_LWF)), translate:print_bexpr(LHS), print(' == FALSE '),nl,
1292	?	X=pred_false
1293		; % print(forcing_conjoin_rhs_false(X,Y,_LWF)), translate:print_bexpr(LHS), print(' == TRUE ; '), nl,
1294		(X,Y)=(pred_true,pred_false)
1295		)
1296		).
1297
1298		% determine when forcing a predicate to true/false does not really help; better choose something else
1299		useless_to_force(b(B,T,I)) :- useless_to_force3(B,T,I).
1300		useless_to_force3(finite(_),_,_). % forcing finite to be false usually not a good idea; we cannot propagate this
1301		% what are other predicates useless to force: some foralls/exists ? some external_pred_call
1302		% in principle a conjunction of useless predicates is also useless: but could be more expensive to check
1303
1304		:- assert_must_succeed(exhaustive_kernel_check(b_interpreter_check:disjoin(pred_false,pred_false,pred_false,_,_,_WF))).
1305		:- assert_must_succeed(exhaustive_kernel_check([commutative],b_interpreter_check:disjoin(pred_false,pred_true,pred_true,_,_,_WF))).
1306		:- assert_must_succeed(exhaustive_kernel_check(b_interpreter_check:disjoin(pred_true,pred_true,pred_true,_,_,_WF))).
1307		:- assert_must_succeed(exhaustive_kernel_fail_check(b_interpreter_check:disjoin(pred_true,pred_true,pred_false,_,_,_WF))).
1308		:- assert_must_succeed(exhaustive_kernel_fail_check(b_interpreter_check:disjoin(pred_true,pred_false,pred_false,_,_,_WF))).
1309		:- assert_must_succeed(exhaustive_kernel_fail_check(b_interpreter_check:disjoin(pred_false,pred_true,pred_false,_,_,_WF))).
1310		:- assert_must_succeed(exhaustive_kernel_fail_check(b_interpreter_check:disjoin(pred_false,pred_false,pred_true,_,_,_WF))).
1311
1312		:- block disjoin(-,-,-,?,?,?).
1313		disjoin(X,Y,Res,LHS,RHS,WF) :- %print(disjoin(X,Y,Res,WF)),nl, %% translate:print_bexpr(LHS),print(' or '),translate:print_bexpr(RHS),nl,%%
1314	?	( Res==pred_false -> X=pred_false,Y=pred_false
1315		; X==pred_true -> Res=pred_true
1316		; X==pred_false -> Res=Y
1317		; Y==pred_true -> Res=pred_true
1318		; Y==pred_false -> Res=X
1319		; Res==pred_true -> disjoin_true0(X,Y,LHS,RHS,WF)
1320		; add_error_fail(disjoin,'Illegal values: ',disjoin(X,Y,Res,LHS,RHS,WF))
1321		).
1322		disjoin_true0(X,Y,_LHS,_RHS,_WF) :- X==Y,!,
1323		%print(disjoin_true_eqeq(X,Y)),nl, translate:print_bexpr(_LHS),nl,
1324		X=pred_true.
1325		%disjoin_true0(X,Y,LHS,_,WF) :- !, disjoin_true(X,Y,_).
1326		disjoin_true0(X,Y,_LHS,_RHS,_WF) :- % X or not(X) -> always true
1327		bool_negate_check(X,Y),!.
1328		%,print(disjoin_true_neqeq(X,Y)),nl,translate:print_bexpr(_LHS),nl.
1329
1330		disjoin_true0(X,Y,LHS,_RHS,WF) :- %% print('disjoin_true0 '), translate:print_bexpr(LHS), print(' OR '), translate:print_bexpr(_RHS),nl, %%
1331		%%(preferences:preference(use_smt_mode,full) -> FullPrio=2.5 ;
1332		% poses problem for test 1096:
1333		% count_number_of_disjuncts(RHS,NrC),
1334		%FullPrio is Prio+(NrC-1)/10, % print(disj_prio(Prio,NrC,RHS,FullPrio)),nl,
1335		%print(prio(FullPrio,NrC)),nl,
1336		%get_wait_flag(FullPrio,disjoin,WF,LWF), %%
1337		get_priority_of_boolean_expression(LHS,StartPrio),
1338		get_binary_choice_wait_flag_exp_backoff(StartPrio,disjunct,WF,LWF),
1339		% TO DO: extract FD information from LHS and RHS and assert, e.g. x:1..2 or x:4..5
1340		disjoin_true(X,Y,LHS,LWF).
1341		% missing rule: if X==Y -> X=pred_true ; if X==~Y -> no need to setup choice point
1342		:- block disjoin_true(-,-,?,-).
1343		disjoin_true(X,Y,LHS,_LWF) :- %% print(disjoin_true(X,Y,_LWF)),nl, %%
1344	?	( X==pred_true -> true
1345	?	; X==pred_false -> pred_true=Y
1346	?	; Y==pred_true -> true
1347	?	; Y==pred_false -> pred_true=X
1348	?	; useless_to_force(LHS) ->
1349		( %% print(forcing_disjoin_true(X,Y,_LWF)),nl, %%
1350		Y=pred_true
1351		;
1352		%%print(forcing_disjoin_false(X,Y,_LWF)),nl,
1353		(Y,X) = (pred_false,pred_true) % these two unifications will happen atomically !
1354		)
1355		; ( %% print(forcing_disjoin_true(X,Y,_LWF)),nl, %%
1356	?	X=pred_true
1357		;
1358		%%print(forcing_disjoin_false(X,Y,_LWF)),nl,
1359	?	(X,Y) = (pred_false,pred_true) % these two unifications will happen atomically !
1360		)
1361		%add_error_fail(disjoin_true,'Illegal values: ',disjoin_true(X,Y))
1362		).
1363
1364		:- assert_must_succeed(exhaustive_kernel_check(b_interpreter_check:impl(pred_false,pred_false,pred_true))).
1365		:- assert_must_succeed(exhaustive_kernel_check(b_interpreter_check:impl(pred_false,pred_true,pred_true))).
1366		:- assert_must_succeed(exhaustive_kernel_check(b_interpreter_check:impl(pred_true,pred_false,pred_false))).
1367		:- assert_must_succeed(exhaustive_kernel_check(b_interpreter_check:impl(pred_true,pred_true,pred_true))).
1368		:- assert_must_succeed(exhaustive_kernel_fail_check(b_interpreter_check:impl(pred_false,pred_false,pred_false))).
1369		:- assert_must_succeed(exhaustive_kernel_fail_check(b_interpreter_check:impl(pred_false,pred_true,pred_false))).
1370		:- assert_must_succeed(exhaustive_kernel_fail_check(b_interpreter_check:impl(pred_true,pred_false,pred_true))).
1371		:- assert_must_succeed(exhaustive_kernel_fail_check(b_interpreter_check:impl(pred_true,pred_true,pred_false))).
1372
1373		impl(X,Y,Res) :- % print(impl(X,Y,Res)),nl,
1374		(var(X),var(Y),var(Res) -> bool_equality(X,Y,EqXY) ; true /* impl4 will not block anyway */),
1375		impl4(X,Y,EqXY,Res).
1376		:- block impl4(-,-,-,-).
1377		impl4(X,Y,EqXY,Res) :-
1378		( Res==pred_false -> X=pred_true,Y=pred_false
1379		; Res==pred_true -> imply_true(X,Y,EqXY)
1380		; X==pred_false -> Res=pred_true
1381		; X==pred_true -> Res=Y
1382		; Y==pred_true -> Res=pred_true
1383		; Y==pred_false -> negate(X,Res)
1384		; EqXY==pred_true -> Res=pred_true % X => X is always true
1385		; EqXY==pred_false -> Y=Res % not(Y) => Y is true iff Y is true
1386		; add_error_fail(impl,'Illegal values: ',impl(X,Y,EqXY,Res))
1387		).
1388		imply_true(X,Y) :- %print(imply_true(X,Y)),nl,
1389		(var(X),var(Y) -> bool_equality(X,Y,EqXY) ; true /* imply_true will not block anyway */),
1390		imply_true(X,Y,EqXY).
1391		:- block imply_true(-,-,-).
1392		imply_true(X,Y,EqXY) :- %print(imply_true(X,Y,EqXY)),nl,
1393		( X==pred_false -> true
1394		; X==pred_true -> Y=pred_true
1395		; Y==pred_true -> true
1396		; Y==pred_false -> X=pred_false
1397		; EqXY==pred_true -> true
1398		; EqXY==pred_false -> X=pred_false % X => not(X) ===> X=pred_false
1399		; add_error_fail(imply_true,'Illegal values: ',imply_true(X,Y,EqXY))
1400		).
1401
1402
1403		:- assert_must_succeed(exhaustive_kernel_check(b_interpreter_check:equiv(pred_false,pred_false,pred_true))).
1404		:- assert_must_succeed(exhaustive_kernel_check(b_interpreter_check:equiv(pred_false,pred_true,pred_false))).
1405		:- assert_must_succeed(exhaustive_kernel_check(b_interpreter_check:equiv(pred_true,pred_false,pred_false))).
1406		:- assert_must_succeed(exhaustive_kernel_check(b_interpreter_check:equiv(pred_true,pred_true,pred_true))).
1407		:- assert_must_succeed(exhaustive_kernel_fail_check(b_interpreter_check:equiv(pred_false,pred_false,pred_false))).
1408		:- assert_must_succeed(exhaustive_kernel_fail_check(b_interpreter_check:equiv(pred_false,pred_true,pred_true))).
1409		:- assert_must_succeed(exhaustive_kernel_fail_check(b_interpreter_check:equiv(pred_true,pred_false,pred_true))).
1410		:- assert_must_succeed(exhaustive_kernel_fail_check(b_interpreter_check:equiv(pred_true,pred_true,pred_false))).
1411
1412		% b_interpreter_check:equiv(X,Y,Res),X=Y, Res==pred_true
1413		equiv(X,Y,Res) :- %print(equiv(X,Y,Res)),nl,
1414		bool_equality(X,Y,Res).
1415
1416