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
7		% first attempt at translator from B AST to ASP
8		% started May 7th 2025, Michael Leuschel, based on analysis of B to ASP translations by Maxime Zielinger
9		% Michael Leuschel, Maxime Zielinger
10
11		:- use_module(library(lists)).
12		:- use_module(library(process)).
13
14
15		%:- op(700,fx,not). % add operator declaration, as we need to print not without parentheses for Clingo
16
17
18
19		:- if(current_module(error_manager)).
20		:- use_module(probsrc(error_manager)).
21		:- use_module(probsrc(debug)).
22		:- use_module(probsrc(preferences)).
23		:- use_module(probsrc(b_global_sets),[b_get_fd_type_bounds/3, lookup_global_constant/2]).
24		:- use_module(probsrc(tools_strings),[ajoin/2,ajoin_with_sep/3, ajoin_path/3]).
25		:- use_module(probsrc(bsyntaxtree),[get_texpr_id/2]).
26		:- use_module(probsrc(version), [version_str/1]).
27		:- use_module(probsrc(system_call),[safe_process_create/3]).
28		add_b2asp_error(Msg,Args) :- add_error(b2asp,Msg,Args).
29		add_b2asp_warning(Msg,Args) :- add_warning(b2asp,Msg,Args).
30		get_clingo_path(Path) :- get_preference(path_to_clingo,Path).
31		get_min_int(X) :- get_preference(minint,X).
32		get_max_int(X) :- get_preference(maxint,X).
33		get_clingo_out_file(File) :-
34		get_preference(tmpdir, TmpDir),
35		ajoin_path(TmpDir, 'prob_clingo_translation.lp', File).
36		% see get_temporary_filename, open_temp_file
37		:- else.
38		add_b2asp_error(Msg,Args) :-
39		write(user_error,Msg), write(user_error,Args), nl(user_error).
40		add_b2asp_warning(Msg,Args) :-
41		add_b2asp_error(Msg,Args).
42		debug_mode(on).
43		debug_format(_,FS,A) :- format(user_output,FS,A).
44		get_clingo_path('C:/Users/hhuri/Desktop/stage/clingo-5.4.0-win64/clingo.exe').
45		get_clingo_path('/opt/homebrew/bin/clingo').
46		get_min_int(-128).
47		get_max_int(127).
48		get_clingo_out_file('out.lp').
49		b_get_fd_type_bounds(_,_,_) :- fail.
50		lookup_global_constant(_,_) :- fail.
51		get_texpr_id(identifier(X,_),X).
52		version_str('b2asp module').
53		safe_process_create(Cmd,Args,Opts) :- process_create(Cmd,Args,Opts).
54		:- endif.
55
56
57		% ------------------------------
58		% translating PREDICATES
59
60		% a top-level translation of predicates
61		% asserts translations as integrity constraint (aka query)
62
63		%top_level_translate_predicate(Formula) :-
64		% trans_pred_positive(Formula,Prop),
65		% gen_clingo_ic_constraint( not(Prop) ). % assert main is false, and Formula is true
66		top_level_translate_predicate(Formula) :-
67		trans_not_pred(Formula,Prop),
68		gen_clingo_ic_constraint( Prop ).
69
70		is_predicate(b(_,pred,_)). % ProB typed AST node
71		is_predicate(BOP) :- bin_op_pred_single_call(BOP,_,_,_).
72		is_predicate(X) :- negate_pred(X,_) ; negate_pred(NX,X), NX \= negation(_).
73		is_predicate(BOP) :- negate_scalar_binary_pred(BOP,_,_,_).
74		is_predicate(conjunct(_,_)).
75		is_predicate(disjunct(_,_)).
76		is_predicate(implication(_,_)).
77		is_predicate(equivalence(_,_)).
78
79		% translating a predicate into a proposition that is true if predicate is true
80		% not sure if we need it
81		%trans_pred_positive(BOP,Prop) :-
82		% bin_op_pred_single_call(BOP,A,B,ClingoOp),
83		% translate_scalar(A,ValA,CallA),
84		% translate_scalar(B,ValB,CallB),
85		% ClingoCall =.. [ClingoOp,ValA,ValB],
86		% gensym_if_necessary(pred,Prop),
87		% gen_clingo_clause(Prop,[], (CallA,CallB, ClingoCall) ).
88
89
90		% translating a predicate into a proposition that is false if predicate is true and can be used as ic constraint
91		% not sure if we need both positive and negative translations
92		trans_not_pred(b(Pred,pred,_Infos),Prop) :- !, % format(user_output,' pred --> ~w~n',[Pred]),
93		trans_not_pred(Pred,Prop).
94		trans_not_pred(truth,Prop) :- !,
95		gen_clingo_pred_clause(falsity,Prop,[], 1=2 ).
96		trans_not_pred(falsity,Prop) :- !,
97		gensym_if_necessary(truth,Prop),
98		gen_clingo_fact(Prop,[]).
99		trans_not_pred(exists(Paras,Pred),Prop) :- !,
100		% TODO: properly pass environment around and register paras, rather than using generated_id/2 facts
101		(member(b(identifier(ID),_,_),Paras), generated_id(ID,_),
102		add_b2asp_error('Identifier clash (B2ASP does not yet support multiple uses of same id): ',ID),fail
103		; true),
104		trans_not_pred(Pred,Prop).
105		trans_not_pred(subset(A,B),Prop) :- !,
106		trans_set(A,P1), trans_set(B,P2),
107		gen_clingo_pred_clause(not_subset,Prop,[], (call(P1,X), not(call(P2,X)) )). % :- P1(X), not P2(X).
108		trans_not_pred(subset_strict(A,B),Prop) :- !,
109		trans_not_pred(conjunct(subset(A,B),not_set_equal(A,B)),Prop).
110		trans_not_pred(member(A,B),Prop) :- !,
111		trans_not_member_pred(A,B,Prop). % dedicated code for translating membership
112		trans_not_pred(set_equal(A,B),Prop) :- !, % could be also translated into conjunction of subset
113		% Note: does not exist as such in B AST: is equal with typing info = set(_)
114		% this could also works with scalars (i.e., if P1/P2 have exactly one solution)
115		trans_set(A,P1), trans_set(B,P2),
116		CallA =..[P1,X], CallB=..[P2,X],
117		gen_clingo_pred_clause(not_set_equal,Prop,[], (CallA, not(CallB) )), % :- P1(X), not P2(X).
118		gen_clingo_clause(Prop,[], (CallB, not(CallA) )). % :- P2(X), not P1(X).
119		trans_not_pred(equal(A,B),Prop) :- A = b(_,set(_),_),!,
120		trans_not_pred(set_equal(A,B),Prop).
121		trans_not_pred(not_equal(A,B),Prop) :- A = b(_,set(_),_),!,
122		trans_not_pred(not_set_equal(A,B),Prop).
123		trans_not_pred(is_partial_function(A),Prop) :- !,
124		trans_set(A,P1),
125		gen_clingo_pred_clause(not_pfun,Prop,[], (call(P1,(X,Y)), call(P1,(X,Z)), '!='(Y,Z)) ). % :- P1((X,Y)),P1((X,Z)), Y!=Z.
126		trans_not_pred(is_injective(A),Prop) :- !,
127		trans_set(A,P1),
128		gen_clingo_pred_clause(not_inj,Prop,[], (call(P1,(Y,X)), call(P1,(Z,X)), '!='(Y,Z)) ). % :- P1((Y,X)),P1((Z,X)), Y!=Z.
129		trans_not_pred(is_sequence_domain(A),Prop) :- !,
130		trans_set(A,P1),
131		gen_clingo_pred_clause(not_seq,Prop,[], (call(P1,X), '<'(X,1) )), % :- P1(X), X < 1. (sequences start at 1)
132		gen_clingo_clause(Prop,[], (call(P1,X), '>'(X,1), '='(X1,X-1), not(call(P1,X1))) ). % :- P1(X), not P1(X-1).
133		trans_not_pred(Arith,Prop) :-
134		negate_scalar_binary_pred(Arith,A,B,ClingoOp),!,
135		translate_scalar(A,X1,CallA),
136		translate_scalar(B,X2,CallB),
137		gen_clingo_pred_clause(arith,Prop,[], (CallA, CallB, call(ClingoOp,X1,X2) )).
138		trans_not_pred(conjunct(P1,P2),Prop) :- !, % not(P1 & P2) <=> not(P1) or not(P2)
139		trans_not_pred(P1,NotP1),
140		trans_not_pred(P2,NotP2),
141		gen_clingo_pred_clause(not_conjunct,Prop,[], NotP1 ),
142		gen_clingo_clause(Prop,[], NotP2 ).
143		trans_not_pred(disjunct(P1,P2),Prop) :- !, % not(P1 or P2) <=> not(P1) & not(P2)
144		trans_not_pred(P1,NotP1),
145		trans_not_pred(P2,NotP2),
146		gen_clingo_pred_clause(not_disjunct,Prop,[], (NotP1 , NotP2) ).
147		trans_not_pred(implication(P1,P2),Prop) :- !, % not(P1 => P2) <=> P1 & not(P2)
148		trans_not_pred(P1,NotP1), % TODO: translate P1 positively?
149		trans_not_pred(P2,NotP2),
150		gen_clingo_pred_clause(not_implicatin,Prop,[], (not(NotP1) , NotP2) ).
151		trans_not_pred(equivalence(P1,P2),Prop) :- !, % not(P1 <=> P2) <=> (P1 & not(P2)) or (not(P1) & P2)
152		trans_not_pred(P1,NotP1),
153		trans_not_pred(P2,NotP2),
154		gensym_if_necessary(not_equiv,Prop),
155		gen_clingo_clause(Prop,[], (not(NotP1) , NotP2) ),
156		gen_clingo_clause(Prop,[], (NotP1 , not(NotP2)) ).
157		trans_not_pred(Pred,Prop) :-
158		negate_pred(Pred,NotPred),!,
159		trans_not_pred(NotPred,NegProp), % translate negation and create auxiliary proposition for it
160		gen_clingo_pred_clause(negated,Prop,[], not(NegProp) ). % negate the proposition
161		trans_not_pred(X,Prop) :-
162		add_b2asp_error('Ignoring unsupported predicate: ',X),
163		trans_not_pred(truth,Prop).
164
165		% TODO: forall, ...
166
167		trans_not_member_pred(A,TB,Prop) :- (TB=b(B,_,_) -> true ; TB=B),
168		specific_trans_not_member_pred(B,A,Prop),!.
169		trans_not_member_pred(A,B,Prop) :- % generic translation rule:
170		translate_scalar(A,X1,CallA),
171		trans_set(B,P2),
172		gen_clingo_pred_clause(not_member,Prop,[], (CallA, not(call(P2,X1)) )). % :- P1(X), not P2(X). (same as subset)
173
174		% special translation rules for member checks:
175		specific_trans_not_member_pred(pow_subset(B),A,Prop) :- !,
176		trans_not_pred(subset(A,B),Prop). % A:POW(B) <=> A <: B
177		specific_trans_not_member_pred(pow1_subset(B),A,Prop) :- !,
178		trans_not_pred(conjunct(subset(A,B),not_equal(A,empty_set)),Prop). % A:POW1(B) <=> A <: B & A /= {}
179		specific_trans_not_member_pred(relations(Dom,Ran),A,Prop) :- !,
180		trans_not_pred(subset(A,cartesian_product(Dom,Ran)),Prop). % A: Dom <-> Ran <=> A <: (Dom*Ran)
181		specific_trans_not_member_pred(partial_function(Dom,Ran),A,Prop) :- !,
182		% A : Dom +-> Ran <=> A <: (Dom*Ran) & A: TypeDom +-> TypeRan
183		trans_not_pred(conjunct(subset(A,cartesian_product(Dom,Ran)),
184		is_partial_function(A)), % TODO avoid translating A twice
185		Prop).
186		specific_trans_not_member_pred(partial_injection(Dom,Ran),A,Prop) :- !,
187		% A : Dom >+> Ran <=> A <: (Dom*Ran) & A: TypeDom +-> TypeRan & A~:TypeRan +-> TypeDom
188		trans_not_pred(conjunct(subset(A,cartesian_product(Dom,Ran)),
189		conjunct(is_partial_function(A),
190		is_injective(A))), % TODO avoid translating A three times
191		Prop).
192		specific_trans_not_member_pred(total_function(Dom,Ran),A,Prop) :- !,
193		% A : Dom --> Ran <=> A <: (Dom*Ran) & A: TypeDom +-> TypeRan & Dom <: domain(A)
194		trans_not_pred(conjunct(subset(A,cartesian_product(Dom,Ran)),
195		conjunct(is_partial_function(A),
196		subset(Dom,domain(A)))), % TODO avoid translating A three times
197		Prop).
198		specific_trans_not_member_pred(seq(Ran),A,Prop) :- !,
199		% A : seq(Ran) <=> ran(A) <: Ran & A: INTEGER +-> TypeRan & domain(A) = 1..N (for some N = size(A))
200		trans_not_pred(conjunct(is_sequence_domain(domain(A)),
201		conjunct(is_partial_function(A),
202		subset(range(A),Ran))), % TODO avoid translating A three times
203		Prop).
204		% TODO: partial_surjection, total_surjection, total_injection, sequence ,...
205
206		negate_pred(negation(Pred),Pred).
207		negate_pred(not_set_equal(A,B),set_equal(A,B)).
208		negate_pred(not_subset(A,B),subset(A,B)).
209		negate_pred(not_subset_strict(A,B),subset_strict(A,B)).
210		negate_pred(not_member(A,B),member(A,B)).
211
212		% arithmetic comparison binary operators along with a translation of the negation to Clingo
213		negate_scalar_binary_pred(less(A,B),A,B,'>=').
214		negate_scalar_binary_pred(greater(A,B),A,B,'<='). % note this is different from Prolog =< comparison syntax
215		negate_scalar_binary_pred(less_equal(A,B),A,B,'>').
216		negate_scalar_binary_pred(greater_equal(A,B),A,B,'<').
217		% can also apply to scalars:
218		negate_scalar_binary_pred(equal(A,B),A,B,'!=').
219		negate_scalar_binary_pred(not_equal(A,B),A,B,'=').
220
221		% binary predicate operators that can be translated into a single constraint
222		bin_op_pred_single_call(equal(A,B),A,B,'='). % equality for scalar
223		bin_op_pred_single_call(not_equal(A,B),A,B,'!=').
224
225		% ------------------------------
226		% translating SET EXPRESSIONS
227
228		is_set(set(BaseType),BaseType).
229		is_set(seq(Type),couple(integer,Type)).
230
231		% translate a B set value (of scalars) to a Clingo predicate Pred(X).
232		% Pred(X) is true if X represents an element of the B set
233		trans_set(b(Expr,Type,_Infos),Pred) :- % format(user_output,' set --> ~w~n',[Expr]),
234		(is_set(Type,BaseType)
235		-> (Expr = identifier(ID) -> NExpr=identifier(ID,BaseType) ; NExpr = Expr)
236		; add_b2asp_error('Type of expression is not a set: ',Type), fail
237		),
238		!,
239		trans_set(NExpr,Pred).
240		trans_set(empty_set,Pred) :- !,
241		DummyArg = 0, % Clingo does not like unbound variables in head??
242		gensym_if_necessary(empty,Pred),
243		gen_clingo_clause(Pred,[DummyArg], 1=2 ).
244		trans_set(bool_set,Pred) :- !,
245		trans_set(set_extension([pred_false,pred_true]),Pred).
246		trans_set(value(V),Pred) :- V==[], !, trans_set(empty_set,Pred).
247		trans_set(value(AVL),Pred) :-
248		custom_explicit_sets:expand_custom_set_to_list_now(AVL,L),!, % this creates Value list not set_extension list ! TODO
249		trans_set(set_extension(L),Pred).
250		trans_set(sequence_extension(L),Pred) :- !,
251		add_indices(L,1,Set),
252		trans_set(set_extension(Set),Pred).
253		trans_set(set_extension(L),Pred) :- !,
254		gensym_if_necessary(set_ext,Pred),
255		maplist(trans_scalar4map(Pred),L).
256		trans_set(union(A,B),Pred) :- !,
257		trans_set(A,P1),
258		trans_set(B,P2),
259		gen_clingo_pred_clause(union,Pred,[X], (call(P1,X)) ),
260		gen_clingo_clause(Pred,[X], (call(P2,X)) ).
261		trans_set(intersection(A,B),Pred) :- !,
262		trans_set(A,P1),
263		trans_set(B,P2),
264		gen_clingo_pred_clause(inter,Pred,[X], (call(P1,X),call(P2,X)) ).
265		trans_set(set_subtraction(A,B),Pred) :- !, % difference set in B
266		trans_set(A,P1),
267		trans_set(B,P2),
268		gen_clingo_pred_clause(diff,Pred,[X], (call(P1,X),not(call(P2,X))) ). % Pred(X) :- P1(X), not P2(X).
269		trans_set(cartesian_product(A,B),Pred) :- !,
270		trans_set(A,P1),
271		trans_set(B,P2),
272		gen_clingo_pred_clause(cart,Pred,[(X,Y)], (call(P1,X),call(P2,Y)) ). % Pred((X,Y)) :- P1(X), P2(Y).
273		trans_set(domain(A),Pred) :- !,
274		trans_set(A,P1),
275		gen_clingo_pred_clause(domain,Pred,[X], call(P1,(X,_)) ). % Pred(X) :- P1((X,_)).
276		trans_set(range(A),Pred) :- !,
277		trans_set(A,P1),
278		gen_clingo_pred_clause(range,Pred,[X], call(P1,(_,X)) ). % Pred(X) :- P1((_,X)).
279		trans_set(image(Rel,Set),Pred) :- !, % relational image B operator
280		trans_set(Rel,P1),
281		trans_set(Set,P2),
282		gen_clingo_pred_clause(image,Pred,[Y], (call(P2,X),call(P1,(X,Y))) ). % Pred(Y) :- P1(X), P2((X,Y)).
283		trans_set(domain_restriction(Set,Rel),Pred) :- !, % domain restriction B operator Set <| Rel
284		trans_set(Set,P1),
285		trans_set(Rel,P2),
286		gen_clingo_pred_clause(dres,Pred,[(X,Y)], (call(P1,X),call(P2,(X,Y))) ). % Pred((X,Y)) :- P1(X), P2((X,Y)).
287		trans_set(domain_subtraction(Set,Rel),Pred) :- !, % domain subtraction B operator Set <<| Rel
288		trans_set(Set,P1),
289		trans_set(Rel,P2),
290		gen_clingo_pred_clause(dsub,Pred,[(X,Y)], (call(P2,(X,Y)),not(call(P1,X))) ). % Pred((X,Y)) :- P2((X,Y)), not P(X).
291		trans_set(range_restriction(Rel,Set),Pred) :- !, % range restriction B operator Rel |> Set
292		trans_set(Set,P1),
293		trans_set(Rel,P2),
294		gen_clingo_pred_clause(rres,Pred,[(X,Y)], (call(P1,Y),call(P2,(X,Y))) ). % Pred((X,Y)) :- P1(Y), P2((X,Y)).
295		trans_set(range_subtraction(Rel,Set),Pred) :- !, % range subtraction B operator Rel |>> Set
296		trans_set(Set,P1),
297		trans_set(Rel,P2),
298		gen_clingo_pred_clause(rsub,Pred,[(X,Y)], (call(P2,(X,Y)), not(call(P1,Y))) ). % Pred((X,Y)) :- P2((X,Y)), not P1(Y).
299		trans_set(composition(A,B),Pred) :- !, % relational composition operator
300		trans_set(A,P1),
301		trans_set(B,P2),
302		gen_clingo_pred_clause(comp,Pred,[(X,Z)], (call(P1,(X,Y)),call(P2,(Y,Z))) ). % Pred((X,Z)) :- P1((X,Y)), P2((Y,Z)).
303		trans_set(closure(A),Pred) :- !, % closure1 transitive operator
304		trans_set(A,P1),
305		gen_clingo_pred_clause(closure1,Pred,[(X,Y)], call(P1,(X,Y)) ), % Pred((X,Y)) :- P1((X,Y)).
306		gen_clingo_clause(Pred,[(X,Z)], ( call(P1,(X,Y)) , call(Pred,(Y,Z))) ). % Pred((X,Z)) :- P1((X,Y)), Pred((Y,Z)).
307		trans_set(overwrite(A,B),Pred) :- !, % relational override operator
308		trans_set(A,P1),
309		trans_set(B,P2),
310		trans_set(domain(B),P3), % we need to create a separate domain encoding to be able to use it inside the "not" below
311		gen_clingo_pred_clause(overwr,Pred,[(X,Y)], call(P2,(X,Y)) ), % Pred((X,Y)) :- P2((X,Y)).
312		gen_clingo_clause(Pred,[(X,Y)], (call(P1,(X,Y)),not(call(P3,X))) ). % Pred((X,Y)) :- P1((X,Y)), not P3(X).
313		trans_set(identity(A),Pred) :- !, % identity operator
314		trans_set(A,P1),
315		gen_clingo_pred_clause(id,Pred,[(X,X)], call(P1,X) ). % Pred((X,X)) :- P1(X).
316		trans_set(reverse(A),Pred) :- !, % reverse B operator r~
317		trans_set(A,P1),
318		gen_clingo_pred_clause(rev,Pred,[(Y,X)], (call(P1,(X,Y)))). % Pred((Y,X)) :- P1((X,Y)).
319		trans_set(interval(A,B),Pred) :- !,
320		translate_scalar(A,X1,C1),
321		translate_scalar(B,X2,C2),
322		gen_clingo_pred_clause(interval,Pred,[X], (C1,C2,'='(X,'..'(X1,X2))) ).
323		trans_set(global(ID),Pred) :- % B value for entire global enumerated/deferred set ID
324		b_get_fd_type_bounds(ID,Low,Up),!,
325		trans_set(interval(Low,Up),Pred).
326		trans_set(identifier(ID,global(ID)),Pred) :- % TODO: proper checking of scoping
327		b_get_fd_type_bounds(ID,Low,Up),!,
328		trans_set(interval(Low,Up),Pred).
329		trans_set(identifier(ID,BaseType),Pred) :- !,
330		gen_clingo_set_identifier(ID,BaseType,Pred).
331		trans_set(X,Pred) :- %write(user_error,X),nl(user_error),
332		add_b2asp_error('Unsupported set: ',X), Pred=fail.
333
334		% add indices to sequence extension list:
335		add_indices([],_,[]).
336		add_indices([H|T],Nr,[couple(integer(Nr),H)|CT]) :- N1 is Nr+1,
337		add_indices(T,N1,CT).
338
339		% an optimised version of translate scalar
340		% may produce true as ClingoCall if value can be represented as Clingo Constant
341		% running ClingoCall in clingo will produce result in ClingoValue
342		translate_scalar(Lit,ClingoValue,ClingoCall) :-
343		valid_literal(Lit,ClingoCst),!,
344		ClingoValue=ClingoCst, ClingoCall=true.
345		translate_scalar(Lit,ClingoValue,ClingoCall) :-
346		trans_scalar(Lit,Pred),
347		ClingoCall =.. [Pred,ClingoValue].
348		% TODO: for identifiers we should also pass an environment storing which Clingo Predicate is mapped to which identifier
349		% ditto for set translation
350
351		scalar_type(boolean).
352		scalar_type(integer).
353		scalar_type(global(_)).
354		scalar_type(couple(A,B)) :- scalar_type(A), scalar_type(B).
355
356
357		% ------------------------------
358		% translating SCALAR EXPRESSIONS
359
360		% special version for maplist:
361		trans_scalar4map(Pred,El) :- trans_scalar(El,Pred).
362
363		% translate a scalar B value V (integers, booleans, strings, ...) to a Clingo predicate Pred(X).
364		% Pred(X) is true if X corresponds to the B value V
365
366		trans_scalar(b(Expr,Type,_Infos),Pred) :-
367		(scalar_type(Type)
368		-> (Expr = identifier(ID) -> NExpr=identifier(ID,Type) ; NExpr = Expr)
369		; is_set(Type,_) -> add_b2asp_error('Set expression is not supported here, scalar expected: ',Type), fail
370		; add_b2asp_error('Type of expression is not a scalar: ',Type), fail
371		),
372		!,
373		trans_scalar(NExpr,Pred).
374		trans_scalar(Lit,Pred) :- valid_literal(Lit,ClingoCst), !,
375		gensym_if_necessary(lit,Pred),
376		gen_clingo_fact(Pred,[ClingoCst]).
377		trans_scalar(BOP,Pred) :- bin_op(BOP,A,B,OP), !,
378		translate_scalar(A,X1,C1),
379		translate_scalar(B,X2,C2),
380		ClingoExpr =.. [OP,X1,X2],
381		clingo_format_comment('% scalar binary operator ~w~n',[OP]),
382		gen_clingo_pred_clause(bop,Pred,[X], (C1,C2,'=='(X,ClingoExpr)) ). % TODO: what is difference to =/2, :=/2 ??
383		trans_scalar(Aggr,Pred) :- set_aggregate(Aggr,Set,ClingoAggr,Prefix),!,
384		trans_set(Set,P1),
385		gen_clingo_count_aggregate(ClingoAggr,P1,P1Aggregate),
386		gen_clingo_pred_clause(Prefix,Pred,[X], '='(X,P1Aggregate) ). % Count = #count{Var : node(Var)} ,....
387		trans_scalar(first_of_pair(A),Pred) :- !, % prj1 (same translation as domain)
388		trans_scalar(A,P1),
389		gen_clingo_pred_clause(prj1,Pred,[X], call(P1,(X,_)) ). % Pred(X) :- P1((X,_)).
390		trans_scalar(second_of_pair(A),Pred) :- !, % prj2 (same translation as range)
391		trans_scalar(A,P1),
392		gen_clingo_pred_clause(prj2,Pred,[X], call(P1,(_,X)) ). % Pred(X) :- P1((_,X)).
393		trans_scalar(function(Rel,Arg),Pred) :- !, % function application operator; same translation as image
394		trans_set(Rel,P1),
395		trans_scalar(Arg,P2),
396		gen_clingo_pred_clause(apply,Pred,[Y], (call(P2,X),call(P1,(X,Y))) ). % Pred(Y) :- P1(X), P2((X,Y)).
397		trans_scalar(fd(Nr,GS),Pred) :- integer(Nr), % enumerated/deferred set element member as B value
398		b_get_fd_type_bounds(GS,Low,Up), Nr>=Low, Nr=<Up, !,
399		trans_scalar(Nr,Pred).
400		trans_scalar(identifier(ID,global(GS)),Pred) :- % TODO: proper checking of scoping and add case to translate_scalar
401		lookup_global_constant(ID,fd(Nr,GS)),!,
402		trans_scalar(Nr,Pred).
403		trans_scalar(identifier(ID,BaseType),Pred) :- !,
404		gen_clingo_scalar_identifier(ID,BaseType,IdPred),
405		gen_clingo_pred_clause(id_scalar,Pred,[X], call(IdPred,X) ). % Pred(X) :- Id(X)
406		trans_scalar(X,P) :- %write(user_error,X),nl(user_error),
407		add_b2asp_error('Unsupported scalar: ',X), P=fail.
408
409		% B set aggregates which can be translated to Clingo aggregates:
410		set_aggregate(card(Set),Set,'#count',count).
411		set_aggregate(min(Set),Set,'#min',min).
412		set_aggregate(max(Set),Set,'#max',max).
413		set_aggregate(GeneralSum,Set,'#sum',sum) :- detect_set_summation(GeneralSum,Set).
414		% Clingo also supports avg
415
416		detect_set_summation(Expr,SET) :- % detect special pattern SIGMA(ID).(ID:SET|ID)
417		Expr = general_sum([TID1],b(member(TID2,SET),pred,_),TID3),
418		get_texpr_id(TID1,ID), get_texpr_id(TID2,ID), get_texpr_id(TID3,ID).
419
420		bin_op(A+B,A,B,+).
421		bin_op(add(A,B),A,B,+).
422		bin_op(A-B,A,B,-).
423		bin_op(minus(A,B),A,B,-).
424		bin_op(A*B,A,B,*).
425		bin_op(multiplication(A,B),A,B,*).
426		bin_op(power_of(A,B),A,B,'**').
427		bin_op(A/B,A,B,/).
428		bin_op(div(A,B),A,B,/).
429		bin_op(A mod B,A,B,\).
430		bin_op(modulo(A,B),A,B,\).
431		bin_op((A,B),A,B,',').
432		bin_op(couple(A,B),A,B,',').
433
434		valid_literal(b(Lit,_,_),Res) :- !, valid_literal(Lit,Res).
435		valid_literal(Lit,Nr) :- number(Lit),!,Nr=Lit.
436		valid_literal(pred_true,pred_true).
437		valid_literal(pred_false,pred_false).
438		valid_literal(boolean_true,pred_true). % AST node for TRUE
439		valid_literal(boolean_false,pred_false). % AST node for FALSE
440		valid_literal(string(S),'#string'(S)).
441		valid_literal(integer(Lit),Nr) :- number(Lit),!,Nr=Lit.
442		valid_literal(int(Lit),Nr) :- number(Lit),!,Nr=Lit. % from B values rather than AST's
443		valid_literal(value(V),Nr) :- nonvar(V),!, valid_literal(V,Nr).
444		valid_literal(couple(A,B),(LA,LB)) :- !, valid_literal(A,LA), valid_literal(B,LB). % Clingo accepts pairs as literals
445		valid_literal((A,B),(LA,LB)) :- !, valid_literal(A,LA), valid_literal(B,LB). % the same for pair values
446		valid_literal(Aggr,Res) :- set_aggregate(Aggr,Set,ClingoAggr,_),
447		trans_set(Set,P1),
448		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
449		% TODO: reals, enumerated set elements, ...
450
451		% ------------------------------
452		% generating CLINGO clauses,...
453
454		:- dynamic generated_id/2, clingo_generated_id/4.
455
456		gen_clingo_scalar_identifier(IDB,B,PredB) :-
457		gen_clingo_scalar_identifier(IDB,B,PredB,top_level).
458
459		gen_clingo_scalar_identifier(ID,_,Pred,_) :- nonvar(Pred),
460		add_b2asp_warning('Identifier Clingo Result should be unbound: ',ID:Pred),fail.
461		gen_clingo_scalar_identifier(ID,_,Pred,_) :- % check if we have already created a Clingo predicate for ID
462		generated_id(ID,P),!, Pred=P. % TODO: pass as environment and check bounds unchanged
463		gen_clingo_scalar_identifier(ID,couple(A,B),Pred,TopLevel) :- !,
464		% improved translation of pairs, instead of 1 { id_pair_scalar_0((-127..128,-127..128))} 1. we generate:
465		% id_pair_scalar_0((A,B)) :- id_A(A), id_B(B).
466		% 1{id_A(-127..128)}1. 1{id_B(-127..128)}1.
467		gensym(ID,IDA),
468		gen_clingo_scalar_identifier(IDA,A,PredA,left_pair),
469		gensym(ID,IDB),
470		gen_clingo_scalar_identifier(IDB,B,PredB,right_pair),
471		gensym_if_necessary(pair,Pred),
472		CallA =.. [PredA,XA], CallB =.. [PredB,XB],
473		clingo_format_comment('~n% clingo encoding of scalar identifier ~w of type ~w:~n',[ID,couple(A,B)]),
474		gen_clingo_clause(Pred,[(XA,XB)], (CallA,CallB) ), % create clause Pred((XA,XB) :- PredA(XA), PredB(XB))
475		assert_gen_id(ID,Pred,scalar,couple(A,B),TopLevel).
476		gen_clingo_scalar_identifier(ID,BaseType,Pred,TL) :- % generate: 1{Pred(Low..Up)}1.
477		gen_clingo_base_set(BaseType,ClingoType,_MaxCard,Prefix),
478		atom_concat(Prefix,'_scalar',Prefix2),
479		gensym_if_necessary(Prefix2,Pred),
480		clingo_format_comment('~n% clingo encoding of scalar identifier ~w of type ~w:~n',[ID,BaseType]),
481		format('1 { ~w(~w)} 1.~n',[Pred,ClingoType]),
482		assert_gen_id(ID,Pred,scalar,BaseType,TL).
483
484		assert_gen_id(ID,Pred,Kind,BaseType,TL) :-
485		(TL=top_level
486		-> assert(generated_id(ID,Pred)),
487		assert(clingo_generated_id(Pred,Kind,BaseType,ID)),
488		debug_format(19,'Generating clingo pred. ~w for B ~w id ~w (type ~w)~n',[Pred,Kind,ID,BaseType])
489		; true). % these are intermediate ids, e.g., generated for pair left/right hand sides
490
491		% generate Clingo integer-set identifier
492		gen_clingo_set_identifier(IDB,B,PredB) :-
493		gen_clingo_set_identifier(IDB,B,PredB,top_level).
494
495		gen_clingo_set_identifier(ID,_,Pred,_) :- % check if we have already created a Clingo predicate for ID
496		generated_id(ID,P),!,
497		% TODO: pass as environment and check bounds unchanged
498		(Pred=P -> true ; add_b2asp_error('Identifier already instantiated: ',ID:Pred),fail).
499		% Note: we cannot use similar code as for scalars for pairs (the relation is not necessarily tuple-distributive)
500		gen_clingo_set_identifier(ID,BaseType,Pred,TL) :- % generate: 1{Pred(Low..Up)}1.
501		gen_clingo_base_set(BaseType,ClingoType,MaxCard,Prefix),
502		atom_concat(Prefix,'_set',Prefix2),
503		gensym_if_necessary(Prefix2,Pred),
504		clingo_format_comment('~n% clingo encoding of set identifier ~w of type ~w:~n',[ID,BaseType]),
505		format('0 { ~w(~w)} ~w.~n',[Pred,ClingoType,MaxCard]),
506		assert_gen_id(ID,Pred,set,BaseType,TL).
507
508		% convert base type into a Clingo expression that can be put into the head of a fact,
509		% together with information about the maximal cardinality of the base type and a prefix for generated identifiers
510		gen_clingo_base_set(integer,Atom,MaxCard,Prefix) :- !,
511		get_min_int(MinInt), get_max_int(MaxInt),
512		add_b2asp_warning('Restricting infinite integer base type to:',(MinInt,MaxInt)),
513		gen_clingo_base_set(interval(MinInt,MaxInt),Atom,MaxCard,Prefix).
514		gen_clingo_base_set(interval(Low,Up),Atom,MaxCard,id_int) :- !,
515		(Up >= Low -> MaxCard is 1+Up-Low ; MaxCard=0),
516		format_to_codes('~w..~w',[Low,Up],Codes),
517		atom_codes(Atom,Codes).
518		gen_clingo_base_set(boolean,Atom,2,id_bool) :- !, Atom = 'pred_true;pred_false'.
519		gen_clingo_base_set(global(GS),Atom,MaxCard,id_glob) :- % user-defined enumerated sets or deferred sets
520		b_get_fd_type_bounds(GS,Low,Up), !,
521		gen_clingo_base_set(interval(Low,Up),Atom,MaxCard,_). % we translate those sets as integers
522		gen_clingo_base_set(couple(A,B),Atom,MaxCard,id_pair) :- !,
523		gen_clingo_base_set(A,AAtom,CardA,_),
524		gen_clingo_base_set(B,BAtom,CardB,_),
525		MaxCard is CardA*CardB,
526		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
527		atom_codes(Atom,Codes).
528		gen_clingo_base_set(BaseType,error,1,id_error) :- add_b2asp_error('Unknown base type: ',BaseType).
529
530
531		% generate a Clingo clause; at the moment we just print it onto user_output
532		gen_clingo_pred_clause(Source,Pred,ArgList,Body) :-
533		gensym_if_necessary(Source,Pred),
534		nl,
535		gen_clingo_clause(Pred,ArgList,Body).
536		gen_clingo_clause(Pred,ArgList,Body) :-
537		Head =.. [Pred|ArgList],
538		simplify_body(Body, SimplifiedBody),
539		my_portray_clause( ( Head :- SimplifiedBody ) ).
540
541		gen_clingo_ic_constraint(Body) :-
542		simplify_body(Body, SimplifiedBody),
543		nl,
544		my_portray_clause( ( :- SimplifiedBody ) ).
545
546		% filter out true literals and rewrite call/2 and call/3 literals
547		simplify_body(X,R) :- var(X),!,R=X.
548		simplify_body((A,B),Res) :- !,
549		( A=true -> simplify_body(B,Res)
550		; B=true -> simplify_body(A,Res)
551		; Res=(SA,SB), simplify_body(A,SA), simplify_body(B,SB)).
552		simplify_body(call(Pred,Arg),Call) :- !, Call =.. [Pred,Arg].
553		simplify_body(call(Pred,Arg1,Arg2),Call) :- !, Call =.. [Pred,Arg1,Arg2].
554		simplify_body(not(B),not(SB)) :- !, simplify_body(B,SB). % TODO: remove double not ?
555		simplify_body('=='(A,B),'=='(SA,SB)) :- !, simplify_expr(A,SA), simplify_expr(B,SB).
556		simplify_body('!='(A,B),'!='(SA,SB)) :- !, simplify_expr(A,SA), simplify_expr(B,SB).
557		simplify_body(B,B).
558
559		simplify_expr(X,R) :- var(X),!,R=X.
560		simplify_expr(call(Pred,Arg),Call) :- !, Call =.. [Pred,Arg].
561		simplify_expr(call(Pred,Arg1,Arg2),Call) :- !, Call =.. [Pred,Arg1,Arg2].
562		simplify_expr(B,B).
563
564		% generate a Clingo fact
565		gen_clingo_fact(Pred,ArgList) :-
566		Head =.. [Pred|ArgList],
567		my_portray_clause( Head ).
568
569		clingo_comment(Comment) :- format('%~w~n',[Comment]).
570		clingo_format_comment(FormatStr,Args) :- format(FormatStr,Args).
571
572		:- dynamic user:portray/2.
573		:- assertz( ( user:portray(X) :- b2asp_portray(X))).
574
575		% TODO: implement a proper pretty_printing for clingo; rather than using portray/2 hook
576		b2asp_portray('#clingo_range'(Low,Call,Up)) :- format('~w{~w}~w',[Low,Call,Up]).
577		%b2asp_portray('#count'(Pred)) :- format('#count{Var : ~w(Var)}',[Pred]).
578		b2asp_portray('#aggregate'(ClingoAggr,Pred)) :- format('~w{Var : ~w(Var)}',[ClingoAggr,Pred]).
579		b2asp_portray('#string'(S)) :- format('"~w"',[S]).
580		b2asp_portray(not(P)) :- write(' not '), print(P).
581		b2asp_portray(BOP) :- clingo_bin_op(BOP,A,B,COP),print_clingo_val(A), format(' ~w ',[COP]), print_clingo_val(B).
582		clingo_bin_op('<='(A,B),A,B,'<=').
583		clingo_bin_op('!='(A,B),A,B,'!=').
584		clingo_bin_op(':='(A,B),A,B,':=').
585		clingo_bin_op('..'(A,B),A,B,'..').
586		print_clingo_val((A,B)) :- !, write('('), print(A), write(','), print(B), write(')'). % we need to print parentheses
587		print_clingo_val(A) :- print(A).
588		my_portray_clause(C) :- numbervars(C,0,_),print(C), write('.'),nl,fail.
589		my_portray_clause(_).
590
591		:- use_module(library(codesio), [format_to_codes/3,write_to_codes/2]).
592		% generate #count{Var : P(Var)} for a predicate P
593		gen_clingo_count_aggregate(Aggr,Pred,'#aggregate'(Aggr,Pred)).
594
595		% -------------------
596		% gensym: generate a fresh symbol (used for Clingo predicates for intermediate values)
597
598		:- dynamic counter/1.
599		counter(0).
600		gensym(Prefix,Symbol) :- retract(counter(N)), N1 is N+1,
601		assert(counter(N1)),
602		atom_codes(Prefix,PC),
603		number_codes(N,NC),
604		append(PC,[0'_|NC],PCNC),
605		atom_codes(Symbol,PCNC).
606
607		gensym_if_necessary(Prefix,Symbol) :- var(Symbol), !, gensym(Prefix,Symbol).
608		gensym_if_necessary(_,_).
609
610		reset_b2asp :-
611		retractall(counter(_)), assert(counter(0)),
612		retractall(generated_id(_,_)),
613		retractall(clingo_generated_id(_,_,_,_)).
614
615
616		% -------------------
617
618		% interface predicate to solve a B predicate with Clingo
619		% TODO: take LocalState into account
620		% if Exhaustive=exhaustive then contradiction found or all solutions will be generated upon backtracking
621		solve_pred_with_clingo(BPred,MaxNrSols,_LocalState,Res,Exhaustive) :-
622		run_clingo_on_formula(BPred,MaxNrSols,Res,Exhaustive).
623
624		run_clingo_on_formula(Formula) :- run_clingo_on_formula(Formula,1,_,_).
625		run_clingo_on_formula(Formula,MaxNrModels,Result,Exhaustive) :-
626		% write(user_output,Formula),nl(user_output),
627		reset_b2asp,
628		get_clingo_out_file(OutFile),
629		catch(tell(OutFile), % TODO: use streams and pass in environment
630		error(existence_error(_,_),_),
631		(add_b2asp_error('Path does not exist, be sure to set tmpdir preference correctly: ',OutFile),
632		fail)),
633		call_cleanup(top_level_trans(Formula),told),
634		!,
635		(debug_mode(on) -> show_file(OutFile) ; true),
636		run_clingo(OutFile,MaxNrModels,_,Result,Exhaustive).
637		run_clingo_on_formula(_,_,Result,non_exhaustive) :-
638		Result=no_solution_found(translation_failed).
639
640		show_file(File) :-
641		format('Contents of file ~w:~n',[File]),
642		format('% --------------~n',[]),
643		open(File,read,Stream),
644		call_cleanup(show_stream(Stream),close(Stream)),
645		format('% --------------~n',[]).
646
647		show_stream(Stream) :-
648		read_line(Stream,Line),
649		Line \= end_of_file,!,
650		format('~s~n',[Line]),
651		show_stream(Stream).
652		show_stream(_).
653
654		top_level_trans(Formula) :-
655		version_str(V),format('% Clingo encoding of B formula created by ProB ~w~n',[V]),
656		% we could call datime(datime(Yr,Mon,Day,Hr,Min,_Sec)),
657		(is_predicate(Formula) -> top_level_translate_predicate(Formula) ; trans_set(Formula,main)),!.
658		top_level_trans(Formula) :- add_b2asp_error('Could not translate: ',Formula).
659
660		:- use_module(library(file_systems),[file_exists/1]).
661
662		run_clingo(File,Result) :- run_clingo(File,1,_,Result,_).
663		run_clingo(File,MaxNrModels,WT,Result,Exhaustive) :-
664		statistics(walltime,[Start,_]),
665		(debug_mode(on) -> DOpt=['-V'] ; DOpt=[]),
666		(MaxNrModels<2 -> ModelsOpt='--models=1' % so that code works without ajoin
667		; ajoin(['--models=',MaxNrModels],ModelsOpt)),
668		OtherOptions = [ModelsOpt|DOpt] , % =0 outputs all models
669		debug_format(19,' Running CLINGO on ~w (options=~w)~n',[File,OtherOptions]),flush_output,
670		Options = [process(Process),stdout(pipe(JStdout,[encoding(utf8)])),
671		stderr(pipe(JStderr,[encoding(utf8)]))],
672		(get_clingo_path(Clingo), file_exists(Clingo)-> true
673		; get_clingo_path(Clingo) -> add_b2asp_error('Cannot find Clingo binary at (be sure to set path_to_clingo preference to point to clingo binary): ',Clingo),fail
674		; add_b2asp_error('Cannot find Clingo binary (be sure to set path_to_clingo preference to point to clingo binary)',''),fail
675		),
676		safe_process_create(Clingo, [File|OtherOptions], Options),
677		read_all(JStdout,Clingo,stdout,OutLines), % read before process_wait; avoid blocking clingo
678		read_all(JStderr,Clingo,stderr,ErrLines),
679		process_wait(Process,Exit),
680		% above almost corresponds to: system_call_with_options(Clingo,[File|OtherOptions],[],OutLines,ErrLines,ExitCode)
681		% except that here we do not call append/2 on OutLines and ErrLines
682		statistics(walltime,[Stop,_]), WT is Stop-Start,
683		format(' CLINGO walltime: ~w ms, ~w~n',[WT,Exit]),flush_output,
684		debug_format(19,'--- CLINGO OUTPUT ----~n',[]),flush_output,
685		process_clingo_output(OutLines,Models),
686		if((Exit=exit(Code), ErrText = [],
687		translate_clingo_exit_code(Code,Models,Result,Exhaustive)),
688		debug_format(19,'Clingo exit code = ~w -> ~w (~w)~n',[Code,Result,Exhaustive]),
689		(append(ErrLines,ErrText),
690		format('STD-ERROR (~w):~n~s~n',[Exit,ErrText]),
691		Result=no_solution_found(Exit))
692		).
693
694
695		% see https://github.com/potassco/clasp/issues/42#issuecomment-459981038%3E
696		translate_clingo_exit_code(0,_,no_solution_found('E_UNKNOWN'),non_exhaustive).
697		translate_clingo_exit_code(1,_,no_solution_found('E_INTERRUPT'),non_exhaustive).
698		translate_clingo_exit_code(33,_,no_solution_found('E_MEMORY'),non_exhaustive).
699		translate_clingo_exit_code(65,_,no_solution_found('E_ERROR'),non_exhaustive).
700		translate_clingo_exit_code(128,_,no_solution_found('E_NO_RUN'),non_exhaustive).
701		translate_clingo_exit_code(20,_,contradiction_found,exhaustive). % UNSATISFIABLE (E_EXHAUST)
702		translate_clingo_exit_code(10,Sols,solution(Sol),non_exhaustive) :-
703		get_sol(Sols,Sol). % E_SAT = 10, /*!< At least one model was found.
704		translate_clingo_exit_code(30,Sols,solution(Sol),exhaustive) :-
705		get_sol(Sols,Sol). %all_solutions_found (E_EXHAUST)
706
707		get_sol([Sol|T],R) :- !, member(R,[Sol|T]).
708		get_sol(L,R) :- add_b2asp_error('Unexpected clingo solution: ',L), R=[].
709
710		get_first_sol([Sol|_],R) :- !, R=Sol.
711		get_first_sol(L,R) :- add_b2asp_error('Unexpected clingo solution: ',L), R=[].
712
713		% process clingo output stream and extract answers (stable models)
714		process_clingo_output([],[]).
715		process_clingo_output([[0'\n]|T],Models) :- !, process_clingo_output(T,Models).
716		process_clingo_output([Line|T],Models) :- debug_format(19,'>>> ~s~n',[Line]),
717		clingo_answer_line(Nr,Line,[]), !,
718		process_clingo_model_line(T,Nr,Models).
719		process_clingo_output([_|T],Models) :- process_clingo_output(T,Models).
720
721		process_clingo_model_line([[0'\n]|T],Nr,Models) :- !, process_clingo_model_line(T,Nr,Models).
722		process_clingo_model_line([ModelLine|T],Nr,[BSolution|TM]) :- clingo_model(Model,ModelLine,[]), !,
723		debug_format(19,'>>> ~s~n',[ModelLine]),
724		length(Model,Len),
725		format('Parsed clingo model ~w with ~w relevant atoms~n',[Nr,Len]),
726		sort(Model,SModel), % TODO: extract solution for registered identifiers
727		keyclumped(SModel,Groups),
728		%write(Groups),nl,
729		translate_clingo_model_to_bindings(Groups,BSolution),
730		%write(BSolution),nl,
731		process_clingo_output(T,TM).
732		process_clingo_model_line(T,Nr,Models) :-
733		add_b2asp_error('Could not parse clingo model answer: ',Nr),
734		process_clingo_output(T,Models).
735
736		% TRANSLATING clingo model atoms back to B values
737		% -----------------------------------------------
738
739		translate_clingo_model_to_bindings(Model,Bindings) :-
740		findall(expected(Pred,Kind,BaseType,BID),clingo_generated_id(Pred,Kind,BaseType,BID),ExpectedPreds),
741		sort(ExpectedPreds,SExpectedPreds),
742		translate_clingo_model_to_bindings3(Model,SExpectedPreds,Bindings).
743
744		translate_clingo_model_to_bindings3([],[],Sol) :- !, Sol=[].
745		translate_clingo_model_to_bindings3([Pred-ModelArgs|TM],[expected(Pred,Kind,BaseType,BID)|ET],
746		[bind(BID,BVal)|BT]) :- !,
747		translate_clingo_value(Kind,BaseType,ModelArgs,BVal),
748		translate_clingo_model_to_bindings3(TM,ET,BT).
749		translate_clingo_model_to_bindings3(Model,[expected(Pred,Kind,_BaseType,BID)|ET],
750		[bind(BID,BVal)|BT]) :- !,
751		(Kind=set
752		-> debug_format(19,'Setting set to empty: ~w (~w)~n',[Pred,BID]),
753		BVal=[] % the clingo identifier represents a set, we have no facts meaning the set is empty
754		; add_b2asp_error('No value for clingo scalar in model: ',Pred),
755		BVal=term(undefined)
756		),
757		translate_clingo_model_to_bindings3(Model,ET,BT).
758
759		% translate a solution for a clingo identifier back to a B value
760		translate_clingo_value(scalar,BaseType,[[ClingoVal]],BVal) :- !, translate_clingo_scalar(BaseType,ClingoVal,BVal).
761		translate_clingo_value(scalar,BaseType,[Sol1|T],BVal) :- !,
762		add_b2asp_warning('Unexpected multiple solutions for clingo scalar: ',[Sol1|T]),
763		translate_clingo_scalar(BaseType,Sol1,BVal).
764		translate_clingo_value(set,BaseType,Sols,BValSetAsList) :-
765		maplist(translate_clingo_arg(BaseType),Sols,BValSetAsList).
766
767		translate_clingo_arg(BaseType,[ClingoVal],BVal) :- translate_clingo_scalar(BaseType,ClingoVal,BVal).
768		% translate_clingo_arg(BaseType,[ClingoVal1,ClingoVal2],BVal) :- ... convert to B pairs
769
770		% translate a solution for a clingo scalar back to a B value
771		translate_clingo_scalar(integer,Nr,BV) :- integer(Nr),!, BV=int(Nr).
772		translate_clingo_scalar(interval(_,_),Nr,BV) :- integer(Nr),!, BV=int(Nr).
773		translate_clingo_scalar(boolean,pred_false,BV) :- !, BV=pred_false.
774		translate_clingo_scalar(boolean,pred_true,BV) :- !, BV=pred_true.
775		translate_clingo_scalar(couple(TA,TB),(CA,CB),(BA,BB)) :- !,
776		translate_clingo_scalar(TA,CA,BA),
777		translate_clingo_scalar(TB,CB,BB).
778		%translate_clingo_scalar(global(_GS),ID,FDVAL) :- atom(ID),!, lookup_global_constant(ID,FDVAL).
779		translate_clingo_scalar(global(GS),Nr,FDVAL) :- integer(Nr),!, FDVAL=fd(Nr,GS).
780		translate_clingo_scalar(T,V,term(V)) :- add_b2asp_warning('Unknown clingo scalar: ',T:V).
781
782		% PARSING CODE for clingo OUTPUT
783		% ---------------------
784		% detect line like Answer: 1 (Time: 0.003s)
785		clingo_answer_line(Nr) --> "Answer: ",clingo_number(Nr), anything.
786
787		clingo_number(Nr) --> digit(X), !, answer_nr_rest(R), {number_codes(Nr,[X|R])}.
788		clingo_number(MinusNr) --> "-", digit(X), !, answer_nr_rest(R), {number_codes(Nr,[X|R]),MinusNr is -Nr}.
789		answer_nr_rest([X|T]) --> digit(X), !, answer_nr_rest(T).
790		answer_nr_rest([]) --> "".
791
792		anything --> [_],!,anything.
793		anything --> "".
794
795		% a clingo identifier (TODO check that this conforms to clingo syntax)
796		clingo_identifier(ID) --> letter(H), !, id2(T), {atom_codes(ID,[H|T])}.
797		id2([H|T]) --> letter(H),!, id2(T).
798		id2([H|T]) --> digit(H),!, id2(T).
799		id2([95|T]) --> "_",!, id2(T).
800		id2([]) --> "".
801
802		% a single stable model generated by clingo, a list of ground atoms separated by single whitespace
803		clingo_model(M) --> " ", !, clingo_model(M).
804		clingo_model(Model) --> clingo_atom(Pred,Args),
805		{(clingo_generated_id(Pred,_,_,_) -> Model = [Pred-Args|T] ; Model = T)},
806		clingo_model(T).
807		clingo_model([]) --> "".
808
809		% a single clingo atom either a ground predicate p(2), p((2,3)), or p(2,3) or a proposition p
810		clingo_atom(Pred,Args) --> clingo_identifier(Pred), clingo_opt_args(Args).
811		clingo_opt_args(Args) --> "(", !, clingo_args(Args),")".
812		clingo_opt_args([]) --> "". % for propositions without arguments
813		clingo_args([A|T]) --> clingo_constant(A),!, clingo_args2(T).
814		clingo_args([(A,B)|T]) --> clingo_pair(A,B),!, clingo_args2(T).
815
816		clingo_constant(A) --> clingo_number(A).
817		clingo_constant(A) --> clingo_identifier(A).
818
819		clingo_args2(T) --> ",", clingo_args(T).
820		clingo_args2([]) --> "".
821
822		clingo_pair(A,B) --> "(", clingo_constant(A),",", clingo_constant(B),")".
823
824		letter(X) --> [X], {letter(X)}.
825		digit(X) --> [X], {digit(X)}.
826		letter(X) :- (X >= 97, X =< 122) ; (X >= 65, X=< 90). % underscore = 95, minus = 45
827		digit(X) :- X >= 48, X =< 57.
828
829		% ---------
830
831		% read all characters from a stream
832		read_all(S,Command,Pipe,Lines) :-
833		call_cleanup(read_all1(S,Command,Pipe,Lines),
834		close(S)).
835		read_all1(S,Command,Pipe,Lines) :-
836		catch(read_all2(S,Lines), error(_,E), ( % E could be system_error('SPIO_E_ENCODING_INVALID')
837		ajoin(['Error reading ',Pipe,' for "',Command,'" due to exception: '],Msg),
838		add_error(system_call,Msg,E),
839		fail
840		)).
841		read_all2(S,Text) :-
842		read_line(S,Line),
843		( Line==end_of_file -> Text=[[]]
844		;
845		Text = [Line, [0'\n] | Rest],
846		read_all2(S,Rest)).
847
848		% -------------------
849		% some tests/examples:
850
851		test(0) :-trans_set(union(empty_set, intersection(set_extension([1,2]), set_extension([2,3]))), main).
852		test(1) :-trans_set(union(empty_set, set_subtraction(set_extension([1,2]), set_extension([2,3]))), main).
853
854		test(2) :- tell('out2.lp'),
855		trans_set(union(set_extension([4]), intersection(set_extension([1,2]), set_extension([2,3]))), main),
856		told.
857		test(3) :- run_clingo_on_formula( set_subtraction(set_extension([1,2+2,5 mod 2]), set_extension([2,4])) ).
858		test(4) :- run_clingo_on_formula( set_subtraction(set_extension([1,2+2,2+4]), interval(2,4)) ).
859		test(5) :- run_clingo_on_formula( set_subtraction(interval(1,100), interval(3,98)) ).
860		test(6) :- run_clingo_on_formula( set_extension([card(set_subtraction(interval(1,100), interval(3,98)))]) ).
861		test(7) :- run_clingo_on_formula( equal(add(identifier(x,interval(1,10)),integer(5)), integer(11))).
862		test(8) :- run_clingo_on_formula( subset(interval(1,5),
863		union(identifier(x,interval(2,6)),set_extension([1])))).
864		test(9) :- run_clingo_on_formula( set_equal(interval(1,5),
865		union(identifier(x,interval(2,6)),set_extension([1])))).
866		test(10) :- run_clingo_on_formula( not_set_equal(interval(1,5),
867		union(identifier(x,interval(2,6)),interval(1,5)))).
868		test(11) :- run_clingo_on_formula( conjunct( subset(interval(1,5),identifier(x,interval(0,6))),
869		subset(identifier(x,interval(0,6)), interval(1,6)))).
870		test(12) :- run_clingo_on_formula( conjunct( conjunct( member(3,identifier(x,interval(0,4))),
871		member(4,identifier(x,interval(0,4)))),
872		not_member(1,identifier(x,interval(0,4))))).
873		test(13) :- run_clingo_on_formula( conjunct( equivalence( member(3,identifier(x,interval(0,4))),
874		member(4,identifier(x,interval(0,4)))),
875		member(4,identifier(x,interval(0,4))))).
876		test(14) :- run_clingo_on_formula( set_equal( union(interval(1,100),set_extension([identifier(x,interval(0,200))])),
877		interval(1,101))). % small performance test
878		test(15) :- run_clingo_on_formula( set_equal( union(identifier(s,boolean),set_extension([identifier(x,boolean)])),
879		set_extension([pred_true,pred_false]))).
880		test(16) :- run_clingo_on_formula( conjunct( less(integer(3),identifier(x,interval(0,6))),
881		greater(integer(5),identifier(x,interval(0,6))))).
882		test(17) :- run_clingo_on_formula( conjunct( less(integer(1),card(identifier(x,interval(0,6)))),
883		greater(integer(3),card(identifier(x,interval(0,6)))))).
884		test(18) :- run_clingo_on_formula( b(equal(b(card(b(identifier(x),set(boolean),'.'(nodeid(p4(-1,1,6,7)),[]))),
885		integer,'.'(nodeid(p4(-1,1,1,8)),[])),b(integer(2),integer,'.'(nodeid(p4(-1,1,9,10)),[]))),
886		pred,'.'(removed_typing,'.'(nodeid(p4(-1,1,1,10)),[])))). % ProB AST example
887		test(19) :- run_clingo_on_formula( conjunct(equal(max(identifier(x,interval(1,10))),integer(3)),
888		equal(card(identifier(x,interval(1,10))),integer(2)))).
889		test(20) :- run_clingo_on_formula(set_extension([string(test1),string(test2)])).
890		test(21) :- run_clingo_on_formula(set_extension([(1,2)])).
891		test(22) :- run_clingo_on_formula(reverse(set_extension([(1,2)]))).
892		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)),[])))).
893		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)),[])))).
894		/*
895
896		$ more out.lp
897		main(4).
898
899		unleft0(1).
900
901		unleft0(2).
902
903		unright1(2).
904
905		unright1(3).
906
907		main(A) :-
908		unleft0(A),
909		unright1(A).
910
911		$ clingo out.lp
912		clingo version 5.8.0
913		Reading from out.lp
914		Solving...
915		Answer: 1 (Time: 0.000s)
916		unright1(2) unright1(3) unleft0(1) unleft0(2) main(4) main(2)
917		SATISFIABLE
918
919		Models : 1
920		Calls : 1
921		Time : 0.000s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
922		CPU Time : 0.000s
923
924		some queries in probcli -repl that work
925
926		:clingo x+1=4
927		:clingo x+1=y & y+x=11
928		:clingo x <: 1..3 & x /= {} & card(x)=3
929		:clingo (x=2 => y=3) & (y=3 => x>0) & x>2
930		:clingo x<:BOOL & card(x)=2
931		:clingo (1,2)=(x,y-1)
932		:clingo x <: BOOL*BOOL & x/= {} & x<<:y
933		:clingo x : BOOL*BOOL & x=(TRUE,FALSE)
934		:clingo x : (1..2)*(1..2) & x=(1,2)
935		:clingo x <: (1..2)*(1..2) & x /= {}
936		:clingo x <: (1..2)*(1..2) & dom(x)=1..2 & ran(x)=1..1
937		:clingo x = {TRUE|->FALSE, FALSE|->TRUE}
938		:clingo x = {TRUE|->FALSE, FALSE|->TRUE} & res=closure1(x)
939		:clingo SIGMA(x).(x:1..3|x) = r
940
941		with prob_examples/public_examples/B/Benchmarks/phonebook7.mch:
942		:clingo-double-check x<:Code & card(x)=2 & x \/ y = Code & c1:x & c1:y
943		:clingo-double-check x<:Code*Code & dom(x)=Code & closure1(x)=Code*Code
944		with card(Name) = 10:
945		:clingo x<:Name*Name & dom(x)=Name & closure1(x)=Name*Name & card(x)<11
946
947		is now fast when encoding #card aggregate as literal (i.e., inlining it)
948		:clingo x <: (1..2)*(1..2) & x /= {} & card(x)=1
949
950		still too slow with minint=-128, maxint=127 (21 seconds):
951		:clingo x = {1|->2} & r=closure1(x)
952
953		with card(Name)=10
954		:clingo x<:Name*Name & dom(x)=Name & closure1(x)=Name*Name& card(x) < 10
955		% ProB finds contradiction immediately; Kodkod is also quite fast
956
957
958		future tests:
959		:clingo z<:1..3 & !x.(x:1..2 => x:z)
960		:clingo z<: 1..5 & !x.(x:0..5 => {y|y:1..x & y<7} /= z)
961		*/