1		% (c) 2009-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(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		!,frozen(X,Goal),
30		%terms:term_size(Goal,Sz), (Sz>200 -> print(large_frozen(X,Y,Sz)),nl,print(Goal),nl ; true),
31		preferences:preference(solver_strength,Strength),
32		Limit is 5+2*Strength,
33		frozen_dif_aux(Goal,Limit,X,Y). % increase required from 5 to 6 for SlotTool_04092017 issue
34		frozen_dif(X,Y) :- var(Y), frozen(Y,Goal), % do we need this in clpfd mode ? should we use solver_strength?
35		preferences:preference(solver_strength,Strength),
36		Limit is 2+Strength,
37		frozen_dif_aux(Goal,Limit,Y,X).
38		frozen_dif_aux(kernel_objects:int_plus4(Nr,A,B),_,X,Y) :- !,
39		number(Nr), % should always be the case, TO DO: maybe use CHR for this
40		Nr \=0, % should normally also always be true, as int_plus4 would not have been called
41		(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
42		; B==X -> A==Y % ditto
43		).
44	?	frozen_dif_aux(prolog:dif(A,B),_,X,Y) :- !,
45	?	(A==X,B==Y ; A==Y,B==X). % , print(frozen_dif(X,Y)),nl.
46		% Nr: put an upper bound on checks; avoid slow-down when frozen goal very large; see e.g. alloc_large in test 1222
47		% TO DO: use attribute and get more efficient lookup
48		frozen_dif_aux((A,B),Nr,X,Y) :-
49		Nr>1, %(Nr>1 -> true ; print(frozen_dif_limit_reached(X,Y,(A,B))),nl,fail),
50		N1 is Nr-1,
51	?	(frozen_dif_aux(A,N1,X,Y) -> true ; frozen_dif_aux(B,N1,X,Y)).
52
53
54
55		% a reified version for syntactic equality ==
56
57		% trigger Res to pred_true when two variables become identical (as CLPFD does not do this)
58		% it is supposed to be used in conjunction with ((X#=Y) #<=> R01)
59		%syntactic_equality_test(X,Y,Res) :- Res==pred_true, !, print(useless_syntactic_test(X,Y,Res)),nl.
60		syntactic_equality_test(X,Y,Res) :-
61		% TO DO: attach attribute/co-routine so that dif will trigger Res to be pred_false ?
62		% 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)
63		%reify(X,Y,Res), % a way to attach information for frozen_eqeq check
64		%when(?=(X,Y),(X==Y -> Res=pred_true ; true)). % CLPFD does not detect variable equality
65		when((?=(X,Y) ; nonvar(Res)),syntactic_eq_prop(Res,X,Y)). % CLPFD does not detect variable equality
66
67	?	syntactic_eq_prop(Res,X,Y) :- var(Res), !,
68	?	(X==Y -> Res=pred_true
69	?	; Res=pred_false). % syntactically not equal, as ?=(X,Y) triggered they must be different FD values
70		syntactic_eq_prop(pred_true,X,Y) :- (var(X),var(Y) -> X=Y ; true). % CLPFD reification does not unify ! required for test 1525
71		syntactic_eq_prop(pred_false,X,Y) :- dif(X,Y). % or frozen_dif ??
72
73
74		/*
75		% currently not used:
76
77		:- block reify(-,-,-).
78		reify(_,_,_).
79
80		post_dif(X,Y) :- dif(X,Y),
81		(frozen_eqeq(X,Y,Res) -> print(frz(X,Y,Res)),nl, Res=pred_false ; true).
82
83		%kernel_dif:syntactic_equality_test(X,Y,R), kernel_dif:post_dif(X,Y), -> R==pred_false
84
85		frozen_eqeq(X,Y,R) :-
86		% print(check_frozen(X,Y)),nl, translate:l_print_frozen_info([X,Y]),nl,
87		var(X),!,frozen(X,Goal),
88		frozen_eqeq_aux(Goal,5,X,Y,R).
89		frozen_eqeq(X,Y,R) :- var(Y), frozen(Y,Goal), % do we need this in clpfd mode ?
90		frozen_eqeq_aux(Goal,2,Y,X,R).
91		frozen_eqeq_aux(kernel_dif:reify(A,B,R),_,X,Y,R) :-
92		(A==X,B==Y ; A==Y,B==X),
93		!. % , print(frozen_dif(X,Y)),nl.
94		% Nr: put an upper bound on checks; avoid slow-down when frozen goal very large; see e.g. alloc_large in test 1220
95		% TO DO: use attribute and get more efficient lookup
96		frozen_eqeq_aux((A,B),Nr,X,Y,R) :- Nr>1, N1 is Nr-1,
97		(frozen_eqeq_aux(A,N1,X,Y,R) -> true ; frozen_eqeq_aux(B,N1,X,Y,R)).
98		*/