1		% (c) 2009-2023 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(kernel_dif,[frozen_dif/2, fd_frozen_dif/2,
6		syntactic_equality_test/3
7		%, post_dif/2
8		]).
9
10
11		:- use_module(module_information,[module_info/2]).
12		:- module_info(group,kernel).
13		:- module_info(description,'This module provides a dif which works with reified equality.').
14
15		:- use_module(clpfd_interface,[clpfd_can_intersect/2]).
16		% a version of frozen_dif which uses FD information to avoid calling frozen_dif if possible
17		fd_frozen_dif(X,Y) :-
18	?	(clpfd_can_intersect(X,Y) -> frozen_dif(X,Y)
19		; true % X and Y must be different
20		).
21
22		:- use_module(preferences).
23		% check if a frozen dif co-routine is pending and stating that the variables are different
24		% cf testcase 1175
25		%frozen_dif(X,Y) :- preferences:preference(use_smt_mode,false),!,fail.
26		frozen_dif(X,Y) :-
27		% print(check_frozen(X,Y)),nl, translate:l_print_frozen_info([X,Y]),nl,
28		var(X),
29		!,
30		X \== Y, % avoid calling frozen when both variables identical
31		frozen(X,Goal), %print(frozen(X,Y)),nl,portray_clause((check_frozen_dif(X,Y) :- Goal)),nl,
32		%terms:term_size(Goal,Sz), (Sz>200 -> print(large_frozen(X,Y,Sz)),nl,print(Goal),nl ; true),
33		preferences:preference(solver_strength,Strength),
34		Limit is 5+2*Strength,
35	?	frozen_dif_aux(Goal,Limit,X,Y). % increase required from 5 to 6 for SlotTool_04092017 issue
36		frozen_dif(X,Y) :- var(Y), frozen(Y,Goal), % do we need this in clpfd mode ? should we use solver_strength?
37		preferences:preference(solver_strength,Strength),
38		Limit is 2+Strength, % with TRACE_INFO or in SWI we may have additional goals and limit may be reached
39	?	frozen_dif_aux(Goal,Limit,Y,X).
40		frozen_dif_aux(kernel_objects:int_plus4(Nr,A,B),_,X,Y) :- !,
41		integer(Nr), % should always be the case, TO DO: maybe use CHR for this
42		Nr \= 0, % should normally also always be true, as int_plus4 would not have been called
43		(A==X -> B==Y % TO DO: maybe check if Y is variable and has int_plus attached wrt B to detect that z+1 is different from z+2
44		; B==X -> A==Y % ditto
45		).
46		frozen_dif_aux(prolog:dif(A,B),_,X,Y) :- !,
47		(A==X,B==Y ; A==Y,B==X). % , print(frozen_dif(X,Y)),nl.
48		frozen_dif_aux(dif(A,B),_,X,Y) :- !,
49		(A==X,B==Y ; A==Y,B==X). % , print(frozen_dif(X,Y)),nl.
50		% Nr: put an upper bound on checks; avoid slow-down when frozen goal very large; see e.g. alloc_large in test 1222
51		% TO DO: use attribute and get more efficient lookup
52		frozen_dif_aux((A,B),Nr,X,Y) :-
53		Nr>1, %(Nr>1 -> true ; print(frozen_dif_limit_reached(X,Y,(A,B))),nl,fail),
54		N1 is Nr-1,
55	?	(frozen_dif_aux(A,N1,X,Y) -> true ; frozen_dif_aux(B,N1,X,Y)).
56
57
58
59		% a reified version for syntactic equality ==
60
61		% trigger Res to pred_true when two variables become identical (as CLPFD does not do this)
62		% it is supposed to be used in conjunction with ((X#=Y) #<=> R01)
63		%syntactic_equality_test(X,Y,Res) :- Res==pred_true, !, print(useless_syntactic_test(X,Y,Res)),nl.
64		syntactic_equality_test(X,Y,Res) :-
65		% TO DO: attach attribute/co-routine so that dif will trigger Res to be pred_false ?
66		% e.g., (X=Y <=> r=TRUE) & X:1..100 & Y /= X does not deterministically set r to FALSE (but does if Y/=X moved to the left)
67		%reify(X,Y,Res), % a way to attach information for frozen_eqeq check
68		%when(?=(X,Y),(X==Y -> Res=pred_true ; true)). % CLPFD does not detect variable equality
69		when((?=(X,Y) ; nonvar(Res)),syntactic_eq_prop(Res,X,Y)). % CLPFD does not detect variable equality
70
71		syntactic_eq_prop(Res,X,Y) :- var(Res), !,
72		(X==Y -> Res=pred_true
73		; Res=pred_false). % syntactically not equal, as ?=(X,Y) triggered they must be different FD values
74		syntactic_eq_prop(pred_true,X,Y) :- (var(X),var(Y) -> X=Y ; true). % CLPFD reification does not unify ! required for test 1525
75		syntactic_eq_prop(pred_false,X,Y) :- dif(X,Y). % or frozen_dif ??
76
77
78		/*
79		% currently not used:
80
81		:- block reify(-,-,-).
82		reify(_,_,_).
83
84		post_dif(X,Y) :- dif(X,Y),
85		(frozen_eqeq(X,Y,Res) -> print(frz(X,Y,Res)),nl, Res=pred_false ; true).
86
87		%kernel_dif:syntactic_equality_test(X,Y,R), kernel_dif:post_dif(X,Y), -> R==pred_false
88
89		frozen_eqeq(X,Y,R) :-
90		% print(check_frozen(X,Y)),nl, translate:l_print_frozen_info([X,Y]),nl,
91		var(X),!,frozen(X,Goal),
92		frozen_eqeq_aux(Goal,5,X,Y,R).
93		frozen_eqeq(X,Y,R) :- var(Y), frozen(Y,Goal), % do we need this in clpfd mode ?
94		frozen_eqeq_aux(Goal,2,Y,X,R).
95		frozen_eqeq_aux(kernel_dif:reify(A,B,R),_,X,Y,R) :-
96		(A==X,B==Y ; A==Y,B==X),
97		!. % , print(frozen_dif(X,Y)),nl.
98		% Nr: put an upper bound on checks; avoid slow-down when frozen goal very large; see e.g. alloc_large in test 1220
99		% TO DO: use attribute and get more efficient lookup
100		frozen_eqeq_aux((A,B),Nr,X,Y,R) :- Nr>1, N1 is Nr-1,
101		(frozen_eqeq_aux(A,N1,X,Y,R) -> true ; frozen_eqeq_aux(B,N1,X,Y,R)).
102		*/