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 | | */ |