1		% (c) 2016-2024 Lehrstuhl fuer Softwaretechnik und Programmiersprachen,
2		% Heinrich Heine Universitaet Duesseldorf
3		% This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html)
4
5		:- module(clpfd_tables,[can_translate_avl_to_table/2, translate_avl_to_table/2, check_element_of_table/4,
6		check_element_of_avl_with_table/4,
7		clpfd_in_table/2,
8
9		can_translate_function_to_element_constraint/2,
10		check_apply_with_element_constraint/5]).
11
12		:- use_module(module_information,[module_info/2]).
13		:- module_info(group,kernel).
14		:- module_info(description,'Provide interface to CLP(FD) table constraint.').
15
16		% Example usage of CLPFD table/2 :
17		%| ?- table([[X,Y]],[[1,2],[2,3],[3,4],[4,5]]), X in 1..2.
18		%X in 1..2,
19		%Y in 2..3 ?
20
21		:- use_module(library(clpfd)).
22		:- use_module(library(avl),[avl_domain/2]).
23		:- use_module(library(lists),[maplist/3, maplist/4, maplist/2]).
24		:- use_module(kernel_waitflags,[add_fd_variables_for_labeling/2]).
25		:- use_module(debug,[debug_println/2]).
26		:- use_module(error_manager,[add_internal_error/2]).
27
28		% can an AVL set be translated into a CLPFD table membership constraint
29		can_translate_avl_to_table(AVL,SkeletonType) :-
30		AVL = node(Element,_True,_,_,_),
31		translate_to_fd_values(Element,SkeletonType,ElVList,[]),
32		l_no_overflow(ElVList), % check that the element constraint will not generate an overflow, e.g., for test 1353
33		% TO DO: ideally we should check avl_min / avl_max
34		% (but with multiple FD values in an element; even that will not guarantee that there are no overflows)
35		SkeletonType \= boolean. % should we also disallow rec([field(_,boolean)]) % boolean treatment causes problems for 1624, 1627, 140, 1426
36
37		l_no_overflow([]).
38		l_no_overflow([H|T]) :- no_overflow(H), l_no_overflow(T).
39
40		:- use_module(tools_platform, [is_tagged_integer/1]).
41		no_overflow(H) :- (var(H) -> true ; is_tagged_integer(H)).
42
43		translate_avl_to_table(AVL,TableList) :-
44		avl_domain(AVL,List),
45		maplist(translate_avl_element_to_fd_list,List,TableList).
46
47		check_element_of_avl_with_table(X,SkeletonType,AVL,WF) :-
48		translate_avl_to_table(AVL,TableList),
49	?	check_element_of_table(X,SkeletonType,TableList,WF).
50
51		check_element_of_table(X,SkeletonType,TableList,WF) :-
52	?	translate_to_fd_values(X,SkeletonType,XList,[]),
53		clpfd_in_table(XList,TableList),
54		add_fd_variables_for_labeling(XList,WF). % important for test 1716
55
56
57		:- use_module(clpfd_interface,[force_clpfd_inlist/2]).
58		get_unique_el([X],X).
59		clpfd_in_table([X],TableList) :- !, maplist(get_unique_el,TableList,FDList),
60		%print(posting_clpfd_inlist(X,FDList)),nl,
61		force_clpfd_inlist(X,FDList).
62		:- if(current_prolog_flag(dialect, sicstus)).
63		:- if((current_prolog_flag(version_data, sicstus(4,VN,_,_,_)),VN>7)).
64		clpfd_in_table(XList,TableList) :-
65		table([XList],TableList,[order(id3)]). % use method(default) (SICStus choice handles propagation as it sees fit)
66		:- else.
67		clpfd_in_table(XList,TableList) :-
68		table([XList],TableList,[method(aux)]).
69		% we use aux to circumvent a bug in SICStus 4.4-4.7
70		% but method(aux) did slow down test 1753 considerably (15 secs down to 1-2 minutes, before not_exists improved)
71		:- endif.
72		:-else.
73		clpfd_in_table(XList,TableList) :-
74		table([XList],TableList). % translated to tuples_in in SWI
75		:- endif.
76		% from the SICStus Manual:
77		% table(+Tuples,+Extension,+Options)
78		% Defines an n-ary constraint by extension. Extension should be a list of lists of
79		% integers, each of length n. Tuples should be a list of lists of domain variables,
80		% each also of length n. The constraint holds if every Tuple in Tuples occurs in
81		% the Extension. The constraint will maintain domain consistency.
82		% For convenience, Extension may contain ConstantRange (see Section 10.10.13.1
83		% [Syntax of Indexicals], page 485) expressions in addition to integers.
84		%
85		% WARNING, SICSTUS 4.7 and earlier has a bug with negative numbers
86		% | ?- clpfd:table([[X,Y]],[[1,0],[2,-1]]).
87		% Y = 0, <-- this should not be !!
88		% X in 1..2
89		% with aux as method we solve the issue
90		% | ?- clpfd:table([[X,Y]],[[1,0],[2,-1]],[method(aux)]).
91		% X in 1..2,
92		% Y in-1..0
93
94		% TO DO: also allow partial FD infos, in which case we would use table/2 just for quick propagation
95		% we could also translate variables into ConstantRange expressions (see above)
96		translate_avl_element_to_fd_list(Val,FDList) :- translate_to_fd_values(Val,_,FDList,[]).
97
98		translate_to_fd_values(FD,fd(T)) --> {var(FD),nonvar(T)},!, % setup FD bounds
99		{get_global_type_value(FD,T,X)},[X].
100		translate_to_fd_values(fd(X,T),fd(T)) --> !, [X].
101		translate_to_fd_values(int(A),integer) --> !, [A]. % warning: could overflow, we check above !
102	?	translate_to_fd_values((A,B),(SkelA,SkelB)) --> !, translate_to_fd_values(A,SkelA), translate_to_fd_values(B,SkelB).
103	?	translate_to_fd_values(rec(F),rec(SkelF)) --> !, l_translate_to_fd_values(F,SkelF).
104		translate_to_fd_values(Var,Type) --> {var(Var),Type==boolean},!, {prop_01(Var,FD)},[FD].
105		translate_to_fd_values(pred_true,boolean) --> [1].
106		translate_to_fd_values(pred_false,boolean) --> [0].
107		% TO DO: also free-types
108
109		l_translate_to_fd_values([],[]) --> [].
110		l_translate_to_fd_values([field(N,F)|T],[field(N,SF)|ST]) -->
111	?	translate_to_fd_values(F,SF),l_translate_to_fd_values(T,ST).
112
113		:- block prop_01(-,-).
114		prop_01(pred_true,1).
115		prop_01(pred_false,0).
116
117		% ----------------------
118
119		:- use_module(bsyntaxtree,[is_set_type/2]).
120		:- use_module(preferences,[preference/2]).
121
122		% can a list be translated into CLPFD element constraints for function application
123		can_translate_function_to_element_constraint(List,FunctionType) :-
124		FunctionType \= unknown,
125		is_list_skeleton(List), % TO DO: allow tail AVL list + enable delaying treatment
126		preference(find_abort_values,false),
127		preference(use_clpfd_solver,true),
128		% initially we checked if chr is false to avoid falling into the SICStus element/3 bug prior to 4.3.6
129		is_set_type(FunctionType,couple(Domain,Range)),
130		is_simple_fd_type(Domain), % Domain must be translatable to simple FD value list
131		is_fd_type(Range).
132
133		is_list_skeleton(X) :- nonvar(X),is_list_skeleton_aux(X).
134		is_list_skeleton_aux([]).
135		is_list_skeleton_aux([_H|T]) :- is_list_skeleton(T).
136
137		is_simple_fd_type(global(_)).
138		is_simple_fd_type(integer).
139		is_simple_fd_type(boolean).
140
141		is_fd_type(couple(A,B)) :- !, is_fd_type(A), is_fd_type(B).
142		is_fd_type(record(F)) :- !, is_fd_field_types(F).
143		is_fd_type(X) :- is_simple_fd_type(X).
144
145		is_fd_field_types([]).
146		is_fd_field_types([field(_,FT)|T]) :- is_fd_type(FT), is_fd_field_types(T).
147
148		:- use_module(b_global_sets,[get_global_type_value/3]).
149		get_fd_type(couple(A,B),(VA,VB)) --> get_fd_type(A,VA), get_fd_type(B,VB).
150		get_fd_type(global(T),FD) --> {get_global_type_value(FD,T,X)}, [X].
151		get_fd_type(integer,int(X)) --> [X].
152		get_fd_type(boolean,B) --> [FD], {prop_01(B,FD)}.
153		get_fd_type(record(Fields),rec(VF)) --> get_field_fd_types(Fields,VF).
154
155		get_field_fd_types([],[]) --> [].
156		get_field_fd_types([field(Name,Type)|FT],[field(Name,VF)|VT]) -->
157		get_fd_type(Type,VF),
158		get_field_fd_types(FT,VT).
159
160		get_fd_types(Domain,Range,(VD,VR),FDDom,FDRList) :- get_fd_type(Domain,VD,[FDDom],[]), get_fd_type(Range,VR,FDRList,[]).
161
162		% Examples:
163		% f = {x|->2, y|->3} & x:1..2 & y:4..5 & r = f(4)
164		% f = {x|->(2,x+1), y|->(3,y+1)} & x:1..2 & y:4..5 & r = f(v) & v:3..4 --> deterministically sets v=4, r=(3,5),y=4
165		% from the SICStus manual:
166		% element(?X,+List,?Y)
167		% where X and Y are domain variables and List is a list of domain variables. True
168		% if the X:th element of List is Y. Operationally, the domains of X and Y are
169		% constrained so that for every element in the domain of X, there is a compatible
170		% element in the domain of Y, and vice versa.
171		% Maintains domain consistency in X and bounds consistency in List and Y.
172		% Corresponds to nth1/3 in library(lists) and to element in MiniZinc
173
174		:- use_module(library(clpfd),[all_distinct/1]).
175		:- use_module(library(lists),[nth1/3]).
176		check_apply_with_element_constraint(List,X,Y,FunctionType,WF) :-
177		is_set_type(FunctionType,couple(Domain,Range)),
178		get_fd_type(Domain,X,[FDX],[]),
179		if(l_get_fd_types(List,DomainList,RangeLists,Domain,Range,FDX,FoundY),true,
180		(add_internal_error('Get FD Types failed: ',get_fd_types(Domain,Range)),fail)),
181		debug_println(4,element_domain_list(FDX,DomainList)),
182		(FoundY \== y_not_found
183		-> FoundY=Y % no need for equal_object: we only have FD types + Bool + couples (+ record of them)
184		% TODO: check that for records we can also use unification
185		; element(Idx,DomainList,FDX), % no need to call equal_object for X as we have simple fd types
186		% DomainList are the elements of the domain of the function
187		(nonvar(Idx)
188		-> nth1(Idx,List,(X,Y)) %relevant for tests 387, 1579
189		; all_distinct(DomainList), % ensures that Idx will get bound eventually if we enumerate DomainList and X (if multiple entries in DomainList then Idx would not get bound)
190		maplist(get_fd_types(Domain,Range),List,DomainList,RangeLists),
191		get_fd_type(Range,Y,FDYList,[]),
192		setup_element_range_constraints(FDYList,Idx,RangeLists),
193		% tools_printing:print_term_summary(element_constraint(FDX,FDYList,Idx,DomainList)),nl,
194		% used to call this: add_fd_variables_for_labeling([FDX|FDYList],WF) but not sure if we need to enumerate FDYList
195		add_fd_variables_for_labeling([FDX],WF) % FDX can have an infinite domain; e.g., test 1717
196		)
197		).
198
199		% an unfolded version of maplist(get_fd_types(Domain,Range),List,DomainList,RangeLists)
200		% we also check if the lookup FD variable occurs in the list; if so we return the Y value in Found
201		% relevant for performance, e.g., for NQueens60; we avoid traversing the list a second time
202		l_get_fd_types([],[],[],_,_,_,y_not_found).
203		l_get_fd_types([Pair|PT],[FDDom|DT],[FDRList|RT],Domain,Range,FDX,FoundY) :-
204		get_fd_types(Domain,Range,Pair,FDDom,FDRList),
205		(FDX==FDDom -> Pair=(_,FoundY), DT=[],RT=[]
206		; l_get_fd_types(PT,DT,RT,Domain,Range,FDX,FoundY)).
207
208
209		setup_element_range_constraints([],_,_).
210		setup_element_range_constraints([FDY|YT],Idx,RangeLists) :-
211		maplist(get_next_fd,RangeLists,FDYList,RestLists),
212		% print(setting_up_range_element_constraint(Idx,FDYList,FDY)),nl,
213		element(Idx,FDYList,FDY),
214		setup_element_range_constraints(YT,Idx,RestLists).
215
216		get_next_fd([H|T],H,T).