1		% (c) 2016-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(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		maplist(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 (but with multiple FD values in an element; even that will not guarantee that there are no overflows)
34		%(ElVList = [_,_|_] -> true ; print(Element),nl,fail,trace,true),
35		SkeletonType \= boolean. % should we also disallow rec([field(_,boolean)]) % boolean treatment causes problems for 1624, 1627, 140, 1426
36
37		:- use_module(tools,[is_tagged_integer/1]).
38		no_overflow(H) :- (var(H) -> true ; is_tagged_integer(H)).
39
40		translate_avl_to_table(AVL,TableList) :-
41		avl_domain(AVL,List),
42		maplist(translate_avl_element_to_fd_list,List,TableList).
43
44		check_element_of_avl_with_table(X,SkeletonType,AVL,WF) :-
45		translate_avl_to_table(AVL,TableList),
46		check_element_of_table(X,SkeletonType,TableList,WF).
47
48		check_element_of_table(X,SkeletonType,TableList,WF) :-
49		translate_to_fd_values(X,SkeletonType,XList,[]),
50		clpfd_in_table(XList,TableList),
51		add_fd_variables_for_labeling(XList,WF).
52
53		:- use_module(clpfd_interface,[clpfd_inlist/2]).
54		get_unique_el([X],X).
55		clpfd_in_table([X],TableList) :- !, maplist(get_unique_el,TableList,FDList),
56		%print(posting_clpfd_inlist(X,FDList)),nl,
57		clpfd_inlist(X,FDList).
58		clpfd_in_table(XList,TableList) :-
59		%print(posting_clpfd_table([XList],TableList)),nl,
60		clpfd:table([XList],TableList). % we could provide optional third argument, e.g., [order(id3)]
61		% from the SICStus Manual:
62		% table(+Tuples,+Extension,+Options)
63		% Defines an n-ary constraint by extension. Extension should be a list of lists of
64		% integers, each of length n. Tuples should be a list of lists of domain variables,
65		% each also of length n. The constraint holds if every Tuple in Tuples occurs in
66		% the Extension. The constraint will maintain domain consistency.
67		% For convenience, Extension may contain ConstantRange (see Section 10.10.13.1
68		% [Syntax of Indexicals], page 485) expressions in addition to integers.
69
70		% TO DO: also allow partial FD infos, in which case we would use table/2 just for quick propagation
71		% we could also translate variables into ConstantRange expressions (see above)
72		translate_avl_element_to_fd_list(Val,FDList) :- translate_to_fd_values(Val,_,FDList,[]).
73
74		translate_to_fd_values(FD,fd(T)) --> {var(FD),nonvar(T)},!, % setup FD bounds
75		{get_global_type_value(FD,T,X)},[X].
76		translate_to_fd_values(fd(X,T),fd(T)) --> !, [X].
77		translate_to_fd_values(int(A),integer) --> !, [A]. % warning: could overflow, we check above !
78		translate_to_fd_values((A,B),(SkelA,SkelB)) --> !, translate_to_fd_values(A,SkelA), translate_to_fd_values(B,SkelB).
79		translate_to_fd_values(rec(F),rec(SkelF)) --> !, l_translate_to_fd_values(F,SkelF).
80		translate_to_fd_values(Var,Type) --> {var(Var),Type==boolean},!, {prop_01(Var,FD)},[FD].
81		translate_to_fd_values(pred_true,boolean) --> [1].
82		translate_to_fd_values(pred_false,boolean) --> [0].
83		% TO DO: also free-types
84
85		l_translate_to_fd_values([],[]) --> [].
86		l_translate_to_fd_values([field(N,F)|T],[field(N,SF)|ST]) -->
87		translate_to_fd_values(F,SF),l_translate_to_fd_values(T,ST).
88
89		:- block prop_01(-,-).
90		prop_01(pred_true,1).
91		prop_01(pred_false,0).
92
93		% ----------------------
94
95		:- use_module(bsyntaxtree,[is_set_type/2]).
96		:- use_module(preferences,[preference/2]).
97
98		% can a list be translated into CLPFD element constraints for function application
99		can_translate_function_to_element_constraint(List,FunctionType) :-
100		FunctionType \= unknown,
101		is_list_skeleton(List), % TO DO: allow tail AVL list + enable delaying treatment
102		preference(find_abort_values,false),
103		preference(use_chr_solver,false), % avoid falling into the SICStus element/3 bug prior to 4.3.6; TO DO: remove later
104		is_set_type(FunctionType,couple(Domain,Range)),
105		is_simple_fd_type(Domain), % Domain must be translatable to simple FD value list
106		is_fd_type(Range).
107
108		is_list_skeleton(X) :- nonvar(X),is_list_skeleton_aux(X).
109		is_list_skeleton_aux([]).
110		is_list_skeleton_aux([_H|T]) :- is_list_skeleton(T).
111
112		is_simple_fd_type(global(_)).
113		is_simple_fd_type(integer).
114		is_simple_fd_type(boolean).
115
116		is_fd_type(couple(A,B)) :- !, is_fd_type(A), is_fd_type(B).
117		is_fd_type(record(F)) :- !, is_fd_field_types(F).
118		is_fd_type(X) :- is_simple_fd_type(X).
119
120		is_fd_field_types([]).
121		is_fd_field_types([field(_,FT)|T]) :- is_fd_type(FT), is_fd_field_types(T).
122
123		:- use_module(b_global_sets,[get_global_type_value/3]).
124		get_fd_type(couple(A,B),(VA,VB)) --> get_fd_type(A,VA), get_fd_type(B,VB).
125		get_fd_type(global(T),FD) --> {get_global_type_value(FD,T,X)}, [X].
126		get_fd_type(integer,int(X)) --> [X].
127		get_fd_type(boolean,B) --> [FD], {prop_01(B,FD)}.
128		get_fd_type(record(Fields),rec(VF)) --> get_field_fd_types(Fields,VF).
129
130		get_field_fd_types([],[]) --> [].
131		get_field_fd_types([field(Name,Type)|FT],[field(Name,VF)|VT]) -->
132		get_fd_type(Type,VF),
133		get_field_fd_types(FT,VT).
134
135		get_fd_types(Domain,Range,(VD,VR),FDDom,FDRList) :- get_fd_type(Domain,VD,[FDDom],[]), get_fd_type(Range,VR,FDRList,[]).
136
137		% Examples:
138		% f = {x|->2, y|->3} & x:1..2 & y:4..5 & r = f(4)
139		% 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
140		% from the SICStus manual:
141		% element(?X,+List,?Y)
142		% where X and Y are domain variables and List is a list of domain variables. True
143		% if the X:th element of List is Y. Operationally, the domains of X and Y are
144		% constrained so that for every element in the domain of X, there is a compatible
145		% element in the domain of Y, and vice versa.
146		% Maintains domain consistency in X and bounds consistency in List and Y.
147
148		:- use_module(library(clpfd),[all_distinct/1]).
149		:- use_module(library(lists),[nth1/3]).
150		check_apply_with_element_constraint(List,X,Y,FunctionType,WF) :-
151		is_set_type(FunctionType,couple(Domain,Range)),
152		get_fd_type(Domain,X,[FDX],[]),
153		if(l_get_fd_types(List,DomainList,RangeLists,Domain,Range,FDX,FoundY),true,
154		(add_internal_error('Get FD Types failed: ',get_fd_types(Domain,Range)),fail)),
155		debug_println(4,element_domain_list(FDX,DomainList)),
156		%print(element_domain_list(FDX,DomainList,FoundY)),nl,
157		(FoundY \== y_not_found
158		-> FoundY=Y % no need for equal_object: we only have FD types + Bool + couples
159		; element(Idx,DomainList,FDX), % no need to call equal_object for X as we have simple fd types
160		(nonvar(Idx)
161		-> nth1(Idx,List,(X,Y)) %relevant for tests 387, 1579
162		; 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)
163		maplist(get_fd_types(Domain,Range),List,DomainList,RangeLists),
164		get_fd_type(Range,Y,FDYList,[]),
165		setup_element_domain_constraints(FDYList,Idx,RangeLists),
166		add_fd_variables_for_labeling([FDX|FDYList],WF)
167		)
168		).
169
170		% an unfolded version of maplist(get_fd_types(Domain,Range),List,DomainList,RangeLists)
171		% we also check if the lookup FD variable occurs in the list; if so we return the Y value in Found
172		% relevant for performance, e.g., for NQueens60; we avoid traversing the list a second time
173		l_get_fd_types([],[],[],_,_,_,y_not_found).
174		l_get_fd_types([Pair|PT],[FDDom|DT],[FDRList|RT],Domain,Range,FDX,FoundY) :-
175		get_fd_types(Domain,Range,Pair,FDDom,FDRList),
176		(FDX==FDDom -> Pair=(_,FoundY), DT=[],RT=[]
177		; l_get_fd_types(PT,DT,RT,Domain,Range,FDX,FoundY)).
178
179
180		setup_element_domain_constraints([],_,_).
181		setup_element_domain_constraints([FDY|YT],Idx,RangeLists) :-
182		maplist(get_next_fd,RangeLists,FDYList,RestLists),
183		%print(setting_up_range_element_constraint(Idx,FDYList,FDY)),nl,
184		element(Idx,FDYList,FDY),
185		setup_element_domain_constraints(YT,Idx,RestLists).
186
187		get_next_fd([H|T],H,T).