1		% (c) 2009-2025 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 global 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		// X1 #= X2 #\/ Y1 #= Y2
54
55		neq_fdpair(X1,Y1,X2,Y2) :-
56		when((?=(X1,X2);?=(Y1,Y2)),
57		(?=(X1,X2) -> (X1 \= X2 -> true ; dif(Y1,Y2))
58		; (Y1 \= Y2 -> true ; dif(X1,X2))
59		)).
60		*/
61
62		:- use_module(kernel_waitflags,[add_fd_variable_for_labeling/2]).
63
64		% Up can be a variable, an integer or the term inf
65		in_fd(X,Low,Up) :- integer(Low), integer(Up), !, X in Low..Up.
66		in_fd(X,Low,Up) :- X #>=Low, inf_leq(X,Up).
67
68		in_fd_wf(X,Low,Up,WF) :- integer(Low), integer(Up), !, X in Low..Up,
69		in_fd_wf2(X,Low,Up,WF).
70		in_fd_wf(X,Low,Up,WF) :- X #>=Low, inf_leq(X,Up),
71		in_fd_wf2(X,Low,Up,WF).
72
73		% less-equal that accepts inf as second argument; e.g., for infinite deferred sets
74		inf_leq(X,Up) :- (Up==inf -> true ; X#=<Up).
75
76		:- block in_fd_wf2(?,-,?,?), in_fd_wf2(?,?,-,?).
77		in_fd_wf2(X,_Low,_Up,WF) :-
78		add_fd_variable_for_labeling(X,WF). % will automatically do enumeration
79
80
81		:- use_module(probsrc(clpfd_interface),[clpfd_in_domain/1]).
82
83		enum_fd(X,Low,Up) :- X in Low..Up,
84	?	clpfd_in_domain(X).
85
86
87		enum_fd_linear(X,Low,Up) :- %write(enum_fd(X,Low,Up)),nl,
88		Low =< Up
89		-> ( %print(enum_fd(X,Low,Up)),translate:print_clpfd_variable(X),nl,
90		X=Low %, tools:print_bt_message(done_enum_fd(X,Low,Up))
91		;
92		%print(continue(X,Low,Up)),nl,
93		% TO DO: We could assert that X>Low and/or try to trigger all equalities for X=y with y<=Low
94	?	L1 is Low+1, enum_fd_linear(X,L1,Up)
95		)
96		; fail.
97
98
99
100		% not really required, would be a type error
101		%:- block not_in_fd(-,?,?), not_in_fd(?,-,?), not_in_fd(?,?,-).
102		%not_in_fd(X,Low,Up) :-
103		% (X < Low ; X > Up),!.