1		% (c) 2025-2026 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(b2asp,[solve_pred_with_clingo/5, run_clingo_on_formula/1, test/1]).
6
7		:- if(current_module(module_information)).
8		:- use_module(probsrc(module_information),[module_info/2]).
9		:- module_info(group,b2asp).
10		:- module_info(description,'Solve B formulas with clingo ASP solver.').
11		:- endif.
12
13
14		% first attempt at translator from B AST to ASP
15		% started May 7th 2025, Michael Leuschel, based on analysis of B to ASP translations by Maxime Zielinger
16		% Michael Leuschel, Maxime Zielinger
17
18		% Current restrictions:
19		% * higher-order values (sets of sets, ...) are not supported
20		% * universal quantification:
21		% - only scalar identifiers can be quantified
22		% - no use of existential quantifiers inside forall yet (gen_clingo_set_identifier cannot yet take Env into account)
23		% - no use of set comprehensions inside forall yet (ditto)
24		% * only certain SIGMA patterns supported: SIGMA(ID).(ID:SET|ID)
25		% * variable clash limitations: no nesting of existential quantifiers with same name
26		%
27		% Still required:
28		% * avoid passing quantified variables (forall) as arguments to Clingo predicates if not necessary
29		% * scope/interval analysis to determine base types for unbounded integer variables
30		% * we could try and inline/partially evaluate the program to avoid redundant intermediate predicates
31
32
33		:- use_module(library(lists)).
34		:- use_module(library(between),[between/3]).
35
36		%:- op(700,fx,not). % add operator declaration, as we need to print not without parentheses for Clingo
37
38		:- use_module(b2asp_code_gen).
39		:- use_module(clingo_interface).
40		:- use_module(bounds_analysis,[infer_bounds/4]).
41
42
43		:- use_module(probsrc(error_manager)).
44		:- use_module(probsrc(debug)).
45		:- use_module(probsrc(preferences)).
46		:- use_module(probsrc(b_global_sets),[b_get_fd_type_bounds/3, lookup_global_constant/2]).
47		:- use_module(probsrc(tools_strings),[ajoin/2,ajoin_path/3]).
48		:- use_module(probsrc(bsyntaxtree),[get_texpr_id/2, get_texpr_ids/2,
49		get_texpr_type/2, create_couple/2, create_cartesian_product/3]).
50		:- use_module(probsrc(version), [version_str/1]).
51		:- use_module(probsrc(translate),[translate_bexpression_with_limit/3]).
52		:- use_module(probsrc(btypechecker), [couplise_list/2]).
53		:- use_module(probsrc(tools),[start_ms_timer/1, stop_ms_timer_with_msg/2, get_elapsed_walltime/2]).
54		:- use_module(covsrc(hit_profiler),[add_to_profile_stats/2]).
55		:- use_module(probsrc(bsyntaxtree), [find_typed_identifier_uses/2,create_exists/3]).
56		% errors are recorded as translation errors, so that clingo is not run (see add_translation_error)
57		add_b2asp_error(Msg,Args) :- add_translation_error(Msg,Args).
58		add_b2asp_error(Msg,Args,Span) :- add_translation_error(Msg,Args,Span).
59		add_b2asp_warning(Msg,Args) :- add_warning(b2asp,Msg,Args).
60		get_clingo_out_file(File) :-
61		get_preference(tmpdir, TmpDir),
62		ajoin_path(TmpDir, 'prob_clingo_translation.lp', File).
63		% see get_temporary_filename, open_temp_file
64
65
66
67		% ------------------------------
68		% translating PREDICATES
69
70		% a top-level translation of predicates
71		% asserts translations as integrity constraint (aka query)
72
73		%top_level_translate_predicate(Formula) :-
74		% trans_pred_positive(Formula,Prop),
75		% gen_clingo_ic_constraint( not(Prop) ). % assert main is false, and Formula is true
76		top_level_translate_predicate(Formula) :-
77		create_new_local_id_env(Env),
78		trans_not_pred(Formula,Env,Prop),
79		gen_clingo_ic_constraint( Prop ).
80
81		is_predicate(b(_,pred,_)). % ProB typed AST node
82		is_predicate(BOP) :- bin_op_pred_single_call(BOP,_,_,_).
83		is_predicate(X) :- negate_pred(X,_) ; negate_pred(NX,X), NX \= negation(_).
84		is_predicate(BOP) :- negate_scalar_binary_pred(BOP,_,_,_).
85		is_predicate(conjunct(_,_)).
86		is_predicate(disjunct(_,_)).
87		is_predicate(implication(_,_)).
88		is_predicate(equivalence(_,_)).
89		is_predicate(if_predicate(_,_,_)).
90
91		% translating a predicate into a proposition that is true if predicate is true
92		% not sure if we need it
93		%trans_pred_positive(BOP,Env,Prop) :-
94		% bin_op_pred_single_call(BOP,A,B,ClingoOp),
95		% translate_scalar(A,Env,ValA,CallA),
96		% translate_scalar(B,Env,ValB,CallB),
97		% ClingoCall =.. [ClingoOp,ValA,ValB],
98		% gen_clingo_clause(pred,Prop,[], (CallA,CallB, ClingoCall) ).
99
100
101		% translating a predicate into a proposition that is true if predicate is true
102		% it is currently use for the left-hand-side of universal quantifiers
103		% not sure that it is really required; it can provide a few optimized translation rules, avoiding negation
104		trans_pos_pred(b(Pred,pred,_Infos),Env,Prop) :- !, % format(user_output,' pred --> ~w~n',[Pred]),
105		trans_pos_pred(Pred,Env,Prop).
106		trans_pos_pred(truth,Env,Prop) :- !,
107		gen_clingo_fact(truth,Prop,[],Env).
108		trans_pos_pred(member(A,B),Env,Prop) :- \+ specific_member_rule_exists(B), !, % otherwise use negation
109		BP = b(member(A,B),pred,[]),
110		register_clingo_predicate(member,BP,Prop,Env,Env2),
111		translate_scalar(A,Env2,X1,CallA),
112		trans_set(B,Env2,P2),
113		clingo_format_comment_with_expr('% member predicate (positive) ~w~n',BP),
114		gen_clingo_pred_clause(member,Prop,[],Env2,
115		(CallA, ecall(P2,[X1],Env2) )). % :- P1(X), P2(X). (same as subset)
116		trans_pos_pred(Arith,Env,Prop) :-
117		scalar_binary_pred(Arith,A,B,ClingoOp),!,
118		translate_top_level_scalars(A,B,Env,X1,CallA,X2,CallB),
119		clingo_format_comment('% arithmetic predicate (positive) ~w~n',[ClingoOp]),
120		gen_clingo_pred_clause(arith,Prop,[],Env, (CallA, CallB, call(ClingoOp,X1,X2) )).
121		trans_pos_pred(conjunct(P1,P2),Env,Prop) :- !,
122		trans_pos_pred(P1,Env,TrueP1),
123		trans_pos_pred(P2,Env,TrueP2),
124		clingo_format_comment('% conjunction (positive)~n',[]),
125		gen_clingo_pred_clause(conjunct,Prop,[],Env,
126		(ecall(TrueP1,Env) , ecall(TrueP2,Env)) ).
127		trans_pos_pred(X,Env,Prop) :-
128		trans_not_pred(negation(X),Env,Prop).
129
130		specific_member_rule_exists(b(E,_,_)) :- !, specific_member_rule_exists(E).
131		specific_member_rule_exists(pow_subset(_)).
132		specific_member_rule_exists(pow1_subset(_)).
133		specific_member_rule_exists(relations(_,_)).
134		specific_member_rule_exists(partial_function(_,_)).
135		specific_member_rule_exists(partial_injection(_,_)).
136		specific_member_rule_exists(total_relation(_,_)).
137		specific_member_rule_exists(total_function(_,_)).
138		specific_member_rule_exists(total_injection(_,_)).
139		specific_member_rule_exists(surjection_relation(_,_)).
140		specific_member_rule_exists(partial_surjection(_,_)).
141		specific_member_rule_exists(total_surjection_relation(_,_)).
142		specific_member_rule_exists(total_surjection(_,_)).
143		specific_member_rule_exists(partial_bijection(_,_)).
144		specific_member_rule_exists(total_bijection(_,_)).
145		specific_member_rule_exists(seq(_)).
146		specific_member_rule_exists(iseq(_)).
147		specific_member_rule_exists(seq1(_)).
148		specific_member_rule_exists(iseq1(_)).
149		specific_member_rule_exists(perm(_)).
150
151		% translating a predicate into a proposition that is false if predicate is true and can be used as ic constraint
152		% not sure if we need both positive and negative translations
153		trans_not_pred(b(Pred,pred,_Infos),Env,Prop) :- !, % format(user_output,' pred --> ~w~n',[Pred]),
154		trans_not_pred(Pred,Env,Prop).
155		trans_not_pred(exists(Paras,Pred),Env,Prop) :- in_non_positive_context, !,
156		% the parameters of an existential quantifier are translated as clingo identifiers whose values clingo can choose;
157		% this is only correct if the quantified predicate must be true (i.e., in a positive context)
158		% in a negative context, e.g., not(#x.P), clingo would simply choose an x for which P is false
159		translate_bexpression_with_limit(b(exists(Paras,Pred),pred,[]),100,ES),
160		add_b2asp_error('Existential quantifier in negative or mixed context (e.g., inside not, <=>, left of =>, IF condition) not yet supported: ',ES,Pred),
161		trans_not_pred(truth,Env,Prop).
162		trans_not_pred(exists(Paras,Pred),Env,Prop) :- !,
163		(member(b(identifier(ID),_,_),Paras),
164		generated_id(ID,_), % TODO: register paras in Env, rather than using generated_id/2 facts
165		add_b2asp_error('Identifier clash (B2ASP does not yet support multiple uses of same id): ',ID),fail
166		; true),
167		check_empty_env(Env,Paras,Pred), % at the moment we do not support exists inside forall
168		infer_bounds_within_env(Paras,Pred,Env,BI),
169		debug_format(19,'exists bounds_info: ~w~n',[BI]),
170		(BI = contradiction_found
171		-> trans_not_pred(falsity,Env,Prop) % no solution for body
172		; add_new_local_id_bounds(BI,Env,Env2),
173		trans_not_pred(Pred,Env2,Prop)
174		).
175		trans_not_pred(forall(Ids,LHS,RHS),Env,Prop) :- !,
176		infer_bounds_within_env(Ids,LHS,Env,BI),
177		add_message(b2asp,'Forall bounds info: ',BI,LHS),
178		trans_not_pred(forall_with_precomputed_bounds(Ids,BI,LHS,RHS),Env,Prop).
179		trans_not_pred(forall_with_precomputed_bounds(Ids,BI,LHS,RHS),Env,Prop) :- !,
180		(BI = contradiction_found
181		-> trans_not_pred(truth,Env,Prop) % no solution for LHS; forall is true
182		; add_local_typed_ids(Ids,BI,Env,LocalIdSetupCode,NewEnv),
183		trans_pos_pred(LHS,NewEnv,P1),
184		trans_not_pred(RHS,NewEnv,NotP2),
185		get_texpr_ids(Ids,II),clingo_format_comment('% forall (negative) over ~w~n',[II]),
186		gen_clingo_pred_clause(not_forall,Prop,[], Env, % this must be Env and not NewEnv !
187		(LocalIdSetupCode ,ecall(P1,NewEnv) , ecall(NotP2,NewEnv)) )
188		).
189		trans_not_pred(truth,Env,Prop) :- !,
190		gen_clingo_pred_clause(falsity,Prop,[],Env, 1=2 ).
191		trans_not_pred(falsity,Env,Prop) :- !,
192		gen_clingo_fact(truth,Prop,[],Env).
193		trans_not_pred(subset(A,B),Env,Prop) :- !,
194		BP = b(subset(A,B),pred,[]),
195		register_clingo_predicate(not_subset,BP,Prop,Env,Env2),
196		trans_set(A,Env2,P1), trans_set(B,Env2,P2),
197		clingo_format_comment_with_expr('% subset (negative) ~w~n',BP),
198		gen_clingo_clause(not_subset,Prop,[], Env2,
199		(ecall(P1,[X],Env2), not(ecall(P2,[X],Env2)) )). % :- P1(X), not P2(X).
200		trans_not_pred(subset_strict(A,B),Env,Prop) :- !,
201		precompile_set(A,Env,TA), % to avoid translating A twice
202		precompile_set(B,Env,TB), % to avoid translating A twice
203		trans_not_pred(conjunct(subset(TA,TB),not_set_equal(TA,TB)),Env,Prop).
204		trans_not_pred(member(A,B),Env,Prop) :- !,
205		trans_not_member_pred(A,B,Env,Prop). % dedicated code for translating membership
206		trans_not_pred(set_equal(A,B),Env,Prop) :- !, % could be also translated into conjunction of subset
207		% Note: does not exist as such in B AST: is equal with typing info = set(_)
208		% this could also works with scalars (i.e., if P1/P2 have exactly one solution)
209		BP = b(equal(A,B),pred,[]),
210		register_clingo_predicate(not_set_equal,BP,Prop,Env,Env2),
211		trans_set(A,Env2,P1), trans_set(B,Env2,P2),
212		CallA = ecall(P1,[X],Env2), CallB = ecall(P2,[X],Env2),
213		clingo_format_comment_with_expr('% set equality (negative) ~w~n',BP),
214		gen_clingo_clause(not_set_equal,Prop,[],Env2, (CallA, not(CallB) )), % :- P1(X), not P2(X).
215		gen_clingo_clause(not_set_equal,Prop,[],Env2, (CallB, not(CallA) )). % :- P2(X), not P1(X).
216		trans_not_pred(equal(A,B),Env,Prop) :- A = b(_,ST,_), is_set_type(ST,_),!,
217		trans_not_pred(set_equal(A,B),Env,Prop).
218		trans_not_pred(not_equal(A,B),Env,Prop) :- A = b(_,ST,_), is_set_type(ST,_),!,
219		trans_not_pred(not_set_equal(A,B),Env,Prop).
220		trans_not_pred(is_partial_function(A),Env,Prop) :- !,
221		register_clingo_predicate(not_pfun,A,Prop,Env,Env2),
222		trans_set(A,Env2,P1),
223		clingo_format_comment_with_expr('% is_partial_function (negative) ~w~n',[A]),
224		gen_clingo_clause(not_pfun,Prop,[],Env2,
225		(ecall(P1,[(X,Y)],Env2), ecall(P1,[(X,Z)],Env2), '!='(Y,Z)) ). % :- P1((X,Y)),P1((X,Z)), Y!=Z.
226		trans_not_pred(is_injective(A),Env,Prop) :- !,
227		register_clingo_predicate(not_inj,A,Prop,Env,Env2),
228		trans_set(A,Env2,P1),
229		clingo_format_comment_with_expr('% is_injective (negative) ~w~n',[A]),
230		gen_clingo_clause(not_inj,Prop,[],Env2,
231		(ecall(P1,[(Y,X)],Env2), ecall(P1,[(Z,X)],Env2), '!='(Y,Z)) ). % :- P1((Y,X)),P1((Z,X)), Y!=Z.
232		trans_not_pred(is_sequence_domain(A),Env,Prop) :- !,
233		register_clingo_predicate(not_seq,A,Prop,Env,Env2),
234		trans_set(A,Env2,P1),
235		clingo_format_comment_with_expr('% is_sequence_domain (negative) ~w~n',[A]),
236		gen_clingo_clause(not_seq,Prop,[],Env2,
237		(ecall(P1,[X],Env2), '<'(X,1) )), % :- P1(X), X < 1. (sequences start at 1)
238		gen_clingo_clause(not_seq,Prop,[],Env2,
239		(ecall(P1,[X],Env2), '>'(X,1), '='(X1,X-1), not(ecall(P1,[X1],Env2))) ). % :- P1(X), not P1(X-1).
240		trans_not_pred(Arith,Env,Prop) :-
241		negate_scalar_binary_pred(Arith,A,B,ClingoOp),!,
242		translate_top_level_scalars(A,B,Env,X1,CallA,X2,CallB),
243		clingo_format_comment('% arithmetic predicate (negative) ~w~n',[ClingoOp]),
244		gen_clingo_pred_clause(arith,Prop,[],Env, (CallA, CallB, call(ClingoOp,X1,X2) )).
245		trans_not_pred(conjunct(P1,P2),Env,Prop) :- !, % not(P1 & P2) <=> not(P1) or not(P2)
246		conjunction_to_list(conjunct(P1,P2),LP12,[]),
247		trans_not_pred(conjunction_list(LP12),Env,Prop).
248		trans_not_pred(conjunction_list(LP12),Env,Prop) :- !,
249		l_trans_not_pred(LP12,Env,[NotP1|NotLP2]),
250		clingo_format_comment('% conjunction (negative)~n',[]),
251		gen_clingo_pred_clause(not_conjunct,Prop,[],Env, ecall(NotP1,Env) ),
252		( member(NotP2,NotLP2),
253		gen_clingo_clause(not_conjunct,Prop,[],Env, ecall(NotP2,Env) ), fail
254		; true).
255		trans_not_pred(disjunct(P1,P2),Env,Prop) :- !, % not(P1 or P2) <=> not(P1) & not(P2)
256		trans_not_pred(P1,Env,NotP1),
257		trans_not_pred(P2,Env,NotP2),
258		clingo_format_comment('% disjunction (negative)~n',[]),
259		gen_clingo_pred_clause(not_disjunct,Prop,[],Env, (ecall(NotP1,Env) , ecall(NotP2,Env)) ).
260		trans_not_pred(implication(P1,P2),Env,Prop) :- !, % not(P1 => P2) <=> P1 & not(P2)
261		non_positive_context(trans_pos_pred(P1,Env,PosP1)),
262		trans_not_pred(P2,Env,NotP2),
263		clingo_format_comment('% implication (negative)~n',[]),
264		gen_clingo_pred_clause(not_implication,Prop,[],Env, (ecall(PosP1,Env) , ecall(NotP2,Env)) ).
265		trans_not_pred(equivalence(P1,P2),Env,Prop) :- !, % not(P1 <=> P2) <=> (P1 & not(P2)) or (not(P1) & P2)
266		non_positive_context(trans_not_pred(P1,Env,NotP1)),
267		non_positive_context(trans_not_pred(P2,Env,NotP2)),
268		gen_clingo_clause(not_equiv,Prop,[],Env, (not(ecall(NotP1,Env)) , ecall(NotP2,Env)) ),
269		gen_clingo_clause(not_equiv,Prop,[],Env, (ecall(NotP1,Env) , not(ecall(NotP2,Env))) ).
270		trans_not_pred(if_predicate(P1,P2,P3),Env,Prop) :- !, % not(IF P1 THEN P2 ELSE P3) <=> (P1 & not(P2)) or (not(P1) & not(P3))
271		non_positive_context(trans_pos_pred(P1,Env,PosP1)),
272		non_positive_context(trans_not_pred(P1,Env,NotP1)),
273		trans_not_pred(P2,Env,NotP2),
274		trans_not_pred(P3,Env,NotP3),
275		clingo_format_comment('% if-then-else-predicate (negative)~n',[]),
276		gen_clingo_pred_clause(not_if_predicate,Prop,[],Env, (ecall(PosP1,Env) , ecall(NotP2,Env)) ),
277		gen_clingo_pred_clause(not_if_predicate,Prop,[],Env, (ecall(NotP1,Env) , ecall(NotP3,Env)) ).
278		trans_not_pred(partition(Set,ListOfSets),Env,Prop) :-
279		maplist(trans_set_4map(Env),ListOfSets,TransSets),
280		trans_not_pred(set_equal(Set,clingo_union(TransSets)),Env,P1), % Set = union(ListOfSets)
281		% TODO: use proper B predicate instead of clingo_union for find_identifier_uses and local_id filtering
282		clingo_format_comment('% partition predicate (negative)~n',[]),
283		gen_clingo_pred_clause(not_partition,Prop,[],Env, P1 ),
284		(append(_,[T1|T],TransSets),
285		member(T2,T), % choose T1, T2 amongst list of translated sets
286		gen_clingo_clause(not_partition,Prop,[],Env,
287		(ecall(T1,[X],Env), ecall(T2,[X],Env)) ), % succeed if common element, i.e., not disjoint
288		fail ; true).
289		trans_not_pred(Pred,Env,Prop) :-
290		negate_pred(Pred,NotPred),!,
291		non_positive_context(trans_not_pred(NotPred,Env,NegProp)), % translate negation and create auxiliary proposition for it
292		clingo_format_comment('% negation~n',[]),
293		gen_clingo_pred_clause(negated,Prop,[],Env, not(ecall(NegProp,Env)) ). % negate the proposition
294		trans_not_pred(X,Env,Prop) :-
295		add_b2asp_error('Unsupported predicate: ',X),
296		functor(X,F,A), format(user_error,'Functor = ~w/~w~n',[F,A]),
297		trans_not_pred(truth,Env,Prop).
298
299
300		% variation of version in bsyntaxtree, also ok with special clingo subgoals
301		conjunction_to_list(conjunct(A,B)) --> !, conjunction_to_list(A),conjunction_to_list(B).
302		conjunction_to_list(b(conjunct(A,B),pred,_)) --> !, conjunction_to_list(A),conjunction_to_list(B).
303		conjunction_to_list(X) --> [X].
304
305		% Tracking the context of a predicate: a predicate is in a positive context if it must be true
306		% for the overall formula to be true (e.g., a conjunct or a disjunct of the formula);
307		% inside negations, equivalences, the left-hand side of implications and IF conditions it is not.
308		% non_positive_context(Goal) translates Goal in a negative or mixed context.
309		:- meta_predicate non_positive_context(0).
310		non_positive_context(Goal) :-
311		get_non_positive_depth(Depth), D1 is Depth+1,
312		bb_put(b2asp_non_positive_depth,D1),
313		call_cleanup(once(Goal), bb_put(b2asp_non_positive_depth,Depth)).
314
315		in_non_positive_context :- get_non_positive_depth(Depth), Depth>0.
316
317		get_non_positive_depth(Depth) :- (bb_get(b2asp_non_positive_depth,D) -> Depth=D ; Depth=0).
318
319		l_trans_not_pred([],_,[]).
320		l_trans_not_pred([P1|TP],Env,[Prop1|TProps]) :-
321		trans_not_pred(P1,Env,Prop1),
322		l_trans_not_pred(TP,Env,TProps).
323
324		% create clingo predicates for local identifiers and generate code that sets up the local ids
325		add_local_typed_ids([],_,Env,true,Env).
326		add_local_typed_ids([TID|T],BoundsInfo,OldEnv, ( Constraint, TSetupCode) ,OutEnv) :-
327		get_texpr_id(TID,ID),
328		!,
329		get_texpr_type(TID,BaseType),
330		%gen_clingo_scalar_identifier(ID,BaseType,OldEnv,ClingoPred),
331		(select(bound_id_info(ID,_,InferredBaseType),BoundsInfo,BI2)
332		-> true %, write(user_output,b(ID,BoundsInfo)), nl(user_output), nl(user_output)
333		; BI2= BoundsInfo, InferredBaseType = BaseType,
334		add_warning(b2asp,'No bounds info for : ',ID,TID)
335		),
336		make_finite(InferredBaseType,ID,FiniteBaseType), % make finite here; to avoid multiple warnings later
337		gen_base_type_constraint(FiniteBaseType,FRESHVAR,Constraint),
338		add_new_local_id(ID,BaseType,FiniteBaseType,FRESHVAR,OldEnv,IntEnv),
339		add_local_typed_ids(T,BI2,IntEnv,TSetupCode, OutEnv).
340
341
342		% translate A : TB membership predicate
343		trans_not_member_pred(A,TB,Env,Prop) :- (TB=b(B,_,_) -> true ; TB=B),
344		specific_trans_not_member_pred(B,A,Env,Prop),!. % specific rule can be applied
345		trans_not_member_pred(A,B,Env,Prop) :- % generic translation rule:
346		translate_scalar(A,Env,X1,CallA),
347		trans_set(B,Env,P2),
348		clingo_format_comment('% member generic (negative)~n',[]),
349		gen_clingo_pred_clause(not_member,Prop,[],Env,
350		(CallA, not(ecall(P2,[X1],Env)) )). % :- P1(X), not P2(X). (same as subset)
351
352
353		% special translation rules for member checks:
354		% specific_trans_not_member_pred(Set,Element,ClingoPred) if successful Element:Set can be translated to ClingoPred
355		specific_trans_not_member_pred(pow_subset(B),A,Env,Prop) :- !,
356		trans_not_pred(subset(A,B),Env,Prop). % A:POW(B) <=> A <: B
357		specific_trans_not_member_pred(pow1_subset(B),A,Env,Prop) :- !,
358		precompile_set(A,Env,TA), % to avoid translating A twice
359		empty_set_texpr(TA,EmptyTA),
360		trans_not_pred(conjunct(subset(TA,B),not_set_equal(TA,EmptyTA)),Env,Prop). % A:POW1(B) <=> A <: B & A /= {}
361		specific_trans_not_member_pred(relations(Dom,Ran),A,Env,Prop) :- !,
362		create_cartesian_product(Dom,Ran,CartDomRan),
363		trans_not_pred(subset(A,CartDomRan),Env,Prop). % A: Dom <-> Ran <=> A <: (Dom*Ran)
364		specific_trans_not_member_pred(partial_function(Dom,Ran),A,Env,Prop) :- !,
365		% A : Dom +-> Ran <=> A <: (Dom*Ran) & A: TypeDom +-> TypeRan
366		precompile_set(A,Env,TA), % to avoid translating A twice
367		create_cartesian_product(Dom,Ran,CartDomRan),
368		TConj = conjunction_list([subset(TA,CartDomRan),is_partial_function(TA)]),
369		trans_not_pred(TConj,Env,Prop).
370		specific_trans_not_member_pred(partial_injection(Dom,Ran),A,Env,Prop) :- !,
371		% A : Dom >+> Ran <=> A <: (Dom*Ran) & A: TypeDom +-> TypeRan & A~:TypeRan +-> TypeDom
372		precompile_set(A,Env,TA),
373		create_cartesian_product(Dom,Ran,CartDomRan),
374		TConj = conjunction_list([subset(TA,CartDomRan),is_partial_function(TA),
375		is_injective(TA)]),
376		trans_not_pred(TConj,Env,Prop).
377		specific_trans_not_member_pred(total_relation(Dom,Ran),A,Env,Prop) :- !,
378		% A : Dom <<-> Ran <=> A <: (Dom*Ran) & Dom <: domain(A)
379		precompile_set(A,Env,TA),
380		domain_texpr(TA,DomTA),
381		create_cartesian_product(Dom,Ran,CartDomRan),
382		TConj = conjunction_list([subset(TA,CartDomRan),subset(Dom,DomTA)]),
383		trans_not_pred(TConj,Env,Prop).
384		specific_trans_not_member_pred(total_function(Dom,Ran),A,Env,Prop) :- !,
385		% A : Dom --> Ran <=> A <: (Dom*Ran) & A: TypeDom +-> TypeRan & Dom <: domain(A)
386		precompile_set(A,Env,TA),
387		domain_texpr(TA,DomTA),
388		create_cartesian_product(Dom,Ran,CartDomRan),
389		TConj = conjunction_list([subset(TA,CartDomRan),is_partial_function(TA),
390		subset(Dom,DomTA)]),
391		trans_not_pred(TConj,Env,Prop).
392		specific_trans_not_member_pred(total_injection(Dom,Ran),A,Env,Prop) :- !,
393		% A : Dom >-> Ran <=> A <: (Dom*Ran) & A: TypeDom +-> TypeRan & Dom <: domain(A) & A~:TypeRan +-> TypeDom
394		precompile_set(A,Env,TA),
395		domain_texpr(TA,DomTA),
396		create_cartesian_product(Dom,Ran,CartDomRan),
397		TConj = conjunction_list([subset(TA,CartDomRan),is_partial_function(TA),
398		is_injective(TA),subset(Dom,DomTA)]),
399		trans_not_pred(TConj,Env,Prop).
400		specific_trans_not_member_pred(surjection_relation(Dom,Ran),A,Env,Prop) :- !,
401		% A : Dom <->> Ran <=> A <: (Dom*Ran) & Ran <: range(A)
402		precompile_set(A,Env,TA),
403		range_texpr(TA,RanTA),
404		create_cartesian_product(Dom,Ran,CartDomRan),
405		TConj = conjunction_list([subset(TA,CartDomRan),subset(Ran,RanTA)]),
406		trans_not_pred(TConj,Env,Prop).
407		specific_trans_not_member_pred(partial_surjection(Dom,Ran),A,Env,Prop) :- !,
408		% A : Dom +->> Ran <=> A <: (Dom*Ran) & A: TypeDom +-> TypeRan & Ran <: range(A)
409		precompile_set(A,Env,TA),
410		range_texpr(TA,RanTA),
411		create_cartesian_product(Dom,Ran,CartDomRan),
412		TConj = conjunction_list([subset(TA,CartDomRan),is_partial_function(TA),
413		subset(Ran,RanTA)]),
414		trans_not_pred(TConj,Env,Prop).
415		specific_trans_not_member_pred(total_surjection_relation(Dom,Ran),A,Env,Prop) :- !,
416		% A : Dom <-->> Ran <=> A <: (Dom*Ran) & Dom <: domain(A) & Ran <: range(A)
417		precompile_set(A,Env,TA),
418		domain_texpr(TA,DomTA), range_texpr(TA,RanTA),
419		create_cartesian_product(Dom,Ran,CartDomRan),
420		TConj = conjunction_list([subset(TA,CartDomRan),
421		subset(Dom,DomTA),subset(Ran,RanTA)]),
422		trans_not_pred(TConj,Env,Prop).
423		specific_trans_not_member_pred(total_surjection(Dom,Ran),A,Env,Prop) :- !,
424		% A : Dom -->> Ran <=> A <: (Dom*Ran) & A: TypeDom +-> TypeRan & Dom <: domain(A) & Ran <: range(A)
425		precompile_set(A,Env,TA),
426		domain_texpr(TA,DomTA), range_texpr(TA,RanTA),
427		create_cartesian_product(Dom,Ran,CartDomRan),
428		TConj = conjunction_list([subset(TA,CartDomRan),is_partial_function(TA),
429		subset(Dom,DomTA),subset(Ran,RanTA)]),
430		trans_not_pred(TConj,Env,Prop).
431		specific_trans_not_member_pred(partial_bijection(Dom,Ran),A,Env,Prop) :- !,
432		% A : Dom >+>> Ran <=> A : Dom +->> Ran & injective(A)
433		precompile_set(A,Env,TA),
434		range_texpr(TA,RanTA),
435		create_cartesian_product(Dom,Ran,CartDomRan),
436		TConj = conjunction_list([subset(TA,CartDomRan),is_partial_function(TA),
437		is_injective(TA),subset(Ran,RanTA)]),
438		trans_not_pred(TConj,Env,Prop).
439		specific_trans_not_member_pred(total_bijection(Dom,Ran),A,Env,Prop) :- !,
440		% A : Dom >->> Ran <=> A : Dom -->> Ran & injective(A)
441		precompile_set(A,Env,TA),
442		domain_texpr(TA,DomTA), range_texpr(TA,RanTA),
443		create_cartesian_product(Dom,Ran,CartDomRan),
444		TConj = conjunction_list([subset(TA,CartDomRan),is_partial_function(TA),
445		is_injective(TA),subset(Dom,DomTA),subset(Ran,RanTA)]),
446		trans_not_pred(TConj,Env,Prop).
447		specific_trans_not_member_pred(seq(Ran),A,Env,Prop) :- !,
448		% A : seq(Ran) <=> ran(A) <: Ran & A: INTEGER +-> TypeRan & domain(A) = 1..N (for some N = size(A))
449		precompile_set(A,Env,TA),
450		domain_texpr(TA,DomTA), range_texpr(TA,RanTA),
451		TConj = conjunction_list([is_sequence_domain(DomTA),is_partial_function(TA),
452		subset(RanTA,Ran)]),
453		trans_not_pred(TConj,Env,Prop).
454		specific_trans_not_member_pred(iseq(Ran),A,Env,Prop) :- !,
455		% A : iseq(Ran) <=> A: seq(Ran) & injective(A)
456		precompile_set(A,Env,TA),
457		domain_texpr(TA,DomTA), range_texpr(TA,RanTA),
458		TConj = conjunction_list([is_sequence_domain(DomTA),is_partial_function(TA),
459		is_injective(TA),subset(RanTA,Ran)]),
460		trans_not_pred(TConj,Env,Prop).
461		specific_trans_not_member_pred(seq1(Ran),A,Env,Prop) :- !,
462		% A : seq1(Ran) <=> A: seq(Ran) & A /= {}
463		precompile_set(A,Env,TA),
464		domain_texpr(TA,DomTA), range_texpr(TA,RanTA), empty_set_texpr(TA,EmptyTA),
465		TConj = conjunction_list([is_sequence_domain(DomTA),is_partial_function(TA),
466		not_set_equal(TA,EmptyTA),subset(RanTA,Ran)]),
467		trans_not_pred(TConj,Env,Prop).
468		specific_trans_not_member_pred(iseq1(Ran),A,Env,Prop) :- !,
469		% A : iseq1(Ran) <=> A: iseq(Ran) & A /= {}
470		precompile_set(A,Env,TA),
471		domain_texpr(TA,DomTA), range_texpr(TA,RanTA), empty_set_texpr(TA,EmptyTA),
472		TConj = conjunction_list([is_sequence_domain(DomTA),is_partial_function(TA),
473		not_set_equal(TA,EmptyTA),is_injective(TA),
474		subset(RanTA,Ran)]),
475		trans_not_pred(TConj,Env,Prop).
476		specific_trans_not_member_pred(perm(Ran),A,Env,Prop) :- !,
477		% A : perm(Ran) <=> A: iseq(Ran) & Ran <: range(A)
478		precompile_set(A,Env,TA),
479		domain_texpr(TA,DomTA), range_texpr(TA,RanTA),
480		precompile_set(RanTA,Env,RTA),
481		TConj = conjunction_list([is_sequence_domain(DomTA),is_partial_function(TA),
482		is_injective(TA),subset(Ran,RTA),subset(RTA,Ran)]),
483		trans_not_pred(TConj,Env,Prop).
484
485
486		% typed expressions for the domain and range of a (pre-compiled) relation TA and for an empty set of its type;
487		% the B AST nodes we create must be typed, e.g., for find_identifier_uses in register_clingo_predicate
488		domain_texpr(TA,b(domain(TA),set(DomType),[])) :- relation_type(TA,DomType,_).
489		range_texpr(TA,b(range(TA),set(RanType),[])) :- relation_type(TA,_,RanType).
490		empty_set_texpr(TA,b(empty_set,Type,[])) :- get_texpr_type(TA,Type).
491		relation_type(TA,DomType,RanType) :-
492		(get_texpr_type(TA,set(couple(D,R))) -> DomType=D, RanType=R
493		; add_b2asp_error('Expected relation type: ',TA), DomType=any, RanType=any).
494
495		negate_pred(negation(Pred),Pred).
496		negate_pred(not_set_equal(A,B),set_equal(A,B)).
497		negate_pred(not_subset(A,B),subset(A,B)).
498		negate_pred(not_subset_strict(A,B),subset_strict(A,B)).
499		negate_pred(not_member(A,B),member(A,B)).
500
501
502		% arithmetic comparison binary operators along with a translation in Clingo
503		scalar_binary_pred(less(A,B),A,B,'<').
504		scalar_binary_pred(greater(A,B),A,B,'>').
505		scalar_binary_pred(less_equal(A,B),A,B,'<='). % note this is different from Prolog =< comparison syntax
506		scalar_binary_pred(greater_equal(A,B),A,B,'>=').
507		% can also apply to scalars other than integers:
508		%scalar_binary_pred(equal(A,B),A,B,'='). % use code in trans_not_pred to handle set equality!
509		%scalar_binary_pred(not_equal(A,B),A,B,'!='). % ditto
510
511		% arithmetic comparison binary operators along with a translation of the negation to Clingo
512		negate_scalar_binary_pred(less(A,B),A,B,'>=').
513		negate_scalar_binary_pred(greater(A,B),A,B,'<='). % note this is different from Prolog =< comparison syntax
514		negate_scalar_binary_pred(less_equal(A,B),A,B,'>').
515		negate_scalar_binary_pred(greater_equal(A,B),A,B,'<').
516		% can also apply to scalars other than integers:
517		negate_scalar_binary_pred(equal(A,B),A,B,'!=').
518		negate_scalar_binary_pred(not_equal(A,B),A,B,'=').
519
520		% binary predicate operators that can be translated into a single constraint
521		bin_op_pred_single_call(equal(A,B),A,B,'='). % equality for scalar
522		bin_op_pred_single_call(not_equal(A,B),A,B,'!=').
523
524		% ------------------------------
525		% translating SET EXPRESSIONS
526		% ------------------------------
527
528		:- use_module(probsrc(bsyntaxtree),[is_set_type/2]).
529
530		% translate a B set value to a Clingo predicate and wrap it into a special BAST constructor
531		% useful to avoid re-translating the same set multiple times, e.g., in partial_function, ...
532		precompile_set(BAST,Env,ResAST) :-
533		trans_set(BAST,Env,ClingoPred),
534		create_clingo_set_texpr(BAST,ClingoPred,ResAST).
535
536		% create a pre-compiled clingo_set node which does not need to be re-translated:
537		% we keep the original AST info, in case we need to find_identifier_uses:
538		create_clingo_set_texpr(BAST,ClingoPred,ResAST) :-
539		add_info(BAST,clingo_set(ClingoPred),ResAST).
540
541		add_info(b(P,T,I),Info,R) :- !, R=b(P,T,[Info|I]).
542		add_info(P,Info,b(P,pred,[Info])).
543
544		trans_set_4map(Env,BAST,ClingoPred) :- trans_set(BAST,Env,ClingoPred).
545
546		:- mode trans_set(+BAST,+LocalID_Env,-ClingoPred).
547		% translate a B set value (of scalars) to a Clingo predicate Pred(X).
548		% Pred(X) is true if X represents an element of the B set
549		trans_set(b(_Expr,_Type,Infos),_Env,Pred) :-
550		Infos = [clingo_set(P)|_],!, % already translated set
551		Pred=P.
552		trans_set(b(Expr,Type,_Infos),Env,Pred) :- % format(user_output,' set --> ~w~n',[Expr]),
553		(is_set_type(Type,BaseType)
554		-> ( Expr = identifier(ID) ->
555		NExpr=identifier(ID,Bounds),
556		find_bounds_info(ID,set(BaseType),Env,set(Bounds))
557		; Expr = comprehension_set(TIds,Body) -> NExpr = comprehension_set(TIds,BaseType,Body)
558		; NExpr = Expr)
559		; add_b2asp_error('Type of expression is not a set: ',Type), fail
560		),
561		!,
562		trans_set(NExpr,Env,Pred).
563		%trans_set(clingo_set(P),_Env,Pred) :- !, Pred=P. % already translated set
564		trans_set(empty_set,Env,Pred) :- !,
565		DummyArg = 0, % Clingo does not like unbound variables in head??
566		gen_clingo_clause(empty,Pred,[DummyArg],Env, 1=2 ).
567		trans_set(bool_set,Env,Pred) :- !,
568		trans_set(set_extension([pred_false,pred_true]),Env,Pred).
569		trans_set(value(V),Env,Pred) :- V==[], !, trans_set(empty_set,Env,Pred).
570		trans_set(value(AVL),Env,Pred) :-
571		custom_explicit_sets:expand_custom_set_to_list_now(AVL,L),!, % this creates Value list not set_extension list ! TODO
572		trans_set(set_extension(L),Env,Pred).
573		trans_set(sequence_extension(L),Env,Pred) :- !,
574		add_indices(L,1,Set),
575		trans_set(set_extension(Set),Env,Pred).
576		trans_set(set_extension(L),Env,Pred) :- !,
577		gensym_if_necessary(set_ext,Pred),
578		maplist(trans_scalar4map(Env,Pred),L).
579		trans_set(union(A,B),Env,Pred) :- !,
580		BP = b(union(A,B),any,[]),
581		register_clingo_predicate(union,BP,Pred,Env,Env2),
582		trans_set(A,Env2,P1),
583		trans_set(B,Env2,P2),
584		clingo_format_comment_with_expr('% union of sets ~w~n',[BP]),
585		gen_clingo_clause(union,Pred,[X],Env2, (ecall(P1,[X],Env2)) ),
586		gen_clingo_clause(union,Pred,[X],Env2, (ecall(P2,[X],Env2)) ).
587		trans_set(clingo_union([P1|T]),Env,Pred) :- !, % a union of a list of already translated sets; used for partition
588		clingo_format_comment('% union of clingo sets~n',[]),
589		gen_clingo_pred_clause(unions,Pred,[X],Env, (ecall(P1,[X],Env)) ),
590		(member(P2,T),
591		gen_clingo_clause(unions,Pred,[X],Env, (ecall(P2,[X],Env)) ),
592		fail ; true).
593		trans_set(intersection(A,B),Env,Pred) :- !,
594		BP = b(intersection(A,B),any,[]),
595		register_clingo_predicate(inter,BP,Pred,Env,Env2),
596		trans_set(A,Env2,P1),
597		trans_set(B,Env2,P2),
598		clingo_format_comment_with_expr('% intersection of sets ~w~n',[BP]),
599		gen_clingo_clause(inter,Pred,[X],Env2, (ecall(P1,[X],Env2),ecall(P2,[X],Env2)) ).
600		trans_set(set_subtraction(A,B),Env,Pred) :- !, % difference set in B
601		BP = b(set_subtraction(A,B),any,[]),
602		register_clingo_predicate(diff,BP,Pred,Env,Env2),
603		trans_set(A,Env2,P1),
604		trans_set(B,Env2,P2),
605		clingo_format_comment_with_expr('% difference of sets ~w~n',[BP]),
606		gen_clingo_clause(diff,Pred,[X],Env2,
607		(ecall(P1,[X],Env2),not(ecall(P2,[X],Env2))) ). % Pred(X) :- P1(X), not P2(X).
608		trans_set(cartesian_product(A,B),Env,Pred) :- !,
609		BP = b(cartesian_product(A,B),any,[]),
610		register_clingo_predicate(cart,BP,Pred,Env,Env2),
611		trans_set(A,Env2,P1),
612		trans_set(B,Env2,P2),
613		clingo_format_comment_with_expr('% Cartesian product ~w~n',[BP]),
614		gen_clingo_clause(cart,Pred,[(X,Y)],Env2, (ecall(P1,[X],Env2),ecall(P2,[Y],Env2)) ). % Pred((X,Y)) :- P1(X), P2(Y).
615		trans_set(domain(A),Env,Pred) :- !,
616		register_clingo_predicate(domain,A,Pred,Env,Env2),
617		trans_set(A,Env2,P1),
618		clingo_format_comment_with_expr('% domain of relation ~w~n',A),
619		gen_clingo_clause(domain,Pred,[X],Env2, ecall(P1,[(X,_)],Env2) ). % Pred(X) :- P1((X,_)).
620		trans_set(range(A),Env,Pred) :- !,
621		register_clingo_predicate(range,A,Pred,Env,Env2),
622		trans_set(A,Env2,P1),
623		clingo_format_comment_with_expr('% range of relation ~w~n',A),
624		gen_clingo_clause(range,Pred,[X],Env2, ecall(P1,[(_,X)],Env2) ). % Pred(X) :- P1((_,X)).
625		trans_set(image(Rel,Set),Env,Pred) :- !, % relational image B operator
626		BP = b(image(Rel,Set),any,[]),
627		register_clingo_predicate(image,BP,Pred,Env,Env2),
628		trans_set(Rel,Env2,P1),
629		trans_set(Set,Env2,P2),
630		clingo_format_comment_with_expr('% relational image ~w~n',BP),
631		gen_clingo_clause(image,Pred,[Y],Env2,
632		(ecall(P2,[X],Env2),ecall(P1,[(X,Y)],Env2)) ). % Pred(Y) :- P1(X), P2((X,Y)).
633		trans_set(domain_restriction(Set,Rel),Env,Pred) :- !, % domain restriction B operator Set <| Rel
634		BP = b(domain_restriction(Set,Rel),any,[]),
635		register_clingo_predicate(dres,BP,Pred,Env,Env2),
636		trans_set(Set,Env2,P1),
637		trans_set(Rel,Env2,P2),
638		clingo_format_comment_with_expr('% domain restriction of relation ~w~n',[BP]),
639		gen_clingo_clause(dres,Pred,[(X,Y)],Env2,
640		(ecall(P1,[X],Env2),ecall(P2,[(X,Y)],Env2)) ). % Pred((X,Y)) :- P1(X), P2((X,Y)).
641		trans_set(domain_subtraction(Set,Rel),Env,Pred) :- !, % domain subtraction B operator Set <<| Rel
642		BP = b(domain_subtraction(Set,Rel),any,[]),
643		register_clingo_predicate(dsub,BP,Pred,Env,Env2),
644		trans_set(Set,Env2,P1),
645		trans_set(Rel,Env2,P2),
646		clingo_format_comment_with_expr('% domain subtraction of relation ~w~n',[BP]),
647		gen_clingo_clause(dsub,Pred,[(X,Y)],Env2,
648		(ecall(P2,[(X,Y)],Env2),not(ecall(P1,[X],Env2))) ). % Pred((X,Y)) :- P2((X,Y)), not P(X).
649		trans_set(range_restriction(Rel,Set),Env,Pred) :- !, % range restriction B operator Rel |> Set
650		BP = b(range_restriction(Rel,Set),any,[]),
651		register_clingo_predicate(rres,BP,Pred,Env,Env2),
652		trans_set(Set,Env2,P1),
653		trans_set(Rel,Env2,P2),
654		clingo_format_comment_with_expr('% range restriction of relation ~w~n',[BP]),
655		gen_clingo_clause(rres,Pred,[(X,Y)],Env2,
656		(ecall(P1,[Y],Env2),ecall(P2,[(X,Y)],Env2)) ). % Pred((X,Y)) :- P1(Y), P2((X,Y)).
657		trans_set(range_subtraction(Rel,Set),Env,Pred) :- !, % range subtraction B operator Rel |>> Set
658		BP = b(range_subtraction(Rel,Set),any,[]),
659		register_clingo_predicate(rsub,BP,Pred,Env,Env2),
660		trans_set(Set,Env2,P1),
661		trans_set(Rel,Env2,P2),
662		clingo_format_comment_with_expr('% range subtraction of relation ~w~n',[BP]),
663		gen_clingo_clause(rsub,Pred,[(X,Y)],Env2,
664		(ecall(P2,[(X,Y)],Env2), not(ecall(P1,[Y],Env2))) ). % Pred((X,Y)) :- P2((X,Y)), not P1(Y).
665		trans_set(composition(A,B),Env,Pred) :- !, % relational composition operator
666		BP = b(composition(A,B),any,[]),
667		register_clingo_predicate(comp,BP,Pred,Env,Env2),
668		trans_set(A,Env2,P1),
669		trans_set(B,Env2,P2),
670		clingo_format_comment_with_expr('% relational composition ~w~n',[BP]),
671		gen_clingo_clause(comp,Pred,[(X,Z)],Env2,
672		(ecall(P1,[(X,Y)],Env2),ecall(P2,[(Y,Z)],Env2)) ). % Pred((X,Z)) :- P1((X,Y)), P2((Y,Z)).
673		trans_set(closure(A),Env,Pred) :- !, % closure1 transitive operator
674		register_clingo_predicate(closure1,A,Pred,Env,Env2),
675		trans_set(A,Env2,P1),
676		clingo_format_comment_with_expr('% transitive closure1 of relation ~w~n',[A]),
677		gen_clingo_clause(closure1,Pred,[(X,Y)],Env2, ecall(P1,[(X,Y)],Env2) ), % Pred((X,Y)) :- P1((X,Y)).
678		gen_clingo_clause(closure1,Pred,[(X,Z)],Env2,
679		( ecall(P1,[(X,Y)],Env2) , ecall(Pred,[(Y,Z)],Env2)) ). % Pred((X,Z)) :- P1((X,Y)), Pred((Y,Z)).
680		trans_set(iteration(A,B),Env,Pred) :- !, % iterate(Rel,Nr) operator
681		BP = b(iteration(A,B),any,[]),
682		register_clingo_predicate(iterate_rec,BP,RecP,Env,Env2),
683		trans_set(A,Env2,P1),
684		trans_scalar(B,Env2,P2),
685		clingo_format_comment_with_expr('% iterate over relation ~w~n',[BP]),
686		gen_clingo_clause(iterate_rec,RecP,[(X,Y),1],Env2, ecall(P1,[(X,Y)],Env2) ), % RecP((X,Y),1) :- P1((X,Y)).
687		gen_clingo_clause(iterate_rec,RecP,[(X,X),0],Env2, ( ecall(P1,[(X,_)],Env2) ) ), % reflexive closure, using domain elements
688		gen_clingo_clause(iterate_rec,RecP,[(X,X),0],Env2, ( ecall(P1,[(_,X)],Env2) ) ), % + range elements (not B-Book semantics)
689		gen_clingo_clause(iterate_rec,RecP,[(X,Z),Nr],Env2,
690		( Nr>1, ecall(P2,[Lim],Env2), '<='(Nr,Lim), N1 = Nr-1, ecall(P1,[(X,Y)],Env2) , ecall(RecP,[(Y,Z),N1],Env2)) ),
691		% RecP((X,Z),Nr) :-Nr>1, N1 is N-1, P1((X,Y)), RecP((Y,Z),N1).
692		register_clingo_predicate(iterate,BP,Pred,Env,Env3),
693		gen_clingo_pred_clause(iterate,Pred,[X],Env3, (ecall(P2,[Nr],Env3), ecall(RecP,[X,Nr],Env3)) ). % Pred(X) :- RecP(X,Nr).
694		trans_set(overwrite(A,B),Env,Pred) :- !, % relational override operator
695		BP = b(overwrite(A,B),any,[]),
696		register_clingo_predicate(overwr,BP,Pred,Env,Env2),
697		trans_set(A,Env2,P1),
698		trans_set(B,Env2,P2),
699		trans_set(domain(B),Env2,P3), % we need to create a separate domain encoding to be able to use it inside the "not" below
700		clingo_format_comment_with_expr('% relational override ~w~n',[BP]),
701		gen_clingo_clause(overwr,Pred,[(X,Y)],Env2, ecall(P2,[(X,Y)],Env2) ), % Pred((X,Y)) :- P2((X,Y)).
702		gen_clingo_clause(overwr,Pred,[(X,Y)],Env2,
703		(ecall(P1,[(X,Y)],Env2),not(ecall(P3,[X],Env2))) ). % Pred((X,Y)) :- P1((X,Y)), not P3(X).
704		trans_set(identity(A),Env,Pred) :- !, % identity operator
705		register_clingo_predicate(id,A,Pred,Env,Env2),
706		trans_set(A,Env2,P1),
707		clingo_format_comment_with_expr('% identity relation ~w~n',[A]),
708		gen_clingo_clause(id,Pred,[(X,X)],Env2, ecall(P1,[X],Env2) ). % Pred((X,X)) :- P1(X).
709		trans_set(reverse(A),Env,Pred) :- !, % reverse B operator r~
710		register_clingo_predicate(rev,A,Pred,Env,Env2),
711		trans_set(A,Env2,P1),
712		clingo_format_comment_with_expr('% relational inverse ~w~n',[A]),
713		gen_clingo_clause(rev,Pred,[(Y,X)],Env2, (ecall(P1,[(X,Y)],Env2))). % Pred((Y,X)) :- P1((X,Y)).
714		trans_set(interval(A,B),Env,Pred) :- !,
715		translate_scalar(A,Env,X1,C1),
716		translate_scalar(B,Env,X2,C2),
717		trans_debug(b(interval(A,B),set(integer),[]),BPS),clingo_format_comment('% interval ~w~n',[BPS]),
718		gen_clingo_pred_clause(interval,Pred,[X],Env, (C1,C2,'='(X,'..'(X1,X2))) ).
719		trans_set(if_then_else(Test,Then,Else),Env,Pred) :- !,
720		non_positive_context(trans_pos_pred(Test,Env,TestProp)),
721		trans_set(Then,Env,PX), trans_set(Else,Env,PY),
722		clingo_format_comment('% IF-THEN-ELSE (for sets)~n',[]),
723		gen_clingo_pred_clause(ifte,Pred,[X],Env, (ecall(TestProp,[],Env), ecall(PX,[X],Env) ) ),
724		gen_clingo_clause(ifte, Pred,[Y],Env, (ecall(PY,[Y],Env), not(ecall(TestProp,[],Env)) ) ).
725		trans_set(global(ID),Env,Pred) :- % B value for entire global enumerated/deferred set ID
726		b_get_fd_type_bounds(ID,Low,Up),!,
727		trans_set(interval(Low,Up),Env,Pred).
728		trans_set(identifier(ID,global(ID)),Env,Pred) :- % TODO: proper checking of scoping
729		b_get_fd_type_bounds(ID,Low,Up),!,
730		trans_set(interval(Low,Up),Env,Pred).
731		trans_set(identifier(ID,_BaseType1),Env,Pred) :- clingo_local_id(ID,Env,_BaseType2,_Var), !,
732		add_b2asp_warning('Local identifier used as set (probably not supported):',ID),
733		Pred = fail.
734		trans_set(identifier(ID,BaseType),_Env,Pred) :- !,
735		gen_clingo_set_identifier(ID,BaseType,Pred,top_level).
736		trans_set(comprehension_set(TIds,BaseType,Body),Env,Pred) :- !,
737		check_empty_env(Env,TIds,Body),
738		infer_bounds_within_env(TIds,Body,Env,BoundsInfo),
739		format(user_output,'~n Comprehension set (~w) bounds: ~w~n',[BaseType,BoundsInfo]),
740		findall(RestrictedType,member(bound_id_info(_,_,RestrictedType),BoundsInfo),ArgTypes),
741		couplise_list(ArgTypes,RestrictedBaseType),
742		gensym_if_necessary(comprehension_set,CompID),
743		gen_clingo_set_identifier(CompID,RestrictedBaseType,Pred,comprehension_set), % create a new id to represent the set
744		create_couple(TIds,Couple),
745		create_clingo_set_texpr(Body,Pred,ClingoSet),
746		trans_not_pred(conjunct( % state that the set contains exactly the solutions to Body
747		forall_with_precomputed_bounds(TIds,BoundsInfo,member(Couple,ClingoSet), Body),
748		forall_with_precomputed_bounds(TIds,BoundsInfo,Body, member(Couple,ClingoSet))), Env, ICProp),
749		gen_clingo_ic_constraint( ICProp ).
750
751		trans_set(X,_Env,Pred) :- %write(user_error,X),nl(user_error),
752		add_b2asp_error('Unsupported set: ',X),Pred=fail.
753
754
755		check_empty_env(env([],_),_,_) :- !.
756		check_empty_env(_,Term,Span) :- add_b2asp_error('Unsupported nesting: ',Term,Span),fail.
757
758
759		% add indices to sequence extension list:
760		add_indices([],_,[]).
761		add_indices([H|T],Nr,[couple(integer(Nr),H)|CT]) :- N1 is Nr+1,
762		add_indices(T,N1,CT).
763
764
765		% translate both sides of a comparison; only one side can be inlined as a set aggregate,
766		% as clingo does not allow comparing two aggregates, e.g., #count{..} = #count{..}
767		translate_top_level_scalars(A,B,Env,X1,CallA,X2,CallB) :-
768		valid_top_level_literal(A,Env,ClingoCst),!,
769		X1=ClingoCst, CallA=true,
770		translate_scalar(B,Env,X2,CallB).
771		translate_top_level_scalars(A,B,Env,X1,CallA,X2,CallB) :-
772		translate_scalar(A,Env,X1,CallA),
773		translate_top_level_scalar(B,Env,X2,CallB).
774
775		translate_top_level_scalar(Lit,Env,ClingoValue,ClingoCall) :-
776		valid_top_level_literal(Lit,Env,ClingoCst),!,
777		% set aggregates can only be used as literals at the top-level; #max(...) + #max(..) is not allowed
778		ClingoValue=ClingoCst, ClingoCall=true.
779		translate_top_level_scalar(Lit,Env,ClingoValue,ClingoCall) :- translate_scalar(Lit,Env,ClingoValue,ClingoCall).
780
781		:- mode translate_scalar(+BAST,+LocalID_Env,-ClingoValue,-ClingoPred).
782		% an optimised version of translate scalar
783		% may produce true as ClingoCall if value can be represented as Clingo Constant
784		% running ClingoCall in clingo will produce result in ClingoValue
785		translate_scalar(Lit,Env,ClingoValue,ClingoCall) :-
786		valid_literal_or_local_id(Lit,Env,ClingoCst),!,
787		ClingoValue=ClingoCst, ClingoCall=true.
788		translate_scalar(BOP,Env,ClingoExpr,C12) :- bin_op(BOP,A,B,OP), !,
789		translate_scalar(A,Env,X1,C1),
790		translate_scalar(B,Env,X2,C2),
791		conjoin_clingo_calls(C1,C2,C12),
792		ClingoExpr =.. [OP,X1,X2].
793		translate_scalar(Lit,Env,ClingoValue,ClingoCall) :-
794		trans_scalar(Lit,Env,Pred),
795		ClingoCall = ecall(Pred,[ClingoValue],Env).
796		% TODO: for identifiers we should also pass an environment storing which Clingo Predicate is mapped to which identifier
797		% ditto for set translation
798
799
800		scalar_type(real). % not supported
801		scalar_type(string).
802		scalar_type(boolean).
803		scalar_type(integer).
804		scalar_type(global(_)).
805		scalar_type(couple(A,B)) :- scalar_type(A), scalar_type(B).
806
807
808		% ------------------------------
809		% translating SCALAR EXPRESSIONS
810
811		% special version for maplist:
812		trans_scalar4map(Env,Pred,El) :- trans_scalar(El,Env,Pred).
813
814
815		:- mode trans_scalar(+BAST,+LocalID_Env,-ClingoPred).
816		% translate a scalar B value V (integers, booleans, strings, ...) to a Clingo predicate Pred(X).
817		% Pred(X) is true if X corresponds to the B value V
818
819		trans_scalar(b(Expr,Type,_Infos),Env,Pred) :-
820		(scalar_type(Type)
821		-> (Expr = identifier(ID) -> NExpr=identifier(ID,Bounds),
822		find_bounds_info(ID,Type,Env,Bounds)
823		; NExpr = Expr)
824		; is_set_type(Type,_) -> add_b2asp_error('Set expression is not supported here, scalar expected: ',Type), fail
825		; add_b2asp_error('Type of expression is not a scalar: ',Type), fail
826		),
827		!,
828		trans_scalar(NExpr,Env,Pred).
829		trans_scalar(Lit,Env,Pred) :- valid_literal(Lit,Env,ClingoCst), !,
830		% cannot deal with local ID, as this result is a variable; we could create proj. function TODO
831		gen_clingo_fact(lit,Pred,[ClingoCst],Env).
832		trans_scalar(BOP,Env,Pred) :- bin_op(BOP,A,B,OP), !,
833		translate_scalar(A,Env,X1,C1),
834		translate_scalar(B,Env,X2,C2),
835		ClingoExpr =.. [OP,X1,X2],
836		clingo_format_comment('% scalar binary operator ~w~n',[OP]),
837		gen_clingo_pred_clause(bop,Pred,[X],Env, (C1,C2,'='(X,ClingoExpr)) ). % TODO: '=' and '==' both seem to work, :=/2 ??
838		trans_scalar(UnOP,Env,Pred) :- un_op(UnOP,A,OP), !,
839		translate_scalar(A,Env,X1,C1),
840		ClingoExpr =.. [OP,X1],
841		clingo_format_comment('% scalar unary operator ~w~n',[OP]),
842		gen_clingo_pred_clause(unop,Pred,[X],Env, (C1,'='(X,ClingoExpr)) ). % TODO: '=' and '==' both seem to work
843		trans_scalar(Aggr,Env,Pred) :- set_aggregate(Aggr,Set,ClingoAggr,Prefix),!,
844		trans_set(Set,Env,P1),
845		gen_clingo_count_aggregate(ClingoAggr,P1,Env,P1Aggregate),
846		clingo_format_comment('% set aggregate ~w~n',[ClingoAggr]),
847		gen_clingo_pred_clause(Prefix,Pred,[X],Env, '='(X,P1Aggregate) ). % Count = #count{Var : node(Var)} ,....
848		trans_scalar(first_of_pair(A),Env,Pred) :- !, % prj1 (same translation as domain)
849		translate_scalar(A,Env,Couple,C1), Couple = (X,_),
850		clingo_format_comment('% projection 1 of pair~n',[]),
851		gen_clingo_pred_clause(prj1,Pred,[X],Env, C1 ). % Pred(X) :- P1((X,_)).
852		trans_scalar(second_of_pair(A),Env,Pred) :- !, % prj2 (same translation as range)
853		translate_scalar(A,Env,Couple,C1), Couple = (_,X),
854		clingo_format_comment('% projection 2 of pair~n',[]),
855		gen_clingo_pred_clause(prj2,Pred,[X],Env, C1 ). % Pred(X) :- P1((_,X)).
856		trans_scalar(function(Rel,Arg),Env,Pred) :- !, % function application operator; same translation as image
857		trans_set(Rel,Env,P1),
858		translate_scalar(Arg,Env,X,C2),
859		clingo_format_comment('% function application~n',[]),
860		gen_clingo_pred_clause(apply,Pred,[Y],Env,
861		(C2, ecall(P1,[(X,Y)],Env)) ). % Pred(Y) :- P1(X), P2((X,Y)).
862		trans_scalar(if_then_else(Test,Then,Else),Env,Pred) :- !, % see also set version
863		non_positive_context(trans_pos_pred(Test,Env,TestProp)),
864		translate_scalar(Then,Env,X,CX), translate_scalar(Else,Env,Y,CY),
865		clingo_format_comment('% IF-THEN-ELSE~n',[]),
866		gen_clingo_pred_clause(ifte,Pred,[X],Env, ( ecall(TestProp,[],Env), CX ) ),
867		gen_clingo_clause(ifte,Pred,[Y],Env, ( CY, not(ecall(TestProp,[],Env)) ) ).
868		trans_scalar(string(String),Env,Pred) :- !,
869		get_string_nr(String,Nr),
870		trans_scalar(Nr,Env,Pred).
871		trans_scalar(fd(Nr,GS),Env,Pred) :- integer(Nr), % enumerated/deferred set element member as B value
872		b_get_fd_type_bounds(GS,Low,Up), Nr>=Low, Nr=<Up, !,
873		trans_scalar(Nr,Env,Pred).
874		trans_scalar(identifier(ID,_BaseType),Env,Pred) :- clingo_local_id(ID,Env, __BaseType,Var), !,
875		% generate a Clingo projection predicate that picks the Var from the Env
876		atom_concat(local_id_,ID,Prefix),
877		clingo_format_comment('% projection for local variable ~w~n',[ID]),
878		gen_clingo_pred_clause(Prefix,Pred,[X],Env, (X = Var) ).
879		trans_scalar(identifier(ID,global(GS)),Env,Pred) :- % TODO: proper checking of scoping and add case to translate_scalar
880		lookup_global_constant(ID,fd(Nr,GS)),!,
881		trans_scalar(Nr,Env,Pred).
882		trans_scalar(identifier(ID,BaseType),Env,Pred) :- !,
883		gen_clingo_scalar_identifier(ID,BaseType,Env,IdPred),
884		(var(Pred) -> Pred=IdPred
885		; clingo_format_comment('% scalar identifier ~w~n',[ID]), % mainly for set_extensions
886		gen_clingo_pred_clause(id_scalar,Pred,[X],Env, ecall(IdPred,[X],Env) )). % Pred(X) :- Id(X)
887		trans_scalar(X,_,P) :- %write(user_error,X),nl(user_error),
888		add_b2asp_error('Unsupported scalar: ',X), P=fail.
889
890		% B set aggregates which can be translated to Clingo aggregates:
891		set_aggregate(card(Set),Set,'#count',count).
892		set_aggregate(min(Set),Set,'#min',min).
893		set_aggregate(max(Set),Set,'#max',max).
894		set_aggregate(GeneralSum,Set,'#sum',sum) :- detect_set_summation(GeneralSum,Set).
895		% Clingo also supports avg
896
897		detect_set_summation(Expr,SET) :- % detect special pattern SIGMA(ID).(ID:SET|ID)
898		Expr = general_sum([TID1],b(member(TID2,SET),pred,_),TID3),
899		get_texpr_id(TID1,ID), get_texpr_id(TID2,ID), get_texpr_id(TID3,ID).
900
901
902		% binary operators and their Clingo Translation
903		bin_op(b(BOP,_,_),A,B,Op) :- bin_op(BOP,A,B,Op).
904		bin_op(A+B,A,B,+).
905		bin_op(add(A,B),A,B,+).
906		bin_op(A-B,A,B,-).
907		bin_op(minus(A,B),A,B,-).
908		bin_op(A*B,A,B,*).
909		bin_op(multiplication(A,B),A,B,*).
910		bin_op(power_of(A,B),A,B,'**').
911		bin_op(A/B,A,B,/).
912		bin_op(div(A,B),A,B,/).
913		% TODO: floored_div
914		bin_op(A mod B,A,B,\).
915		bin_op(modulo(A,B),A,B,\).
916		bin_op((A,B),A,B,',').
917		bin_op(couple(A,B),A,B,',').
918
919		% unary operators and their Clingo Translation
920		un_op(unary_minus(A),A,-).
921
922
923		:- mode valid_literal_or_local_id(+BAST,+LocalID_Environment,-ClingoLiteral).
924		valid_literal_or_local_id(TID,Env,Res) :- is_identifier(TID,ID),
925		clingo_local_id(ID,Env,_BaseType,Var),!,
926		Res = Var. % not really a literal, but local id
927		valid_literal_or_local_id(BAST,Env, ClingoLiteral) :- valid_literal(BAST, Env,ClingoLiteral).
928
929		is_identifier(identifier(ID),ID).
930		is_identifier(b(TID,_,_),ID) :- is_identifier(TID,ID).
931
932		:- mode valid_literal(+BAST,+Env,-ClingoLiteral).
933		% is true if the B AST directly represents a valid Clingo literal
934		valid_literal(b(Lit,_,_),Env,Res) :- !, valid_literal(Lit,Env,Res).
935		valid_literal(Lit,_,Nr) :- number(Lit),!,Nr=Lit.
936		valid_literal(identifier(ID),_,Nr) :- !,deterministic_id_value(ID,Nr).
937		valid_literal(fd(LitNr,_GS),_,Nr) :- !, Nr=LitNr.
938		valid_literal(pred_true,_,pred_true).
939		valid_literal(pred_false,_,pred_false).
940		valid_literal(boolean_true,_,pred_true). % AST node for TRUE
941		valid_literal(boolean_false,_,pred_false). % AST node for FALSE
942		valid_literal(string(S),_,Nr) :- !, get_string_nr(S,Nr).
943		valid_literal(integer(Lit),_,Nr) :- number(Lit),!,Nr=Lit.
944		valid_literal(int(Lit),_,Nr) :- number(Lit),!,Nr=Lit. % from B values rather than AST's
945		valid_literal(max_int,_,Nr) :- get_preference(maxint,Nr).
946		valid_literal(min_int,_,Nr) :- get_preference(minint,Nr).
947		valid_literal(value(V),Env,Nr) :- nonvar(V),!, valid_literal(V,Env,Nr).
948		valid_literal(BOP,Env,Nr) :- binary_arith_op(BOP,A,B,Op),
949		valid_literal(A,Env,LA), number(LA),
950		valid_literal(B,Env,LB), number(LB),
951		Call =.. [Op,LA,LB], Nr is Call.
952		valid_literal(div(A,B),Env,Nr) :- % TODO: also modulo; but be careful with negative nrs!
953		valid_literal(B,Env,LB), integer(LB), LB \= 0,
954		valid_literal(A,Env,LA), integer(LA),
955		Nr is LA//LB.
956		valid_literal(couple(A,B),Env,(LA,LB)) :- !,
957		valid_literal(A,Env,LA), valid_literal(B,Env,LB). % Clingo accepts pairs as literals
958		valid_literal((A,B),Env,(LA,LB)) :- !,
959		valid_literal(A,Env,LA), valid_literal(B,Env,LB). % the same for pair valuesvariable which has been set-up
960
961		% binary operator that can be pre-computed
962		binary_arith_op(add(A,B),A,B,+).
963		binary_arith_op(minus(A,B),A,B,-).
964		binary_arith_op(multiplication(A,B),A,B,*).
965		binary_arith_op(power_of(A,B),A,B,'^').
966
967
968		% clingo does not seem to allow to use set aggregates withing arithmetic operations
969		valid_top_level_literal(b(Lit,_,_),Env,Res) :- !, valid_top_level_literal(Lit,Env,Res).
970		valid_top_level_literal(Aggr,Env,Res) :- set_aggregate(Aggr,Set,ClingoAggr,_),
971		trans_set(Set,Env,P1),
972		gen_clingo_count_aggregate(ClingoAggr,P1,Env,Res). % treat aggregates as literals, to enable more efficient encoding by clingo, e.g., for things like #card(...) = 1
973		% TODO: reals, enumerated set elements, ...
974
975
976		% ------------------------------
977
978		% LOCAL Environment manipulation
979
980		% environment contains list of universally quantified local variables and bounds info for existential ones
981		create_new_local_id_env(env(LocalIds,ExistsBoundsInfo)) :- LocalIds = [], ExistsBoundsInfo=[].
982
983		clingo_local_id(ID,env(Env,_),BaseType,Var) :- member(local_id(ID,_,BaseType,Var),Env).
984		add_new_local_id(ID,Type,FiniteBaseType,Var,env(Env,LB),env(NewEnv,LB)) :-
985		%format(user_output,'Adding local id ~w to ~w~n',[ID,Env]),
986		NewEnv = [local_id(ID,Type,FiniteBaseType,Var)|Env]. % TODO: proper update
987
988		add_new_local_id_bounds(BI,env(Local,B),env(Local,NewB)) :-
989		append(BI,B,NewB).
990
991		infer_bounds_within_env(Paras,Pred,Env,BoundsInfo) :-
992		start_ms_timer(T1),
993		get_full_bounds_information(Env,OB),
994		infer_bounds(Paras,Pred,[outer_bounds(OB)],BoundsInfo),
995		get_elapsed_walltime(T1,WT1),add_to_profile_stats(b2asp_bounds_analysis_time,WT1).
996
997		get_full_bounds_information(env(TypedIds,LocalBounds),FullLocalBounds) :-
998		findall(bound_id_info(ID,Type,Bound),
999		member(local_id(ID,Type,Bound,_Var),TypedIds), FullLocalBounds, LocalBounds).
1000
1001		find_bounds_info(ID,Type,env(_,BI),Res) :-
1002		(member(bound_id_info(ID,Type,Bounds),BI) -> Res = Bounds
1003		; Res=Type, format(user_output,'No bounds for ~w~n',[ID])).
1004
1005
1006
1007		reset_b2asp :-
1008		bb_put(b2asp_non_positive_depth,0),
1009		reset_b2asp_code_gen,
1010		reset_clingo_interface.
1011
1012		% -------------------
1013
1014		% interface predicate to solve a B predicate with Clingo
1015		% TODO: take LocalState into account
1016		% if Exhaustive=exhaustive then contradiction found or all solutions will be generated upon backtracking
1017		solve_pred_with_clingo(BPred,MaxNrSols,_LocalState,Res,Exhaustive) :-
1018		run_clingo_on_formula(BPred,MaxNrSols,Res,Exhaustive).
1019
1020
1021		pre_process_formula(Pred,QPred) :- is_predicate(Pred),
1022		find_typed_identifier_uses(Pred,Ids),!,
1023		create_exists(Ids,Pred,QPred). % create exists for open ids, so that we can annotate them with bounds
1024		pre_process_formula(F,F).
1025
1026
1027		run_clingo_on_formula(Formula) :- run_clingo_on_formula(Formula,1,_,_).
1028		run_clingo_on_formula(Formula,MaxNrModels,Result,Exhaustive) :-
1029		% write(user_output,Formula),nl(user_output),
1030		reset_b2asp,
1031		pre_process_formula(Formula,AnnFormula),
1032		register_formula_strings(AnnFormula),
1033		current_output(SavedOut),
1034		get_clingo_out_file(OutFile),
1035		catch(open(OutFile,write,Stream,[encoding(utf8)]), % TODO: pass in environment
1036		error(existence_error(_,_),_),
1037		(add_b2asp_error('Path does not exist, be sure to set tmpdir preference correctly: ',OutFile),
1038		fail)),
1039		start_ms_timer(T1),
1040		call_cleanup((set_output(Stream),top_level_trans(AnnFormula)),(close(Stream),set_output(SavedOut))),
1041		get_elapsed_walltime(T1,WT1),add_to_profile_stats(b2asp_translation_time,WT1),
1042		stop_ms_timer_with_msg(T1,'translating formula for clingo'),
1043		!,
1044		(debug_mode(on) -> show_file(OutFile) ; true),
1045		(translation_error_occurred
1046		-> % the clingo program does not fully encode the formula; its solutions or contradictions could be wrong
1047		add_message(b2asp,'Not running clingo due to errors during translation: ',OutFile),
1048		Result=no_solution_found(translation_failed), Exhaustive=non_exhaustive
1049		; get_preference(time_out,Timeout), TimeoutSec is (Timeout+999) // 1000,
1050		run_clingo(OutFile,MaxNrModels,TimeoutSec,_,Result,Exhaustive)
1051		).
1052		run_clingo_on_formula(_,_,Result,non_exhaustive) :-
1053		Result=no_solution_found(translation_failed).
1054
1055
1056		% Strings are represented by numbers in clingo (see get_string_nr).
1057		% We register all strings of the formula before translating it, so that the range 0..N of registered
1058		% string numbers is known when generating clingo identifiers for string values without bounds.
1059		% In addition to the strings of the formula, the range contains fresh strings (one for each identifier
1060		% with strings in its type), so that string identifiers can also take values different from these strings.
1061		register_formula_strings(Formula) :-
1062		findall(S,(sub_term_of(Sub,Formula), Sub=string(S), atom(S)),Strings),
1063		sort(Strings,SStrings),
1064		maplist(get_string_nr,SStrings,_),
1065		findall(ID,(sub_term_of(Sub,Formula), Sub=b(identifier(ID),Type,_), type_contains_string(Type)),Ids),
1066		sort(Ids,SIds), length(SIds,NrIds),
1067		register_fresh_strings(NrIds).
1068
1069		% enumerate the non-variable sub-terms of a term
1070		sub_term_of(Term,Term) :- nonvar(Term).
1071		sub_term_of(Sub,Term) :- compound_arg(Term,Arg), sub_term_of(Sub,Arg).
1072
1073		type_contains_string(Type) :- var(Type),!,fail.
1074		type_contains_string(string) :- !.
1075		type_contains_string(Type) :- compound_arg(Type,Arg), type_contains_string(Arg), !.
1076
1077		% enumerate the arguments of a compound term (SICStus arg/3 requires the argument number to be bound)
1078		compound_arg(Term,Arg) :- compound(Term), functor(Term,_,Arity), between(1,Arity,N), arg(N,Term,Arg).
1079
1080		show_file(File) :-
1081		format('Contents of file ~w:~n',[File]),
1082		format('% --------------~n',[]),
1083		open(File,read,Stream),
1084		call_cleanup(show_stream(Stream),close(Stream)),
1085		format('% --------------~n',[]).
1086
1087		show_stream(Stream) :-
1088		read_line(Stream,Line),
1089		Line \= end_of_file,!,
1090		format('~s~n',[Line]),
1091		show_stream(Stream).
1092		show_stream(_).
1093
1094		top_level_trans(Formula) :-
1095		version_str(V),format('% Clingo encoding of B formula created by ProB ~w~n',[V]),
1096		translate_bexpression_with_limit(Formula,200,FS),
1097		% we could call datime(datime(Yr,Mon,Day,Hr,Min,_Sec)),
1098		format('% :clingo ~w~n',[FS]),
1099		(is_predicate(Formula) -> top_level_translate_predicate(Formula)
1100		; create_new_local_id_env(Env), trans_set(Formula,Env,main)),!,
1101		write_clingo_show_directive. % to only transmit back relevant atoms in the model
1102		top_level_trans(Formula) :- add_b2asp_error('Could not translate: ',Formula).
1103
1104		trans_debug(BPred,S) :- debug_mode(on),!,
1105		translate_bexpression_with_limit(BPred, 60, S).
1106		trans_debug(_,'').
1107
1108		clingo_format_comment_with_expr(FormatStr,BPred) :-
1109		trans_debug(BPred,BPS),
1110		clingo_format_comment(FormatStr,[BPS]).
1111		%clingo_format_comment_with_exprs(FormatStr,BExprs) :-
1112		% maplist(trans_debug,BExprs,Args),
1113		% clingo_format_comment(FormatStr,Args).
1114
1115		% -------------------
1116		% some tests/examples:
1117
1118		test(0) :-trans_set(union(empty_set, intersection(set_extension([1,2]), set_extension([2,3]))), [], main).
1119		test(1) :-trans_set(union(empty_set, set_subtraction(set_extension([1,2]), set_extension([2,3]))), [], main).
1120
1121		test(2) :- tell('out2.lp'),
1122		trans_set(union(set_extension([4]), intersection(set_extension([1,2]), set_extension([2,3]))), [], main),
1123		told.
1124		test(3) :- run_clingo_on_formula( set_subtraction(set_extension([1,2+2,5 mod 2]), set_extension([2,4])) ).
1125		test(4) :- run_clingo_on_formula( set_subtraction(set_extension([1,2+2,2+4]), interval(2,4)) ).
1126		test(5) :- run_clingo_on_formula( set_subtraction(interval(1,100), interval(3,98)) ).
1127		test(6) :- run_clingo_on_formula( set_extension([card(set_subtraction(interval(1,100), interval(3,98)))]) ).
1128		test(7) :- run_clingo_on_formula( equal(add(identifier(x,interval(1,10)),integer(5)), integer(11))).
1129		test(8) :- run_clingo_on_formula( subset(interval(1,5),
1130		union(identifier(x,interval(2,6)),set_extension([1])))).
1131		test(9) :- run_clingo_on_formula( set_equal(interval(1,5),
1132		union(identifier(x,interval(2,6)),set_extension([1])))).
1133		test(10) :- run_clingo_on_formula( not_set_equal(interval(1,5),
1134		union(identifier(x,interval(2,6)),interval(1,5)))).
1135		test(11) :- run_clingo_on_formula( conjunct( subset(interval(1,5),identifier(x,interval(0,6))),
1136		subset(identifier(x,interval(0,6)), interval(1,6)))).
1137		test(12) :- run_clingo_on_formula( conjunct( conjunct( member(3,identifier(x,interval(0,4))),
1138		member(4,identifier(x,interval(0,4)))),
1139		not_member(1,identifier(x,interval(0,4))))).
1140		test(13) :- run_clingo_on_formula( conjunct( equivalence( member(3,identifier(x,interval(0,4))),
1141		member(4,identifier(x,interval(0,4)))),
1142		member(4,identifier(x,interval(0,4))))).
1143		test(14) :- run_clingo_on_formula( set_equal( union(interval(1,100),set_extension([identifier(x,interval(0,200))])),
1144		interval(1,101))). % small performance test
1145		test(15) :- run_clingo_on_formula( set_equal( union(identifier(s,boolean),set_extension([identifier(x,boolean)])),
1146		set_extension([pred_true,pred_false]))).
1147		test(16) :- run_clingo_on_formula( conjunct( less(integer(3),identifier(x,interval(0,6))),
1148		greater(integer(5),identifier(x,interval(0,6))))).
1149		test(17) :- run_clingo_on_formula( conjunct( less(integer(1),card(identifier(x,interval(0,6)))),
1150		greater(integer(3),card(identifier(x,interval(0,6)))))).
1151		test(18) :- run_clingo_on_formula( b(equal(b(card(b(identifier(x),set(boolean),'.'(nodeid(p4(-1,1,6,7)),[]))),
1152		integer,'.'(nodeid(p4(-1,1,1,8)),[])),b(integer(2),integer,'.'(nodeid(p4(-1,1,9,10)),[]))),
1153		pred,'.'(removed_typing,'.'(nodeid(p4(-1,1,1,10)),[])))). % ProB AST example
1154		test(19) :- run_clingo_on_formula( conjunct(equal(max(identifier(x,interval(1,10))),integer(3)),
1155		equal(card(identifier(x,interval(1,10))),integer(2)))).
1156		test(20) :- run_clingo_on_formula(set_extension([string(test1),string(test2)])).
1157		test(21) :- run_clingo_on_formula(set_extension([(1,2)])).
1158		test(22) :- run_clingo_on_formula(reverse(set_extension([(1,2)]))).
1159		test(23) :- run_clingo_on_formula(b(exists('.'(b(identifier(f),set(couple(boolean,boolean)),[]),[]),b(conjunct(b(member(b(identifier(f),set(couple(boolean,boolean)),'.'(nodeid(p4(-1,1,1,2)),[])),b(partial_function(b(bool_set,set(boolean),'.'(nodeid(p4(-1,1,3,7)),[])),b(bool_set,set(boolean),'.'(nodeid(p4(-1,1,10,14)),[]))),set(set(couple(boolean,boolean))),'.'(nodeid(p4(-1,1,3,14)),[]))),pred,'.'(nodeid(p4(-1,1,1,14)),[])),b(equal(b(card(b(identifier(f),set(couple(boolean,boolean)),'.'(nodeid(p4(-1,1,22,23)),[]))),integer,'.'(nodeid(p4(-1,1,17,24)),[])),b(integer(2),integer,'.'(nodeid(p4(-1,1,25,26)),[]))),pred,'.'(nodeid(p4(-1,1,17,26)),[]))),pred,'.'(nodeid(p4(-1,1,1,26)),[]))),pred,'.'(used_ids([]),'.'(nodeid(p4(-1,1,1,26)),[])))).
1160		test(24) :- run_clingo_on_formula(b(exists('.'(b(identifier(f),set(couple(boolean,boolean)),[]),[]),b(conjunct(b(member(b(identifier(f),set(couple(boolean,boolean)),'.'(nodeid(p4(-1,1,1,2)),[])),b(total_function(b(bool_set,set(boolean),'.'(nodeid(p4(-1,1,3,7)),[])),b(bool_set,set(boolean),'.'(nodeid(p4(-1,1,10,14)),[]))),set(set(couple(boolean,boolean))),'.'(nodeid(p4(-1,1,3,14)),[]))),pred,'.'(nodeid(p4(-1,1,1,14)),[])),b(equal(b(card(b(identifier(f),set(couple(boolean,boolean)),'.'(nodeid(p4(-1,1,22,23)),[]))),integer,'.'(nodeid(p4(-1,1,17,24)),[])),b(integer(2),integer,'.'(nodeid(p4(-1,1,25,26)),[]))),pred,'.'(nodeid(p4(-1,1,17,26)),[]))),pred,'.'(nodeid(p4(-1,1,1,26)),[]))),pred,'.'(used_ids([]),'.'(nodeid(p4(-1,1,1,26)),[])))).
1161		/*
1162
1163		$ more out.lp
1164		main(4).
1165
1166		unleft0(1).
1167
1168		unleft0(2).
1169
1170		unright1(2).
1171
1172		unright1(3).
1173
1174		main(A) :-
1175		unleft0(A),
1176		unright1(A).
1177
1178		$ clingo out.lp
1179		clingo version 5.8.0
1180		Reading from out.lp
1181		Solving...
1182		Answer: 1 (Time: 0.000s)
1183		unright1(2) unright1(3) unleft0(1) unleft0(2) main(4) main(2)
1184		SATISFIABLE
1185
1186		Models : 1
1187		Calls : 1
1188		Time : 0.000s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
1189		CPU Time : 0.000s
1190
1191		some queries in probcli -repl that work
1192
1193		:clingo x+1=4
1194		:clingo x+1=y & y+x=11
1195		:clingo x <: 1..3 & x /= {} & card(x)=3
1196		:clingo (x=2 => y=3) & (y=3 => x>0) & x>2
1197		:clingo x<:BOOL & card(x)=2
1198		:clingo (1,2)=(x,y-1)
1199		:clingo x <: BOOL*BOOL & x/= {} & x<<:y
1200		:clingo x : BOOL*BOOL & x=(TRUE,FALSE)
1201		:clingo x : (1..2)*(1..2) & x=(1,2)
1202		:clingo x <: (1..2)*(1..2) & x /= {}
1203		:clingo x <: (1..2)*(1..2) & dom(x)=1..2 & ran(x)=1..1
1204		:clingo x = {TRUE|->FALSE, FALSE|->TRUE}
1205		:clingo x = {TRUE|->FALSE, FALSE|->TRUE} & res=closure1(x)
1206		:clingo SIGMA(x).(x:1..3|x) = r
1207
1208		with prob_examples/public_examples/B/Benchmarks/phonebook7.mch:
1209		:clingo-double-check x<:Code & card(x)=2 & x \/ y = Code & c1:x & c1:y
1210		:clingo-double-check x<:Code*Code & dom(x)=Code & closure1(x)=Code*Code
1211		with card(Name) = 10:
1212		:clingo x<:Name*Name & dom(x)=Name & closure1(x)=Name*Name & card(x)<11
1213
1214		is now fast when encoding #card aggregate as literal (i.e., inlining it)
1215		:clingo x <: (1..2)*(1..2) & x /= {} & card(x)=1
1216
1217		still too slow with minint=-128, maxint=127 (21 seconds):
1218		:clingo x = {1|->2} & r=closure1(x)
1219
1220		with card(Name)=10
1221		:clingo x<:Name*Name & dom(x)=Name & closure1(x)=Name*Name& card(x) < 10
1222		% ProB finds contradiction immediately; Kodkod is also quite fast
1223
1224
1225		future tests:
1226		:clingo z<:1..3 & !x.(x:1..2 => x:z) -> now works
1227		:clingo z<: 1..5 & !x.(x:0..5 => {y|y:1..x & y<7} /= z)
1228		:clingo {S,E,N,D, M,O,R, Y} <: 0..9 & S >0 & M >0 & card({S,E,N,D, M,O,R, Y}) = n & S*1000 + E*100 + N*10 + D + M*1000 + O*100 + R*10 + E =M*10000 + O*1000 + N*100 + E*10 + Y
1229		*/