1		% (c) 2021-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		:- 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(off) -> true
246		; format('Trying to expand (timeout ~w ms): ',[TimeOutVal]),
247		translate:print_bexpr_with_limit(CompSet,500),nl),
248		call_cleanup(safe_time_out(
249		(b_compute_expression_nowf(CompSet, [], Bindings, TPrecomputedVals,
250		'SMT quantifier precomputation', 0), !,
251		(enumeration_warning_occured_in_error_scope
252		-> perfmessage(Kind,not_expanding_quantifier_due_to_enum_warning(Kind),Span)
253		; true)
254		),
255		TimeOutVal, TimeOutRes),
256		(exit_error_scope(ScopeID, _, compute_instantiations_from_compset),
257		reset_temporary_preference(strict_raise_enum_warnings))),
258		(TimeOutRes == time_out
259		-> perfmessage(Kind,not_expanding_quantifier_due_to_timeout(Kind,TimeOutVal),Span),
260		fail
261		; true),
262		!,
263		expand_computed_val(TPrecomputedVals,Kind,Options,PrecomputedVals,Span).
264
265		:- use_module(probsrc(custom_explicit_sets),[is_interval_closure/3]).
266		expand_computed_val(global_set(GS),Kind,Options,Res,Span) :-
267		% for deferred sets: we check list_contains_unfixed_deferred_set_id above
268		(enumerated_set(GS) -> true
269		; member(instantiate_deferred_sets,Options), % Z3 cannot deal with deferred set values, see test 2063
270		perfmessage(Kind,not_expanding_quantifier_with_global_deferred_set(Kind),GS,Span)
271		),!,
272		try_expand_and_convert_to_avl_with_check(global_set(GS),Res,quantifier_instantiation(Kind)).
273		% Should we expand some closures like intervals here? b_compute_expression_nowf probably has already tried to expand closures
274		% However, intervals starting at size 101 are returned as symbolic:
275		expand_computed_val(Closure,Kind,Options,Res,Span) :-
276		is_interval_closure(Closure,Low,Up),
277		number(Low), number(Up),
278		Card is Up-Low+1,
279		(member(instantiate_quantifier_limit(Lim),Options) -> true ; Lim=200),
280		(Lim >= Card -> true
281		; perfmessage(Kind,not_expanding_interval(Kind,Card,limit(Lim)),Low:Up,Span),
282		fail
283		),
284		try_expand_and_convert_to_avl_with_check(Closure,Res,quantifier_instantiation(Kind)).
285		expand_computed_val(Val,_,_,Val,_).
286
287
288		% fails if containing any variable that is not a global constant
289		create_global_state_bindings([], []).
290		create_global_state_bindings([Id|T], [bind(Id,Val)|NT]) :-
291		lookup_global_constant(Id, Val),
292		create_global_state_bindings(T, NT).
293
294		:- use_module(probsrc(tools),[split_list/4]).
295		filter_lhs_distinct_from_ids(LHS, IdNames, RelevantLHS, RestLHS) :-
296		conjunction_to_list(LHS, List),
297		list_to_ord_set(IdNames,SIds),
298		split_list(irrelevant_or_non_ground_conjunct(SIds),List,TList,RList),
299		conjunct_predicates(RList, RelevantLHS),
300		conjunct_predicates(TList, RestLHS).
301
302		irrelevant_or_non_ground_conjunct(_,Conj) :- \+ ground_bexpr(Conj),!.
303		irrelevant_or_non_ground_conjunct(IdNames,Conj) :-
304		find_identifier_uses(Conj, [], UsedIds),
305		\+ ord_intersect(UsedIds, IdNames).
306
307		get_id_names([], []).
308		get_id_names([b(identifier(IdName),_,_)|T], [IdName|NT]) :-
309		get_id_names(T, NT).
310
311		get_couple_type_for_ids([TID1], Type1) :- !, get_texpr_type(TID1, Type1).
312		get_couple_type_for_ids([TID1,TID2|T], CType) :-
313		get_texpr_type(TID1, Type1),
314		get_texpr_type(TID2, Type2),
315		get_couple_type_for_ids(T, couple(Type1,Type2), CType).
316
317		get_couple_type_for_ids([], CType, CType).
318		get_couple_type_for_ids([TID|T], Acc, CType) :-
319		get_texpr_type(TID, Type),
320		get_couple_type_for_ids(T, couple(Acc,Type), CType).
321
322		% for quantifiers with n variables and each variable's domain is set by a simple membership
323		instantiate_paras_possible_nary_member([], RestLHS, [], LAcc, _, _, LAcc, RestLHS).
324		instantiate_paras_possible_nary_member([TID|T], LHS, [Id|IdNames], LAcc, ScopeIds, Options, ListOfPairs, RestLHS) :-
325		get_texpr_id(TID,Id),
326		TID = b(IdTerm,IdType,_),
327	?	get_member_for_id(IdTerm,IdType,LHS,Set,RestLHS1),
328		NScopeIds = [Id|ScopeIds],
329		rewrite_set_to_list_of_asts(Set, NScopeIds, Options, ListOfValues),
330		( LAcc == []
331	?	-> instantiate_paras_possible_nary_member(T, RestLHS1, IdNames, ListOfValues, NScopeIds, Options, ListOfPairs, RestLHS)
332	?	; create_cartesian_product_list(LAcc, ListOfValues, NLAcc),
333	?	instantiate_paras_possible_nary_member(T, RestLHS1, IdNames, NLAcc, NScopeIds, Options, ListOfPairs, RestLHS)
334		).
335
336		get_member_for_id(IdTerm,IdType,LHS,Set,RestLHS) :-
337		MEM = b(member(b(IdTerm,IdType,_),Set),pred,_),
338	?	select_member_in_conjunction(MEM, LHS, RestLHS).
339		% we could try and constrain sets like intervals further, probably better to use instantiate_paras_comp_set
340		get_member_for_id(_Id,IdType,LHS,Set,Rest) :- Rest=LHS,
341		(IdType = global(GS)
342		-> Set = b(value(global_set(GS)),set(IdType),[]) % we have a finite enumerated or def. set as type
343		; IdType = boolean
344		-> Set = b(boolean_set,set(IdType),[])
345		).
346
347
348		% rewrite (nested) couples to a list of lists with [val1,..,valn]
349		couples_to_list_of_tuples([], _, []).
350		couples_to_list_of_tuples([b(value(ValueCouple),CoupleType,_)|T], RTIDS, [ListOfAsts|NT]) :-
351		value_couple_to_list_of_asts(ValueCouple, RTIDS, CoupleType, ListOfAsts),
352		couples_to_list_of_tuples(T, RTIDS, NT).
353
354		% assuming that couples are left-associative
355		value_couple_to_list_of_asts((VCouple,Value), [_|TRTIDS], couple(CoupleType,VType), ListOfAsts) :-
356		VCouple = (_,_),
357		!,
358		value_couple_to_list_of_asts(VCouple, TRTIDS, CoupleType, TListOfAst),
359		append(TListOfAst, [b(value(Value),VType,[])], ListOfAsts).
360		value_couple_to_list_of_asts((Value1,Value2), [_], couple(VType1,VType2), ListOfAsts) :-
361		ListOfAsts = [b(couple(b(value(Value1),VType1,[]),b(value(Value2),VType2,[])),couple(VType1,VType2),[])].
362		value_couple_to_list_of_asts((Value1,Value2), [_,_], couple(VType1,VType2), ListOfAsts) :-
363		ListOfAsts = [b(value(Value1),VType1,[]),b(value(Value2),VType2,[])].
364
365		% create a list of lists with [val1,..,valn]
366		create_cartesian_product_list(ListOfValues1, ListOfValues2, ListOfPairs) :-
367	?	create_cartesian_product_list(ListOfValues1, ListOfValues2, [], ListOfPairs).
368
369		create_cartesian_product_list([], _, Acc, Acc).
370		create_cartesian_product_list([Val1|T], ListOfValues2, Acc, ListOfPairs) :-
371	?	create_cartesian_product_list_val(Val1, ListOfValues2, Acc, NAcc),
372	?	create_cartesian_product_list(T, ListOfValues2, NAcc, ListOfPairs).
373
374		create_cartesian_product_list_val(_, [], Acc, Acc).
375		create_cartesian_product_list_val(ValList, [Val2|T], Acc, NAcc) :-
376		is_list(ValList),
377		!,
378		append(ValList, [Val2], NValList),
379	?	create_cartesian_product_list_val(ValList, T, [NValList|Acc], NAcc).
380		create_cartesian_product_list_val(Val1, [Val2|T], Acc, NAcc) :-
381	?	create_cartesian_product_list_val(Val1, T, [[Val1,Val2]|Acc], NAcc).
382
383		finite_base_type(boolean,b(boolean_set,set(boolean),[])).
384		finite_base_type(couple(TA,TB),b(cartesian_product(VA,VB),set(couple(TA,TB)),[])) :-
385		finite_base_type(TA,VA),
386		finite_base_type(TB,VB).
387		% TODO: add more, e.g., enumerated sets
388
389		check_quantifier_limit(Options, Len, Kind, Span, NewOptions) :-
390	?	select(instantiate_quantifier_limit(Limit),Options,NO),
391		Len \== 0,
392		!,
393		( Len =< Limit
394		-> perfmessage(good(Kind),expanding_quantifier(Len,limit(Limit)),Span),
395		NewLimit is Limit // Len,
396		NewOptions = [instantiate_quantifier_limit(NewLimit)|NO]
397		; perfmessage(Kind,not_expanding_quantifier(Kind,Len,limit(Limit)),Span),
398		fail
399		).
400		check_quantifier_limit(O, _, _, _, O).
401
402		% TO DO: detect more cases ?
403		convert_to_couple(b(value(V),couple(T1,T2),I), [BV1,BV2]) :-
404		nonvar(V),
405		V = (V1,V2),
406		!,
407		BV1 = b(value(V1),T1,I),
408		BV2 = b(value(V2),T2,I).
409		convert_to_couple(b(couple(V1,V2),_,_), [V1,V2]).
410
411		% if instantiate_quantifier_possible then this can be used to retrieve values for expansion
412		get_instantiation_value([_], List, Res) :- !, Res=[Val],
413	?	member(Val,List).
414		get_instantiation_value(L, List, ValList) :-
415		length(L, Len),
416		Len > 1,
417		length(ValList, Len),
418	?	member(ValList, List).
419
420
421