1		% (c) 2009-2016 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(fd_utils_clpfd,[eq_fd/2, neq_fd/3,
6		in_fd/3, in_fd_wf/4,
7		/* neq_fdpair/4, not_in_fd/3, not used anymore */
8		enum_fd/3, enum_fd_linear/3]).
9
10		:- use_module(module_information).
11		:- module_info(group,kernel).
12		:- module_info(description,'Basic checks for SET elements (equality, ...); maps to CLP(FD).').
13
14		/* File: fd_utils_clpfd.pl */
15		/* Created: 21/3/06 by Michael Leuschel */
16
17
18		:- use_module(self_check).
19
20		:- use_module(library(clpfd)).
21
22		:- assert_must_succeed(( fd_utils_clpfd:eq_fd(2,2) )).
23		:- assert_must_fail(( fd_utils_clpfd:eq_fd(2,3) )).
24
25	?	eq_fd(X,Y) :- X=Y.
26
27		%eq_fd(X,Y) :- %print_message(informational,eq_fd(X,Y)),
28		% %((var(X),frozen(X,G)) -> print_message(informational,frozen(X,G)) ; true),
29		% X = Y,
30		% print_message(informational,done_eq(X,Y)).
31
32
33		:- assert_must_succeed(( fd_utils_clpfd:in_fd(X,1,3),
34		fd_utils_clpfd:neq_fd(X,1,'Name'), fd_utils_clpfd:neq_fd(X,3,'Name'), X==2 )).
35
36		:- assert_must_succeed(( fd_utils_clpfd:neq_fd(1,2,'Name') )).
37		:- assert_must_fail(( fd_utils_clpfd:neq_fd(2,2,'Name') )).
38
39		neq_fd(X,Y,_Type) :- %print(neq_fd(X,Y,_Type)),nl,
40		% sometimes no CLP(FD) constraints set up for X or Y; can mean that we only detect inconsistencies much later
41		%(var(X) -> b_global_sets:global_type(fd(X,_Type),_Type) ; true), % commenting it in causes test 496 to fail;
42		%(var(Y) -> b_global_sets:global_type(fd(Y,_Type),_Type) ; true), % TO DO: investigate
43		X #\= Y,
44		((var(X),var(Y)) -> dif(X,Y) ; true). % even for finite domains X in 1..10, Y in 1..10, X#\=Y, X=Y. does not fail;
45
46
47
48		/*
49		:- assert_must_succeed(( fd_utils_clpfd:neq_fdpair(2,3,2,4) )).
50		:- assert_must_succeed(( fd_utils_clpfd:neq_fdpair(2,3,3,3) )).
51		:- assert_must_fail(( fd_utils_clpfd:neq_fdpair(2,3,2,3) )).
52
53		neq_fdpair(X1,Y1,X2,Y2) :-
54		when((?=(X1,X2);?=(Y1,Y2)),
55		(?=(X1,X2) -> (X1 \= X2 -> true ; dif(Y1,Y2))
56		; (Y1 \= Y2 -> true ; dif(X1,X2))
57		)).
58		*/
59
60		:- use_module(kernel_waitflags,[add_fd_variable_for_labeling/2]).
61
62		in_fd(X,Low,Up) :- number(Low), number(Up), !, X in Low..Up.
63		in_fd(X,Low,Up) :- X #>=Low, X#=<Up. %when((ground(Low),ground(Up)), X in Low..Up).
64
65		in_fd_wf(X,Low,Up,WF) :- number(Low), number(Up), !, X in Low..Up,
66		in_fd_wf2(X,Low,Up,WF).
67		in_fd_wf(X,Low,Up,WF) :- X #>=Low, X#=<Up, in_fd_wf2(X,Low,Up,WF).
68
69		:- block in_fd_wf2(?,-,?,?), in_fd_wf2(?,?,-,?).
70		in_fd_wf2(X,_Low,_Up,WF) :-
71		(ground(X) -> true
72		; %Size is Up+1-Low,
73		%fd_size(X,Size),
74		add_fd_variable_for_labeling(X,WF) % will automatically do enumeration
75		).
76
77		/* TO DO: check if we have to add FD variables to kernel_waitflags store using label_clpfd_vars
78		in other circumstances;
79		Provide support for x: {aa,bb,cc} ... constraints
80		*/
81
82
83
84
85		enum_fd(X,Low,Up) :- % we could use clpfd labeling
86	?	preferences:get_preference(randomise_enumeration_order,true)
87		-> %print(random_enum(X,Low,Up)),nl,
88		enum_fd_random(X,Low,Up)
89	?	; enum_fd_linear(X,Low,Up).
90		enum_fd_linear(X,Low,Up) :-
91	?	Low =< Up
92		-> ( %print(enum_fd(X,Low,Up)),translate:print_clpfd_variable(X),nl,
93	?	X=Low %, tools:print_bt_message(done_enum_fd(X,Low,Up))
94		;
95		%print(continue(X,Low,Up)),nl,
96		% TO DO: We could assert that X>Low and/or try to trigger all equalities for X=y with y<=Low
97	?	L1 is Low+1, enum_fd_linear(X,L1,Up)
98		)
99		; fail.
100
101
102		:- use_module(library(random)).
103		:- use_module(extension('random_permutations/random_permutations')).
104		enum_fd_random(Var,Low,Up) :-
105		init_random_permutations,
106		IntervalLength is Up - Low + 1,
107		get_num_bits(IntervalLength,MaxIdx,NumBits),
108		get_masks(NumBits,LeftMask,RightMask),
109		% the seed relies on the random predicate, not on now/1, thus prob can be made deterministic by setting a central random seed
110		random(TempSeed),
111		Seed is floor(TempSeed * 10000),
112		enum_fd_random_aux(Var,0,MaxIdx,Low,Up,Seed,NumBits,LeftMask,RightMask).
113
114		enum_fd_random_aux(Var,CurIdx,MaxIdx,From,To,Seed,NumBits,LeftMask,RightMask) :-
115		random_permutation_element(CurIdx,MaxIdx,From,To,Seed,NumBits,LeftMask,RightMask,Drawn,NextIdx),
116		(Var=Drawn ; enum_fd_random_aux(Var,NextIdx,MaxIdx,From,To,Seed,NumBits,LeftMask,RightMask)).
117
118
119		% not really required, would be a type error
120		%:- block not_in_fd(-,?,?), not_in_fd(?,-,?), not_in_fd(?,?,-).
121		%not_in_fd(X,Low,Up) :-
122		% (X < Low ; X > Up),!.