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		clpfd_in_table(XList,TableList) :-
64		%print(posting_clpfd_table([XList],TableList)),nl,
65	?	table([XList],TableList,[method(aux)]). % we use aux to circumvent a bug in SICStus 4.4-4.7
66		% we could provide in third argument, e.g., [order(id3)]
67		:-else.
68		clpfd_in_table(XList,TableList) :-
69		%print(posting_clpfd_table([XList],TableList)),nl,
70		table([XList],TableList). % translated to tuples_in in SWI
71		:- endif.
72		% from the SICStus Manual:
73		% table(+Tuples,+Extension,+Options)
74		% Defines an n-ary constraint by extension. Extension should be a list of lists of
75		% integers, each of length n. Tuples should be a list of lists of domain variables,
76		% each also of length n. The constraint holds if every Tuple in Tuples occurs in
77		% the Extension. The constraint will maintain domain consistency.
78		% For convenience, Extension may contain ConstantRange (see Section 10.10.13.1
79		% [Syntax of Indexicals], page 485) expressions in addition to integers.
80		%
81		% WARNING, SICSTUS 4.7 and earlier has a bug with negative numbers
82		% | ?- clpfd:table([[X,Y]],[[1,0],[2,-1]]).
83		% Y = 0, <-- this should not be !!
84		% X in 1..2
85		% with aux as method we solve the issue
86		% | ?- clpfd:table([[X,Y]],[[1,0],[2,-1]],[method(aux)]).
87		% X in 1..2,
88		% Y in-1..0
89
90		% TO DO: also allow partial FD infos, in which case we would use table/2 just for quick propagation
91		% we could also translate variables into ConstantRange expressions (see above)
92		translate_avl_element_to_fd_list(Val,FDList) :- translate_to_fd_values(Val,_,FDList,[]).
93
94		translate_to_fd_values(FD,fd(T)) --> {var(FD),nonvar(T)},!, % setup FD bounds
95		{get_global_type_value(FD,T,X)},[X].
96		translate_to_fd_values(fd(X,T),fd(T)) --> !, [X].
97		translate_to_fd_values(int(A),integer) --> !, [A]. % warning: could overflow, we check above !
98	?	translate_to_fd_values((A,B),(SkelA,SkelB)) --> !, translate_to_fd_values(A,SkelA), translate_to_fd_values(B,SkelB).
99	?	translate_to_fd_values(rec(F),rec(SkelF)) --> !, l_translate_to_fd_values(F,SkelF).
100		translate_to_fd_values(Var,Type) --> {var(Var),Type==boolean},!, {prop_01(Var,FD)},[FD].
101		translate_to_fd_values(pred_true,boolean) --> [1].
102		translate_to_fd_values(pred_false,boolean) --> [0].
103		% TO DO: also free-types
104
105		l_translate_to_fd_values([],[]) --> [].
106		l_translate_to_fd_values([field(N,F)|T],[field(N,SF)|ST]) -->
107	?	translate_to_fd_values(F,SF),l_translate_to_fd_values(T,ST).
108
109		:- block prop_01(-,-).
110		prop_01(pred_true,1).
111		prop_01(pred_false,0).
112
113		% ----------------------
114
115		:- use_module(bsyntaxtree,[is_set_type/2]).
116		:- use_module(preferences,[preference/2]).
117
118		% can a list be translated into CLPFD element constraints for function application
119		can_translate_function_to_element_constraint(List,FunctionType) :-
120		FunctionType \= unknown,
121		is_list_skeleton(List), % TO DO: allow tail AVL list + enable delaying treatment
122		preference(find_abort_values,false),
123		preference(use_clpfd_solver,true),
124		% initially we checked if chr is false to avoid falling into the SICStus element/3 bug prior to 4.3.6
125		is_set_type(FunctionType,couple(Domain,Range)),
126		is_simple_fd_type(Domain), % Domain must be translatable to simple FD value list
127		is_fd_type(Range).
128
129		is_list_skeleton(X) :- nonvar(X),is_list_skeleton_aux(X).
130		is_list_skeleton_aux([]).
131		is_list_skeleton_aux([_H|T]) :- is_list_skeleton(T).
132
133		is_simple_fd_type(global(_)).
134		is_simple_fd_type(integer).
135		is_simple_fd_type(boolean).
136
137		is_fd_type(couple(A,B)) :- !, is_fd_type(A), is_fd_type(B).
138		is_fd_type(record(F)) :- !, is_fd_field_types(F).
139		is_fd_type(X) :- is_simple_fd_type(X).
140
141		is_fd_field_types([]).
142		is_fd_field_types([field(_,FT)|T]) :- is_fd_type(FT), is_fd_field_types(T).
143
144		:- use_module(b_global_sets,[get_global_type_value/3]).
145		get_fd_type(couple(A,B),(VA,VB)) --> get_fd_type(A,VA), get_fd_type(B,VB).
146		get_fd_type(global(T),FD) --> {get_global_type_value(FD,T,X)}, [X].
147		get_fd_type(integer,int(X)) --> [X].
148		get_fd_type(boolean,B) --> [FD], {prop_01(B,FD)}.
149		get_fd_type(record(Fields),rec(VF)) --> get_field_fd_types(Fields,VF).
150
151		get_field_fd_types([],[]) --> [].
152		get_field_fd_types([field(Name,Type)|FT],[field(Name,VF)|VT]) -->
153		get_fd_type(Type,VF),
154		get_field_fd_types(FT,VT).
155
156		get_fd_types(Domain,Range,(VD,VR),FDDom,FDRList) :- get_fd_type(Domain,VD,[FDDom],[]), get_fd_type(Range,VR,FDRList,[]).
157
158		% Examples:
159		% f = {x|->2, y|->3} & x:1..2 & y:4..5 & r = f(4)
160		% 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
161		% from the SICStus manual:
162		% element(?X,+List,?Y)
163		% where X and Y are domain variables and List is a list of domain variables. True
164		% if the X:th element of List is Y. Operationally, the domains of X and Y are
165		% constrained so that for every element in the domain of X, there is a compatible
166		% element in the domain of Y, and vice versa.
167		% Maintains domain consistency in X and bounds consistency in List and Y.
168		% Corresponds to nth1/3 in library(lists) and to element in MiniZinc
169
170		:- use_module(library(clpfd),[all_distinct/1]).
171		:- use_module(library(lists),[nth1/3]).
172		check_apply_with_element_constraint(List,X,Y,FunctionType,WF) :-
173		is_set_type(FunctionType,couple(Domain,Range)),
174		get_fd_type(Domain,X,[FDX],[]),
175		if(l_get_fd_types(List,DomainList,RangeLists,Domain,Range,FDX,FoundY),true,
176		(add_internal_error('Get FD Types failed: ',get_fd_types(Domain,Range)),fail)),
177		debug_println(4,element_domain_list(FDX,DomainList)),
178		(FoundY \== y_not_found
179		-> FoundY=Y % no need for equal_object: we only have FD types + Bool + couples (+ record of them)
180		% TODO: check that for records we can also use unification
181		; element(Idx,DomainList,FDX), % no need to call equal_object for X as we have simple fd types
182		% DomainList are the elements of the domain of the function
183		(nonvar(Idx)
184		-> nth1(Idx,List,(X,Y)) %relevant for tests 387, 1579
185		; 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)
186		maplist(get_fd_types(Domain,Range),List,DomainList,RangeLists),
187		get_fd_type(Range,Y,FDYList,[]),
188		setup_element_range_constraints(FDYList,Idx,RangeLists),
189		% tools_printing:print_term_summary(element_constraint(FDX,FDYList,Idx,DomainList)),nl,
190		% used to call this: add_fd_variables_for_labeling([FDX|FDYList],WF) but not sure if we need to enumerate FDYList
191		add_fd_variables_for_labeling([FDX],WF) % FDX can have an infinite domain; e.g., test 1717
192		)
193		).
194
195		% an unfolded version of maplist(get_fd_types(Domain,Range),List,DomainList,RangeLists)
196		% we also check if the lookup FD variable occurs in the list; if so we return the Y value in Found
197		% relevant for performance, e.g., for NQueens60; we avoid traversing the list a second time
198		l_get_fd_types([],[],[],_,_,_,y_not_found).
199		l_get_fd_types([Pair|PT],[FDDom|DT],[FDRList|RT],Domain,Range,FDX,FoundY) :-
200		get_fd_types(Domain,Range,Pair,FDDom,FDRList),
201		(FDX==FDDom -> Pair=(_,FoundY), DT=[],RT=[]
202		; l_get_fd_types(PT,DT,RT,Domain,Range,FDX,FoundY)).
203
204
205		setup_element_range_constraints([],_,_).
206		setup_element_range_constraints([FDY|YT],Idx,RangeLists) :-
207		maplist(get_next_fd,RangeLists,FDYList,RestLists),
208		% print(setting_up_range_element_constraint(Idx,FDYList,FDY)),nl,
209		element(Idx,FDYList,FDY),
210		setup_element_range_constraints(YT,Idx,RestLists).
211
212		get_next_fd([H|T],H,T).