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