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(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		:- use_module(tools_portability, [exists_source/1]).
17
18		:- use_module(module_information,[module_info/2]).
19		:- module_info(group,kernel).
20		:- module_info(description,'This module provides reified equality and negation for pred_true/pred_false.').
21
22		% Portable attributed variable handling.
23		% Use SICStus-style library(atts) and verify_attributes/3 if available,
24		% otherwise the SWI/hProlog-style attr builtins and attr_unify_hook/2.
25		:- if(\+ exists_source(library(atts))).
26
27		get_bool_pred_info(Var,Neg,ReifList) :- get_attr(Var,bool_pred,bool_pred_info(Neg,ReifList)).
28		put_bool_pred_info(Var,Neg,ReifList) :- put_attr(Var,bool_pred,bool_pred_info(Neg,ReifList)).
29
30		attr_unify_hook(bool_pred_info(NegThis,ThisReifList),Value) :-
31		(var(Value) -> (get_attr(Value,bool_pred,bool_pred_info(NegValue,ValReifList))
32		-> check_equalities(ThisReifList,Value,NegValue,EqGoal1,NewReifList,RR),
33		check_equalities(ValReifList,Value,NegThis,EqGoal2,RR,[]),
34		(nonvar(Value) -> print(attr_unify_hook_instantiated_value(Value)),nl /* check equalities could have forced value to be known now; should not happen */
35		; put_attr(Value,bool_pred,bool_pred_info(NegValue,NewReifList))),
36		NegThis = NegValue,
37		Value \== NegThis,
38		EqGoal1,
39		EqGoal2
40		; put_attr(Value,bool_pred,bool_pred_info(NegThis,ThisReifList))
41		)
42		; (ThisReifList=[]
43		-> negate3(Value,NegThis)
44		; negate3(Value,NegThis), check_inst_equalities(ThisReifList,Value))
45		).
46
47		:- else.
48
49		:- use_module(library(atts)).
50
51		:- attribute bool_pred_info/2.
52
53		get_bool_pred_info(Var,Neg,ReifList) :- get_atts(Var,+bool_pred_info(Neg,ReifList)).
54		put_bool_pred_info(Var,Neg,ReifList) :- put_atts(Var,+bool_pred_info(Neg,ReifList)).
55
56		% verify_attributes is called whenever a variable Var that might have attributes is about to be bound to Value (it might have none).
57		% verify(VariableBeforeUnification, ValueWithWhichVariableUnifies, GoalWhichSICStusShouldCallAfterUnif)
58		verify_attributes(ThisVar,Value,Goal) :- get_atts(ThisVar,+bool_pred_info(NegThis,ThisReifList)),!,
59		% enter_log(ThisVar=Value), %% print(verify(ThisVar,Value,NegThis,ThisReifList)),nl, %%
60		(var(Value) -> (get_atts(Value,+bool_pred_info(NegValue,ValReifList))
61		-> Goal=[NegThis=NegValue,ThisVar\==NegThis,EqGoal1,EqGoal2],
62		check_equalities(ThisReifList,Value,NegValue,EqGoal1,NewReifList,RR),
63		check_equalities(ValReifList,ThisVar,NegThis,EqGoal2,RR,[]),
64		(nonvar(Value) -> print(verify_attribute_instantiated_value(Value)),nl /* check equalities could have forced value to be known now; should not happen */
65		; put_atts(Value,+bool_pred_info(NegValue,NewReifList)))
66		; put_atts(Value,+bool_pred_info(NegThis,ThisReifList)), Goal=[]
67		)
68		; (ThisReifList=[]
69		-> Goal=[negate3(Value,NegThis)] %(var(NegThis) -> Goal=[negate3(Value,NegThis)] ; Goal=[])
70		; Goal=[negate3(Value,NegThis),check_inst_equalities(ThisReifList,Value)])
71		). %, exit_log(Goal),trace. %, print(done_verify(ThisVar,Value,Goal)),nl.
72		verify_attributes(_, _, [] ).
73
74
75		:- endif.
76
77		% store for each bool value the negated variable & list of reifications it is involved in
78		% bool_pred_info(NegationOfVariable, List of eqcheck(OtherVariable,ReificationVariable)
79
80		% check that we have a real variable without any bool_pred constraints attached
81		free_var(X) :- var(X), \+ get_bool_pred_info(X,_,_).
82
83		% check if currently X is negation of Y; call only for variable X
84		bool_negate_check(X,Y) :- get_bool_pred_info(X,OtherX,_),Y==OtherX.
85
86		negate(X,Y) :- %enter_log(negate(X,Y)),
87	?	(nonvar(X) -> negate3(X,Y)
88		; nonvar(Y) -> negate3(Y,X)
89		; get_bool_pred_info(X,OtherX,_) -> Y=OtherX, X \== Y, update_bool_pred_negation(Y,X)
90		; get_bool_pred_info(Y,OtherY,_) -> put_bool_pred_info(X,Y,[]), X=OtherY, X \== Y
91		; X \== Y, put_bool_pred_info(Y,X,[]), put_bool_pred_info(X,Y,[])
92		).% ,exit_log(negate(X,Y)).
93
94		update_bool_pred_negation(X,_NegX) :- nonvar(X),!.
95		update_bool_pred_negation(X,NegX) :-
96		(get_bool_pred_info(OtherX,_,_) -> OtherX=NegX
97		; put_bool_pred_info(X,NegX,[])).
98
99		%negate3(X,Y) :- print(negate3(X,Y)),nl,fail.
100		negate3(pred_true,pred_false). % for kernel_equality,... results
101		negate3(pred_false,pred_true).
102		%negate3(bool_true,bool_false). % for boolean values
103		%negate3(bool_false,bool_true).
104
105
106		:- assert_must_succeed((bool_pred:enter_log(a),bool_pred:enter_log(b),
107		bool_pred:exit_log(b),bool_pred:exit_log(a))).
108		% a simple logging facility to replay calls later
109		:- dynamic logging_level/1.
110		logging_level(0).
111
112		enter_log(X) :- retract(logging_level(L)),
113		indent_ws(L),print(X), print(','),nl,
114		L1 is L+1, assertz(logging_level(L1)).
115		exit_log(G) :- retract(logging_level(L)),
116		(L>0 -> L1 is L-1, assertz(logging_level(L1)), indent_ws(L1), print('exit '), print(G),nl
117		; add_internal_error('*** negative - logging level !',L),
118		assertz(logging_level(L))).
119		indent_ws(X) :- X<1,!.
120		indent_ws(X) :- print(' '), X1 is X-1, indent_ws(X1).
121
122
123		% check if any reification can now be determined
124		% Idea: add other boolean operators here as well: imply, and, or ??
125		check_equalities([],_,_,true) --> [].
126		check_equalities([eqcheck(V2,Res)|T],V1,NegV1,Goal) -->
127		( {V2==V1} -> {Goal=(Res=pred_true,G2)}
128		; {V2==NegV1} -> {Goal=(Res=pred_false,G2)}
129		; {V1==Res} -> {Goal=(V2=pred_true,G2)} % Warning: V2 could expect bool_true !
130		; {NegV1==Res} -> {Goal=(V2=pred_false,G2)} % Warning: V2 could expect bool_false !
131		; %{print(no_new_info),nl},
132		[eqcheck(V2,Res)], {Goal=G2}
133		),check_equalities(T,V1,NegV1,G2).
134
135		% will be called with second argument instantiated to pred_false/pred_true
136
137		:- public check_inst_equalities/2. % used above
138		check_inst_equalities([],_).
139		check_inst_equalities([eqcheck(V2,Res)|T],V1) :-
140		(nonvar(V2) -> (V1=V2 -> Res=pred_true ; Res=pred_false)
141		; V1=pred_true -> Res=V2
142	?	; negate(V2,Res)
143	?	), check_inst_equalities(T,V1).
144
145		:- assert_must_succeed((bool_pred:negate(X,Y), bool_pred:negate(X,Z), Y==Z, Z=pred_true, X==pred_false)).
146		% bool_pred:negate(X,Y), bool_pred:negate(X,Z), Y==Z, Z=pred_true, X==pred_false.
147		/*
148		CLP(FD) cannot do this:
149		| ?- X in 0..1, Y in 0..1, Z in 0..1, X #\= Y, X#\=Z.
150		X in 0..1,
151		Y in 0..1,
152		Z in 0..1 ?
153		yes
154		*/
155
156		:- assert_must_succeed(( bool_pred:negate(X,Y), bool_pred:negate(Y,Z), X==Z, Z=pred_true, X==pred_true, Y==pred_false)).
157		:- assert_must_succeed((bool_pred:negate(X,Y), bool_pred:negate(X2,Y2), X=X2, Y==Y2, Y=pred_false, X2==pred_true)).
158		:- assert_must_succeed((bool_pred:negate(X,Y), bool_pred:negate(X,Z), Y==Z, Z=pred_true, X==pred_false)).
159		:- assert_must_succeed((bool_pred:negate(X,Y), bool_pred:negate(Y,Z), \+ bool_pred:negate(Z,X))).
160		:- assert_must_succeed((bool_pred:negate(X,Y), bool_pred:negate(Y,Z), bool_pred:negate(Z,X2), \+ X2=X)).
161		:- assert_must_succeed((bool_pred:negate(X,Y), bool_pred:negate(Y,Z), X2=X, \+ bool_pred:negate(Z,X2))).
162		:- assert_must_fail(bool_pred:negate(X,X)).
163		:- 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)).
164		:- 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)).
165		:- 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)).
166		:- 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)).
167		:- assert_must_succeed((Y=pred_true, bool_pred:bool_equality(X,Y,R) , R==X)).
168		:- assert_must_fail((Y=pred_false, bool_pred:bool_equality(X,Y,R) , R=X)).
169
170
171		%:- attribute bool_equality/2.
172		% bool_equality is actually solving: (X<=>Y) <=> R
173		% Note this is commutative and associative in its three arguments
174		bool_equality(X,Y,Res) :- %print(bool_equality(X,Y,Res)),nl, %% enter_log(bool_equality(X,Y,Res)), %%
175	?	( nonvar(X) -> eq1(X,Y,Res)
176		; nonvar(Y) -> eq1(Y,X,Res)
177		; nonvar(Res) -> eq1(Res,X,Y)
178		; X==Y -> Res=pred_true
179		; X==Res -> Y=pred_true % Warning: Y could expect bool_true !
180		; Y==Res -> X=pred_true % Warning: X could expect bool_true !
181		; get_bool_pred_info(X,NX,XList)
182		-> (NX==Y -> Res=pred_false % Y is the negation of X
183		; NX==Res -> Y=pred_false % Warning: Y could expect bool_false !
184		; put_bool_pred_info(X,NX,[eqcheck(Y,Res)|XList]),
185		add_equality(Y,X,Res)
186		),
187		blocking_force_eq3(Res,X,Y)
188		; add_new_equality(X,Y,Res),add_equality(Y,X,Res),
189		blocking_force_eq3(Res,X,Y)
190		). % ,exit_log(eq(X,Y,Res)).
191
192		% Missing rules (requires merging bool_true/pred_true, ...)
193		% X==Res -> Y=pred_true && Y==Res -> X=pred_true
194		% X==~Res -> Y=pred_false && Y==~Res -> X=pred_false [Missing above]
195
196		add_equality(X,Y,Res) :-
197		(get_bool_pred_info(X,NX,List)
198		-> put_bool_pred_info(X,NX,[eqcheck(Y,Res)|List])
199		; add_new_equality(X,Y,Res)
200		).
201		add_new_equality(X,Y,Res) :-
202		put_bool_pred_info(NX,X,[]),% NX is a fresh variable, no need to go through negate/2
203		put_bool_pred_info(X,NX,[eqcheck(Y,Res)]).
204
205		% X -> bool_equality(Y,Res) : check if X==Y -> Res=pred_true or if Y==NegatedX -> Res=pred_false
206		% we could also check if Res==X -> Y=pred_true
207
208
209		eq1(pred_true,X,X).
210	?	eq1(pred_false,X,Y) :- negate(X,Y).
211
212		% equality if one of the bools (second arg) is known: wait for other bool (arg1) or result
213		%:- block eq2(-,?,-).
214		%eq2(X,Y,Res) :- nonvar(Res),!,eq1(Res,X,Y).
215		%eq2(X,Y,Res) :- (X=Y -> Res=pred_true ; Res=pred_false).
216
217		%:- block blocking_force_eq(-,?,?). % when((?=(Res,X) ; nonvar(Res)), --> we could detect force_eq(A,A,pred_true/false)
218		%blocking_force_eq(Res,X,Y) :- force_eq(Res,X,Y).
219
220		blocking_force_eq3(Res,X,Y) :-
221		when((?=(Res,X) ; ?=(Res,Y) ; ?=(X,Y) ; nonvar(Res) ; nonvar(X) ; nonvar(Y)), bool_equality(X,Y,Res)).
222
223		%blocking_force_eq2(Res,X,Y) :- when((?=(Res,X) ; ?=(Res,Y) ; ?=(X,Y) ; nonvar(Res)), force_eq2(Res,X,Y)).
224		%
225		%force_eq2(Res,X,Y) :- X==Res,!, %print(forcing_eq_eq1(Res,X,Y)),nl,
226		% Y=pred_true.
227		%force_eq2(Res,X,Y) :- Y==Res,!, %print(forcing_eq_eq2(Res,X,Y)),nl,
228		% X=pred_true.
229		%force_eq2(Res,X,Y) :- X==Y,!, %aprint(forcing_eq_eq3(Res,X,Y)),nl,
230		% Res=pred_true.
231		%force_eq2(pred_true,X,X).
232		%force_eq2(pred_false,X,Y) :- negate(X,Y).
233