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(ast_optimizer_for_smt, [reset_optimizer_state/0,
5		precompute_values/3,
6		precompute_values_non_recursive/3,
7		assert_state_id_values/2,
8		assert_ground_id_values/2,
9		replace_ids_with_ground_values/4,
10		replace_ids_with_eq_ids_top_level/2]).
11
12		:- use_module(library(lists)).
13
14		:- use_module(smt_solvers_interface(set_rewriter)).
15		:- use_module(smt_solvers_interface(quantifier_instantiation)).
16		:- use_module(probsrc(preferences), [get_preference/2]).
17		:- use_module(probsrc(kernel_objects), [infer_value_type/2]).
18		:- use_module(probsrc(bmachine), [b_get_named_machine_set/2]).
19		:- use_module(probsrc(b_interpreter), [b_compute_expression_nowf/6]).
20		:- use_module(probsrc(bsyntaxtree), [remove_all_infos/2,
21		get_texpr_id/2,
22		get_texpr_expr/2,
23		get_texpr_type/2,
24		safe_create_texpr/4,
25		find_identifier_uses/3,
26		conjunction_to_list/2,
27		syntaxtransformation/5]).
28		:- use_module(probsrc(store), [normalise_value_for_var/4]).
29		:- use_module(probsrc(module_information), [module_info/2]).
30		:- use_module(probsrc(error_manager), [add_internal_error/2]).
31		:- use_module(probsrc(kernel_tools), [ground_value/1]).
32		%:- use_module(wdsrc(well_def_analyser), [prove_sequent/1]).
33
34		:- module_info(group, smt_solvers).
35		:- module_info(description, 'This module implements transformations to simplify SMT-LIB translations.').
36
37		:- dynamic id_ground_value/3, id_equality/3.
38
39		reset_optimizer_state :-
40		retractall(id_ground_value(_,_,_)),
41		retractall(id_equality(_,_,_)).
42
43		%% precompute_values(+Ast, -AstOpt).
44		% Compute some ground operations in Prolog to simplify SMT-Lib constraints.
45		% We split this from the actual cleanup since we use information on ground
46		% values in the cleanup, e.g., to optimize cardinality constraints.
47		% Computes some more values than b_compile/6.
48		precompute_values(Ast, Options, AstOpt) :-
49		precompute_values3(Ast, [allow_recursive_call|Options], [], AstOpt).
50
51		precompute_values_non_recursive(Options, Ast, AstOpt) :-
52		precompute_values_non_recursive(Options, [], Ast, AstOpt).
53
54		precompute_values_non_recursive(Options, ScopeIds, Ast, AstOpt) :-
55		precompute_values3(Ast, Options, ScopeIds, AstOpt).
56
57		precompute_values3(Ast, Options, ScopeIds, AstOpt) :-
58		Ast = b(Expr,Type,Info), !,
59		( precompute_values_e(Expr, Type, Info, Options, ScopeIds, NExpr)
60		-> safe_create_texpr(NExpr, Type, Info, AstOpt)
61		; add_internal_error('Call failed: ',precompute_values_e(Expr, Type, Info, Options, ScopeIds, _)),
62		AstOpt = Ast
63		).
64		precompute_values3(L, _, _, R) :-
65		add_internal_error('Not a B AST:', precompute_values3(L, _, _, R) ),
66		R = L.
67
68		precompute_values_e(min_int, _, _, _, _, integer(MinInt)) :- !,
69		get_preference(minint, MinInt).
70		precompute_values_e(max_int, _, _, _, _, integer(MaxInt)) :- !,
71		get_preference(maxint, MaxInt).
72		/*precompute_values_e(function(Fun,Elm), Type, Info, _, AstOpt) :-
73		Ast = b(function(Fun,Elm),Type,Info),
74		Fun \= b(identifier(_),_,_), % uninterpreted functions can not be precomputed
75		prove_sequent(Ast),
76		!,
77		find_typed_identifier_uses(Ast, [], UsedIds),
78		set_up_typed_localstate(UsedIds, _, SmtTypedVals, [], Bindings, positive),
79		init_wait_flags(WFStore, [wf_fun]),
80		( b_tighter_enumerate_all_values(SmtTypedVals, WFStore),
81		b_interpreter:b_compute_expression(Ast, Bindings, Bindings, Res, WFStore),
82		ground_wait_flags(WFStore)
83		-> AstOpt = b(value(Res),Type,Info)
84		; AstOpt = Ast
85		).*/
86		precompute_values_e(forall(TIDs,LHS,RHS), pred, Info, Options, ScopeIds, Res) :-
87		member(instantiate_quantifier_limit(L), Options),
88		L \== 0,
89		instantiate_quantifier_possible(forall(TIDs,LHS,RHS), pred, Info, Options, ScopeIds, NOptions, TRes),
90		( TRes == truth
91		-> Res = truth % no instantiation found, universal quantification is true
92		; precompute_values3(TRes, NOptions, [], b(Res,pred,_)) % TODO: check this, what about ScopeIDs?
93		).
94		precompute_values_e(exists(TIDs,LHS), pred, Info, Options, ScopeIds, Res) :-
95		member(instantiate_quantifier_limit(L), Options),
96		L \== 0,
97		instantiate_quantifier_possible(exists(TIDs,LHS), pred, Info, Options, ScopeIds, NOptions, TRes),
98		( TRes == falsity
99		-> Res = falsity % no instantiation found, existential quantification is false
100		; precompute_values3(TRes, NOptions, [], b(Res,pred,_)) % TODO: check this, what about ScopeIDs?
101		).
102		precompute_values_e(comprehension_set([Id,LambdaRes],Body), _, _, Options, ScopeIds, SetExtension) :-
103		% e.g., %(i : 1..3|0)
104		LambdaRes = b(identifier('_lambda_result_'),_,_),
105		Body = b(conjunct(Member,LambdaEq),pred,_),
106		remove_all_infos(Id, CId),
107		remove_all_infos(LambdaRes, CLambdaRes),
108		Member = b(member(CId,Domain),pred,_),
109		LambdaEq = b(equal(CLambdaRes,RangeVal),pred,_),
110		compute_ground_lambda(Id, Domain, RangeVal, ScopeIds, Options, ComputedSet),
111		!,
112		construct_set_extension(ComputedSet,SetExtension).
113		precompute_values_e(interval(A,B), _, _, Options, ScopeIds, SetExtension) :-
114		rewrite_set_to_list_of_asts(b(interval(A,B),set(integer),[]), ScopeIds, Options, List),
115		!,
116		construct_set_extension(List,SetExtension).
117		precompute_values_e(Pow, _, _, Options, ScopeIds, Precomputed) :-
118		SetAst = b(set_extension(List),set(Type),[]),
119		( Pow = pow_subset(Arg),
120		PowAst = b(pow_subset(SetAst),set(set(Type)),[])
121		; Pow = pow1_subset(Arg),
122		PowAst = b(pow1_subset(SetAst),set(set(Type)),[])
123		),
124		rewrite_set_to_list_of_asts(Arg, ScopeIds, Options, List),
125		is_a_list_of_values(List),
126		length(List, Len),
127		( Pow = pow_subset(Arg)
128		-> PowCard is 2**Len
129		; PowCard is 2**Len - 1
130		),
131		( member(instantiate_sets_limit(SetLimit), Options)
132		-> PowCard =< SetLimit
133		; true
134		),
135		List = [b(_,Type,_)|_],
136		!,
137		b_compute_expression_nowf(PowAst, [], [], TPrecomputedVal,'SMT precomputation',0),
138		normalise_value_for_var(solver_result, force, TPrecomputedVal, PrecomputedVal),
139		Precomputed = value(PrecomputedVal).
140		precompute_values_e(reverse(Arg), _, _, Options, ScopeIds, SetExtension) :-
141		rewrite_set_to_list_of_asts(Arg, ScopeIds, Options, List),
142		is_a_list_of_values(List),
143		compute_inverse(List, InvList),
144		!,
145		construct_set_extension(InvList,SetExtension).
146		precompute_values_e(cartesian_product(SetA,SetB), _, _, Options, ScopeIds, SetExtension) :-
147		rewrite_set_to_list_of_asts(SetA, ScopeIds, Options, ListA),
148		rewrite_set_to_list_of_asts(SetB, ScopeIds, Options, ListB),
149		get_texpr_type(SetA, set(InTypeA)),
150		get_texpr_type(SetB, set(InTypeB)),
151		compute_cartesian_product(InTypeA, InTypeB, ListA, ListB, CartList),
152		!,
153		construct_set_extension(CartList,SetExtension).
154		precompute_values_e(BOP, _Type, _Info, Options, ScopeIds, Res) :-
155		binary_connective(BOP,F,A,B),
156		!,
157		binary_connective(Res,F,NA,NB),
158		precompute_values_non_recursive(Options, ScopeIds, A, NA),
159		precompute_values_non_recursive(Options, ScopeIds, B, NB). % we ignore allow_recursive_call option; all optimisations are local
160		precompute_values_e(Expr, Type, Info, Options, ScopeIds, Res) :-
161		syntaxtransformation(Expr, Subs, Names, NSubs, NExpr),
162		( Names \= []
163		-> maplist(get_texpr_id, Names, IdNames),
164		append(IdNames, ScopeIds, NScopeIds)
165		; NScopeIds = ScopeIds),
166		!,
167		maplist(precompute_values_non_recursive(Options, NScopeIds), Subs, NSubs),
168		( ( select(allow_recursive_call, Options, Options2),
169		\+ no_recursive_computation(NExpr)
170		)
171		-> precompute_values_e(NExpr, Type, Info, Options2, NScopeIds, Res) % Warning: this can cause a quadratic processing time !
172		; Res = NExpr
173		).
174		precompute_values_e(Expr, _, _, _, _, Res) :-
175		add_internal_error('Unknown AST node:', precompute_values_e(Expr, _, _, _, Res)),
176		Res = Expr.
177
178		no_recursive_computation(set_extension(_)).
179		no_recursive_computation(sequence_extension(_)).
180		no_recursive_computation(value(_)).
181
182		binary_connective(conjunct(A,B),conjunct,A,B).
183		binary_connective(disjunct(A,B),disjunct,A,B).
184		binary_connective(implication(A,B),implication,A,B).
185		binary_connective(equivalence(A,B),equivalence,A,B).
186
187		construct_set_extension([],Res) :- !, Res=empty_set.
188		construct_set_extension(List,set_extension(List)).
189
190		is_asserted_ground_value(IdName, _, GroundAst) :-
191		id_ground_value(_, IdName, TGroundAst),
192		!,
193		GroundAst = TGroundAst.
194		is_asserted_ground_value(IdName, EqVals, GroundAst) :-
195		% transitive equality
196		(id_equality(_, IdName, EqIdName); id_equality(_, EqIdName, IdName)),
197		\+ member(EqIdName, EqVals),
198		!,
199		is_asserted_ground_value(EqIdName, [EqIdName|EqVals], GroundAst).
200
201		% TO DO: improve, use a normalized order for equalities
202		replace_ids_with_eq_ids_top_level(Pred, NPred) :-
203		Pred = b(Expr,Type,Info),
204		replace_ids_with_eq_ids_top_level_e(Expr, NExpr),
205		NPred = b(NExpr,Type,Info).
206
207		% all solutions on bt
208		replace_ids_with_eq_ids_top_level_e(identifier(IdName), NExpr) :-
209		findall(A-B-C, id_equality(A,B,C), _),
210		(id_equality(0, IdName, EqIdName); id_equality(0, EqIdName, IdName)),
211		NExpr = identifier(EqIdName).
212		replace_ids_with_eq_ids_top_level_e(negation(TExpr), NExpr) :-
213		!,
214		replace_ids_with_eq_ids_top_level(TExpr, NTExpr),
215		NExpr = negation(NTExpr).
216		replace_ids_with_eq_ids_top_level_e(Expr, NExpr) :-
217		Expr \= identifier(_),
218		syntaxtransformation(Expr,Subs,_,NSubs,NExpr),
219		!,
220		l_replace_ids_with_eq_ids_top_level(Subs,NSubs).
221		replace_ids_with_eq_ids_top_level_e(Expr, Expr) :-
222		Expr \= identifier(_).
223
224		l_replace_ids_with_eq_ids_top_level([],[]).
225		l_replace_ids_with_eq_ids_top_level([H|T],[NH|NT]) :-
226		replace_ids_with_eq_ids_top_level(H,NH),
227		l_replace_ids_with_eq_ids_top_level(T,NT).
228
229		%% replace_ids_with_ground_values(+Ast, +ScopeId, +ExcludeScopeIds, -AstOpt).
230		% Replace S in card(S) if S is a ground finite set, e.g., a ground interval.
231		% Do not optimise scoped ids if they have the same name as a top-level variable,
232		% e.g., as introduced by an existential quantifier.
233		% +ScopeId is used when entering scopes or dependend logical operators such as implication or disjunction to assert scoped id equalities.
234		% This predicate uses the dynamic facts id_ground_value/3 and is_asserted_ground_value/3.
235		replace_ids_with_ground_values(Ast, ScopeId, ExcludeScopeIds, AstOpt) :-
236		Ast = b(Expr,Type,Info),
237		\+ member(do_not_optimize_away, Info),
238		!,
239		replace_ids_with_ground_values_e(Expr, ScopeId, ExcludeScopeIds, NExpr),
240		AstOpt = b(NExpr,Type,Info).
241		replace_ids_with_ground_values(A, _, _, A).
242
243		replace_ids_with_ground_values_e(identifier(IdName), _, ExcludeScopeIds, NExpr) :-
244		is_asserted_ground_value(IdName, [], GroundAst),
245		!,
246		( \+ member(b(identifier(IdName),_,_), ExcludeScopeIds)
247		-> get_texpr_expr(GroundAst, NExpr)
248		; NExpr = identifier(IdName)
249		).
250		replace_ids_with_ground_values_e(Eq, _, _, NEq) :-
251		% do not remove ground equality since this will be the last occurrence of the variable
252		( Eq = equal(Id,GroundValOrId)
253		; Eq = equal(GroundValOrId,Id)
254		),
255		( Id = b(identifier(_),_,_),
256		get_texpr_expr(GroundValOrId, GroundExpr),
257		is_ground_b_value(GroundExpr)
258		; id_equality(_, Id, GroundValOrId)
259		; id_equality(_, GroundValOrId, Id)
260		),
261		!,
262		NEq = Eq.
263		replace_ids_with_ground_values_e(equal(Id1,Id2), _, ExcludeScopeIds, NEq) :-
264		Id1 = b(identifier(IdName1),Type,_),
265		Id2 = b(identifier(IdName2),Type,_),
266		( id_ground_value(_, IdName1, GroundAst1),
267		\+ member(b(identifier(IdName1),Type,_), ExcludeScopeIds)
268		-> NArg1 = GroundAst1
269		; NArg1 = Id1
270		),
271		( id_ground_value(_, IdName2, GroundAst2),
272		\+ member(b(identifier(IdName2),Type,_), ExcludeScopeIds)
273		-> NArg2 = GroundAst2
274		; NArg2 = Id2
275		),
276		!,
277		NEq = equal(NArg1,NArg2).
278		replace_ids_with_ground_values_e(set_extension([Id]), _, ExcludeScopeIds, NUnary) :-
279		Id = b(identifier(IdName),_,_),
280		\+ member(b(identifier(IdName),_,_), ExcludeScopeIds),
281		!,
282		( id_ground_value(_, IdName, GroundVal)
283		-> NUnary = set_extension([GroundVal])
284		; NUnary = set_extension([Id])
285		).
286		replace_ids_with_ground_values_e(Expr, ScopeId, ExcludeScopeIds, NExpr) :-
287		functor(Expr, Functor, 2),
288		( Functor = implication
289		; Functor = disjunct
290		),
291		arg(1, Expr, Arg1),
292		arg(2, Expr, Arg2),
293		!,
294		NScopeId is ScopeId + 1,
295		assert_ground_id_values(NScopeId, Arg1),
296		replace_ids_with_ground_values(Arg1, NScopeId, ExcludeScopeIds, NArg1),
297		retract_ground_id_values_for_scope(NScopeId),
298		assert_ground_id_values(NScopeId, Arg2),
299		replace_ids_with_ground_values(Arg2, NScopeId, ExcludeScopeIds, NArg2),
300		retract_ground_id_values_for_scope(NScopeId),
301		functor(NExpr, Functor, 2),
302		arg(1, NExpr, NArg1),
303		arg(2, NExpr, NArg2).
304		replace_ids_with_ground_values_e(Expr, ScopeId, ExcludeScopeIds, NExpr) :-
305		functor(Expr, Functor, 2),
306		( Functor = conjunct
307		; Functor = equivalence
308		),
309		arg(1, Expr, Arg1),
310		arg(2, Expr, Arg2),
311		!,
312		% ground ids already asserted for top-level conjunction
313		replace_ids_with_ground_values(Arg1, ScopeId, ExcludeScopeIds, NArg1),
314		replace_ids_with_ground_values(Arg2, ScopeId, ExcludeScopeIds, NArg2),
315		functor(NExpr, Functor, 2),
316		arg(1, NExpr, NArg1),
317		arg(2, NExpr, NArg2).
318		replace_ids_with_ground_values_e(negation(Pred), ScopeId, ExcludeScopeIds, NNeg) :-
319		!,
320		NScopeId is ScopeId + 1,
321		assert_ground_id_values(NScopeId, Pred),
322		replace_ids_with_ground_values(Pred, NScopeId, ExcludeScopeIds, NPred),
323		retract_ground_id_values_for_scope(NScopeId),
324		NNeg = negation(NPred).
325		replace_ids_with_ground_values_e(forall(Ids,Lhs,Rhs), ScopeId, ExcludeScopeIds, NForall) :-
326		!,
327		append(ExcludeScopeIds, Ids, NExcludeScopeIds),
328		replace_ids_with_ground_values(Lhs, ScopeId, NExcludeScopeIds, NLhs),
329		NScopeId is ScopeId + 1,
330		assert_ground_id_values(NScopeId, Rhs),
331		replace_ids_with_ground_values(Rhs, NScopeId, NExcludeScopeIds, NRhs),
332		retract_ground_id_values_for_scope(NScopeId),
333		NForall = forall(Ids,NLhs,NRhs).
334		replace_ids_with_ground_values_e(Expr, ScopeId, ExcludeScopeIds, NExpr) :-
335		functor(Expr, Functor, 2),
336		( Functor = exists
337		; Functor = comprehension_set
338		; Functor = lambda
339		; Functor = general_sum
340		; Functor = general_product
341		; Functor = quantified_union
342		; Functor = quantified_intersection
343		; Functor = event_b_comprehension_set
344		),
345		!,
346		arg(1, Expr, Ids),
347		arg(2, Expr, Pred),
348		NScopeId is ScopeId + 1,
349		assert_ground_id_values(NScopeId, Pred),
350		append(ExcludeScopeIds, Ids, NExcludeScopeIds),
351		replace_ids_with_ground_values(Pred, NScopeId, NExcludeScopeIds, NPred),
352		retract_ground_id_values_for_scope(NScopeId),
353		functor(NExpr, Functor, 2),
354		arg(1, NExpr, Ids),
355		arg(2, NExpr, NPred).
356		replace_ids_with_ground_values_e(Expr, ScopeId, ExcludeScopeIds,NExpr) :-
357		syntaxtransformation(Expr,Subs,Names,NSubs,NExpr),
358		!,
359		append(Names, ExcludeScopeIds, NExcludeScopeIds),
360		l_replace_ids_with_ground_values(Subs,ScopeId,NExcludeScopeIds,NSubs).
361		replace_ids_with_ground_values_e(Expr, _, _, Expr).
362
363
364		l_replace_ids_with_ground_values([],_,_,[]).
365		l_replace_ids_with_ground_values([H|T],ScopeId,Excl,[NH|NT]) :-
366		replace_ids_with_ground_values(H,ScopeId,Excl,NH),
367		l_replace_ids_with_ground_values(T,ScopeId,Excl,NT).
368
369
370		%% assert_state_id_values(+ProBState).
371		% Assert global state id values to be replaced syntactically afterwards.
372		assert_state_id_values(_, NoState) :-
373		NoState == no_state, !.
374		assert_state_id_values(_, []).
375		assert_state_id_values(TypedIds, [bind(IdName,Value)|T]) :-
376		( member(b(identifier(IdName),TType,_), TypedIds)
377		-> Type = TType
378		; infer_value_type(Value, Type)
379		),
380		asserta(id_ground_value(0,IdName,b(value(Value),Type,[]))),
381		assert_state_id_values(TypedIds, T).
382
383		%% assert_ground_id_values(+ScopeId, +Ast).
384		% Assert ground id values originating from identifier equalities such as x=[1,2].
385		% We are then able to precompute some constraints which improves performance.
386		% See, for instance, :z3 x = [2,3] & y = x~ & d = y[{3,4}], where Z3 answers unknown without rewriting.
387		% Note: Only obvious ground equalities on the top-level of a conjunction are considered.
388		% +ScopeId is an integer, 0 at the top-level and +1 for each quantified scope.
389		assert_ground_id_values(ScopeId, Ast) :-
390		conjunction_to_list(Ast, List),
391		maplist(assert_ground_id_value(ScopeId), List).
392
393		assert_ground_id_value(ScopeId, b(Eq,pred,_)) :-
394		( Eq = equal(Id,GroundAst)
395		; Eq = equal(GroundAst,Id)
396		),
397		Id = b(identifier(IdName),_,_),
398		get_texpr_expr(GroundAst, GroundVal),
399		is_ground_b_value(GroundVal),
400		!,
401		asserta(id_ground_value(ScopeId,IdName,GroundAst)).
402		assert_ground_id_value(ScopeId, b(equal(Id1,Id2),pred,_)) :-
403		Id1 = b(identifier(IdName1),_,_),
404		Id2 = b(identifier(IdName2),_,_),
405		!,
406		asserta(id_equality(ScopeId,IdName1,IdName2)).
407		assert_ground_id_value(_, _).
408
409		retract_ground_id_values_for_scope(ScopeId) :-
410		retractall(id_ground_value(ScopeId,_,_)),
411		retractall(id_equality(ScopeId,_,_)).
412
413		is_ground_b_value(boolean_false).
414		is_ground_b_value(boolean_true).
415		is_ground_b_value(bool_set).
416		is_ground_b_value(empty_sequence).
417		is_ground_b_value(empty_set).
418		is_ground_b_value(integer(_)).
419		is_ground_b_value(int(_)).
420		is_ground_b_value(integer_set(_)).
421		is_ground_b_value(max_int).
422		is_ground_b_value(min_int).
423		is_ground_b_value(float_set).
424		is_ground_b_value(real(_)).
425		is_ground_b_value(real_set).
426		is_ground_b_value(string(_)).
427		is_ground_b_value(string_set).
428		is_ground_b_value(value(_)).
429		is_ground_b_value(interval(_,_)).
430		is_ground_b_value(set_extension(_)).
431		is_ground_b_value(identifier(EnumId)) :-
432		b_get_named_machine_set(_, EnumIds),
433		member(EnumId, EnumIds), !.
434
435		%% compute_ground_lambda(+LambdaId, +Domain, +Range, +ScopeIds, +Options, -ComputedSet)
436		compute_ground_lambda(LambdaId, Domain, Range, ScopeIds, Options, ComputedSet) :-
437		rewrite_set_to_list_of_asts(Domain, ScopeIds, Options, LoAsts),
438		( member(instantiate_sets_limit(SetLimit), Options)
439		-> length(LoAsts, Len),
440		Len =< SetLimit
441		; true
442		),
443		get_texpr_type(Range, RT),
444		find_identifier_uses(Range, [], UsedIds),
445		LambdaId = b(identifier(LambdaIdName),_,_),
446		LoAsts = [b(_,DT,_)|_],
447		( UsedIds = []
448		-> % for instance, %i.(i : 1 .. 10|0)
449		findall(b(couple(A,Range),couple(DT,RT),[]),
450		member(A, LoAsts),
451		ComputedSet)
452		; % for instance, %i.(i : 1 .. 10|i + i)
453		UsedIds = [LambdaIdName],
454		findall(b(couple(A,ComputedRange),couple(DT,RT),[]),
455		( member(A, LoAsts),
456		b_compute_expression_nowf(A, [], [], DomValue,'SMT precomputation',0),
457		b_compute_expression_nowf(Range, [bind(LambdaIdName,DomValue)], [], Res,'SMT precomputation',0),
458		ComputedRange = b(value(Res),RT,[])
459		),
460		ComputedSet)
461		).
462
463		%% compute_inverse(+List, -InvList)
464		compute_inverse([], []).
465		compute_inverse(List, InvList) :-
466		List = [Couple|_],
467		get_texpr_type(Couple, CoupleType),
468		CoupleType = couple(A,B),
469		compute_inverse(couple(B,A), List, [], InvList).
470
471		compute_inverse(_, [], Acc, Acc).
472		compute_inverse(InvCoupleType, [Couple|T], Acc, InvList) :-
473		get_elements_of_couple(Couple, A, B),
474		compute_inverse(InvCoupleType, T, [b(couple(B,A),InvCoupleType,[])|Acc], InvList).
475
476		get_elements_of_couple(b(couple(A,B),_,_), A, B).
477		get_elements_of_couple(b(value((A,B)),couple(TA,TB),[]), AstA, AstB) :-
478		AstA = b(value(A),TA,[]),
479		AstB = b(value(B),TB,[]).
480
481		%% compute_cartesian_product(+InTypeA, +InTypeB, +ListA, +ListB, -CartList).
482		compute_cartesian_product(InTypeA, InTypeB, ListA, ListB, CartList) :-
483		compute_cartesian_product(InTypeA, InTypeB, ListA, ListB, [], CartList).
484
485		compute_cartesian_product(_, _, [], _, Acc, Acc).
486		compute_cartesian_product(InTypeA, InTypeB, [H|T], SetB, Acc, CartList) :-
487		compute_single_cartesian_product(InTypeA, InTypeB, H, SetB, Acc, NAcc),
488		compute_cartesian_product(InTypeA, InTypeB, T, SetB, NAcc, CartList).
489
490		compute_single_cartesian_product(_, _, _, [], Acc, Acc).
491		compute_single_cartesian_product(InTypeA, InTypeB, H, [H2|T], Acc, NAcc) :-
492		Couple = b(couple(H,H2),couple(InTypeA, InTypeB),[]),
493		NAcc1 = [Couple|Acc],
494		compute_single_cartesian_product(InTypeA, InTypeB, H, T, NAcc1, NAcc).
495
496		% check if we have a list of values, without identifiers
497		is_a_list_of_values([]).
498		is_a_list_of_values([H|T]) :- is_a_value(H),is_a_list_of_values(T).
499
500		is_a_value(b(V,_,_)) :- is_a_value_aux(V).
501		is_a_value_aux(value(V)) :- ground_value(V).
502		is_a_value_aux(integer(_)).
503		is_a_value_aux(boolean_false).
504		is_a_value_aux(boolean_true).
505		is_a_value_aux(string(_)).
506		is_a_value_aux(real(_)).
507		is_a_value_aux(empty_set).
508		is_a_value_aux(empty_sequence).
509		is_a_value_aux(bool_set).
510		is_a_value_aux(max_int).
511		is_a_value_aux(min_int).
512		is_a_value_aux(couple(A,B)) :- is_a_value(A), is_a_value(B).
513		% TODO: extend (records), and possibly move somewhere else