| 1 | % (c) 2021-2023 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 | :- module(set_rewriter, [rewrite_set_to_list_of_asts/3, | |
| 5 | rewrite_set_to_list_of_asts/4, | |
| 6 | avl_list_to_list_of_asts/4, | |
| 7 | rewrite_finite_card/3]). | |
| 8 | ||
| 9 | :- use_module(library(avl), [avl_to_list/2]). | |
| 10 | ||
| 11 | :- use_module(probsrc(b_global_sets), [enumerated_set/1, | |
| 12 | all_elements_of_type/2]). | |
| 13 | :- use_module(probsrc(preferences), [get_preference/2]). | |
| 14 | :- use_module(probsrc(bsyntaxtree), [get_integer/2, | |
| 15 | conjunct_predicates/2, | |
| 16 | disjunct_predicates/2, | |
| 17 | get_texpr_type/2, | |
| 18 | get_texpr_expr/2, | |
| 19 | safe_create_texpr/4]). | |
| 20 | ||
| 21 | :- use_module(probsrc(performance_messages), [perfmessage/3]). | |
| 22 | ||
| 23 | rewrite_set_to_list_of_asts(b(E,Type,Info), ScopeIds, L) :- | |
| 24 | rewrite_set_aux(E, Type, Info, ScopeIds, [], L). | |
| 25 | ||
| 26 | rewrite_set_to_list_of_asts(b(E,Type,Info), ScopeIds, Options, L) :- | |
| 27 | rewrite_set_aux(E, Type, Info, ScopeIds, Options, L). | |
| 28 | ||
| 29 | rewrite_set_aux(identifier(EnumSet), set(global(EnumSet)), Info, ScopeIds, _, SetAsts) :- | |
| 30 | enumerated_set(EnumSet), | |
| 31 | \+ memberchk(EnumSet, ScopeIds), | |
| 32 | \+ memberchk(introduced_by(_), Info), | |
| 33 | all_elements_of_type(EnumSet, SetValues), | |
| 34 | !, | |
| 35 | findall(b(value(Val),global(EnumSet),[]), member(Val, SetValues), SetAsts). | |
| 36 | rewrite_set_aux(boolean_set, _, _, _, _, L) :- | |
| 37 | !, | |
| 38 | L = [b(boolean_true,boolean,[]), b(boolean_false,boolean,[])]. | |
| 39 | rewrite_set_aux(interval(From,To), _, Info, _, Options, L) :- | |
| 40 | !, | |
| 41 | get_integer_constant(From, FI), | |
| 42 | get_integer_constant(To, TI), | |
| 43 | check_limit(FI, TI, Info, Options), | |
| 44 | !, | |
| 45 | constant_interval_as_list(FI, TI, L). | |
| 46 | rewrite_set_aux(set_extension(L), _, _, _, _, R) :- | |
| 47 | !, | |
| 48 | R = L. | |
| 49 | rewrite_set_aux(value(Value), Type, _, _, Options, L) :- nonvar(Value), | |
| 50 | !, | |
| 51 | rewrite_value(Value, Type, Options, L). | |
| 52 | rewrite_set_aux(cartesian_product(A,B), set(Type), _, ScopeIds, Options, L) :- !, | |
| 53 | rewrite_set_to_list_of_asts(A, ScopeIds, Options, AL), | |
| 54 | rewrite_set_to_list_of_asts(B, ScopeIds, Options, BL), | |
| 55 | findall(b(couple(VA,VB),Type,[]), (member(VA,AL),member(VB,BL)), L). | |
| 56 | %rewrite_set_aux(E, Type, _, L) :- write(impossible(E)), nl, fail. | |
| 57 | ||
| 58 | rewrite_value(global_set(EnumSet), _, _, L) :- | |
| 59 | enumerated_set(EnumSet), | |
| 60 | all_elements_of_type(EnumSet, SetValues), | |
| 61 | !, | |
| 62 | findall(b(value(Val),global(EnumSet),[]), member(Val, SetValues), L). | |
| 63 | rewrite_value(avl_set(AvlSet), Type, _, L) :- | |
| 64 | !, | |
| 65 | ( Type = set(InType) | |
| 66 | ; Type = seq(SeqType), | |
| 67 | InType = couple(integer,SeqType) | |
| 68 | ), | |
| 69 | avl_to_list(AvlSet, AvlList), | |
| 70 | avl_list_to_list_of_asts(InType, AvlList, [], L). | |
| 71 | rewrite_value(closure(P,T,B), _Type, Options, L) :- | |
| 72 | custom_explicit_sets:is_interval_closure(P,T,B,FI,TI), integer(FI),integer(TI), | |
| 73 | check_limit(FI, TI, B, Options), | |
| 74 | !, | |
| 75 | constant_interval_as_list(FI, TI, L). | |
| 76 | ||
| 77 | ||
| 78 | check_limit(FI, TI, Info, Options) :- | |
| 79 | Card is TI - FI, | |
| 80 | ( ( memberchk(instantiate_sets_limit(SetLimit), Options) -> true | |
| 81 | ; memberchk(instantiate_quantifier_limit(SetLimit), Options) | |
| 82 | ) | |
| 83 | -> ( Card =< SetLimit | |
| 84 | -> true | |
| 85 | ; perfmessage(quantifier,not_expanding_interval_in_quantifier(FI,TI,limit(SetLimit)),Info), | |
| 86 | fail | |
| 87 | ) | |
| 88 | ; true | |
| 89 | ). | |
| 90 | ||
| 91 | ||
| 92 | avl_list_to_list_of_asts(_, [], Acc, Acc). | |
| 93 | avl_list_to_list_of_asts(InType, [Val-_|T], Acc, L) :- | |
| 94 | avl_list_to_list_of_asts(InType, T, [b(value(Val),InType,[])|Acc], L). | |
| 95 | ||
| 96 | get_integer_constant(Ast, IntConst) :- | |
| 97 | get_integer(Ast, IntConst). | |
| 98 | get_integer_constant(b(min_int,integer,_), MinInt) :- | |
| 99 | get_preference(minint, MinInt). | |
| 100 | get_integer_constant(b(max_int,integer,_), MaxInt) :- | |
| 101 | get_preference(maxint, MaxInt). | |
| 102 | ||
| 103 | %% constant_interval_as_list(+Lower, +Upper, -List). | |
| 104 | constant_interval_as_list(FI,TI,[]) :- | |
| 105 | FI > TI. | |
| 106 | constant_interval_as_list(FI,FI,[BI]) :- | |
| 107 | !, %safe_create_texpr(integer(FI), integer, [], BI). | |
| 108 | BI = b(value(int(FI)),integer,[]). | |
| 109 | constant_interval_as_list(FI,TI,[BI|BIs]) :- | |
| 110 | %safe_create_texpr(integer(FI), integer, [], BI), | |
| 111 | BI = b(value(int(FI)),integer,[]), | |
| 112 | NFI is FI + 1, | |
| 113 | constant_interval_as_list(NFI,TI,BIs). | |
| 114 | ||
| 115 | %% rewrite_finite_card(+GL, -Res, -RuleDescr). | |
| 116 | % Rewrite some cardinality constraints on finite sets to prevent the translation to SMT-LIB using quantifiers. | |
| 117 | % TODO: card({a1,..,ak}) > j where j < k --> at least j equalities (watch out for exponential blowup) | |
| 118 | % TODO: card({a1,..,ak}) = k - 1 (watch out for exponential blowup) | |
| 119 | rewrite_finite_card(less(Card,Integer), Res, card_to_at_least_one_eq) :- | |
| 120 | % card({a1,..,ak}) < k --> at least one eq (has n*log(n) disjuncts) | |
| 121 | rewrite_finite_card_k_less_k(Card, Integer, Res). | |
| 122 | rewrite_finite_card(greater(Integer,Card), Res, card_to_at_least_one_eq) :- | |
| 123 | % k > card({a1,..,ak}) --> at least one eq (has n*log(n) disjuncts) | |
| 124 | rewrite_finite_card_k_less_k(Card, Integer, Res). | |
| 125 | rewrite_finite_card(less_equal(Card,Integer), Res, card_to_at_least_one_eq) :- | |
| 126 | % card({a1,..,ak}) <= k - 1 --> at least one eq (has n*log(n) disjuncts) | |
| 127 | rewrite_finite_card_k_leq_k_minus_1(Card, Integer, Res). | |
| 128 | rewrite_finite_card(greater_equal(Integer,Card), Res, card_to_at_least_one_eq) :- | |
| 129 | % k - 1 >= card({a1,..,ak}) --> at least one eq (has n*log(n) disjuncts) | |
| 130 | rewrite_finite_card_k_leq_k_minus_1(Card, Integer, Res). | |
| 131 | rewrite_finite_card(less_equal(Card,Integer), Res, card_to_truth_leq_k) :- | |
| 132 | % card({a1,..,ak}) <= k --> truth | |
| 133 | rewrite_finite_card_k_leq_k(Card, Integer, Res). | |
| 134 | rewrite_finite_card(greater_equal(Integer,Card), Res, card_to_truth_leq_k) :- | |
| 135 | % k >= card({a1,..,ak}) --> truth | |
| 136 | rewrite_finite_card_k_leq_k(Card, Integer, Res). | |
| 137 | rewrite_finite_card(less(Card,Integer), Res, card_to_truth_leq_k1) :- | |
| 138 | % card({a1,..,ak}) < k + 1 --> truth | |
| 139 | rewrite_finite_card_k_leq_k_plus_1(Card, Integer, Res). | |
| 140 | rewrite_finite_card(greater(Integer,Card), Res, card_to_truth_leq_k1) :- | |
| 141 | % k + 1 > card({a1,..,ak}) --> truth | |
| 142 | rewrite_finite_card_k_leq_k_plus_1(Card, Integer, Res). | |
| 143 | rewrite_finite_card(greater_equal(Card,Integer), Res, card_to_all_different_greater_eq) :- | |
| 144 | % card({a1,..,ak}) >= k --> all_different | |
| 145 | rewrite_finite_card_k_eq_k(Card, Integer, Res). | |
| 146 | rewrite_finite_card(less_equal(Integer,Card), Res, card_to_all_different_greater_eq) :- | |
| 147 | % k <= card({a1,..,ak}) --> all_different | |
| 148 | rewrite_finite_card_k_eq_k(Card, Integer, Res). | |
| 149 | rewrite_finite_card(greater(Card,Integer), Res, card_to_falsity) :- | |
| 150 | % card({a1,..,ak}) > n --> falsity if n>=k | |
| 151 | rewrite_finite_card_greater_less_k(Card, Integer, Res). | |
| 152 | rewrite_finite_card(less(Integer,Card), Res, card_to_falsity) :- | |
| 153 | % n < card({a1,..,ak}) --> falsity if n>=k | |
| 154 | rewrite_finite_card_greater_less_k(Card, Integer, Res). | |
| 155 | rewrite_finite_card(greater_equal(Card,Integer), Res, card_to_falsity) :- | |
| 156 | % card({a1,..,ak}) >= n --> falsity if n>k | |
| 157 | rewrite_finite_card_greatereq_lesseq_n(Card, Integer, Res). | |
| 158 | rewrite_finite_card(less_equal(Integer,Card), Res, card_to_falsity) :- | |
| 159 | % n <= card({a1,..,ak}) --> falsity if n>k | |
| 160 | rewrite_finite_card_greatereq_lesseq_n(Card, Integer, Res). | |
| 161 | rewrite_finite_card(greater(Card,Integer), Res, card_to_all_different_greater) :- | |
| 162 | % card({a1,..,ak}) > k - 1 --> all different | |
| 163 | rewrite_finite_card_greater_less_k1(Card, Integer, Res). | |
| 164 | rewrite_finite_card(less(Integer,Card), Res, card_to_all_different_greater) :- | |
| 165 | % k - 1 < card({a1,..,ak}) --> all different | |
| 166 | rewrite_finite_card_greater_less_k1(Card, Integer, Res). | |
| 167 | rewrite_finite_card(greater_equal(Card,Integer1), Res, card_to_truth) :- | |
| 168 | % card({a1,..,ak}) >= 1 --> truth | |
| 169 | rewrite_finite_card_geq_leq_1(Card, Integer1, Res). | |
| 170 | rewrite_finite_card(less_equal(Integer1,Card), Res, card_to_truth) :- | |
| 171 | % 1 <= card({a1,..,ak}) --> truth | |
| 172 | rewrite_finite_card_geq_leq_1(Card, Integer1, Res). | |
| 173 | rewrite_finite_card(equal(Card,Integer), Res, card_to_single_equality) :- | |
| 174 | % card({a1,a2}) = 1 --> a1=a2 | |
| 175 | rewrite_finite_card_2_eq_1(Card, Integer, Res). | |
| 176 | rewrite_finite_card(equal(Integer,Card), Res, card_to_single_equality) :- | |
| 177 | % 1 = card({a1,a2}) --> a1=a2 | |
| 178 | rewrite_finite_card_2_eq_1(Card, Integer, Res). | |
| 179 | rewrite_finite_card(not_equal(Card,Integer), Res, card_to_single_non_equality) :- | |
| 180 | % card({a1,a2}) /= 1 --> a1/=a2 | |
| 181 | rewrite_finite_card_2_neq_1(Card, Integer, Res). | |
| 182 | rewrite_finite_card(not_equal(Integer,Card), Res, card_to_single_non_equality) :- | |
| 183 | % 1 /= card({a1,a2}) --> a1/=a2 | |
| 184 | rewrite_finite_card_2_neq_1(Card, Integer, Res). | |
| 185 | rewrite_finite_card(equal(Card,Integer), Res, card_to_falsity_nonempty_eq_zero) :- | |
| 186 | % card({a1,..,ak}) = 0 --> falsity | |
| 187 | rewrite_finite_card_eq_0(Card, Integer, Res). | |
| 188 | rewrite_finite_card(equal(Integer,Card), Res, card_to_falsity_nonempty_eq_zero) :- | |
| 189 | % card({a1,..,ak}) = 0 --> falsity | |
| 190 | rewrite_finite_card_eq_0(Card, Integer, Res). | |
| 191 | rewrite_finite_card(equal(Card,Integer), Res, card_to_all_different_eq_k) :- | |
| 192 | % card({a1,..,ak}) = k --> all different | |
| 193 | rewrite_finite_card_k_eq_k(Card, Integer, Res). | |
| 194 | rewrite_finite_card(equal(Integer,Card), Res, card_to_all_different_eq_k) :- | |
| 195 | % k = card({a1,..,ak}) --> all different | |
| 196 | rewrite_finite_card_k_eq_k(Card, Integer, Res). | |
| 197 | rewrite_finite_card(greater_equal(Card,Integer), Res, card_to_all_different_geq_k) :- | |
| 198 | % card({a1,..,ak}) >= k --> all different | |
| 199 | rewrite_finite_card_k_eq_k(Card, Integer, Res). | |
| 200 | rewrite_finite_card(less_equal(Integer,Card), Res, card_to_all_different_geq_k) :- | |
| 201 | % k >= card({a1,..,ak}) --> all different | |
| 202 | rewrite_finite_card_k_eq_k(Card, Integer, Res). | |
| 203 | ||
| 204 | rewrite_finite_card_k_less_k(Card, Integer, Res) :- | |
| 205 | Card = b(card(SetExtension),integer,_), | |
| 206 | (Integer = b(integer(ICard),integer,_); Integer = b(value(int(ICard)),integer,_)), | |
| 207 | SetExtension = b(set_extension(L),_,_), | |
| 208 | length(L, Len), | |
| 209 | ICard =:= Len, | |
| 210 | !, | |
| 211 | create_at_least_one_eq(L, AtLeastOneEqAst), | |
| 212 | get_texpr_expr(AtLeastOneEqAst, Res). | |
| 213 | ||
| 214 | rewrite_finite_card_k_leq_k_minus_1(Card, Integer, Res) :- | |
| 215 | Card = b(card(SetExtension),integer,_), | |
| 216 | (Integer = b(integer(ICard),integer,_); Integer = b(value(int(ICard)),integer,_)), | |
| 217 | SetExtension = b(set_extension(L),_,_), | |
| 218 | length(L, Len), | |
| 219 | ICard =:= Len - 1, | |
| 220 | !, | |
| 221 | create_at_least_one_eq(L, AtLeastOneEqAst), | |
| 222 | get_texpr_expr(AtLeastOneEqAst, Res). | |
| 223 | ||
| 224 | rewrite_finite_card_k_leq_k(Card, Integer, Res) :- | |
| 225 | Card = b(card(SetExtension),integer,_), | |
| 226 | (Integer = b(integer(ICard),integer,_); Integer = b(value(int(ICard)),integer,_)), | |
| 227 | SetExtension = b(set_extension(L),_,_), | |
| 228 | length(L, Len), | |
| 229 | ICard >= Len, | |
| 230 | !, | |
| 231 | get_texpr_type(SetExtension, SetType), | |
| 232 | % don't create simple truth to keep variables in scope, could be the only occurrence | |
| 233 | Res = not_equal(SetExtension,b(empty_set,SetType,[])). | |
| 234 | ||
| 235 | rewrite_finite_card_k_leq_k_plus_1(Card, Integer, Res) :- | |
| 236 | Card = b(card(SetExtension),integer,_), | |
| 237 | (Integer = b(integer(ICard),integer,_); Integer = b(value(int(ICard)),integer,_)), | |
| 238 | SetExtension = b(set_extension(L),_,_), | |
| 239 | length(L, Len), | |
| 240 | ICard1 is ICard + 1, | |
| 241 | ICard1 >= Len, | |
| 242 | !, | |
| 243 | get_texpr_type(SetExtension, SetType), | |
| 244 | % don't create simple truth to keep variables in scope, could be the only occurrence | |
| 245 | Res = not_equal(SetExtension,b(empty_set,SetType,[])). | |
| 246 | ||
| 247 | rewrite_finite_card_geq_leq_k(Card, Integer, Res) :- | |
| 248 | Card = b(card(SetExtension),integer,_), | |
| 249 | (Integer = b(integer(ICard),integer,_); Integer = b(value(int(ICard)),integer,_)), | |
| 250 | SetExtension = b(set_extension(L),_,_), | |
| 251 | length(L, Len), | |
| 252 | ICard > Len, | |
| 253 | !, | |
| 254 | Res = falsity. | |
| 255 | ||
| 256 | rewrite_finite_card_greatereq_lesseq_n(Card, Integer, Res) :- | |
| 257 | Card = b(card(SetExtension),integer,_), | |
| 258 | (Integer = b(integer(ICard),integer,_); Integer = b(value(int(ICard)),integer,_)), | |
| 259 | SetExtension = b(set_extension(L),_,_), | |
| 260 | length(L, Len), | |
| 261 | ICard > Len, | |
| 262 | !, | |
| 263 | Res = falsity. | |
| 264 | ||
| 265 | rewrite_finite_card_greater_less_k(Card, Integer, Res) :- | |
| 266 | Card = b(card(SetExtension),integer,_), | |
| 267 | (Integer = b(integer(ICard),integer,_); Integer = b(value(int(ICard)),integer,_)), | |
| 268 | SetExtension = b(set_extension(L),_,_), | |
| 269 | length(L, Len), | |
| 270 | ICard >= Len, | |
| 271 | !, | |
| 272 | Res = falsity. | |
| 273 | ||
| 274 | rewrite_finite_card_greater_less_k1(Card, Integer, Res) :- | |
| 275 | Card = b(card(SetExtension),integer,_), | |
| 276 | (Integer = b(integer(ICard),integer,_); Integer = b(value(int(ICard)),integer,_)), | |
| 277 | SetExtension = b(set_extension(L),_,_), | |
| 278 | length(L, Len), | |
| 279 | ICard =:= Len - 1, | |
| 280 | !, | |
| 281 | create_all_different(L, AllDiffAst), | |
| 282 | get_texpr_expr(AllDiffAst, Res). | |
| 283 | ||
| 284 | rewrite_finite_card_geq_leq_1(Card, Integer1, Res) :- | |
| 285 | Card = b(card(SetExtension),integer,_), | |
| 286 | (Integer1 = b(integer(1),integer,_); Integer1 = b(value(int(1)),integer,_)), | |
| 287 | SetExtension = b(set_extension(L),_,_), | |
| 288 | L \== [], | |
| 289 | !, | |
| 290 | get_texpr_type(SetExtension, SetType), | |
| 291 | % don't create simple truth to keep variables in scope, could be the only occurrence | |
| 292 | Res = not_equal(SetExtension,b(empty_set,SetType,[])). | |
| 293 | ||
| 294 | rewrite_finite_card_2_eq_1(Card, Integer, Res) :- | |
| 295 | Card = b(card(SetExtension),integer,_), | |
| 296 | (Integer = b(integer(1),integer,_); Integer = b(value(int(1)),integer,_)), | |
| 297 | SetExtension = b(set_extension([A1,A2]),_,_), | |
| 298 | !, | |
| 299 | Res = equal(A1,A2). | |
| 300 | ||
| 301 | rewrite_finite_card_2_neq_1(Card, Integer, Res) :- | |
| 302 | Card = b(card(SetExtension),integer,_), | |
| 303 | (Integer = b(integer(1),integer,_); Integer = b(value(int(1)),integer,_)), | |
| 304 | SetExtension = b(set_extension([A1,A2]),_,_), | |
| 305 | !, | |
| 306 | Res = not_equal(A1,A2). | |
| 307 | ||
| 308 | rewrite_finite_card_eq_0(Card, Integer, Res) :- | |
| 309 | Card = b(card(SetExtension),integer,_), | |
| 310 | (Integer = b(integer(0),integer,_); Integer = b(value(int(0)),integer,_)), | |
| 311 | SetExtension = b(set_extension(L),_,_), | |
| 312 | L \== [], | |
| 313 | !, | |
| 314 | Res = falsity. | |
| 315 | ||
| 316 | rewrite_finite_card_k_eq_k(Card, Integer, Res) :- | |
| 317 | Card = b(card(SetExtension),integer,_), | |
| 318 | (Integer = b(integer(ICard),integer,_); Integer = b(value(int(ICard)),integer,_)), | |
| 319 | SetExtension = b(set_extension(L),_,_), | |
| 320 | length(L, Len), | |
| 321 | ICard == Len, | |
| 322 | !, | |
| 323 | create_all_different(L, AllDiffAst), | |
| 324 | get_texpr_expr(AllDiffAst, Res). | |
| 325 | ||
| 326 | % {x1,..,xk} -> x1 = x2 or ... or xk-1 = xk | |
| 327 | create_at_least_one_eq(L, AtLeastOneEq) :- | |
| 328 | create_at_least_one_eq(L, [], Eqs), | |
| 329 | disjunct_predicates(Eqs, AtLeastOneEq). | |
| 330 | ||
| 331 | create_at_least_one_eq([], Acc, Acc). | |
| 332 | create_at_least_one_eq([A|T], Acc, List) :- | |
| 333 | create_all_same_fixed(A, T, Acc, NAcc), | |
| 334 | create_at_least_one_eq(T, NAcc, List). | |
| 335 | ||
| 336 | create_all_different(Asts, AllDiffAst) :- | |
| 337 | create_all_different(Asts, [], InEqs), | |
| 338 | conjunct_predicates(InEqs, AllDiffAst). | |
| 339 | ||
| 340 | create_all_different([], Acc, Acc). | |
| 341 | create_all_different([A|T], Acc, InEqs) :- | |
| 342 | create_all_different_fixed(A, T, Acc, NAcc), | |
| 343 | create_all_different(T, NAcc, InEqs). | |
| 344 | ||
| 345 | create_all_different_fixed(_, [], Acc, Acc). | |
| 346 | create_all_different_fixed(A, [B|T], Acc, InEqs) :- | |
| 347 | safe_create_texpr(not_equal(A,B), pred, [], InEq), | |
| 348 | NAcc = [InEq|Acc], | |
| 349 | create_all_different_fixed(A, T, NAcc, InEqs). | |
| 350 | ||
| 351 | create_all_same_fixed(_, [], Acc, Acc). | |
| 352 | create_all_same_fixed(A, [B|T], Acc, InEqs) :- | |
| 353 | safe_create_texpr(equal(A,B), pred, [], InEq), | |
| 354 | NAcc = [InEq|Acc], | |
| 355 | create_all_same_fixed(A, T, NAcc, InEqs). |