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