1		% Heinrich Heine Universitaet Duesseldorf
2		% (c) 2023-2024 Lehrstuhl fuer Softwaretechnik und Programmiersprachen,
3		% This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html)
4
5		:- module(b2setlog,
6		[bexpr2setlog/4,
7		bpred2setlog/3,
8		solve_pred_with_setlog/3,
9		prove_using_setlog/5
10		]).
11
12		:- use_module(probsrc(module_information)).
13		:- module_info(group,setlog).
14		:- module_info(description,'This module provides a translation from B to Setlog').
15
16		:- use_module(library(lists),[maplist/2, maplist/3, include/3, exclude/3]).
17		:- use_module(probsrc(error_manager)).
18		:- use_module(probsrc(preferences), [get_preference/2]).
19		:- use_module(probsrc(debug)).
20		:- use_module(probsrc(bsyntaxtree), [same_id/3, conjunct_predicates/2, create_negation/2]).
21
22		% Translating expressions to setlog
23		% b2setlog(BAST, Environment, SetLogTranslation, ResultVariable)
24		bexpr2setlog(b(E,_Type,_I),Env,SetLogConstr,Res) :- b2e(E,Env,C,R),!, SetLogConstr=C,Res=R.
25		bexpr2setlog(TE,Env,_,_) :- add_translation_error(Env,'Cannot convert B expression to setlog:',TE),fail.
26
27
28		b2e(UnOP,Env,SetLogConstr,Res) :- % Res is a fresh existential variable
29		un_op(UnOP,A,SetLogOperator),!,
30		bexpr2setlog(A,Env,CA,RA),
31		SLOG =.. [SetLogOperator,RA,Res],
32		sconjoin(CA,SLOG,SetLogConstr).
33		b2e(BOP,Env,SetLogConstr,Res) :- % ditto
34		bin_op(BOP,A,B,SetLogOperator),!,
35		bexpr2setlog(A,Env,CA,RA), bexpr2setlog(B,Env,CB,RB),
36		SLOG =.. [SetLogOperator,RA,RB,Res],
37		sconj([CA,CB,SLOG],SetLogConstr).
38		b2e(UNOP,Env,SetLogConstr,Res) :- % ditto
39		arith_un_op(UNOP,A,SetLogOperator),!,
40		barithexpr2setlog(A,Env,CA,RA),
41		SLOG =.. [SetLogOperator,RA],
42		sconj([CA,'is'(Res,SLOG)],SetLogConstr).
43		b2e(BOP,Env,SetLogConstr,Res) :- % ditto
44		arith_bin_op(BOP,A,B,SetLogOperator),!,
45		barithexpr2setlog(A,Env,CA,RA), barithexpr2setlog(B,Env,CB,RB),
46		SLOG =.. [SetLogOperator,RA,RB],
47		sconj([CA,CB,'is'(Res,SLOG)],SetLogConstr).
48		b2e(identifier(ID),Env,true,PrologVar) :- % var is not fresh and cannot be freely unified
49		lookup_identifier(Env,ID,PrologVar). % could also be global_set or global constant
50		b2e(integer(I),_,true,I).
51		b2e(empty_set,_,true,'{}').
52		b2e(string(S),_,true,string(S)).
53		b2e(boolean_false,_,true,pred_false).
54		b2e(boolean_true,_,true,pred_true).
55		b2e(max_int,_,true,MaxInt) :-
56		get_preference(maxint, MaxInt).
57		b2e(min_int,_,true,MinInt) :-
58		get_preference(minint, MinInt).
59		b2e(bool_set,Env,Constr,R) :-
60		b2sext([b(boolean_false,boolean,[]),
61		b(boolean_true, boolean,[])],Env,Constr,R).
62		% setlog set representations: int/2: interval, cp/2: cartesian_product, List of length 2: couple
63		b2e(cartesian_product(A,B),Env,Constr,R) :-
64		bexpr2setlog(A,Env,CA,RA),bexpr2setlog(B,Env,CB,RB),
65		sconjoin(CA,CB,Constr), R=cp(RA,RB).
66		b2e(interval(A,B),Env,Constr,R) :-
67		bexpr2setlog(A,Env,CA,RA),bexpr2setlog(B,Env,CB,RB), sconjoin(CA,CB,Constr), R=int(RA,RB).
68		b2e(couple(A,B),Env,Constr,R) :- bexpr2setlog(A,Env,CA,RA),bexpr2setlog(B,Env,CB,RB),
69		sconjoin(CA,CB,Constr),R=[RA,RB].
70		%b2e(convert_bool(A),Env,Constr,R) :- bpred2setlog(A,Env,CA),sconjoin(CA,bool(A,R),Constr).
71		b2e(first_projection(A),Env,Constr,R) :- bexpr2setlog(A,Env,CA,RA),sconjoin(CA,RA=[R,_],Constr). % existential Prolog variable could be problem inside negation
72		b2e(second_projection(A),Env,Constr,R) :- bexpr2setlog(A,Env,CA,RA),sconjoin(CA,RA=[_,R],Constr).
73		b2e(set_extension(L),Env,Constr,R) :- b2sext(L,Env,Constr,R).
74		b2e(value(Val),Env,Constr,R) :- b2v(Val,Env,Constr,R).
75		b2e(comprehension_set(Ids,Body),Env,true,Res) :-
76		Ids=[ID], % TODO: support multiple ids
77		extract_membership(Body,ID,Env,MemberConstr,RestBody),
78		Res = ris(MemberConstr,FilterConstr,Pattern), % intensional setlog set
79		bexpr2setlog(ID,Env,CA,Pattern),
80		bpred2setlog(RestBody,Env,CB),
81		sconjoin(CA,CB,FilterConstr).
82		b2e(pow_subset(BSet),Env, Constr, GIS) :-
83		GIS = '{}'(':'(X,subset(X,SET))),
84		bexpr2setlog(BSet,Env,Constr,SET).
85		% TODO: pow1_subset
86
87		:- use_module(probsrc(b_global_sets),[lookup_global_constant/2, b_global_set/1]).
88		lookup_identifier(Var,ID,Value) :- (var(Var) ; Var==[]), !,
89		(lookup_global_constant(ID,Val) -> b2v(Val,[],true,Value) % TODO: remove Env and Constr from b2v pred
90		; b_global_set(ID) -> b2v(global_set(ID),[],true,Value)
91		; Var = [bind(ID,Value)|_]). % add fresh value to environment, this var is not fresh and cannot be freely unified
92		lookup_identifier([bind(ID1,Val1)|T],ID,Value) :-
93		(ID=ID1 -> Value=Val1 % identifier already exists in environment
94		; lookup_identifier(T,ID,Value)).
95
96		% extract membership constraints for Setlog quantifiers and intensional sets
97		extract_membership(b(member(TID1,Set),pred,_),TID2,Env,Constr,Rest) :-
98		same_id(TID1,TID2,_), Rest=b(truth,pred,[]),
99		b2p(member(TID1,Set),Env,Constr),
100		Constr = in(_,_). % just a simple in constraint; TODO: maybe perform type inference
101		extract_membership(b(conjunct(LHS,RHS),pred,_),TID,Env,Constr,Rest) :-
102		(extract_membership(LHS,TID,Env,Constr,LRest)
103		-> conjunct_predicates([LRest,RHS],Rest)
104		; extract_membership(RHS,TID,Env,Constr,RRest),
105		conjunct_predicates([LHS,RRest],Rest)
106		).
107
108		:- use_module(probsrc(custom_explicit_sets),[expand_custom_set_to_list/4]).
109		% translation of B values to setlog
110		b2v(Val,Env,_,_) :- var(Val),!,
111		add_translation_error(Env,'Cannot convert compiled B value variable to setlog:',Val),fail.
112		b2v(pred_false,_,true,pred_false).
113		b2v(pred_true,_,true,pred_true).
114		b2v(int(I),_,true,I).
115		b2v(string(S),_,true,string(S)).
116		b2v(fd(Nr,Set),_,true,SetlogTerm) :- translate_global_fd_value(Nr,Set,SetlogTerm).
117		b2v([],Env,C,R) :- b2e(empty_set,Env,C,R).
118		b2v(couple(A,B),Env,Constr,R) :- b2v(A,Env,CA,RA),b2v(B,Env,CB,RB),
119		sconjoin(CA,CB,Constr),R=[RA,RB].
120		b2v(avl_set(A),Env,Constr,R) :-
121		expand_custom_set_to_list(avl_set(A),List,_,b2v),
122		b2vlist(List,Env,Constr,R).
123		b2v(global_set(A),Env,Constr,R) :-
124		expand_custom_set_to_list(global_set(A),List,_,b2v), % for deferred sets this will use the scope of ProB
125		b2vlist(List,Env,Constr,R).
126		b2v(Val,Env,_,_) :- print(Val),nl,
127		add_translation_error(Env,'Cannot convert compiled B value to setlog:',Val), fail.
128
129		translate_global_fd_value(Nr,Set,fd(Nr,Set)). % or should we use numbers?
130
131		% converting list of B values to setlog
132		b2vlist([],Env,Constr,Res) :- !, b2e(empty_set,Env,Constr,Res).
133		b2vlist([A],Env,Constr,Res) :- !, Res = '{}'(RA), b2v(A,Env,Constr,RA).
134		b2vlist([A|T],Env,Constr,Res) :- b2v(A,Env,CA,RA),
135		Res = '{}'(RA/RT), % Setlog {RA/RT}
136		b2vlist(T,Env,CT,RT),
137		sconjoin(CA,CT,Constr).
138
139		% translation for arithmetic expressions; avoid creating nested is/2 if possible
140
141		barithexpr2setlog(b(E,_T,_I),Env,SetLogConstr,Res) :- b2arithe(E,Env,C,R),!, SetLogConstr=C,Res=R.
142		barithexpr2setlog(TE,Env,_,_) :-
143		add_translation_error(Env,'Cannot convert B arithmetic expression to setlog:',TE),fail.
144
145		b2arithe(integer(I),_,true,I) :- !.
146		b2arithe(UNOP,Env,SetLogConstr,SLOG) :- % ditto
147		arith_un_op(UNOP,A,SetLogOperator),!,
148		barithexpr2setlog(A,Env,SetLogConstr,RA),
149		SLOG =.. [SetLogOperator,RA].
150		b2arithe(BOP,Env,SetLogConstr,SLOG) :- % ditto
151		arith_bin_op(BOP,A,B,SetLogOperator),!,
152		barithexpr2setlog(A,Env,CA,RA), barithexpr2setlog(B,Env,CB,RB),
153		SLOG =.. [SetLogOperator,RA,RB],
154		sconj([CA,CB],SetLogConstr).
155		b2arithe(BExpr,Env,SetLogConstr,Res) :- b2e(BExpr,Env,SetLogConstr,Res).
156
157		% binary B operators mapped to Setlog ternary predicates:
158		bin_op(union(A,B),A,B,un).
159		bin_op(intersection(A,B),A,B,inters).
160		bin_op(set_subtraction(A,B),A,B,diff).
161		bin_op(function(A,B),A,B,apply).
162		bin_op(rel_composition(A,B),A,B,comp).
163		bin_op(image(A,B),A,B,rimg).
164		bin_op(domain_restriction(A,B),A,B,dres).
165		bin_op(domain_subtraction(A,B),A,B,dares).
166		bin_op(range_restriction(A,B),A,B,rres).
167		bin_op(range_subtraction(A,B),A,B,rares).
168		bin_op(overwrite(A,B),A,B,oplus).
169
170
171		% TODO: use disjointness disj, ndisj
172		% Other candidates: symmetric difference sdiff, composition partial fun: comppf, and dompf, drespf
173
174		% unary B operators mapped to Setlog binary predicates:
175		un_op(card(A),A,size).
176		un_op(domain(A),A,dom).
177		un_op(id(A),A,id).
178		un_op(max(A),A,smax).
179		un_op(min(A),A,smin).
180		un_op(range(A),A,ran).
181		un_op(reverse(A),A,inv).
182
183		% unary B arithmetic operators mapped to Setlog is call:
184		arith_un_op(unary_minus(A),A,'-').
185
186		% binary B arithmetic operators mapped to Setlog is call:
187		arith_bin_op(add(A,B),A,B,'+').
188		arith_bin_op(div(A,B),A,B,'div').
189		arith_bin_op(minus(A,B),A,B,'-').
190		arith_bin_op(modulo(A,B),A,B,'mod').
191		arith_bin_op(multiplication(A,B),A,B,'*').
192		arith_bin_op(power_of(A,B),A,B,'**'). %% Not sure if this works
193
194		% unsupported: closure, closure1, iterate, union, inter, UNION, INTER, {x | x>2 & x<3}, !x.(x>2 => x>1)
195		% can we support less_real, ...
196
197		% translate set_extensions
198		b2sext([],Env,Constr,Res) :- !, b2e(empty_set,Env,Constr,Res).
199		b2sext([A],Env,Constr,Res) :- !, Res = '{}'(RA), bexpr2setlog(A,Env,Constr,RA).
200		b2sext([A|T],Env,Constr,Res) :- bexpr2setlog(A,Env,CA,RA),
201		Res = '{}'(RA/RT), % Setlog {RA/RT}
202		b2sext(T,Env,CT,RT),
203		sconjoin(CA,CT,Constr).
204
205		do_not_generate_errors(Env) :- nonvar(Env), Env=[bind('$NO_ERRORS',V)|_], V==pred_true.
206
207		add_translation_error(Env,Msg,TE) :-
208		(do_not_generate_errors(Env)
209		-> debug_mode(on),
210		add_message(b2setlog,Msg,TE,TE)
211		; add_error(b2setlog,Msg,TE,TE)
212		).
213
214		% Translating predicates to setlog
215		% TO DO : quantifiers foreach/2, foreach/4, exists/2, exists/4
216		bpred2setlog(b(E,_T,_I),Env,SetLogConstr) :- b2p(E,Env,C),!, SetLogConstr=C.
217		bpred2setlog(TE,Env,_) :-
218		add_translation_error(Env,'Cannot convert B predicate to setlog:',TE),
219		fail.
220
221		b2p(BOP,Env,SetLogConstr) :-
222		bin_pred(BOP,A,B,SetLogOperator),!,
223		bexpr2setlog(A,Env,CA,RA),
224		bexpr2setlog(B,Env,CB,RB),
225		SLOG =.. [SetLogOperator,RA,RB],
226		sconj([CA,CB,SLOG],SetLogConstr).
227		b2p(truth,_,true).
228		b2p(falsity,_,false). % TODO: check this
229		% TODO: subset_strict for symbolic
230		b2p(not_subset_strict(A,B),Env,Constr) :-
231		bexpr2setlog(A,Env,CA,RA),
232		bexpr2setlog(B,Env,CB,RB),
233		create_not_subset(RA,B,Env,NotSubsetConstr),
234		sdisjoin('='(RA,RB),NotSubsetConstr,Disj),
235		sconj([CA,CB,Disj],Constr).
236		b2p(subset(A,B),Env,Constr) :-
237		bexpr2setlog(A,Env,CA,RA),
238		create_subset(RA,B,Env,SubsetConstr),
239		sconj([CA,SubsetConstr],Constr).
240		b2p(not_subset(A,B),Env,Constr) :-
241		bexpr2setlog(A,Env,CA,RA),
242		create_not_subset(RA,B,Env,NotSubsetConstr),
243		sconj([CA,NotSubsetConstr],Constr).
244		b2p(member(A,B),Env,Constr) :-
245		bexpr2setlog(A,Env,CA,RA),
246		bmember2setlog(B,RA,Env,CB), sconjoin(CA,CB,Constr).
247		b2p(not_member(A,B),Env,Constr) :-
248		bexpr2setlog(A,Env,CA,RA),
249		bnotmember2setlog(B,RA,Env,CB), sconjoin(CA,CB,Constr).
250		%b2p(partition(A,List),Env,Constr) :-
251		% bexpr2setlog(A,Env,CA,RA), ...
252		b2p(equal(A,B),Env,Constr) :-
253		bexpr2setlog(A,Env,CA,RA),
254		bexpr2setlog(B,Env,CB,RB),
255		(can_be_unified_in_translation(RA,A,RB,B)
256		-> RA=RB, sconjoin(CA,CB,Constr) % perform unification here to avoid creating internal fresh Prolog vars
257		; sconj([CA,CB,'='(RA,RB)],Constr)).
258		b2p(not_equal(A,B),Env,Constr) :-
259		bexpr2setlog(A,Env,CA,RA),
260		bexpr2setlog(B,Env,CB,RB),
261		(can_be_unified_in_translation(RA,A,RB,B),
262		can_be_negated(CA,NCA)
263		-> RA=RB, sconjoin(CB,NCA,Constr) % perform unification here to avoid creating internal fresh Prolog vars
264		; can_be_unified_in_translation(RA,A,RB,B),
265		can_be_negated(CB,NCB)
266		-> RA=RB, sconjoin(CA,NCB,Constr)
267		; sconj([CA,CB,'neq'(RA,RB)],Constr)).
268		b2p(negation(A),Env,CA) :- bnegpred2setlog(A,Env,CA).
269		b2p(conjunct(A,B),Env,Constr) :- bpred2setlog(A,Env,CA), bpred2setlog(B,Env,CB), sconjoin(CA,CB,Constr).
270		b2p(disjunct(A,B),Env,or(CA,CB)) :- bpred2setlog(A,Env,CA), bpred2setlog(B,Env,CB).
271		b2p(implication(A,B),Env,implies(CA,CB)) :- bpred2setlog(A,Env,CA), bpred2setlog(B,Env,CB).
272		b2p(equivalence(A,B),Env,Constr) :-
273		bpred2setlog(A,Env,CA), bpred2setlog(B,Env,CB),
274		sconjoin(implies(CA,CB),implies(CB,CA),Constr).
275		b2p(exists(TypedIds,Body),Env,Constr) :-
276		exclude(can_translate_typing_to_setlog,TypedIds,Rest),
277		Rest=[],!, % TODO: extract typing from Body
278		Constr = exists(Typing,CB),
279		generate_typing_predicates(TypedIds,TypingPreds),
280		conjunct_predicates(TypingPreds,TPS),
281		bpred2setlog(TPS,Env,Typing), bpred2setlog(Body,Env,CB).
282		b2p(forall(TypedIds,LHS,RHS),Env,Constr) :-
283		include(can_translate_typing_to_setlog,TypedIds,Translatable),
284		generate_typing_predicates(Translatable,TypingPreds),
285		conjunct_predicates(TypingPreds,TPS),
286		bpred2setlog(TPS,Env,Typing),
287		bpred2setlog(LHS,Env,CLHS), % TODO: filter LHS into setlog typing and rest and provide warnings
288		sconjoin(Typing,CLHS,SetLogLHS),
289		Constr = foreach(SetLogLHS,SetLogRHS),
290		bpred2setlog(RHS,Env,SetLogRHS).
291
292
293		negate_pred(equal(A,B),not_equal(A,B)).
294		negate_pred(not_equal(A,B),equal(A,B)).
295		negate_pred(member(A,B),not_member(A,B)).
296		negate_pred(not_member(A,B),member(A,B)).
297		negate_pred(subset(A,B),not_subset(A,B)).
298		negate_pred(not_subset(A,B),subset(A,B)).
299		negate_pred(subset_strict(A,B),not_subset_strict(A,B)).
300		negate_pred(not_subset_strict(A,B),subset_strict(A,B)).
301		negate_pred(less(A,B),greater_equal(A,B)).
302		negate_pred(greater_equal(A,B),less(A,B)).
303		negate_pred(greater(A,B),less_equal(A,B)).
304		negate_pred(less_equal(A,B),greater(A,B)).
305
306
307		bnegpred2setlog(b(E,_T,_I),Env,SetLogConstr) :- b2p_neg(E,Env,C),!, SetLogConstr=C.
308		bnegpred2setlog(TE,Env,_) :- add_translation_error(Env,'Cannot convert negated B predicate to setlog:',TE),fail.
309
310		% translate negated predicate:
311		b2p_neg(Pred,Env,CA) :- negate_pred(Pred,NPred),!, b2p(NPred,Env,CA).
312		b2p_neg(negation(A),Env,CA) :- !, bpred2setlog(A,Env,CA).
313		b2p_neg(disjunct(A,B),Env,Constr) :- !, bnegpred2setlog(A,Env,CA), bnegpred2setlog(B,Env,CB), sconjoin(CA,CB,Constr).
314		b2p_neg(conjunct(A,B),Env,or(CA,CB)) :- !, bnegpred2setlog(A,Env,CA), bnegpred2setlog(B,Env,CB).
315		b2p_neg(implication(A,B),Env,Constr) :- !, % not(a=>b) = not(not(a) or b) = a & not(b)
316		bpred2setlog(A,Env,CA), bnegpred2setlog(B,Env,CB), sconjoin(CA,CB,Constr).
317		b2p_neg(equivalence(A,B),Env,Constr) :- !, % not(a<=>b) = (a & not(b) or (not(a) & b))
318		NB = b(negation(B),pred,[]),
319		ANB = b(conjunct(A,NB),pred,[]),
320		NA = b(negation(A),pred,[]),
321		NAB = b(conjunct(NA,B),pred,[]),
322		b2p(disjunct(ANB,NAB),Env,Constr).
323		b2p_neg(A,Env,neg(CA)) :- bpred2setlog(A,Env,CA).
324
325		% check if we can unify two result variables in the translator, rather than at runtime
326		can_be_unified_in_translation(RA,A,_,_) :- fresh_result_variable(RA,A).
327		can_be_unified_in_translation(_,_,RB,B) :- fresh_result_variable(RB,B).
328		fresh_result_variable(RA,BExpr) :- var(RA), \+ creates_bound_result_variable(BExpr).
329		creates_bound_result_variable(b(identifier(_),_,_)).
330
331		% declare which Setlog operators have a negative counterpart
332		can_be_negated(un(A,B),nun(A,B)).
333		can_be_negated(inters(A,B),ninters(A,B)).
334		can_be_negated(diff(A,B),ndiff(A,B)).
335		can_be_negated(inv(A,B),ninv(A,B)).
336		can_be_negated(id(A,B),nid(A,B)).
337		can_be_negated(dom(A,B),ndom(A,B)).
338		can_be_negated(dompf(A,B),ndompf(A,B)).
339		can_be_negated(ran(A,B),nran(A,B)).
340		can_be_negated(comp(A,B,C),ncomp(A,B,C)).
341		can_be_negated(dres(A,B,C),ndres(A,B,C)).
342		can_be_negated(dares(A,B,C),ndares(A,B,C)).
343		can_be_negated(drres(A,B,C),nrres(A,B,C)).
344		can_be_negated(rares(A,B,C),nrares(A,B,C)).
345		can_be_negated(oplus(A,B,C),noplus(A,B,C)).
346		can_be_negated(rimg(A,B,C),nrimg(A,B,C)).
347		can_be_negated(apply(A,B,C),napply(A,B,C)).
348
349		% binary B predicates mapped to Setlog binary predicates:
350		%bin_pred(member(A,B),A,B,in). % dealt with specially above
351		%bin_pred(not_member(A,B),A,B,nin). % ditto
352		%bin_pred(subset(A,B),A,B,subset). % explicit rules for symbolic values
353		bin_pred(subset_strict(A,B),A,B,ssubset).
354		%bin_pred(not_subset(A,B),A,B,nsubset). % explicit rules for symbolic values
355		%bin_pred(not_subset_strict(A,B),A,B,nssubset). % does not exist in setlog!
356		bin_pred(less(A,B),A,B,'<').
357		bin_pred(less_equal(A,B),A,B,'=<').
358		bin_pred(greater(A,B),A,B,'>').
359		bin_pred(greater_equal(A,B),A,B,'>=').
360		%bin_pred(equal(A,B),A,B,'='). % dealt with specially above
361		%bin_pred(not_equal(A,B),A,B,neq). % dealt with specially above to use negated Setlog operators if possible
362
363
364		bmember2setlog(b(Set,_,_),Element,Env,Constr) :-
365		b2mem(Set,Element,Env,Constr),!.
366		bmember2setlog(Set,Element,Env,Constr) :- % default case: no special rule available
367		bexpr2setlog(Set,Env,CA,RSet),
368		sconjoin(CA,in(Element,RSet),Constr).
369
370		b2mem(pow_subset(A),Element,Env,Constr) :- !,
371		create_subset(Element,A,Env,Constr).
372		b2mem(pow1_subset(A),Element,Env,Constr) :- !,
373		create_subset(Element,A,Env,SubsetConstr),
374		sconj([SubsetConstr,'neq'(Element,'{}')],Constr).
375		b2mem(fin_subset(A),Element,Env,Constr) :- !, % Same, because Setlog only has finite sets anyway!
376		b2mem(pow_subset(A),Element,Env,Constr).
377		b2mem(fin1_subset(A),Element,Env,Constr) :- !, % Same, because Setlog only has finite sets anyway!
378		b2mem(pow1_subset(A),Element,Env,Constr).
379		b2mem(relations(A,B),Element,Env,Constr) :- !,
380		create_domain(A,Element,Env,DomConstr),
381		create_range(B,Element,Env,RanConstr),
382		sconj([rel(Element),DomConstr,RanConstr],Constr).
383		b2mem(partial_function(A,B),Element,Env,Constr) :- !,
384		create_dom_pf(A,Element,Env,DomConstr),
385		create_range(B,Element,Env,RanConstr),
386		sconj([pfun(Element),DomConstr,RanConstr],Constr).
387		b2mem(total_function(A,B),Element,Env,Constr) :- !,
388		create_dom_tf(A,Element,Env,DomConstr),
389		create_range(B,Element,Env,RanConstr),
390		sconj([pfun(Element),DomConstr,RanConstr],Constr).
391		b2mem(Set,Element,Env,Constr) :-
392		is_symbolic_set(Set,Element,Env,ElConstr,_), !, % NATURAL(1)
393		Constr = ElConstr.
394		% there is no tfun use domain / range, for injective inverse and pfun
395		% there is npfun and ndompf
396
397
398		bnotmember2setlog(b(Set,_,_),Element,Env,Constr) :-
399		b2not_mem(Set,Element,Env,Constr),!.
400		bnotmember2setlog(Set,Element,Env,Constr) :- % default case: no special rule available
401		bexpr2setlog(Set,Env,CA,RSet),
402		sconjoin(CA,nin(Element,RSet),Constr).
403
404		% special rules for not_member
405		b2not_mem(relations(A,B),Element,Env,Constr) :- !,
406		create_not_domain(A,Element,Env,NotDomConstr),
407		is_just_type_and_infinite(B), % TODO: extend and disjoin
408		sconj([rel(Element),NotDomConstr],Constr).
409		b2not_mem(pow_subset(A),Element,Env,Constr) :- !,
410		create_not_subset(Element,A,Env,Constr).
411		b2not_mem(pow1_subset(A),Element,Env,Constr) :- !,
412		create_not_subset(Element,A,Env,SubsetConstr),
413		sdisjoin(SubsetConstr,'='(Element,'{}'),Constr).
414		b2not_mem(fin_subset(A),Element,Env,Constr) :- !, % Same, because Setlog only has finite sets anyway!
415		b2not_mem(pow_subset(A),Element,Env,Constr).
416		b2not_mem(fin1_subset(A),Element,Env,Constr) :- !, % Same, because Setlog only has finite sets anyway!
417		b2not_mem(pow1_subset(A),Element,Env,Constr).
418		b2not_mem(partial_function(A,B),Element,Env,Constr) :- !,
419		create_not_domain(A,Element,Env,DomConstr),
420		create_not_range(B,Element,Env,NotRanConstr),
421		sdisj([npfun(Element),DomConstr,NotRanConstr],Constr).
422		% Note: we do not use create_not_dom_pf
423		% somehow setlog does not seem to deal correctly with dompf inside a disjunction
424		% example: :slog-double-check f:1..2 +-> 1..2 & not(f \/ {1 |-> 3} : 1..2 +->INTEGER)
425		b2not_mem(Set,Element,Env,Constr) :-
426		is_symbolic_set(Set,Element,Env,_,NegElConstr), !, % NATURAL(1)
427		Constr = NegElConstr.
428
429		create_dom_pf(A,_,_,Constr) :- is_just_type_and_infinite(A),!,
430		% for finite types like BOOL we need to create the constraints below to let Setlog know the cardinality
431		Constr=true.
432		create_dom_pf(A,Func,Env,Constr) :-
433		create_subset(Domain,A,Env,SubsetConstr),
434		sconj([dompf(Func,Domain),SubsetConstr],Constr).
435		% TODO: check if local variable Domain poses problem with setlog/Prolog negation; we may have to extract let-equalities separately from the constraints or maybe setlog could add a let_predicate construct
436
437		create_domain(A,_,_,Constr) :- is_just_type_and_infinite(A),!, Constr=true.
438		create_domain(A,Func,Env,Constr) :-
439		create_subset(Domain,A,Env,SubsetConstr),
440		sconj([dom(Func,Domain),SubsetConstr],Constr).
441
442		% check if domain of a partial function is not a subset of a provided set A
443		create_not_dom_pf(A,_,_,Constr) :- is_just_type_and_infinite(A),!,
444		% for finite types like BOOL we need to create the constraints below to let Setlog know the cardinality
445		Constr=false.
446		create_not_dom_pf(A,Func,Env,Constr) :-
447		create_not_subset(Domain,A,Env,NotSubsetConstr),
448		sconj([dompf(Func,Domain),NotSubsetConstr],Constr).
449
450		create_not_domain(A,_,_,Constr) :- is_just_type_and_infinite(A),!, Constr=false.
451		create_not_domain(A,Func,Env,Constr) :-
452		create_not_subset(Domain,A,Env,SubsetConstr),
453		sconj([dom(Func,Domain),SubsetConstr],Constr).
454
455		create_dom_tf(A,Func,Env,Constr) :-
456		bexpr2setlog(A,Env,CA,DomType),
457		sconj([CA,dompf(Func,DomType)],Constr).
458
459		% create range constraint for a function
460		create_range(A,_,_,Constr) :- is_just_type_and_infinite(A),!, Constr=true.
461		create_range(A,Func,Env,Constr) :-
462		create_subset(Range,A,Env,SubsetConstr),
463		sconj([ran(Func,Range),SubsetConstr],Constr).
464
465		% create setlog constraint for Set1 <: Set2, where Set1 already transformed
466		create_subset(SetlogSet1,b(Set2,_,_),Env,Constr) :-
467		b2mem(Set2,VAR,Env,VAR_Constr),!, % we can create a membership constraint
468		Constr = foreach(in(VAR,SetlogSet1),VAR_Constr).
469		create_subset(SetlogSet1,BSet2,Env,Constr) :-
470		bexpr2setlog(BSet2,Env,CA,SetlogSet2),
471		sconj([CA,subset(SetlogSet1,SetlogSet2)],Constr).
472
473		% create range constraint for a function
474		create_not_range(A,_,_,Constr) :- is_just_type_and_infinite(A),!, Constr=false.
475		create_not_range(A,Func,Env,Constr) :-
476		create_not_subset(Range,A,Env,SubsetConstr),
477		sconj([ran(Func,Range),SubsetConstr],Constr).
478
479		% create setlog constraint for not (Set1 <: Set2), where Set1 already transformed
480		create_not_subset(SetlogSet1,b(Set2,_,_),Env,Constr) :-
481		b2not_mem(Set2,VAR,Env,VAR_NegConstr),!, % we can create a not-membership constraint
482		Constr = exists(in(VAR,SetlogSet1),VAR_NegConstr).
483		create_not_subset(SetlogSet1,BSet2,Env,Constr) :-
484		bexpr2setlog(BSet2,Env,CA,SetlogSet2),
485		sconj([CA,nsubset(SetlogSet1,SetlogSet2)],Constr).
486
487		% translate symbolic set in set of VAR satisfying constraint
488		is_symbolic_set(integer_set('NATURAL'),VAR,_,'>='(VAR,0),'<'(VAR,0)).
489		is_symbolic_set(integer_set('NATURAL1'),VAR,_,'>'(VAR,0),'=<'(VAR,0)).
490		%TODO: support comprehension sets; we could move code to b2mem and b2not_mem
491
492		:- use_module(probsrc(typing_tools),[is_infinite_type/1, is_provably_finite_type/1]).
493		:- use_module(probsrc(bsyntaxtree),[is_just_type/1, get_texpr_type/2]).
494		is_just_type_and_infinite(A) :- is_just_type(A),
495		get_texpr_type(A,Type),
496		is_infinite_type(Type).
497
498
499		% utilities to conjoin Setlog predicates:
500		sconjoin(false,_,R) :- !, R=false.
501		sconjoin(true,A,R) :- !, R=A.
502		sconjoin(_,false,R) :- !,R=false.
503		sconjoin(A,true,R) :- !,R=A.
504		sconjoin(A,B,'&'(A,B)).
505
506		sconj([],true).
507		sconj([H],R) :- !, R=H.
508		sconj([H|T],R) :- sconj(T,TC),sconjoin(H,TC,R).
509
510
511		sdisjoin(true,_,R) :- !, R=true.
512		sdisjoin(false,A,R) :- !, R=A.
513		sdisjoin(A,false,R) :- !,R=A.
514		sdisjoin(_,true,R) :- !,R=true.
515		sdisjoin(A,B,'or'(A,B)).
516
517		sdisj([],false).
518		sdisj([H],R) :- !, R=H.
519		sdisj([H|T],R) :- sdisj(T,TC),sdisjoin(H,TC,R).
520
521		:- dynamic path_to_setlog/1, path_to_setlog_wrapper_binary/1.
522		:- if(current_prolog_flag(dialect, swi)).
523		path_to_setlog('../prob_related/setlog_wrapper/setlog498-13h1.pl').
524		:- endif.
525
526		:- use_module(probsrc(pathes_lib),[check_lib_contents/3]).
527		:- use_module(library(file_systems),[file_exists/1]).
528		get_path_to_setlog_cli_wrapper_qlf(Path) :-
529		absolute_file_name(prob_lib('setlog-cli.qlf'), Path),
530		(file_exists(Path) -> true
531		; add_warning(b2setlog,'No setlog wrapper available at: ',Path),
532		check_lib_contents(user_error,setlog,verbose),
533		fail
534		).
535		% project for wrapper is https://gitlab.cs.uni-duesseldorf.de/stups/prob/setlog_wrapper
536
537		% ---------------------------------------------------
538
539		:- use_module(probsrc(translate), [generate_typing_predicates/2]).
540		:- use_module(probsrc(bsyntaxtree), [find_typed_identifier_uses/2, conjunct_predicates/2]).
541		add_typing_pred(BPred,BPred2) :-
542		find_typed_identifier_uses(BPred,TypedIds), % we will have to do this also for quantifiers/set compr. later
543		include(can_translate_typing_to_setlog,TypedIds,TranslatableIds),
544		generate_typing_predicates(TranslatableIds,TypingPreds),
545		%translate:nested_print_bexpr(TypingPreds),nl,
546		conjunct_predicates([BPred|TypingPreds],BPred2).
547
548		can_translate_typing_to_setlog(b(identifier(ID),Type,Pos)) :-
549		(simple_finite_type(Type) -> true
550		; only_infinite_type(Type) -> fail
551		% TODO: we can check things like set(couple(integer,boolean)) by using range(f) <: BOOL
552		; add_message(b2setlog,'Not translating to Setlog typing for ',ID,Pos),fail
553		).
554
555		simple_finite_type(boolean).
556		simple_finite_type(global(G)) :- is_provably_finite_type(global(G)).
557		simple_finite_type(set(boolean)).
558		simple_finite_type(set(global(G))) :- is_provably_finite_type(global(G)).
559
560		only_infinite_type(integer).
561		only_infinite_type(real).
562		only_infinite_type(string).
563		only_infinite_type(set(T)) :- only_infinite_type(T).
564		only_infinite_type(couple(A,B)) :- only_infinite_type(A), only_infinite_type(B).
565
566		solve_pred_with_setlog(BPred,LocalState,Res) :-
567		get_preference(time_out, Timeout),
568		solve_pred_with_setlog(BPred,LocalState,[timeout(Timeout)],Res).
569		solve_pred_with_setlog(BPred,LocalState,Options,Res) :-
570		add_typing_pred(BPred,BPred2),
571		write('Translating: '),translate:print_bexpr(BPred2),nl,
572		bpred2setlog(BPred2,LocalState,SetlogConstraint),!,
573		length(LocalState,Len), % fix length
574		!,
575		( numbervars(LocalState,0,_),
576		format('Setlog translation (~w ids):~n ~w~n',[Len,SetlogConstraint]),
577		fail ; true),
578		(path_to_setlog(Path),
579		use_module(Path,[setlog/1])
580		-> setlog_solve_direct(SetlogConstraint,LocalState,Options,Res)
581		; get_path_to_setlog_cli_wrapper_qlf(QlfPath)
582		-> setlog_solve_with_wrapper(QlfPath,SetlogConstraint,LocalState,Options,Res)
583		; Res=no_solution_found(setlog_not_available)
584		).
585		solve_pred_with_setlog(_,[],_,Res) :- Res=no_solution_found(translation_failed).
586
587		% solve setlog constraint directly with loaded setlog module (works when running ProB from SWI)
588		setlog_solve_direct(SetlogConstraint,LocalState,Options,Res) :-
589		member(timeout(TimeOutMs),Options),!,
590		safe_time_out(setlog_solve_direct(SetlogConstraint,LocalState,Res),TimeOutMs,TimeOutRes),
591		(TimeOutRes=time_out ->
592		format('Timeout in Setlog Prover (~w ms)~n',[TimeOutMs]),
593		Res=no_solution_found(time_out)
594		; true).
595		setlog_solve_direct(SetlogConstraint,LocalState,_Options,Res) :-
596		setlog_solve_direct(SetlogConstraint,LocalState,Res).
597
598		setlog_solve_direct(SetlogConstraint,LocalState,Res) :-
599		catch(
600		(setlog(SetlogConstraint)
601		-> format('Setlog solution:~n ~w~n',[LocalState]), % todo: translate to B, possibly ground empty sets
602		maplist(setlog_bind2b,LocalState,Sol),
603		Res=solution(Sol)
604		; Res=contradiction_found
605		),
606		setlog_excpt(Exc),
607		Res=no_solution_found(setlog_excpt(Exc))
608		).
609
610		:- use_module(library(codesio),[format_to_codes/3,write_to_codes/2,read_term_from_codes/3]).
611		:- use_module(probsrc(system_call), [system_call/5]).
612		% solve setlog constraint via external setlog wrapper binary or via swipl
613		setlog_solve_with_wrapper(QlfPath,SetlogConstraint,LocalState,Options,Res) :-
614		term_variables(SetlogConstraint,Vars),
615		maplist(get_variable_name,Vars,VarNames),
616		%format('VarNames: ~q ~n',[VarNames]),
617		%numbervars(SetlogConstraint,0,_),
618		format_to_codes('~q',[SetlogConstraint],SlogCS),
619		atom_codes(SlogConstraintAtom,SlogCS),
620		(member(timeout(TO),Options) -> get_atom(TO,TOAtom) ; TOAtom='2500'),
621		format_to_codes('consult(~q), main, halt ; halt(1).',[QlfPath],GoalCodes),
622		atom_codes(SwiGoal,GoalCodes),
623		debug_format(19,'Calling setlog wrapper (goal ~w) with ~w --groundsol --timeout ~w (vars ~w)~n',
624		[SwiGoal,SlogConstraintAtom,TOAtom,Vars]),
625		% TODO Allow changing swipl command/path
626		%debug_format(19,'Using SWI Prolog binary at: ~w~n',[SwiPath]),
627		(debug_mode(on) -> TArgs = ['--verbose'] ; TArgs=[]),
628		system_call(path(swipl),['-g',SwiGoal,
629		'--',SlogConstraintAtom,
630		'--groundsol','--timeout',TOAtom|TArgs],Text,ErrorTextAsCodeList,Exit),
631		debug_format(9,'Exit Status: ~w~n-----~nStdout: ~s~n-----~nStderr: ~s~n',[Exit,Text,ErrorTextAsCodeList]),
632		(ErrorTextAsCodeList=[],
633		Exit=exit(0)
634		-> process_setlog_result(Text,VarNames,Res),
635		(var(Res)
636		-> maplist(setlog_bind2b,LocalState,Sol),Res=solution(Sol)
637		; true)
638		; add_error(b2setlog,'Errors occured when running setlog wrapper, exit status:',Exit),
639		format(user_error,'Error Messages:~n~s~n',[ErrorTextAsCodeList]),
640		format(user_error,'Output Messages:~n~s~n',[Text]),
641		Res=error
642		).
643
644		% convert number to atom if necessary, system call does not like numbers as args
645		get_atom(A,R) :- atom(A),!,R=A.
646		get_atom(Nr,Atom) :- number(Nr), number_codes(Nr,C),atom_codes(Atom,C).
647
648		% get the name of a Prolog variable
649		get_variable_name(Var,Name=Var) :-
650		write_to_codes(Var,Codes),
651		atom_codes(Name,Codes).
652		%get_variable_name(Var,Name=Var) :-
653		% format_to_codes('var(~q).',[Var],Codes),
654		% read_term_from_codes(Codes,_,[variable_names(Names)]),
655		% Names = [Name=Var].
656
657		process_setlog_result([],_,_) :- !.
658		process_setlog_result(Codes,VarNames,Res) :-
659		append("setlog_",_,Codes), % we have a setlog result fact
660		skip_until_eol(Codes,Line1,Rest),!,
661		%format('Processing : ~s~n',[Line1]),
662		read_term_from_codes(Line1,Term,[variable_names(_VN2)]),
663		debug_format(19,'Read term: ~w~n',[Term]),
664		procces_setlog_result_term(Term,VarNames,Res),
665		process_setlog_result(Rest,VarNames,Res).
666		process_setlog_result(Codes,VarNames,Res) :-
667		skip_until_eol(Codes,_Skipping,Rest),!,
668		process_setlog_result(Rest,VarNames,Res).
669
670		procces_setlog_result_term(setlog_variable_bindings(Bindings),VarNames,_) :- !,
671		maplist(process_setlog_binding(VarNames),Bindings).
672		procces_setlog_result_term(setlog_version(Version),_,_) :- !,
673		format('Setlog version: ~w~n',[Version]).
674		procces_setlog_result_term(setlog_result(Result),_,Res) :- !,
675		format('Setlog result: ~w~n',[Result]), % should be success for solved constraint
676		(convert_setlog_result(Result,Res) -> true
677		; add_error(b2setlog,'Illegal setlog result:',Result),
678		Res = error).
679		procces_setlog_result_term(_,_,_).
680
681		convert_setlog_result(success,_). % keep variable, will be bound to solution(_) later
682		convert_setlog_result(failure,contradiction_found).
683		convert_setlog_result(time_out,no_solution_found(time_out)).
684		convert_setlog_result(timeout,no_solution_found(time_out)).
685
686		process_setlog_binding(_,true) :- !.
687		process_setlog_binding(VarNames,'='(VariableName,Term)) :-
688		debug_format(9,'~q~n',[equality(VariableName,Term,VarNames)]),
689		member(VariableName=Var,VarNames),!,
690		if(Var=Term,true,
691		format('Cannot apply setlog binding to B: ~w=~w~n',[VariableName,Term])).
692		process_setlog_binding(_,Binding) :-
693		add_error(b2setlog,'Illegal setlog result binding:',Binding).
694
695		% skip until end of line or file
696		skip_until_eol([],[],[]).
697		skip_until_eol([10|Rest],[],Rest).
698		skip_until_eol([13|Rest],[],Rest).
699		skip_until_eol([H|T],[H|LT],Rest) :- skip_until_eol(T,LT,Rest).
700
701		% -------------------------
702
703		setlog_bind2b(bind(ID,Val),bind(ID,TVal)) :- (setlog_value2b(Val,TVal) -> true ; TVal = term(Val)).
704
705		:- use_module(probsrc(custom_explicit_sets),[construct_interval_closure/3]).
706		%setlog_value2b(F,_) :- nonvar(F),functor(F,FF,NN), print(setlog_value2b(FF/NN,F)),nl,fail.
707		setlog_value2b(V,Res) :- var(V),!,Res=V.
708		setlog_value2b(Nr,Res) :- integer(Nr),!,Res=int(Nr).
709		setlog_value2b(pred_false,Res) :- !, Res=pred_false.
710		setlog_value2b(pred_true,Res) :- !, Res=pred_true.
711		setlog_value2b([A,B],(TA,TB)) :- !,
712		setlog_value2b(A,TA), setlog_value2b(B,TB).
713		setlog_value2b('{}',R) :- !, R=[].
714		setlog_value2b('{}'(A/T),R) :- !, R=[TA|TT], setlog_value2b(A,TA),setlog_value2b(T,TT).
715		setlog_value2b('{}'(A),TA) :- !, setlog_set_value2b(A,TA).
716		setlog_value2b(string(S),R) :- !, R=string(S).
717		setlog_value2b(fd(Nr,S),R) :- !, R=fd(Nr,S).
718		setlog_value2b(int(From,To),R) :-
719		setlog_value2b(From,int(F)),
720		setlog_value2b(To,int(T)),!, construct_interval_closure(F,T,R).
721		setlog_value2b(Val,_R) :- Val=..[Func|Args],length(Args,Len),
722		print(unsupported_val(Val,func(Func/Len),args(Args))),nl,
723		true. %R=term(Val).
724		% TODO: sometimes we get quoted variable names from setlog via setlog-wrapper
725
726		setlog_set_value2b(Var,R) :- var(Var),!,R=Var.
727		%setlog_set_value2b(F,_) :- functor(F,FF,NN), print(setv(FF/NN,F)),nl,fail.
728		setlog_set_value2b(','(A,T),R) :- !, R=[TA|TB], setlog_value2b(A,TA),
729		setlog_set_value2b(T,TB).
730		setlog_set_value2b('/'(A,T),R) :- !, R=[TA|TT], setlog_value2b(A,TA),setlog_value2b(T,TT).
731		setlog_set_value2b(A,R) :- setlog_value2b(A,TA),!,R=[TA].
732		setlog_set_value2b(Val,term(Val)) :- print(unsupported_set_val(Val)),nl.
733
734		% ----------------
735
736
737		:- use_module(probsrc(tools), [start_ms_timer/1,stop_ms_timer_with_msg/2]).
738		:- use_module(probsrc(tools_meta),[safe_time_out/3]).
739		prove_using_setlog(Goal,Hypotheses,Opts,TimeOutMs,Res) :-
740		% quite often 0 or 1 ms are enough for TimeOutMs
741		(member(disprover_option(po_label(Label)),Opts) -> true ; Label='?'),
742		format('Starting Setlog Prover (timeout ~w ms) for \'~w\' ~n',[TimeOutMs,Label]),
743		start_ms_timer(Timer),
744		prove_sequent_with_setlog(Goal,Hypotheses,[timeout(TimeOutMs)],Res),
745		stop_ms_timer_with_msg(Timer,'Setlog Prover completed').
746
747		prove_sequent_with_setlog(TGoal,THypotheses,Options,Res) :-
748		% build predicate H1 & H2 .... & not Goal
749		create_negation(TGoal,NegatedGoal),
750		(can_translate_to_setlog(NegatedGoal)
751		-> include(can_translate_to_setlog,THypotheses,OkHyps),
752		conjunct_predicates([NegatedGoal|OkHyps],Predicate),
753		(debug_mode(on) -> write('SETLOG:'),nl,translate:nested_print_bexpr(Predicate),nl ; true),
754		solve_pred_with_setlog(Predicate,_,Options,Res)
755		; Res = no_solution_found(cannot_translate_goal)
756		),
757		format('Setlog prover result: ~w~n',[Res]).
758
759		can_translate_to_setlog(b(E,_T,_I)) :-
760		b2p(E,[bind('$NO_ERRORS',pred_true)|_Env],_C),!.
761		can_translate_to_setlog(E) :-
762		debug_mode(on),
763		add_message(b2setlog,'Ignoring hypothesis: ',E,E),fail.
764
765		/*
766		| ?- b2e(union(b(identifier(a),any,[]),b(identifier(A),any,[])),Env,Constraints,ResultVar).
767		A = a,
768		Env = [a/_A|_B],
769		Constraints = un(_A,_A,ResultVar) ?
770
771		| ?- | ?- b2p(member(b(integer(1),integer,[]),b(union(b(identifier(A),any,[]),b(identifier(A),any,[])),any,[])),Env,Constraints).
772		A = a,
773		Env = [a/_A|_B],
774		Constraints = &(un(_A,_A,_C),in(1,_C)) ?
775
776		>>> :slog f:INTEGER +-> INTEGER & f(x)=y & g=f<+{x|->y+1} & g(x)=y
777
778		% :slog n>0 & f:1..n +-> 1..n & x:1..n & not(f<+{1|->x}:1..n +->1..n)
779
780		x<:{5,10,15,20,25,30,35,40,45,50,55,60,65,70,75,80,85,90,95,100} & card(x)=15 & (55/:x => 65:x) & (45/:x => 75:x) & (35 /:x => 85:x)
781		*/