1 | % (c) 2021-2024 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(quantifier_instantiation, [instantiate_quantifiers/3, | |
5 | instantiate_quantifier_possible/7, | |
6 | instantiate_exists_to_list/5]). | |
7 | ||
8 | :- use_module(library(lists)). | |
9 | :- use_module(library(ordsets), [ord_intersect/2, list_to_ord_set/2]). | |
10 | :- use_module(library(avl), [avl_to_list/2]). | |
11 | ||
12 | :- use_module(smt_solvers_interface(set_rewriter)). | |
13 | :- use_module(probsrc(preferences), [temporary_set_preference/2, | |
14 | reset_temporary_preference/1]). | |
15 | :- use_module(probsrc(b_global_sets), [lookup_global_constant/2, enumerated_set/1, | |
16 | list_contains_unfixed_deferred_set_id/1]). | |
17 | :- use_module(probsrc(bsyntaxtree), [get_texpr_type/2, | |
18 | find_identifier_uses/3, | |
19 | get_texpr_expr/2, | |
20 | conjunct_predicates/2, | |
21 | conjunction_to_list/2, | |
22 | replace_ids_by_exprs/4, | |
23 | select_member_in_conjunction/3, | |
24 | safe_create_texpr/4, | |
25 | disjunct_predicates/2, | |
26 | get_texpr_id/2, | |
27 | create_implication/3, | |
28 | is_membership_or_equality/3, | |
29 | syntaxtransformation_det/5]). | |
30 | :- use_module(probsrc(tools_meta),[safe_time_out/3]). | |
31 | :- use_module(probsrc(b_interpreter), [b_compute_expression_nowf/6]). | |
32 | :- use_module(probsrc(error_manager), [add_internal_error/2, | |
33 | enter_new_error_scope/2, | |
34 | exit_error_scope/3, | |
35 | enumeration_warning_occured_in_error_scope/0, | |
36 | clear_enumeration_warning_in_error_scope/1]). | |
37 | :- use_module(probsrc(performance_messages), [perfmessage_bexpr/3,perfmessage/3, perfmessage/4]). | |
38 | :- use_module(probsrc(module_information), [module_info/2]). | |
39 | :- use_module(probsrc(debug), [debug_mode/1]). | |
40 | ||
41 | :- module_info(group, smt_solvers). | |
42 | :- module_info(description, 'This module implements transformations to simplify SMT-LIB translations.'). | |
43 | ||
44 | %% instantiate_quantifiers(+Options, +Ast, -AstOpt). | |
45 | % Options: | |
46 | % - instantiate_quantifier_limit(Limit) | |
47 | % - not_instantiate_unfixed_deferred_sets (necessary for Z3 since unfixed deferred set ids are invented by ProB) | |
48 | instantiate_quantifiers(Options, Ast, AstOpt) :- | |
49 | instantiate_quantifiers(Options, [], Ast, AstOpt). %bsyntaxtree:check_ast(AstOpt). | |
50 | ||
51 | instantiate_quantifiers(Options, ScopeIds, Ast, AstOpt) :- | |
52 | Ast = b(Expr,Type,Info), | |
53 | !, | |
54 | (%contains_no_quantifiers(Expr) -> AstOpt=Ast | |
55 | Type \= pred -> AstOpt = Ast % do we want to instantiate quantifiers inside set comprehensions / bool ...? | |
56 | ; instantiate_quantifiers_e(Expr, Type, Info, Options, ScopeIds, NExpr) | |
57 | -> safe_create_texpr(NExpr, Type, Info, AstOpt) | |
58 | ; add_internal_error('Call failed: ',instantiate_quantifiers_e(Expr, Type, Info, Options, ScopeIds, _)), | |
59 | AstOpt=Ast | |
60 | ). | |
61 | instantiate_quantifiers(_, _, L, R) :- | |
62 | add_internal_error('Not a B AST:',instantiate_quantifiers(_, _, L, R) ), | |
63 | R = L. | |
64 | ||
65 | instantiate_quantifiers_e(forall(TIDs,LHS,RHS), pred, Info, Options, ScopeIds, Res) :- | |
66 | instantiate_quantifier_possible(forall(TIDs,LHS,RHS), pred, Info, Options, ScopeIds, NOptions, TRes), | |
67 | ( TRes == truth | |
68 | -> Res = truth % no instantiation found, universal quantification is true | |
69 | ; contains_quantifiers_e(impliation(LHS,RHS)) -> instantiate_quantifiers(NOptions, ScopeIds, TRes, b(Res,pred,_)) | |
70 | ; get_texpr_expr(TRes,Res) % no quantifiers, no need to traverse | |
71 | ). | |
72 | instantiate_quantifiers_e(exists(TIDs,LHS), pred, Info, Options, ScopeIds, Res) :- | |
73 | instantiate_quantifier_possible(exists(TIDs,LHS), pred, Info, Options, ScopeIds, NOptions, TRes), | |
74 | ( TRes == falsity | |
75 | -> Res = falsity % no instantiation found, existential quantification is false | |
76 | ; contains_quantifiers(LHS) -> instantiate_quantifiers(NOptions, ScopeIds, TRes, b(Res,pred,_)) | |
77 | ; get_texpr_expr(TRes,Res) % no quantifiers, no need to traverse | |
78 | ). | |
79 | instantiate_quantifiers_e(Expr, _, _, Options, ScopeIds, Res) :- | |
80 | % TODO: only proceed if we do not have a top-level exists/forall | |
81 | %hit_profiler:add_profile_hit(Expr), | |
82 | syntaxtransformation_det(Expr,Subs,_,NSubs,NExpr), | |
83 | !, | |
84 | %maplist(instantiate_quantifiers(Options, ScopeIds),Subs,NSubs), | |
85 | l_instantiate_quantifiers(Subs,Options,ScopeIds,NSubs), | |
86 | Res = NExpr. | |
87 | instantiate_quantifiers_e(Expr, _, _, _, ScopeIds, Res) :- | |
88 | add_internal_error('Unknown AST node:', instantiate_quantifiers_e(Expr, _, _, _, ScopeIds, Res)), | |
89 | Res = Expr. | |
90 | ||
91 | %contains_no_quantifiers(identifier(_)). | |
92 | %contains_no_quantifiers(integer(_)). | |
93 | %contains_no_quantifiers(string(_)). | |
94 | %contains_no_quantifiers(value(_)). | |
95 | ||
96 | % quick check if a predicate contains quantifiers at the outer-predicate level (not inside bool(.), ...) | |
97 | % check is applied to predicate before expansion; possibly avoiding costly traversal of thousands of conjuncts | |
98 | contains_quantifiers(b(E,pred,_)) :- contains_quantifiers_e(E). | |
99 | contains_quantifiers_e(negation(A)) :- contains_quantifiers(A). | |
100 | contains_quantifiers_e(conjunct(A,B)) :- (contains_quantifiers(A) -> true ; contains_quantifiers(B)). | |
101 | contains_quantifiers_e(disjunct(A,B)) :- (contains_quantifiers(A) -> true ; contains_quantifiers(B)). | |
102 | contains_quantifiers_e(implication(A,B)) :- (contains_quantifiers(A) -> true ; contains_quantifiers(B)). | |
103 | contains_quantifiers_e(equivalence(A,B)) :- (contains_quantifiers(A) -> true ; contains_quantifiers(B)). | |
104 | contains_quantifiers_e(forall(_,_,_)). | |
105 | contains_quantifiers_e(exists(_,_)). | |
106 | ||
107 | ||
108 | l_instantiate_quantifiers([],_,_,[]). | |
109 | l_instantiate_quantifiers([S1|TS],Options,ScopeIds,[NS1|NTS]) :- | |
110 | instantiate_quantifiers(Options,ScopeIds,S1,NS1), | |
111 | l_instantiate_quantifiers(TS,Options,ScopeIds,NTS). | |
112 | ||
113 | :- use_module(probsrc(bsyntaxtree), [get_texpr_ids/2]). | |
114 | instantiate_quantifier_possible(forall(TIDs,LHS,RHS), pred, Info, Options, ScopeIds, NOptions, Res) :- | |
115 | instantiate_paras_possible(TIDs, LHS, forall, Info, Options, Ids, ScopeIds, List, RestLHS), | |
116 | ( List == [] | |
117 | -> % no instantiation found, universal quantification is true | |
118 | Res = b(truth,pred,[]) | |
119 | ; length(List,Len), | |
120 | check_quantifier_limit(Options, Len, forall, Info, NOptions), | |
121 | !, | |
122 | create_implication(RestLHS, RHS, BODY),% translate:nested_print_bexpr(BODY),nl, | |
123 | % Note: it is important that List contains only ground values; otherwise findall will copy variables: | |
124 | findall(Vals, get_instantiation_value(Ids, List, Vals),Vs), | |
125 | maplist(replace_ids_by_exprs(BODY,Ids),Vs,Bodies), | |
126 | Bodies \== [], | |
127 | %Bodies = [B1|_], translate:print_bexpr(B1),nl, | |
128 | conjunct_predicates(Bodies, Res) | |
129 | ). | |
130 | instantiate_quantifier_possible(exists(TIDs,LHS), pred, Info, Options, ScopeIds, NOptions, Res) :- | |
131 | instantiate_quantifier_to_list(TIDs,LHS,exists,Info,Options,ScopeIds,NOptions,Bodies), | |
132 | disjunct_predicates(Bodies, Res). | |
133 | ||
134 | % try and instantiate an existential quantifier into a list of candidates | |
135 | % used e.g., in b_to_cnf to translate cardinality constraints | |
136 | % it is important that every disjunct represents a distinct candidate element | |
137 | instantiate_exists_to_list(TIDs,LHS,Info,Options,Bodies) :- | |
138 | instantiate_quantifier_to_list(TIDs,LHS,exists,Info,Options,[],_NOptions,Bodies). | |
139 | ||
140 | % instantiate a quantifier to list of body candidates, without conjoining/disjoining them | |
141 | instantiate_quantifier_to_list(TIDs,LHS,Kind,Info,Options,ScopeIds,NOptions,Bodies) :- | |
142 | instantiate_paras_possible(TIDs, LHS, Kind, Info, Options, Ids, ScopeIds, List, BODY), | |
143 | ( List == [] | |
144 | -> % no instantiation found, existential quantification is false | |
145 | Bodies = [] % falsity for disjunction | |
146 | ; length(List,Len), | |
147 | check_quantifier_limit(Options, Len, Kind, Info, NOptions), | |
148 | !, | |
149 | findall(Vals, get_instantiation_value(Ids, List, Vals),Vs), | |
150 | maplist(replace_ids_by_exprs(BODY,Ids),Vs,Bodies), | |
151 | Bodies \== [] | |
152 | ). | |
153 | ||
154 | % detect whether a quantifier expansion is possible | |
155 | instantiate_paras_possible(TIDs, LHS, Kind, Info, Options, Ids, ScopeIds, List, RestLHS) :- | |
156 | \+ possibly_reject_unfixed_deferred_set_id(TIDs, Options), | |
157 | (nonmember(instantiate_precisely_only,Options), | |
158 | instantiate_paras_by_membership(TIDs, LHS, Kind, Info, Options, Ids, ScopeIds, List, RestLHS) | |
159 | ; | |
160 | instantiate_paras_comp_set(TIDs, LHS, Kind, Info, Options, Ids, ScopeIds, List, RestLHS)). | |
161 | instantiate_paras_possible(TIDS, LHS, Kind, _, _Span, _, _, _, _) :- | |
162 | TIDS = [TID1|_], | |
163 | get_texpr_id(TID1,Id1), | |
164 | perfmessage_bexpr(Kind, ['Quantifier (',Kind,' over ',Id1,', ...) expansion not possible: '], LHS), | |
165 | fail. | |
166 | ||
167 | % try and instantiate by finding specific membership predicates or look at types | |
168 | instantiate_paras_by_membership([TID], LHS, _, _, Options, [Id], ScopeIds, ListOfValues, RestLHS) :- | |
169 | get_texpr_id(TID, Id), | |
170 | ( get_texpr_id(TID2, Id), | |
171 | is_membership_or_equality(MEM, TID2, Set), | |
172 | select_member_in_conjunction(MEM, LHS, TRestLHS) | |
173 | ; get_texpr_type(TID, Type), | |
174 | finite_base_type(Type, Set), | |
175 | TRestLHS = LHS | |
176 | ), | |
177 | rewrite_set_to_list_of_asts(Set, [Id|ScopeIds], Options, TListOfValues), | |
178 | !, | |
179 | ListOfValues = TListOfValues, | |
180 | RestLHS = TRestLHS. | |
181 | instantiate_paras_by_membership([TID1,TID2], LHS, _Kind, _, Options, [Id1,Id2], ScopeIds, ListOfPairs, RestLHS) :- | |
182 | get_texpr_id(TID1, Id1), | |
183 | get_texpr_id(TID2, Id2), | |
184 | Couple = b(couple(A,B),_,_), get_texpr_id(A,Id1), get_texpr_id(B,Id2), | |
185 | MEM = b(member(Couple,Set),pred,_), | |
186 | select_member_in_conjunction(MEM, LHS, RestLHS), | |
187 | rewrite_set_to_list_of_asts(Set, [Id1,Id2|ScopeIds], Options, ListOfValues), | |
188 | maplist(convert_to_couple, ListOfValues, ListOfPairs), | |
189 | !. | |
190 | instantiate_paras_by_membership(TIDS, LHS, _, _, Options, IdNames, ScopeIds, ListOfTuples, RestLHS) :- | |
191 | % !(x1,..xn).(x1:S1 & .. & xn:Sn & RestLHS => BODY) | #(x1,..xn).(x1:S1 & .. & xn:Sn & RestLHS) | |
192 | instantiate_paras_possible_nary_member(TIDS, LHS, IdNames, [], ScopeIds, Options, TListOfTuples, TRestLHS), | |
193 | !, | |
194 | ListOfTuples = TListOfTuples, | |
195 | RestLHS = TRestLHS. | |
196 | ||
197 | ||
198 | % try and instantiate by expanding a filtered comprehension set of possible parameter values | |
199 | % will be more precise by considering all constraints (e.g., symmetry breaking), but can have issues like time-outs, ... | |
200 | instantiate_paras_comp_set(TIDS, LHS, Kind, Info, Options, IdNames, _ScopeIds, ListOfTuples, RestLHS) :- | |
201 | % any other quantifier where domains are, e.g., defined in nested couples such as !(a,b,c).(0|->1|-a|->b|->c : S => BODY), also for exists | |
202 | get_couple_type_for_ids(TIDS, CType), | |
203 | get_id_names(TIDS, TIdNames), | |
204 | filter_lhs_distinct_from_ids(LHS, TIdNames, RelevantLHS, RestLHS), | |
205 | CompSet = b(comprehension_set(TIDS,RelevantLHS),set(CType),[]), | |
206 | find_identifier_uses(CompSet, [], UsedIds), | |
207 | ( create_global_state_bindings(UsedIds, Bindings) | |
208 | -> true | |
209 | ; % cannot instantiate due to free variables that are not quantified | |
210 | fail | |
211 | ), | |
212 | % Default timeout 100ms, can be overridden with expansion_time_out option | |
213 | % write('TRY EXPANDING: '),nl,translate:print_bexpr(CompSet),nl, | |
214 | compute_instantiations_from_compset(Kind,Options,CompSet, Bindings, PrecomputedVals,Options, Info), | |
215 | !, | |
216 | IdNames = TIdNames, | |
217 | ( PrecomputedVals == [] | |
218 | -> ListOfTuples = [] % no instantiation found, quantifier is false/true | |
219 | ; PrecomputedVals = avl_set(Avl), | |
220 | avl_to_list(Avl, AvlList), | |
221 | avl_list_to_list_of_asts(CType, AvlList, [], ListOfValues), | |
222 | (TIDS = [_] % single identifier | |
223 | -> ListOfTuples=ListOfValues | |
224 | ; reverse(TIDS, RTIDS), | |
225 | couples_to_list_of_tuples(ListOfValues, RTIDS, ListOfTuples) | |
226 | ) | |
227 | ). | |
228 | ||
229 | possibly_reject_unfixed_deferred_set_id(TIDS, Options) :- | |
230 | member(not_instantiate_unfixed_deferred_sets, Options), | |
231 | list_contains_unfixed_deferred_set_id(TIDS). | |
232 | ||
233 | :- use_module(probsrc(custom_explicit_sets),[try_expand_and_convert_to_avl_with_check/3]). | |
234 | :- use_module(probsrc(kernel_tools),[ground_bexpr/1]). | |
235 | compute_instantiations_from_compset(Kind,Options,CompSet, Bindings, PrecomputedVals,Options,Span) :- | |
236 | ground_bexpr(CompSet), % should now be always true | |
237 | temporary_set_preference(strict_raise_enum_warnings, false), | |
238 | enter_new_error_scope(ScopeID, compute_instantiations_from_compset), | |
239 | ( true | |
240 | ; clear_enumeration_warning_in_error_scope(ScopeID), | |
241 | fail | |
242 | ), | |
243 | (member(expansion_time_out(Val),Options) -> TimeOutVal=Val ; TimeOutVal=100), | |
244 | % things like !i.(i:dom(f) => f(x)=TRUE) cannot be expanded if f not fully known at the moment | |
245 | (debug_mode(on) -> format('Trying to expand (timeout ~w ms): ',[TimeOutVal]),translate:print_bexpr(CompSet),nl ; true), | |
246 | call_cleanup(safe_time_out( | |
247 | (b_compute_expression_nowf(CompSet, [], Bindings, TPrecomputedVals, | |
248 | 'SMT quantifier precomputation', 0), !, | |
249 | (enumeration_warning_occured_in_error_scope | |
250 | -> perfmessage(Kind,not_expanding_quantifier_due_to_enum_warning(Kind),Span) | |
251 | ; true) | |
252 | ), | |
253 | TimeOutVal, TimeOutRes), | |
254 | (exit_error_scope(ScopeID, _, compute_instantiations_from_compset), | |
255 | reset_temporary_preference(strict_raise_enum_warnings))), | |
256 | (TimeOutRes == time_out | |
257 | -> perfmessage(Kind,not_expanding_quantifier_due_to_timeout(Kind,TimeOutVal),Span), | |
258 | fail | |
259 | ; true), | |
260 | !, | |
261 | expand_computed_val(TPrecomputedVals,Kind,Options,PrecomputedVals,Span). | |
262 | ||
263 | :- use_module(probsrc(custom_explicit_sets),[is_interval_closure/3]). | |
264 | expand_computed_val(global_set(GS),Kind,Options,Res,Span) :- | |
265 | % for deferred sets: we check list_contains_unfixed_deferred_set_id above | |
266 | (enumerated_set(GS) -> true | |
267 | ; member(instantiate_deferred_sets,Options), % Z3 cannot deal with deferred set values, see test 2063 | |
268 | perfmessage(Kind,not_expanding_quantifier_with_global_deferred_set(Kind),GS,Span) | |
269 | ),!, | |
270 | try_expand_and_convert_to_avl_with_check(global_set(GS),Res,quantifier_instantiation(Kind)). | |
271 | % Should we expand some closures like intervals here? b_compute_expression_nowf probably has already tried to expand closures | |
272 | % However, intervals starting at size 101 are returned as symbolic: | |
273 | expand_computed_val(Closure,Kind,Options,Res,Span) :- | |
274 | is_interval_closure(Closure,Low,Up), | |
275 | number(Low), number(Up), | |
276 | Card is Up-Low+1, | |
277 | (member(instantiate_quantifier_limit(Lim),Options) -> true ; Lim=200), | |
278 | (Lim >= Card -> true | |
279 | ; perfmessage(Kind,not_expanding_interval(Kind,Card,limit(Lim)),Low:Up,Span), | |
280 | fail | |
281 | ), | |
282 | try_expand_and_convert_to_avl_with_check(Closure,Res,quantifier_instantiation(Kind)). | |
283 | expand_computed_val(Val,_,_,Val,_). | |
284 | ||
285 | ||
286 | % fails if containing any variable that is not a global constant | |
287 | create_global_state_bindings([], []). | |
288 | create_global_state_bindings([Id|T], [bind(Id,Val)|NT]) :- | |
289 | lookup_global_constant(Id, Val), | |
290 | create_global_state_bindings(T, NT). | |
291 | ||
292 | :- use_module(probsrc(tools),[split_list/4]). | |
293 | filter_lhs_distinct_from_ids(LHS, IdNames, RelevantLHS, RestLHS) :- | |
294 | conjunction_to_list(LHS, List), | |
295 | list_to_ord_set(IdNames,SIds), | |
296 | split_list(irrelevant_or_non_ground_conjunct(SIds),List,TList,RList), | |
297 | conjunct_predicates(RList, RelevantLHS), | |
298 | conjunct_predicates(TList, RestLHS). | |
299 | ||
300 | irrelevant_or_non_ground_conjunct(_,Conj) :- \+ ground_bexpr(Conj),!. | |
301 | irrelevant_or_non_ground_conjunct(IdNames,Conj) :- | |
302 | find_identifier_uses(Conj, [], UsedIds), | |
303 | \+ ord_intersect(UsedIds, IdNames). | |
304 | ||
305 | get_id_names([], []). | |
306 | get_id_names([b(identifier(IdName),_,_)|T], [IdName|NT]) :- | |
307 | get_id_names(T, NT). | |
308 | ||
309 | get_couple_type_for_ids([TID1], Type1) :- !, get_texpr_type(TID1, Type1). | |
310 | get_couple_type_for_ids([TID1,TID2|T], CType) :- | |
311 | get_texpr_type(TID1, Type1), | |
312 | get_texpr_type(TID2, Type2), | |
313 | get_couple_type_for_ids(T, couple(Type1,Type2), CType). | |
314 | ||
315 | get_couple_type_for_ids([], CType, CType). | |
316 | get_couple_type_for_ids([TID|T], Acc, CType) :- | |
317 | get_texpr_type(TID, Type), | |
318 | get_couple_type_for_ids(T, couple(Acc,Type), CType). | |
319 | ||
320 | % for quantifiers with n variables and each variable's domain is set by a simple membership | |
321 | instantiate_paras_possible_nary_member([], RestLHS, [], LAcc, _, _, LAcc, RestLHS). | |
322 | instantiate_paras_possible_nary_member([TID|T], LHS, [Id|IdNames], LAcc, ScopeIds, Options, ListOfPairs, RestLHS) :- | |
323 | get_texpr_id(TID,Id), | |
324 | TID = b(IdTerm,IdType,_), | |
325 | get_member_for_id(IdTerm,IdType,LHS,Set,RestLHS1), | |
326 | NScopeIds = [Id|ScopeIds], | |
327 | rewrite_set_to_list_of_asts(Set, NScopeIds, Options, ListOfValues), | |
328 | ( LAcc == [] | |
329 | -> instantiate_paras_possible_nary_member(T, RestLHS1, IdNames, ListOfValues, NScopeIds, Options, ListOfPairs, RestLHS) | |
330 | ; create_cartesian_product_list(LAcc, ListOfValues, NLAcc), | |
331 | instantiate_paras_possible_nary_member(T, RestLHS1, IdNames, NLAcc, NScopeIds, Options, ListOfPairs, RestLHS) | |
332 | ). | |
333 | ||
334 | get_member_for_id(IdTerm,IdType,LHS,Set,RestLHS) :- | |
335 | MEM = b(member(b(IdTerm,IdType,_),Set),pred,_), | |
336 | select_member_in_conjunction(MEM, LHS, RestLHS). | |
337 | % we could try and constrain sets like intervals further, probably better to use instantiate_paras_comp_set | |
338 | get_member_for_id(_Id,IdType,LHS,Set,Rest) :- Rest=LHS, | |
339 | (IdType = global(GS) | |
340 | -> Set = b(value(global_set(GS)),set(IdType),[]) % we have a finite enumerated or def. set as type | |
341 | ; IdType = boolean | |
342 | -> Set = b(boolean_set,set(IdType),[]) | |
343 | ). | |
344 | ||
345 | ||
346 | % rewrite (nested) couples to a list of lists with [val1,..,valn] | |
347 | couples_to_list_of_tuples([], _, []). | |
348 | couples_to_list_of_tuples([b(value(ValueCouple),CoupleType,_)|T], RTIDS, [ListOfAsts|NT]) :- | |
349 | value_couple_to_list_of_asts(ValueCouple, RTIDS, CoupleType, ListOfAsts), | |
350 | couples_to_list_of_tuples(T, RTIDS, NT). | |
351 | ||
352 | % assuming that couples are left-associative | |
353 | value_couple_to_list_of_asts((VCouple,Value), [_|TRTIDS], couple(CoupleType,VType), ListOfAsts) :- | |
354 | VCouple = (_,_), | |
355 | !, | |
356 | value_couple_to_list_of_asts(VCouple, TRTIDS, CoupleType, TListOfAst), | |
357 | append(TListOfAst, [b(value(Value),VType,[])], ListOfAsts). | |
358 | value_couple_to_list_of_asts((Value1,Value2), [_], couple(VType1,VType2), ListOfAsts) :- | |
359 | ListOfAsts = [b(couple(b(value(Value1),VType1,[]),b(value(Value2),VType2,[])),couple(VType1,VType2),[])]. | |
360 | value_couple_to_list_of_asts((Value1,Value2), [_,_], couple(VType1,VType2), ListOfAsts) :- | |
361 | ListOfAsts = [b(value(Value1),VType1,[]),b(value(Value2),VType2,[])]. | |
362 | ||
363 | % create a list of lists with [val1,..,valn] | |
364 | create_cartesian_product_list(ListOfValues1, ListOfValues2, ListOfPairs) :- | |
365 | create_cartesian_product_list(ListOfValues1, ListOfValues2, [], ListOfPairs). | |
366 | ||
367 | create_cartesian_product_list([], _, Acc, Acc). | |
368 | create_cartesian_product_list([Val1|T], ListOfValues2, Acc, ListOfPairs) :- | |
369 | create_cartesian_product_list_val(Val1, ListOfValues2, Acc, NAcc), | |
370 | create_cartesian_product_list(T, ListOfValues2, NAcc, ListOfPairs). | |
371 | ||
372 | create_cartesian_product_list_val(_, [], Acc, Acc). | |
373 | create_cartesian_product_list_val(ValList, [Val2|T], Acc, NAcc) :- | |
374 | is_list(ValList), | |
375 | !, | |
376 | append(ValList, [Val2], NValList), | |
377 | create_cartesian_product_list_val(ValList, T, [NValList|Acc], NAcc). | |
378 | create_cartesian_product_list_val(Val1, [Val2|T], Acc, NAcc) :- | |
379 | create_cartesian_product_list_val(Val1, T, [[Val1,Val2]|Acc], NAcc). | |
380 | ||
381 | finite_base_type(boolean,b(boolean_set,set(boolean),[])). | |
382 | finite_base_type(couple(TA,TB),b(cartesian_product(VA,VB),set(couple(TA,TB)),[])) :- | |
383 | finite_base_type(TA,VA), | |
384 | finite_base_type(TB,VB). | |
385 | % TODO: add more, e.g., enumerated sets | |
386 | ||
387 | check_quantifier_limit(Options, Len, Kind, Span, NewOptions) :- | |
388 | select(instantiate_quantifier_limit(Limit),Options,NO), | |
389 | Len \== 0, | |
390 | !, | |
391 | ( Len =< Limit | |
392 | -> perfmessage(good(Kind),expanding_quantifier(Len,limit(Limit)),Span), | |
393 | NewLimit is Limit // Len, | |
394 | NewOptions = [instantiate_quantifier_limit(NewLimit)|NO] | |
395 | ; perfmessage(Kind,not_expanding_quantifier(Kind,Len,limit(Limit)),Span), | |
396 | fail | |
397 | ). | |
398 | check_quantifier_limit(O, _, _, _, O). | |
399 | ||
400 | % TO DO: detect more cases ? | |
401 | convert_to_couple(b(value(V),couple(T1,T2),I), [BV1,BV2]) :- | |
402 | nonvar(V), | |
403 | V = (V1,V2), | |
404 | !, | |
405 | BV1 = b(value(V1),T1,I), | |
406 | BV2 = b(value(V2),T2,I). | |
407 | convert_to_couple(b(couple(V1,V2),_,_), [V1,V2]). | |
408 | ||
409 | % if instantiate_quantifier_possible then this can be used to retrieve values for expansion | |
410 | get_instantiation_value([_], List, Res) :- !, Res=[Val], | |
411 | member(Val,List). | |
412 | get_instantiation_value(L, List, ValList) :- | |
413 | length(L, Len), | |
414 | Len > 1, | |
415 | length(ValList, Len), | |
416 | member(ValList, List). | |
417 | ||
418 | ||
419 |