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