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