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