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