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 | */ |