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(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		% see ../prob_examples/examples/B/ClearSy/alloc_large.mch where frozen_dif is a bottleneck
18		fd_frozen_dif(X,Y) :-
19		( clpfd_can_intersect(X,Y)
20		-> var(X),var(Y), % CLP(FD) at least on SICStus can propagate X#\=Nr : X #\= 5. --> X in(inf..4)\/(6..sup) ?
21		% so there cannot be a frozen dif constraint (if a corresponding CLP #\= was posted)
22		frozen_dif(X,Y)
23		; true % X and Y must be different
24		).
25
26		:- use_module(preferences).
27		% check if a frozen dif co-routine is pending and stating that the variables are different
28		% cf testcase 1175
29		%frozen_dif(X,Y) :- preferences:preference(use_smt_mode,false),!,fail.
30		frozen_dif(X,Y) :-
31		% print(check_frozen(X,Y)),nl, translate:l_print_frozen_info([X,Y]),nl,
32		var(X),
33		!,
34		X \== Y, % avoid calling frozen when both variables identical
35		frozen(X,Goal), %print(frozen(X,Y)),nl,portray_clause((check_frozen_dif(X,Y) :- Goal)),nl,
36		%terms:term_size(Goal,Sz), (Sz>200 -> print(large_frozen(X,Y,Sz)),nl,print(Goal),nl ; true),
37		preferences:preference(solver_strength,Strength),
38		Limit is 5+2*Strength,
39	?	frozen_dif_aux(Goal,Limit,X,Y). % increase required from 5 to 6 for SlotTool_04092017 issue
40		frozen_dif(X,Y) :- var(Y), frozen(Y,Goal), % do we need this in clpfd mode ? should we use solver_strength?
41		preferences:preference(solver_strength,Strength),
42		Limit is 2+Strength, % with TRACE_INFO or in SWI we may have additional goals and limit may be reached
43		frozen_dif_aux(Goal,Limit,Y,X).
44		frozen_dif_aux(kernel_objects:int_plus4(Nr,A,B),_,X,Y) :- !,
45		integer(Nr), % should always be the case, TO DO: maybe use CHR for this
46		Nr \= 0, % should normally also always be true, as int_plus4 would not have been called
47		(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
48		; B==X -> A==Y % ditto
49		).
50		frozen_dif_aux(prolog:dif(A,B),_,X,Y) :- !,
51		(A==X,B==Y ; A==Y,B==X). % , print(frozen_dif(X,Y)),nl.
52		frozen_dif_aux(dif(A,B),_,X,Y) :- !,
53		(A==X,B==Y ; A==Y,B==X). % , print(frozen_dif(X,Y)),nl.
54		% Nr: put an upper bound on checks; avoid slow-down when frozen goal very large; see e.g. alloc_large in test 1222
55		% TO DO: use attribute and get more efficient lookup
56		frozen_dif_aux((A,B),Nr,X,Y) :-
57		Nr>1, %(Nr>1 -> true ; print(frozen_dif_limit_reached(X,Y,(A,B))),nl,fail),
58		N1 is Nr-1,
59	?	(frozen_dif_aux(A,N1,X,Y) -> true ; frozen_dif_aux(B,N1,X,Y)).
60
61
62
63		% a reified version for syntactic equality ==
64
65		% trigger Res to pred_true when two variables become identical (as CLPFD does not do this)
66		% it is supposed to be used in conjunction with ((X#=Y) #<=> R01)
67		%syntactic_equality_test(X,Y,Res) :- Res==pred_true, !, print(useless_syntactic_test(X,Y,Res)),nl.
68		syntactic_equality_test(X,Y,Res) :-
69		% TO DO: attach attribute/co-routine so that dif will trigger Res to be pred_false ?
70		% 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)
71		%reify(X,Y,Res), % a way to attach information for frozen_eqeq check
72		%when(?=(X,Y),(X==Y -> Res=pred_true ; true)). % CLPFD does not detect variable equality
73		when((?=(X,Y) ; nonvar(Res)),syntactic_eq_prop(Res,X,Y)). % CLPFD does not detect variable equality
74
75		syntactic_eq_prop(Res,X,Y) :- var(Res), !,
76		(X==Y
77		-> Res=pred_true
78		; Res=pred_false). % syntactically not equal, as ?=(X,Y) triggered they must be different FD values
79		syntactic_eq_prop(pred_true,X,Y) :-
80		(var(X),var(Y) -> X=Y ; true). % CLPFD reification does not unify ! required for test 1525
81		syntactic_eq_prop(pred_false,X,Y) :-
82		(var(X),var(Y)
83		-> dif(X,Y)
84		; true). % CLPFD can handle X #= Nr without dif; see NinePrisoners performance when dif is unnecessarily posted
85
86
87		/*
88		% currently not used:
89
90		:- block reify(-,-,-).
91		reify(_,_,_).
92
93		post_dif(X,Y) :- dif(X,Y),
94		(frozen_eqeq(X,Y,Res) -> print(frz(X,Y,Res)),nl, Res=pred_false ; true).
95
96		%kernel_dif:syntactic_equality_test(X,Y,R), kernel_dif:post_dif(X,Y), -> R==pred_false
97
98		frozen_eqeq(X,Y,R) :-
99		% print(check_frozen(X,Y)),nl, translate:l_print_frozen_info([X,Y]),nl,
100		var(X),!,frozen(X,Goal),
101		frozen_eqeq_aux(Goal,5,X,Y,R).
102		frozen_eqeq(X,Y,R) :- var(Y), frozen(Y,Goal), % do we need this in clpfd mode ?
103		frozen_eqeq_aux(Goal,2,Y,X,R).
104		frozen_eqeq_aux(kernel_dif:reify(A,B,R),_,X,Y,R) :-
105		(A==X,B==Y ; A==Y,B==X),
106		!. % , print(frozen_dif(X,Y)),nl.
107		% Nr: put an upper bound on checks; avoid slow-down when frozen goal very large; see e.g. alloc_large in test 1220
108		% TO DO: use attribute and get more efficient lookup
109		frozen_eqeq_aux((A,B),Nr,X,Y,R) :- Nr>1, N1 is Nr-1,
110		(frozen_eqeq_aux(A,N1,X,Y,R) -> true ; frozen_eqeq_aux(B,N1,X,Y,R)).
111		*/