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