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