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).