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(bool_pred,[free_var/1, bool_negate_check/2, | |
6 | negate/2, bool_equality/3]). | |
7 | ||
8 | /* | |
9 | a module that supports a boolean type: pred_false, pred_true | |
10 | with an efficient negation procedure | |
11 | */ | |
12 | ||
13 | :- use_module(tools). | |
14 | :- use_module(self_check). | |
15 | :- use_module(error_manager). | |
16 | ||
17 | :- use_module(module_information,[module_info/2]). | |
18 | :- module_info(group,kernel). | |
19 | :- module_info(description,'This module provides reified equality and negation for pred_true/pred_false.'). | |
20 | ||
21 | :- use_module(library(atts)). | |
22 | ||
23 | ||
24 | :- attribute bool_pred_info/2. | |
25 | % store for each bool value the negated variable & list of reifications it is involved in | |
26 | % bool_pred_info(NegationOfVariable, List of eqcheck(OtherVariable,ReificationVariable) | |
27 | ||
28 | % check that we have a real variable without any bool_pred constraints attached | |
29 | free_var(X) :- var(X), \+ get_atts(X,+bool_pred_info(_,_)). | |
30 | ||
31 | % check if currently X is negation of Y; call only for variable X | |
32 | bool_negate_check(X,Y) :- get_atts(X,+bool_pred_info(OtherX,_)),Y==OtherX. | |
33 | ||
34 | negate(X,Y) :- %enter_log(negate(X,Y)), | |
35 | (nonvar(X) -> negate3(X,Y) | |
36 | ; nonvar(Y) -> negate3(Y,X) | |
37 | ; get_atts(X,+bool_pred_info(OtherX,_)) -> Y=OtherX, X \== Y, update_bool_pred_negation(Y,X) | |
38 | ; get_atts(Y,+bool_pred_info(OtherY,_)) -> put_atts(X,+bool_pred_info(Y,[])), X=OtherY, X \== Y | |
39 | ; X \== Y, put_atts(Y,+bool_pred_info(X,[])), put_atts(X,+bool_pred_info(Y,[])) | |
40 | ).% ,exit_log(negate(X,Y)). | |
41 | ||
42 | update_bool_pred_negation(X,_NegX) :- nonvar(X),!. | |
43 | update_bool_pred_negation(X,NegX) :- | |
44 | (get_atts(X,+bool_pred_info(OtherX,_)) -> OtherX=NegX | |
45 | ; put_atts(X,+bool_pred_info(NegX,[]))). | |
46 | ||
47 | %negate3(X,Y) :- print(negate3(X,Y)),nl,fail. | |
48 | negate3(pred_true,pred_false). % for kernel_equality,... results | |
49 | negate3(pred_false,pred_true). | |
50 | %negate3(bool_true,bool_false). % for boolean values | |
51 | %negate3(bool_false,bool_true). | |
52 | ||
53 | % verify(VariableBeforeUnification, ValueWithWhichVariableUnifies, GoalWhichSICStusShouldCallAfterUnif) | |
54 | verify_attributes(ThisVar,Value,Goal) :- get_atts(ThisVar,+bool_pred_info(NegThis,ThisReifList)),!, | |
55 | % enter_log(ThisVar=Value), %% print(verify(ThisVar,Value,NegThis,ThisReifList)),nl, %% | |
56 | (var(Value) -> (get_atts(Value,+bool_pred_info(NegValue,ValReifList)) | |
57 | -> %% print(other_val(ThisVar,Value,NegValue,ValReifList)),nl, %% | |
58 | Goal=[NegThis=NegValue,ThisVar\==NegThis,EqGoal1,EqGoal2], | |
59 | check_equalities(ThisReifList,Value,NegValue,EqGoal1,NewReifList,RR), | |
60 | check_equalities(ValReifList,ThisVar,NegThis,EqGoal2,RR,[]), | |
61 | %% print(new_reif_list(ThisVar,Value,NewReifList)),nl,%% | |
62 | (nonvar(Value) -> print(verify_attribute_instantiated_value(Value)),nl /* check equalities could have forced value to be known now; should not happen */ | |
63 | ; put_atts(Value,+bool_pred_info(NegValue,NewReifList))) | |
64 | ; put_atts(Value,+bool_pred_info(NegThis,ThisReifList)), Goal=[] | |
65 | ) | |
66 | ; (ThisReifList=[] | |
67 | -> Goal=[negate3(Value,NegThis)] %(var(NegThis) -> Goal=[negate3(Value,NegThis)] ; Goal=[]) | |
68 | ; Goal=[negate3(Value,NegThis),check_inst_equalities(ThisReifList,Value)]) | |
69 | ). %, exit_log(Goal),trace. %, print(done_verify(ThisVar,Value,Goal)),nl. | |
70 | verify_attributes(_, _, [] ). | |
71 | ||
72 | ||
73 | :- assert_must_succeed((bool_pred:enter_log(a),bool_pred:enter_log(b), | |
74 | bool_pred:exit_log(b),bool_pred:exit_log(a))). | |
75 | % a simple logging facility to replay calls later | |
76 | :- dynamic logging_level/1. | |
77 | logging_level(0). | |
78 | ||
79 | enter_log(X) :- retract(logging_level(L)), | |
80 | indent_ws(L),print(X), print(','),nl, | |
81 | L1 is L+1, assert(logging_level(L1)). | |
82 | exit_log(G) :- retract(logging_level(L)), | |
83 | (L>0 -> L1 is L-1, assert(logging_level(L1)), indent_ws(L1), print('exit '), print(G),nl | |
84 | ; add_internal_error('*** negative - logging level !',L), | |
85 | assert(logging_level(L))). | |
86 | indent_ws(X) :- X<1,!. | |
87 | indent_ws(X) :- print(' '), X1 is X-1, indent_ws(X1). | |
88 | ||
89 | ||
90 | % check if any reification can now be determined | |
91 | % Idea: add other boolean operators here as well: imply, and, or ?? | |
92 | check_equalities([],_,_,true) --> []. | |
93 | check_equalities([eqcheck(V2,Res)|T],V1,NegV1,Goal) --> %{print(eqcheck(V2,Res,V1,NegV1)),nl}, | |
94 | ( {V2==V1} -> {Goal=(Res=pred_true,G2)} | |
95 | ; {V2==NegV1} -> {Goal=(Res=pred_false,G2)} | |
96 | ; {V1==Res} -> {Goal=(V2=pred_true,G2)} % Warning: V2 could expect bool_true ! | |
97 | ; {NegV1==Res} -> {Goal=(V2=pred_false,G2)} % Warning: V2 could expect bool_false ! | |
98 | ; %{print(no_new_info),nl}, | |
99 | [eqcheck(V2,Res)], {Goal=G2} | |
100 | ),check_equalities(T,V1,NegV1,G2). | |
101 | ||
102 | % will be called with second argument instantiated to pred_false/pred_true | |
103 | ||
104 | :- public check_inst_equalities/2. % used above | |
105 | check_inst_equalities([],_). | |
106 | check_inst_equalities([eqcheck(V2,Res)|T],V1) :- %print(eq_inst_check(V1,V2,Res)),nl, | |
107 | (nonvar(V2) -> (V1=V2 -> Res=pred_true ; Res=pred_false) | |
108 | ; V1=pred_true -> Res=V2 | |
109 | ; negate(V2,Res) | |
110 | ), check_inst_equalities(T,V1). | |
111 | ||
112 | :- assert_must_succeed((bool_pred:negate(X,Y), bool_pred:negate(X,Z), Y==Z, Z=pred_true, X==pred_false)). | |
113 | % bool_pred:negate(X,Y), bool_pred:negate(X,Z), Y==Z, Z=pred_true, X==pred_false. | |
114 | /* | |
115 | CLP(FD) cannot do this: | |
116 | | ?- X in 0..1, Y in 0..1, Z in 0..1, X #\= Y, X#\=Z. | |
117 | X in 0..1, | |
118 | Y in 0..1, | |
119 | Z in 0..1 ? | |
120 | yes | |
121 | */ | |
122 | ||
123 | :- assert_must_succeed(( bool_pred:negate(X,Y), bool_pred:negate(Y,Z), X==Z, Z=pred_true, X==pred_true, Y==pred_false)). | |
124 | :- assert_must_succeed((bool_pred:negate(X,Y), bool_pred:negate(X2,Y2), X=X2, Y==Y2, Y=pred_false, X2==pred_true)). | |
125 | :- assert_must_succeed((bool_pred:negate(X,Y), bool_pred:negate(X,Z), Y==Z, Z=pred_true, X==pred_false)). | |
126 | :- assert_must_succeed((bool_pred:negate(X,Y), bool_pred:negate(Y,Z), \+ bool_pred:negate(Z,X))). | |
127 | :- assert_must_succeed((bool_pred:negate(X,Y), bool_pred:negate(Y,Z), bool_pred:negate(Z,X2), \+ X2=X)). | |
128 | :- assert_must_succeed((bool_pred:negate(X,Y), bool_pred:negate(Y,Z), X2=X, \+ bool_pred:negate(Z,X2))). | |
129 | :- assert_must_fail(bool_pred:negate(X,X)). | |
130 | :- assert_must_succeed(( bool_pred:negate(X,Y), bool_pred:negate(V,Z), bool_pred:bool_equality(X,V,RXV), Z=Y, X==V, RXV==pred_true)). | |
131 | :- assert_must_succeed(( bool_pred:negate(X,Y), bool_pred:negate(V,Z), bool_pred:bool_equality(X,V,RXV), Z=X, Y==V, RXV==pred_false)). | |
132 | :- assert_must_succeed(( bool_pred:negate(X,Y), bool_pred:negate(V,Z), bool_pred:bool_equality(X,V,RXV), RXV=pred_false, Y==V, X==Z)). | |
133 | :- assert_must_succeed(( bool_pred:negate(X,Y), bool_pred:negate(V,Z), bool_pred:bool_equality(X,V,RXV), RXV=pred_true, Y==Z, X==V)). | |
134 | :- assert_must_succeed((Y=pred_true, bool_pred:bool_equality(X,Y,R) , R==X)). | |
135 | :- assert_must_fail((Y=pred_false, bool_pred:bool_equality(X,Y,R) , R=X)). | |
136 | ||
137 | ||
138 | %:- attribute bool_equality/2. | |
139 | % bool_equality is actually solving: (X<=>Y) <=> R | |
140 | bool_equality(X,Y,Res) :- %% enter_log(bool_equality(X,Y,Res)), %% | |
141 | ( nonvar(X) -> eq1(X,Y,Res) | |
142 | ; nonvar(Y) -> eq1(Y,X,Res) | |
143 | ; nonvar(Res) -> force_eq(Res,X,Y) | |
144 | ; X==Y -> Res=pred_true | |
145 | ; X==Res -> Y=pred_true % Warning: Y could expect bool_true ! | |
146 | ; Y==Res -> X=pred_true % Warning: X could expect bool_true ! | |
147 | ; get_atts(X,+bool_pred_info(NX,XList)) | |
148 | -> (NX==Y -> Res=pred_false % Y is the negation of X | |
149 | ; NX==Res -> Y=pred_false % Warning: Y could expect bool_false ! | |
150 | ; put_atts(X,+bool_pred_info(NX,[eqcheck(Y,Res)|XList])), | |
151 | add_equality(Y,X,Res) | |
152 | ), | |
153 | blocking_force_eq(Res,X,Y) | |
154 | ; add_new_equality(X,Y,Res),add_equality(Y,X,Res), | |
155 | blocking_force_eq(Res,X,Y) | |
156 | ). % ,exit_log(eq(X,Y,Res)). | |
157 | ||
158 | % Missing rules (requires merging bool_true/pred_true, ...) | |
159 | % X==Res -> Y=pred_true && Y==Res -> X=pred_true | |
160 | % X==~Res -> Y=pred_false && Y==~Res -> X=pred_false [Missing above] | |
161 | ||
162 | add_equality(X,Y,Res) :- | |
163 | (get_atts(X,+bool_pred_info(NX,List)) | |
164 | -> put_atts(X,+bool_pred_info(NX,[eqcheck(Y,Res)|List])) | |
165 | ; add_new_equality(X,Y,Res) | |
166 | ). | |
167 | add_new_equality(X,Y,Res) :- | |
168 | put_atts(NX,+bool_pred_info(X,[])),% NX is a fresh variable, no need to go through negate/2 | |
169 | put_atts(X,+bool_pred_info(NX,[eqcheck(Y,Res)])). | |
170 | ||
171 | % X -> bool_equality(Y,Res) : check if X==Y -> Res=pred_true or if Y==NegatedX -> Res=pred_false | |
172 | % we could also check if Res==X -> Y=pred_true | |
173 | ||
174 | ||
175 | eq1(pred_true,X,X). | |
176 | eq1(pred_false,X,Y) :- negate(X,Y). | |
177 | ||
178 | % equality if one of the bools (second arg) is known: wait for other bool (arg1) or result | |
179 | %:- block eq2(-,?,-). | |
180 | %eq2(X,Y,Res) :- nonvar(Res),!,force_eq(Res,X,Y). | |
181 | %eq2(X,Y,Res) :- (X=Y -> Res=pred_true ; Res=pred_false). | |
182 | ||
183 | force_eq(pred_true,X,X). | |
184 | force_eq(pred_false,X,Y) :- negate(X,Y). | |
185 | ||
186 | :- block blocking_force_eq(-,?,?). | |
187 | blocking_force_eq(Res,X,Y) :- force_eq(Res,X,Y). |