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