| 1 | % (c) 2025-2026 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_code_gen,[gen_clingo_fact/4, | |
| 6 | register_clingo_predicate/5, | |
| 7 | gen_clingo_pred_clause/5, | |
| 8 | gen_clingo_clause/5, | |
| 9 | gen_clingo_ic_constraint/1, | |
| 10 | gen_clingo_set_identifier/4, gen_clingo_scalar_identifier/4, | |
| 11 | gen_clingo_count_aggregate/4, | |
| 12 | gen_base_type_constraint/3, make_finite/3, % TODO: remove from export, move add_local_typed_ids inside | |
| 13 | conjoin_clingo_calls/3, | |
| 14 | clingo_format_comment/2, | |
| 15 | generated_id/2, deterministic_id_value/2, | |
| 16 | gensym_if_necessary/2, | |
| 17 | add_translation_error/2, add_translation_error/3, translation_error_occurred/0, | |
| 18 | reset_b2asp_code_gen/0]). | |
| 19 | ||
| 20 | :- if(current_module(module_information)). | |
| 21 | :- use_module(probsrc(module_information),[module_info/2]). | |
| 22 | :- module_info(group,b2asp). | |
| 23 | :- module_info(description,'Generate Clingo Predicates and Clauses.'). | |
| 24 | :- endif. | |
| 25 | ||
| 26 | :- use_module(library(lists)). | |
| 27 | :- use_module(library(ordsets),[ord_member/2, ord_intersection/3]). | |
| 28 | :- use_module(library(codesio), [format_to_codes/3]). | |
| 29 | :- use_module(clingo_interface,[register_clause_head/2, register_clingo_generated_id/4, clingo_generated_id/4, | |
| 30 | get_nr_of_registered_strings/1]). | |
| 31 | :- use_module(probsrc(error_manager)). | |
| 32 | :- use_module(probsrc(debug)). | |
| 33 | :- use_module(probsrc(preferences),[get_preference/2]). | |
| 34 | :- use_module(probsrc(b_global_sets),[b_get_fd_type_bounds/3, lookup_global_constant/2]). | |
| 35 | ||
| 36 | ||
| 37 | % Errors during the translation are recorded, so that clingo is not run on an incomplete translation: | |
| 38 | % the clingo program would then not encode the B formula and could produce wrong solutions or contradictions | |
| 39 | :- dynamic translation_error_occurred/0. | |
| 40 | add_translation_error(Msg,Args) :- add_error(b2asp,Msg,Args), set_translation_error. | |
| 41 | add_translation_error(Msg,Args,Span) :- add_error(b2asp,Msg,Args,Span), set_translation_error. | |
| 42 | set_translation_error :- (translation_error_occurred -> true ; assertz(translation_error_occurred)). | |
| 43 | ||
| 44 | % call before generating first clause of a Clingo predicate | |
| 45 | % BPred is the B predicate for which this clause is generated | |
| 46 | % this predicate will try and filter unused local identifiers away | |
| 47 | register_clingo_predicate(SourcePrefix,BPred,FPred,Env,NewEnv) :- | |
| 48 | var(FPred), | |
| 49 | Env = env(LocalEnv,Bounds), LocalEnv = [_|_], % at least one local variable to possible filter away | |
| 50 | gensym_if_necessary(SourcePrefix,Pred), | |
| 51 | bsyntaxtree:find_identifier_uses(BPred, [], UsedIds), | |
| 52 | maplist(get_local_id,LocalEnv,EnvVars), sort(EnvVars,SE), | |
| 53 | ord_intersection(SE,UsedIds,UsefulIds), | |
| 54 | include(local_id_is_used(UsefulIds),LocalEnv,FilteredEnv), | |
| 55 | %format(user_output,'ids for ~w : ~w : used ~w : local ~w~n',[Pred,UsefulIds,UsedIds,EnvVars]), | |
| 56 | !, | |
| 57 | FPred = filter_pred(Pred,UsefulIds), | |
| 58 | NewEnv = env(FilteredEnv,Bounds). | |
| 59 | register_clingo_predicate(SourcePrefix,_BPred,Pred,Env,Env) :- | |
| 60 | gensym_if_necessary(SourcePrefix,Pred). | |
| 61 | ||
| 62 | ||
| 63 | ||
| 64 | ||
| 65 | % generate a Clingo clause and predicate name if necessary, at the moment we just print it onto user_output | |
| 66 | gen_clingo_pred_clause(SourcePrefix,Pred,ArgList,Env,Body) :- | |
| 67 | add_env_local_ids_to_arg_list(Pred,ArgList,Env,NewArgList), | |
| 68 | env_setup_code(Env,Pred,SetupCode), | |
| 69 | gen_clingo_pred_clause4(SourcePrefix,Pred,NewArgList,(SetupCode,Body)). | |
| 70 | ||
| 71 | gen_clingo_pred_clause4(SourcePrefix,Pred,ArgList,Body) :- | |
| 72 | gensym_if_necessary(SourcePrefix,Pred), | |
| 73 | %nl, | |
| 74 | gen_clingo_clause3(Pred,ArgList,Body). | |
| 75 | ||
| 76 | ||
| 77 | gen_clingo_clause(SourcePrefix,Pred,ArgList,Env,Body) :- | |
| 78 | gensym_if_necessary(SourcePrefix,Pred), | |
| 79 | gen_clingo_clause4(Pred,ArgList,Env,Body). | |
| 80 | ||
| 81 | % generate a Clingo clause for a predicate that has already been generated | |
| 82 | gen_clingo_clause4(Pred,ArgList,Env,Body) :- | |
| 83 | add_env_local_ids_to_arg_list(Pred,ArgList,Env,NewArgList), | |
| 84 | env_setup_code(Env,Pred,SetupCode), | |
| 85 | gen_clingo_clause3(Pred,NewArgList,(SetupCode,Body)). | |
| 86 | gen_clingo_clause3(Pred,ArgList,Body) :- | |
| 87 | construct_clingo_pred_call(Pred,ArgList,Head), | |
| 88 | register_clause_head(Pred,ArgList), | |
| 89 | simplify_body(Body, SimplifiedBody), | |
| 90 | my_portray_clause( Head , SimplifiedBody ). | |
| 91 | ||
| 92 | gen_clingo_ic_constraint(Body) :- | |
| 93 | simplify_body(Body, SimplifiedBody), | |
| 94 | nl, | |
| 95 | my_portray_clause( ( :- SimplifiedBody ) ). | |
| 96 | ||
| 97 | % ----------- | |
| 98 | ||
| 99 | % generate a Clingo fact | |
| 100 | gen_clingo_fact(Prefix,Pred,ArgList,Env) :- | |
| 101 | gensym_if_necessary(Prefix,Pred), | |
| 102 | add_env_local_ids_to_arg_list(Pred,ArgList,Env,NewArgList), | |
| 103 | env_setup_code(Env,Pred,Code), simplify_body(Code,SCode), | |
| 104 | construct_clingo_pred_call(Pred,NewArgList,Head), | |
| 105 | register_clause_head(Pred,NewArgList), | |
| 106 | my_portray_clause( Head, SCode ). | |
| 107 | ||
| 108 | ||
| 109 | % ----------- | |
| 110 | ||
| 111 | ||
| 112 | % filter out true literals and rewrite call/2 and call/3 literals | |
| 113 | simplify_body(X,R) :- var(X),!,R=X. | |
| 114 | simplify_body((A,B),Res) :- !, | |
| 115 | ( A=true -> simplify_body(B,Res) | |
| 116 | ; B=true -> simplify_body(A,Res) | |
| 117 | ; simplify_body(A,SA), simplify_body(B,SB), conjoin_clingo_calls(SA,SB,Res)). | |
| 118 | simplify_body(call(Pred,Arg),Call) :- !, Call =.. [Pred,Arg]. | |
| 119 | simplify_body(call(Pred,Arg1,Arg2),Call) :- !, Call =.. [Pred,Arg1,Arg2]. | |
| 120 | simplify_body(not(B),not(SB)) :- !, simplify_body(B,SB). % TODO: remove double not ? | |
| 121 | simplify_body(ecall(Pred,ArgList,Env),Call) :- !, | |
| 122 | (var(Pred) -> add_internal_error('Unknown ecall predicate: ',simplify_body(ecall(Pred,ArgList,Env),Call)) ; true), | |
| 123 | % ecall are calls where we add the local variables from the environment | |
| 124 | add_env_local_ids_to_arg_list(Pred,ArgList,Env,NewArgList), | |
| 125 | construct_clingo_pred_call(Pred,NewArgList,Call). | |
| 126 | simplify_body(ecall(Pred,Env),Call) :- !, | |
| 127 | add_env_local_ids_to_arg_list(Pred,[],Env,NewArgList), | |
| 128 | construct_clingo_pred_call(Pred,NewArgList,Call). | |
| 129 | simplify_body('='(A,B),'='(SA,SB)) :- !, simplify_expr(A,SA), simplify_expr(B,SB). | |
| 130 | simplify_body('=='(A,B),'=='(SA,SB)) :- !, simplify_expr(A,SA), simplify_expr(B,SB). | |
| 131 | simplify_body('!='(A,B),'!='(SA,SB)) :- !, simplify_expr(A,SA), simplify_expr(B,SB). | |
| 132 | simplify_body(B,B). | |
| 133 | ||
| 134 | % we need to flatten conjunctions, clingo can not deal with goals with arbitrary use of ( , ) | |
| 135 | conjoin_clingo_calls(true,B,Res) :- !, Res=B. | |
| 136 | conjoin_clingo_calls((A,B),C,Res) :- !, Res=(A,BC), conjoin_clingo_calls(B,C,BC). | |
| 137 | conjoin_clingo_calls(A,true,Res) :- !, Res=A. | |
| 138 | conjoin_clingo_calls(A,B,(A,B)). | |
| 139 | ||
| 140 | simplify_expr(X,R) :- var(X),!,R=X. | |
| 141 | simplify_expr(call(Pred,Arg),Call) :- !, Call =.. [Pred,Arg]. | |
| 142 | simplify_expr(call(Pred,Arg1,Arg2),Call) :- !, Call =.. [Pred,Arg1,Arg2]. | |
| 143 | simplify_expr(B,B). | |
| 144 | ||
| 145 | % ----------------------------- | |
| 146 | ||
| 147 | construct_clingo_pred_call(Pred,NewArgList,Call) :- %format(user_output,'Gen: ~w ~w~n',[Pred,NewArgList]), | |
| 148 | var(Pred),!, | |
| 149 | add_internal_error('Unknown Clingo predicate: ',construct_clingo_pred_call(Pred,NewArgList,Call)), | |
| 150 | set_translation_error, | |
| 151 | Call = fail. | |
| 152 | construct_clingo_pred_call(filter_pred(Pred,_Ids),NewArgList,Call) :- !, | |
| 153 | Call =.. [Pred|NewArgList]. | |
| 154 | construct_clingo_pred_call(Pred,NewArgList,Call) :- | |
| 155 | Call =.. [Pred|NewArgList]. | |
| 156 | ||
| 157 | % add environment local variables at end of argument list of a Clingo Predicate | |
| 158 | % these local quantified variables need to be passed as extra parameters (e.g., inside forall) | |
| 159 | :- mode add_env_local_ids_to_arg_list(+ClingoPred,+Args,+Env,-NewArgList). | |
| 160 | add_env_local_ids_to_arg_list(Pred,A,_,R) :- | |
| 161 | nonvar(Pred), top_level_or_auxiliary_clingo_pred(Pred), !, | |
| 162 | R=A. % At the moment we do not support exists inside forall,...: do not add anything | |
| 163 | add_env_local_ids_to_arg_list(Pred,ArgList,env(Env,_),NewArgList) :- | |
| 164 | nonvar(Pred), Pred = filter_pred(_,UsefulIds), | |
| 165 | include(local_id_is_used(UsefulIds),Env,FilteredEnv), | |
| 166 | maplist(get_var,FilteredEnv,EnvVars),!, | |
| 167 | append(ArgList,EnvVars,NewArgList). | |
| 168 | add_env_local_ids_to_arg_list(_,ArgList,env(Env,_),NewArgList) :- | |
| 169 | maplist(get_var,Env,EnvVars),!, | |
| 170 | append(ArgList,EnvVars,NewArgList). | |
| 171 | add_env_local_ids_to_arg_list(_,_,Env,_) :- | |
| 172 | add_translation_error('Illegal environment: ',Env),fail. | |
| 173 | ||
| 174 | get_var(local_id(_,_,_,VAR),VAR). | |
| 175 | get_local_id(local_id(Id,_,_,_),Id). | |
| 176 | ||
| 177 | local_id_is_used(UsedIds,local_id(Id,_,_,_)) :- ord_member(Id,UsedIds). | |
| 178 | ||
| 179 | top_level_or_auxiliary_clingo_pred(Pred) :- clingo_generated_id(Pred,_,_,_ID). | |
| 180 | top_level_or_auxiliary_clingo_pred(Pred) :- auxiliary_clingo_pred(Pred,_). | |
| 181 | ||
| 182 | ||
| 183 | % ------------------------------ | |
| 184 | ||
| 185 | ||
| 186 | % code to setup bounded possible values for local ids in environment | |
| 187 | % required to make Clingo clauses safe | |
| 188 | env_setup_code(env(Local,_),Pred,Code) :- env_setup_code2(Local,Pred,Code). | |
| 189 | env_setup_code2([],_,true). | |
| 190 | env_setup_code2([local_id(_ID,_Type,BaseType,Var)|T],Pred,(CodeToSetupID,RestCode)) :- | |
| 191 | % todo: filter out local variables that are not needed by Pred | |
| 192 | gen_base_type_constraint(BaseType,Var,CodeToSetupID), | |
| 193 | env_setup_code2(T,Pred,RestCode). | |
| 194 | ||
| 195 | % creates base-type constraints that can be used in body of a clause to constrain the possible values of a local id | |
| 196 | % see also gen_clingo_base_set | |
| 197 | gen_base_type_constraint(integer,Var, Constraint) :- !, | |
| 198 | get_min_int(MinInt), get_max_int(MaxInt), | |
| 199 | add_warning(b2asp,'Restricting infinite integer base type of local id to:',(MinInt,MaxInt)), | |
| 200 | gen_base_type_constraint(integer_in_range(MinInt,MaxInt,integer),Var,Constraint). | |
| 201 | gen_base_type_constraint(integer_in_range(From,To,_),Var, Constraint) :- !, | |
| 202 | make_interval_finite(From,To,'?',From2,To2),Constraint = (Var = '..'(From2,To2)). | |
| 203 | gen_base_type_constraint(string,Var, Constraint) :- !, | |
| 204 | get_nr_of_registered_strings(Nr), | |
| 205 | add_warning(b2asp,'Restricting infinite string base type to:',(0,Nr)), | |
| 206 | Constraint = (Var = '..'(0,Nr)). | |
| 207 | gen_base_type_constraint(string_in_list(List),Var, Constraint) :- !, | |
| 208 | (List=[] -> Constraint = (1=2) ; list_to_disj(List,Disj), Constraint = (Var=Disj)). | |
| 209 | gen_base_type_constraint(boolean,Var, Constraint) :- !, Constraint = (Var=(pred_true ; pred_false)). | |
| 210 | gen_base_type_constraint(global(GS),Var, Constraint) :- | |
| 211 | b_get_fd_type_bounds(GS,Low,Up), !, | |
| 212 | gen_base_type_constraint(integer_in_range(Low,Up,integer),Var,Constraint). | |
| 213 | %TODO: couples | |
| 214 | gen_base_type_constraint(empty_set,_Var, Constraint) :- !, Constraint = (1=2). | |
| 215 | gen_base_type_constraint(couple(TA,TB),Var,Constraint) :- !, | |
| 216 | Constraint = ('='(Var,(VarA,VarB)), CA, CB), | |
| 217 | gen_base_type_constraint(TA,VarA,CA), gen_base_type_constraint(TB,VarB,CB). | |
| 218 | %gen_base_type_constraint(set(integer_in_range(From,To)),Var, Constraint) :- !, | |
| 219 | % gen_base_type_constraint(integer_in_range(From,To),Var, Constraint) | |
| 220 | gen_base_type_constraint(seq(BaseType),_Var,true) :- !, | |
| 221 | add_translation_error('Seq base type not supported for local ids: ',seq(BaseType)). | |
| 222 | gen_base_type_constraint(set(BaseType),_Var,true) :- !, | |
| 223 | add_translation_error('Set base type not supported for local ids: ',set(BaseType)). | |
| 224 | gen_base_type_constraint(BaseType,_Var,true) :- | |
| 225 | add_translation_error('Unknown or unsupported base type for local id: ',BaseType). | |
| 226 | ||
| 227 | list_to_disj([X],R) :- !, R=X. | |
| 228 | list_to_disj([X,Y|T],';'(X,R)) :- list_to_disj([Y|T],R). | |
| 229 | ||
| 230 | ||
| 231 | get_min_int(X) :- get_preference(minint,X). | |
| 232 | get_max_int(X) :- get_preference(maxint,X). | |
| 233 | ||
| 234 | % ------------------------------------------------------- | |
| 235 | ||
| 236 | % Insert a comment into the generated code | |
| 237 | clingo_format_comment(FormatStr,Args) :- (debug_mode(on) -> nl ; true), | |
| 238 | format(FormatStr,Args). | |
| 239 | ||
| 240 | :- dynamic user:portray/2. | |
| 241 | :- assertz( ( user:portray(X) :- b2asp_portray(X))). | |
| 242 | ||
| 243 | :- public b2asp_portray/1. | |
| 244 | % TODO: implement a proper pretty_printing for clingo; rather than using portray/2 hook | |
| 245 | b2asp_portray('#clingo_range'(Low,Call,Up)) :- format('~w{~w}~w',[Low,Call,Up]). | |
| 246 | %b2asp_portray('#count'(Pred)) :- format('#count{Var : ~w(Var)}',[Pred]). | |
| 247 | b2asp_portray('#aggregate'(ClingoAggr,Pred,Env)) :- | |
| 248 | add_env_local_ids_to_arg_list(Pred,['Var'],Env,NewArgList), | |
| 249 | construct_clingo_pred_call(Pred,NewArgList,Call), | |
| 250 | format('~w{Var : ~w}',[ClingoAggr,Call]). | |
| 251 | b2asp_portray('#string'(S)) :- format('"~w"',[S]). | |
| 252 | b2asp_portray(not(P)) :- write(' not '), print(P). | |
| 253 | b2asp_portray(BOP) :- clingo_bin_op(BOP,A,B,COP),print_clingo_val(A), format(' ~w ',[COP]), print_clingo_val(B). | |
| 254 | clingo_bin_op('<='(A,B),A,B,'<='). | |
| 255 | clingo_bin_op('!='(A,B),A,B,'!='). | |
| 256 | clingo_bin_op(':='(A,B),A,B,':='). | |
| 257 | clingo_bin_op('..'(A,B),A,B,'..'). | |
| 258 | print_clingo_val((A,B)) :- !, write('('), print(A), write(','), print(B), write(')'). % we need to print parentheses | |
| 259 | print_clingo_val(A) :- print(A). | |
| 260 | ||
| 261 | my_portray_clause(Head,true) :- !, my_portray_clause(Head). | |
| 262 | my_portray_clause(Head,Body) :- my_portray_clause((Head :- Body)). | |
| 263 | ||
| 264 | my_portray_clause(C) :- numbervars(C,0,_),print(C), write('.'),nl,fail. | |
| 265 | my_portray_clause(_). | |
| 266 | ||
| 267 | % generate #count{Var : P(Var)} for a predicate P (also works for sum,...) | |
| 268 | gen_clingo_count_aggregate(Aggr,Pred,Env,'#aggregate'(Aggr,Pred,Env)). | |
| 269 | ||
| 270 | ||
| 271 | % ------------------------------------------------------- | |
| 272 | ||
| 273 | ||
| 274 | ||
| 275 | % ------------------------------ | |
| 276 | % generating CLINGO clauses,... | |
| 277 | ||
| 278 | :- dynamic generated_id/2, auxiliary_clingo_pred/2, deterministic_id_value/2. | |
| 279 | ||
| 280 | ||
| 281 | ||
| 282 | reset_b2asp_code_gen :- | |
| 283 | retractall(translation_error_occurred), | |
| 284 | retractall(counter(_)), assert(counter(0)), | |
| 285 | retractall(generated_id(_,_)), | |
| 286 | retractall(deterministic_id_value(_,_)), | |
| 287 | retractall(auxiliary_clingo_pred(_,_)). | |
| 288 | ||
| 289 | ||
| 290 | :- mode gen_clingo_scalar_identifier(+ID,+BaseType,+LocalID_Env,-ClingoPred). | |
| 291 | % generate a Clingo predicate to represent a B identifier whose value is a scalar | |
| 292 | gen_clingo_scalar_identifier(IDB,BaseType,Env,PredB) :- | |
| 293 | gen_clingo_scalar_identifier(IDB,BaseType,Env,PredB,top_level). | |
| 294 | ||
| 295 | gen_clingo_scalar_identifier(ID,_,_,Pred,_) :- nonvar(Pred), | |
| 296 | add_warning(b2asp,'Identifier Clingo Result should be unbound: ',ID:Pred),fail. | |
| 297 | gen_clingo_scalar_identifier(ID,_,_,Pred,_) :- % check if we have already created a Clingo predicate for ID | |
| 298 | generated_id(ID,P),!, Pred=P. % TODO: pass as environment and check bounds unchanged | |
| 299 | gen_clingo_scalar_identifier(ID,couple(A,B),Env,Pred,TopLevel) :- !, | |
| 300 | % improved translation of pairs, instead of 1 { id_pair_scalar_0((-127..128,-127..128))} 1. we generate: | |
| 301 | % id_pair_scalar_0((A,B)) :- id_A(A), id_B(B). | |
| 302 | % 1{id_A(-127..128)}1. 1{id_B(-127..128)}1. | |
| 303 | gensym(ID,IDA), | |
| 304 | gen_clingo_scalar_identifier(IDA,A,Env,PredA,left_pair), | |
| 305 | gensym(ID,IDB), | |
| 306 | gen_clingo_scalar_identifier(IDB,B,Env,PredB,right_pair), | |
| 307 | gensym_if_necessary(pair,Pred), | |
| 308 | assert_gen_id(ID,Pred,scalar,couple(A,B),TopLevel), | |
| 309 | clingo_format_comment('~n% clingo encoding of scalar identifier ~w of type ~w:~n',[ID,couple(A,B)]), | |
| 310 | gen_clingo_clause4(Pred,[(XA,XB)],Env, (ecall(PredA,[XA],Env), | |
| 311 | ecall(PredB,[XB],Env)) ). | |
| 312 | % create clause Pred((XA,XB)) :- PredA(XA), PredB(XB)). | |
| 313 | gen_clingo_scalar_identifier(ID,BaseType,_Env,Pred,TL) :- % generate: 1{Pred(Low..Up)}1. | |
| 314 | gen_clingo_base_set(BaseType,ID,ClingoType,_MaxCard,Prefix), | |
| 315 | atom_concat(Prefix,'_scalar',Prefix2), | |
| 316 | gensym_if_necessary(Prefix2,Pred), | |
| 317 | clingo_format_comment('~n% clingo encoding of scalar identifier ~w of type ~w:~n',[ID,BaseType]), | |
| 318 | format('1 { ~w(~w)} 1.~n',[Pred,ClingoType]), % TODO: add ENV !! | |
| 319 | assert_gen_id(ID,Pred,scalar,BaseType,TL), | |
| 320 | register_clause_head(Pred,[ClingoType]). % at the moment these identifiers all have arity of 1 (TODO: enable nesting) | |
| 321 | ||
| 322 | assert_gen_id(ID,Pred,Kind,BaseType,TL) :- | |
| 323 | (deterministic_value(BaseType,Value) -> assert(deterministic_id_value(ID,Value)) ; true), | |
| 324 | (TL=top_level | |
| 325 | -> assert(generated_id(ID,Pred)), | |
| 326 | register_clingo_generated_id(Pred,Kind,BaseType,ID), % for back-translating models from clingo | |
| 327 | debug_format(19,'Generating clingo pred. ~w for B ~w id ~w (type ~w)~n',[Pred,Kind,ID,BaseType]) | |
| 328 | ; assert(auxiliary_clingo_pred(Pred,TL)) % only register; no need to back-translate in model | |
| 329 | % these are intermediate ids, e.g., generated for pair left/right hand sides | |
| 330 | % TODO: check that we do not need to add other arguments; pass environment to asser_gen_id | |
| 331 | ). | |
| 332 | ||
| 333 | % detect deterministic values, so that we can inline their values | |
| 334 | % this can be important for #count cardinality constraints for clingo performance | |
| 335 | deterministic_value(integer_in_range(Low,Up,_),Low) :- number(Low), Low=Up. | |
| 336 | ||
| 337 | ||
| 338 | :- mode gen_clingo_set_identifier(+ID,+BaseType,-ClingoPred,+TopLevel). | |
| 339 | % generate a Clingo predicate to represent a B identifier whose value is a set | |
| 340 | %gen_clingo_set_identifier(IDB,BaseType,PredB) :- gen_clingo_set_identifier(IDB,BaseType,PredB,top_level). | |
| 341 | ||
| 342 | gen_clingo_set_identifier(ID,_,Pred,_) :- % check if we have already created a Clingo predicate for ID | |
| 343 | generated_id(ID,P),!, | |
| 344 | % TODO: pass as environment and check bounds unchanged | |
| 345 | (Pred=P -> true ; add_translation_error('Identifier already instantiated: ',ID:Pred),fail). | |
| 346 | % Note: we cannot use similar code as for scalars for pairs (the relation is not necessarily tuple-distributive) | |
| 347 | gen_clingo_set_identifier(ID,BaseType,Pred,TL) :- % generate: 1{Pred(Low..Up)}1. | |
| 348 | gen_clingo_base_set(BaseType,ID,ClingoType,MaxCard,Prefix), | |
| 349 | atom_concat(Prefix,'_set',Prefix2), | |
| 350 | gensym_if_necessary(Prefix2,Pred), | |
| 351 | clingo_format_comment('~n% clingo encoding of set identifier ~w of type ~w:~n',[ID,BaseType]), | |
| 352 | format('0 { ~w(~w)} ~w.~n',[Pred,ClingoType,MaxCard]), | |
| 353 | assert_gen_id(ID,Pred,set,BaseType,TL), | |
| 354 | register_clause_head(Pred,[ClingoType]). % at the moment these ids all have arity of 1 (TODO: enable nesting). | |
| 355 | ||
| 356 | :- use_module(probsrc(tools), [ajoin_with_sep/3]). | |
| 357 | ||
| 358 | % convert base type into a Clingo expression that can be put into the head of a fact, | |
| 359 | % together with information about the maximal cardinality of the base type and a prefix for generated identifiers | |
| 360 | gen_clingo_base_set(integer,ID,Atom,MaxCard,Prefix) :- !, | |
| 361 | gen_clingo_base_set(integer_in_range(inf,sup,integer),ID,Atom,MaxCard,Prefix). | |
| 362 | gen_clingo_base_set(string,ID,Atom,MaxCard,Prefix) :- !, | |
| 363 | gen_clingo_base_set(integer_in_range(inf,sup,string),ID,Atom,MaxCard,Prefix). | |
| 364 | %gen_clingo_base_set(integer_set_in_range(Low,Up),ID,Atom,MaxCard,Prefix) :- !, | |
| 365 | % gen_clingo_base_set(integer_in_range(Low,Up),ID,Atom,MaxCard,Prefix). | |
| 366 | gen_clingo_base_set(integer_in_range(Low0,Up0,Type),ID,Atom,MaxCard,Prefix) :- !, | |
| 367 | (Type=string | |
| 368 | -> atom_concat(id_string_,ID,Prefix), | |
| 369 | make_string_interval_finite(Low0,Up0,ID,Low,Up) | |
| 370 | ; atom_concat(id_int_,ID,Prefix), | |
| 371 | make_interval_finite(Low0,Up0,ID,Low,Up) | |
| 372 | ), | |
| 373 | (Up >= Low -> MaxCard is 1+Up-Low ; MaxCard=0), | |
| 374 | format_to_codes('~w..~w',[Low,Up],Codes), | |
| 375 | atom_codes(Atom,Codes). | |
| 376 | gen_clingo_base_set(string_in_list(List),ID,Atom,MaxCard,Prefix) :- !, atom_concat(id_string_,ID,Prefix), | |
| 377 | length(List,MaxCard), | |
| 378 | ajoin_with_sep(List,';',Atom). | |
| 379 | gen_clingo_base_set(boolean,ID,Atom,2,Prefix) :- !, atom_concat(id_bool_,ID,Prefix), | |
| 380 | Atom = 'pred_true;pred_false'. | |
| 381 | gen_clingo_base_set(global(GS),ID,Atom,MaxCard,Prefix) :- % user-defined enumerated sets or deferred sets | |
| 382 | b_get_fd_type_bounds(GS,Low,Up), !, atom_concat(id_glob_,ID,Prefix), | |
| 383 | gen_clingo_base_set(integer_in_range(Low,Up,integer),ID,Atom,MaxCard,_). % we translate those sets as integers | |
| 384 | gen_clingo_base_set(couple(A,B),ID,Atom,MaxCard,Prefix) :- !, atom_concat(id_pair_,ID,Prefix), | |
| 385 | gen_clingo_base_set(A,ID,AAtom,CardA,_), | |
| 386 | gen_clingo_base_set(B,ID,BAtom,CardB,_), | |
| 387 | MaxCard is CardA*CardB, | |
| 388 | 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 | |
| 389 | atom_codes(Atom,Codes). | |
| 390 | gen_clingo_base_set(empty_set,ID,Atom,0,Prefix) :- !, atom_concat(no_solution_,ID,Prefix), | |
| 391 | Atom = '2..1'. | |
| 392 | gen_clingo_base_set(set(BaseType),ID,error,1,id_error) :- !, | |
| 393 | add_translation_error('Expecting scalar base type: ',ID:set(BaseType)). | |
| 394 | gen_clingo_base_set(seq(BaseType),ID,error,1,id_error) :- !, | |
| 395 | add_translation_error('Expecting scalar base type: ',ID:seq(BaseType)). | |
| 396 | gen_clingo_base_set(BaseType,ID,error,1,id_error) :- add_translation_error('Unknown or unsupported base type: ',ID:BaseType). | |
| 397 | ||
| 398 | make_finite(integer,ID,FiniteType) :- !, make_finite(integer_in_range(inf,sup,integer),ID,FiniteType). | |
| 399 | make_finite(string,ID,FiniteType) :- !, | |
| 400 | make_finite(integer_in_range(inf,sup,string),ID,FiniteType). | |
| 401 | make_finite(integer_in_range(Low0,Up0,string),ID,integer_in_range(Low,Up,string)) :- !, | |
| 402 | make_string_interval_finite(Low0,Up0,ID,Low,Up). | |
| 403 | make_finite(integer_in_range(Low0,Up0,Type),ID,integer_in_range(Low,Up,Type)) :- !, | |
| 404 | make_interval_finite(Low0,Up0,ID,Low,Up). | |
| 405 | make_finite(couple(A,B),ID,couple(FA,FB)) :- !, make_finite(A,ID,FA), make_finite(B,ID,FB). | |
| 406 | make_finite(Type,_ID,Type). | |
| 407 | ||
| 408 | make_interval_finite(inf,sup,ID,X,Y) :- !, | |
| 409 | get_min_int(X), | |
| 410 | get_max_int(Y), | |
| 411 | add_warning(b2asp,'Restricting bounds of integer base type to: ',ID:(X,Y)). | |
| 412 | make_interval_finite(inf,Y,ID,X,Y) :- !, | |
| 413 | get_min_int(Min), (Min =< Y -> X=Min ; X=Y), | |
| 414 | add_warning(b2asp,'Restricting lower-bound of integer base type to: ',ID:(X,Y)). | |
| 415 | make_interval_finite(X,sup,ID,X,Y) :- !, | |
| 416 | get_max_int(Mx), (Mx>= X -> Y=Mx ; Y=X), | |
| 417 | add_warning(b2asp,'Restricting upper-bound of integer base type to: ',ID:(X,Y)). | |
| 418 | make_interval_finite(A,B,ID,X,Y) :- (\+ integer(A) ; \+ integer(B)), !, | |
| 419 | add_translation_error('Illegal integer base type:',ID:(A,B)), | |
| 420 | make_interval_finite(inf,sup,ID,X,Y). | |
| 421 | make_interval_finite(X,Y,_,X,Y). | |
| 422 | ||
| 423 | % strings are represented by the numbers 0..N of the registered strings (see register_formula_strings in b2asp); | |
| 424 | % other numbers do not correspond to a string | |
| 425 | make_string_interval_finite(Low0,Up0,ID,Low,Up) :- | |
| 426 | get_nr_of_registered_strings(N), | |
| 427 | (number(Low0) -> Low is max(0,Low0) ; Low=0), | |
| 428 | (number(Up0) -> Up is min(N,Up0) | |
| 429 | ; Up=N, add_warning(b2asp,'Restricting infinite string base type to the strings of the formula and fresh strings: ',ID:(Low,Up))). | |
| 430 | ||
| 431 | ||
| 432 | ||
| 433 | % ------------------- | |
| 434 | % gensym: generate a fresh symbol (used for Clingo predicates for intermediate values) | |
| 435 | ||
| 436 | :- dynamic counter/1. | |
| 437 | counter(0). | |
| 438 | gensym(Prefix,Symbol) :- retract(counter(N)), N1 is N+1, | |
| 439 | assert(counter(N1)), | |
| 440 | atom_codes(Prefix,PC), | |
| 441 | number_codes(N,NC), | |
| 442 | append(PC,[0'_|NC],PCNC), | |
| 443 | atom_codes(Symbol,PCNC). | |
| 444 | ||
| 445 | gensym_if_necessary(Prefix,Symbol) :- var(Symbol), !, gensym(Prefix,Symbol). | |
| 446 | gensym_if_necessary(_,_). | |
| 447 |