1		% (c) 2009-2026 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
5		:- module(ast_cleanup_for_smt, [smt_clean_up/2,
6		smt_clean_up/3,
7		smt_clean_up/4,
8		smt_clean_up_opts/4,
9		smt_clean_up_pre/4,
10		smt_clean_up_post/4]).
11
12		:- use_module(library(lists),[maplist/3,
13		append/2,
14		is_list/1]).
15		:- use_module(library(avl), [avl_to_list/2]).
16		:- use_module(probsrc(bsyntaxtree),[is_texpr/1,
17		add_texpr_infos/3,
18		remove_bt/4,
19		safe_create_texpr/4,
20		create_texpr/4,
21		get_texpr_expr/2,
22		get_texpr_type/2,
23		create_negation/2,
24		conjunct_predicates/2,
25		disjunct_predicates/2,
26		create_forall/3,
27		create_exists/3,
28		create_implication/3,
29		conjunction_to_list/2,
30		%create_couple/2,
31		syntaxtransformation/5,
32		unique_typed_id/3,
33		find_typed_identifier_uses/3,
34		%always_well_defined_or_disprover_mode/1,
35		is_pow_subset/2, is_pow1_subset/2,
36		%get_integer/2,
37		is_just_type/1]).
38		:- use_module(probsrc(solver_interface),[solve_predicate/3]).
39		:- use_module(probsrc(custom_explicit_sets),[is_interval_closure/3]).
40		:- use_module(probsrc(b_interpreter_components),[extract_equalities_in_quantifier/4]).
41		:- use_module(probsrc(error_manager), [add_internal_error/2,add_error_fail/3,add_message/2,add_message/3,add_debug_message/3]).
42		:- use_module(probsrc(debug), [debug_println/2]).
43		:- use_module(probsrc(bsyntaxtree), [find_identifier_uses/3,find_typed_identifier_uses/2]).
44		:- use_module(probsrc(b_global_sets), [unfixed_deferred_set/1]).
45		:- use_module(probsrc(b_compiler), [b_compile/6]).
46		:- use_module(probsrc(preferences), [get_preference/2,temporary_set_preference/3,reset_temporary_preference/2]).
47		:- use_module(probsrc(store),[normalise_value_for_var/4]).
48		:- use_module(smt_solvers_interface(quantifier_instantiation)).
49		:- use_module(smt_solvers_interface(smt_common_predicates)).
50		:- use_module(smt_solvers_interface(ast_optimizer_for_smt)).
51		:- use_module(smt_solvers_interface(seq_rewriter)).
52		:- use_module(smt_solvers_interface(set_rewriter)).
53		:- use_module(cdclt_solver('cdclt_pred_to_sat'), [predicate_to_sat/6]).
54		:- use_module(extension('banditfuzz/welldef')).
55		:- use_module(probsrc('well_def/well_def_analyser'), [analyse_wd_for_expr/3]).
56		:- use_module(probsrc('debug'), [set_silent_mode/1, silent_mode/1]).
57
58		:- use_module(probsrc(module_information),[module_info/2]).
59		:- module_info(group,smt_solvers).
60		:- module_info(description,'This module implements transformations needed by the SMT-LIB translation.').
61
62		:- set_prolog_flag(double_quotes, codes).
63
64		:- dynamic translation_type/1.
65
66		%% smt_clean_up(+Ast, -Out).
67		smt_clean_up(Ast, Out) :-
68		smt_clean_up(axiomatic, Ast, Out).
69
70		%% smt_clean_up_opts(+TranslationType, +Ast, +Options, -Out).
71		% Cleanup without global state using Options instantiate_quantifier_limit(L).
72		smt_clean_up_opts(TranslationType, Ast, Options, Out) :-
73		smt_clean_up_pre(Ast, [], Options, CAst),
74		smt_clean_up_post(TranslationType, CAst, Options, Out).
75
76		%% smt_clean_up(+TranslationType, +Ast, -Out).
77		% Cleanup without global state.
78		smt_clean_up(TranslationType, Ast, Out) :-
79		smt_clean_up_pre(Ast, [], [], CAst),
80		smt_clean_up_post(TranslationType, CAst, [], Out).
81
82		%% smt_clean_up(+TranslationType, +Ast, +ProBState, -Out).
83		% Cleanup with global state.
84		smt_clean_up(TranslationType, Ast, ProBState, Out) :-
85		smt_clean_up_pre(Ast, ProBState, [], CAst),
86		smt_clean_up_post(TranslationType, CAst, [], Out).
87
88		get_ids_not_in_state([], _, Acc, Acc).
89		get_ids_not_in_state([IdName|T], State, Acc, IdsNotInState) :-
90		( (
91	?	member(bind(IdName,_), State),
92		\+ unfixed_deferred_set(IdName)
93		)
94		-> get_ids_not_in_state(T, State, Acc, IdsNotInState)
95		; get_ids_not_in_state(T, State, [IdName|Acc], IdsNotInState)
96		).
97
98		%% smt_clean_up_pre(+Ast, +ProBState, +Options, -CleanAst).
99		% Cleanup without internal rewriting rules and independent of any translation type.
100		% WD conditions are added if the input is not well-defined.
101		smt_clean_up_pre(Ast, ProBState, _Options, CleanAst) :-
102		reset_optimizer_state,
103		( get_preference(add_wd_pos_for_z3, true)
104		-> % this prints missing wd conditions
105		silent_mode(Old), set_silent_mode(on),
106		analyse_wd_for_expr(Ast, _ResStr, TIsWd),
107		( ground(TIsWd)
108		-> IsWd = TIsWd
109		; IsWd = 'FALSE'
110		),
111		set_silent_mode(Old)
112		; IsWd = 'TRUE'
113		),
114	?	rewrite_seq_to_set(IsWd, Ast, AstWithoutSeq),
115		welldef:filter_typing_pos(true),
116		welldef:preprocess_pos_for_cdclt(false),
117		( IsWd == 'TRUE'
118		-> WDPred = AstWithoutSeq
119	?	; ensure_wd(AstWithoutSeq, WDPred),
120		( AstWithoutSeq \= WDPred
121		-> add_message(smt_clean_up_pre, 'Input not well-defined: automatically added WD POs'),
122		add_debug_message(smt_clean_up_pre,'Full predicate: ',WDPred)
123		; true
124		)
125		),
126		find_typed_identifier_uses(WDPred, TypedIds),
127	?	assert_state_id_values(TypedIds, ProBState),
128		assert_ground_id_values(0, WDPred),
129		replace_ids_with_ground_values(WDPred, 0, [], AstGroundOpt),
130		precompute_values_non_recursive([instantiate_quantifier_limit(0),instantiate_sets_limit(1000)], AstGroundOpt, AstGroundOpt2),
131		find_identifier_uses(AstGroundOpt2, [], UsedIds),
132		get_ids_not_in_state(UsedIds, ProBState, [], IdsNotInState),
133		temporary_set_preference(data_validation_mode, true, DVChange),
134	?	catch(b_compile(AstGroundOpt2, IdsNotInState, ProBState, ProBState, AstOpt, no_wf_available),
135		enumeration_warning(_,_,_,_,_), % cancel if enumeration warning has occurred
136		AstOpt = AstGroundOpt2),
137		reset_temporary_preference(data_validation_mode,DVChange),
138		temporary_set_preference(allow_improving_wd_mode, true,Change),
139		b_ast_cleanup:clean_up(AstOpt, [], TCleanAst), !,
140		reset_temporary_preference(allow_improving_wd_mode,Change),
141		CleanAst = TCleanAst.
142
143		%% smt_clean_up_post(+TranslationType, +CleanAst, +Options, -Out).
144		% Cleanup with translation type specific internal rewriting rules.
145		smt_clean_up_post(TranslationType, CleanAst, Options, Out) :-
146		atom(TranslationType),
147		retractall(translation_type(_)),
148		asserta(translation_type(TranslationType)),
149		internal_clean_up(CleanAst, TOut),
150		reset_optimizer_state, !,
151		( ( memberchk(instantiate_quantifier_limit(IQLIMIT), Options),
152		IQLIMIT > 0
153		)
154		-> instantiate_quantifiers([instantiate_quantifier_limit(IQLIMIT),not_instantiate_unfixed_deferred_sets], TOut, Out)
155		; Out = TOut
156		).
157
158		internal_clean_up(ExprWithoutSeq,Out) :-
159		clean_up(ExprWithoutSeq,CExpr,[],AC,IDs),
160		!,
161		combine_pred_and_ac(CExpr,AC,IDs,Out).
162
163		clean_up(Expr,CExprOut,Path,ACOut,IDsOut) :-
164		cleanups(pre,Expr,[],TPExpr,Path,ACPre,IDsPre),
165		remove_bt(TPExpr,PExpr,LExpr,TLExpr),
166		syntaxtransformation(PExpr,Subs,_,NewSubs,LExpr),
167		functor(PExpr,F,N),
168		% recursively clean up sub-expressions
169		maplist(internal_clean_up,ACPre,ACPreClean),
170		clean_up_l(Subs,NewSubs,F/N,1,Path,ACL,IDsL),
171		maplist(internal_clean_up,ACL,ACLClean),
172		cleanups(post,TLExpr,[],CExpr,Path,ACPost,IDsPost),
173		maplist(internal_clean_up,ACPost,ACPostClean),
174		append([ACPreClean,ACLClean,ACPostClean],AC),
175		append([IDsPre,IDsL,IDsPost],IDs),
176		(AC \= [], get_texpr_type(CExpr,pred)
177		-> combine_pred_and_ac(CExpr,AC,IDs,CExprOut),
178		% the accumulator contains additional constraints and new existentially quantified vars IDs
179		IDsOut = [], ACOut = []
180		; CExprOut = CExpr, ACOut = AC, IDsOut = IDs).
181
182		combine_pred_and_ac(Pred,AC,IDs,Out) :-
183		conjunct_predicates(AC,ACPred),
184		conjunct_predicates([Pred,ACPred],OutInnerPred),
185		extract_equalities_in_quantifier(IDs,OutInnerPred,I2,P2), % used in create_and_simplify_exists; can be expensive
186		create_exists(I2,P2,Out). % TO DO: use more intelligence from create_exists_opt or similar??
187
188		clean_up_l([],[],_Functor,_Nr,_Path,[],[]).
189		clean_up_l([Expr|Rest],[CExpr|CRest],Functor,ArgNr,Path,AC,IDs) :-
190		clean_up(Expr,CExpr,[arg(Functor,ArgNr)|Path],ACC,IDsC),
191		A1 is ArgNr+1,
192		clean_up_l(Rest,CRest,Functor,A1,Path,ACL,IDsL),
193		append(ACC,ACL,AC),
194		append(IDsC,IDsL,IDs).
195
196		cleanups(Phase,Expr,AppliedRules,Result,Path,ACS,IDs) :-
197		start_profile_rule(RuleInfos),
198		assure_single_rules(AppliedRules,Rule),
199	?	( cleanup_phase(Phase,Expr,NExpr,Mode/Rule,Path,ACPhase,IDsPhase)
200		-> % try to apply a rule (matching the current phase)
201		( Mode == single
202		-> AppRules = [Rule|AppliedRules] % if the rule is marked as "single", we add to the list of already applied rules
203		; Mode == multi
204		-> AppRules = AppliedRules % if "multi", we do not add it to the list, the rule might be applied more than once
205		; add_error_fail(ast_cleanup_for_smt,'Unexpected rule mode ',Mode)
206		),
207		%format('Applied smt cleanup rule ~w (mode:~w)~n',[Rule,Mode]), translate:print_bexpr(NExpr),nl,
208		stop_profile_rule(Rule,Mode,Phase,Expr,RuleInfos),
209		cleanups(Phase,NExpr,AppRules,Result,Path,ACRec,IDsRec), % continue recursively with the new expression
210		append(ACPhase,ACRec,ACS),
211		append(IDsPhase,IDsRec,IDs)
212		; % if no rule matches anymore,
213		stop_profile_rule(finalise,finished,Phase,Expr,RuleInfos),
214		Result = Expr, % we leave the expression unmodified
215		ACS = [], IDs = [],
216		Rule = none
217		). % and unblock the co-routine (see assure_single_rules/2)
218
219		:- if(fail). % comment in to see expensive cleanup rules
220		start_profile_rule([R1,W1]) :- statistics(runtime,[R1,_]),statistics(walltime,[W1,_]).
221		stop_profile_rule(Rule,Mode,Phase,Expr,[R1,W1]) :-
222		statistics(runtime,[R2,_]),statistics(walltime,[W2,_]),
223		DeltaW is W2-W1, DeltaR is R2-R1,
224		(DeltaW < 20 -> true ; format('Firing SMT AST cleanup rule ~w (mode:~w) in phase ~w took ~w ms (~w ms walltime)~n',[Rule,Mode,Phase,DeltaR,DeltaW]), translate:print_span(Expr),nl),
225		runtime_profiler:register_profiler_runtime(Rule,ast_cleanup,unknown,DeltaR,DeltaW).
226		:- else.
227		start_profile_rule(_).
228		stop_profile_rule(_,_,_,_,_).
229		:- endif.
230
231
232		assure_single_rules([],_Rule) :- !.
233		assure_single_rules(AppliedRules,Rule) :-
234		assure_single_rules2(AppliedRules,Rule).
235		:- block assure_single_rules2(?,-).
236		assure_single_rules2(_AppliedRules,none) :- !.
237		assure_single_rules2(AppliedRules,Rule) :-
238		\+ member(Rule, AppliedRules).
239
240		cleanup_phase(Phase,OTExpr,NTExpr,Mode/Rule,Path,AC,IDs) :-
241		create_texpr(OExpr,OType,OInfo,OTExpr),
242		create_texpr(NExpr,NType,NInfo,NTExpr),
243	?	cleanup_phase2(Phase,OExpr,OType,OInfo,NExpr,NType,NInfo,Mode/Rule,Path,AC,IDs).
244		cleanup_phase2(pre,OExpr,OType,OInfo,NExpr,NType,NInfo,Mode/Rule,_Path,AC,IDs) :-
245	?	cleanup_pre(OExpr,OType,OInfo,NExpr,NType,NInfo,Mode_Rule,AC,IDs),
246		(functor(Mode_Rule,'/',2) -> Mode_Rule = Mode/Rule
247		; add_internal_error('Illegal cleanup_pre rule, missing mode: ',Mode_Rule),fail).
248		cleanup_phase2(post,OExpr,OType,OInfo,NExpr,NType,NInfo,Mode/Rule,Path,AC,IDs) :-
249		cleanup_post_with_path(OExpr,OType,OInfo,NExpr,NType,NInfo,Mode_Rule,Path,AC,IDs),
250		(functor(Mode_Rule,'/',2)
251		-> Mode_Rule = Mode/Rule %,format(' cleanup_post Rule: ~w/~w~n',[Mode,Rule])
252		; add_internal_error('Illegal cleanup_post rule, missing mode: ',Mode_Rule),fail).
253
254		replace_prob_closure_record_field(field(FName,Val), NField) :-
255		Val = closure(['_zzzz_unary'],[InnerType],_),
256		replace_prob_closure(Val, NVal),
257		!,
258		NField = field(FName,b(NVal,set(InnerType),[])).
259
260		replace_prob_closure(closure(['_zzzz_unary'],_,P), NExpr) :-
261		P = b(member(b(identifier('_zzzz_unary'),_,_),ClosurePred),pred,_),
262		find_typed_identifier_uses(ClosurePred, [], UsedIds),
263		UsedIds == [],
264		!,
265		get_texpr_expr(ClosurePred, NExpr).
266		replace_prob_closure(closure(['_zzzz_unary'],T,P), value(ComputedVal)) :-
267		normalise_value_for_var(solver_result, force, closure(['_zzzz_unary'],T,P), ComputedVal),
268		ComputedVal \== closure(['_zzzz_unary'],T,P).
269
270		% enforce well-definedness of division
271		cleanup_pre(div(A,B),integer,I,div(A,B),integer,[smt_wd_added|I],multi/div_wd,[AC],[]) :-
272	?	\+ member(smt_wd_added,I), !,
273		create_texpr(not_equal(B,b(integer(0),integer,[])),pred,[],AC).
274		% replace not_equal(..) by not(equal(..))
275		% and not_member(..) by not(member(..))
276		% and not_subset_strict(..) by not(subset_strict(..))
277		% and not_subset(..) by subset(..)
278		cleanup_pre(value(closure(['_zzzz_unary'],T,P)),Type,I,Expr,Type,I,multi/rewrite_prob_closure,[],[]) :-
279		replace_prob_closure(closure(['_zzzz_unary'],T,P), Expr).
280		cleanup_pre(union(A,B),Type,_,reflexive_closure(Rel),Type,I,multi/replace_not_equal,[],[]) :-
281		A = b(event_b_identity,_,_),
282		B = b(closure(Rel),Type,I).
283		cleanup_pre(not_equal(A,B),pred,I,negation(Equal),pred,[],multi/replace_not_equal,[],[]) :-
284		create_texpr(equal(A,B),pred,I,Equal).
285		cleanup_pre(not_member(A,B),pred,I,negation(Member),pred,[],multi/replace_not_member,[],[]) :-
286		create_texpr(member(A,B),pred,I,Member).
287		cleanup_pre(not_subset_strict(A,B),pred,I,negation(Subset),pred,[],multi/replace_not_subset_strict,[],[]) :-
288		create_texpr(subset_strict(A,B),pred,I,Subset).
289		cleanup_pre(greater(Card,Integer0),pred,I,Res,pred,I,multi/replace_card_0_with_neq_empty,[],[]) :-
290		% card(S) > 0 --> S /= {}
291		Card = b(card(Set),integer,_),
292		(Integer0 = b(integer(0),integer,_); Integer0 = b(value(int(0)),integer,_)),
293		!,
294		get_texpr_type(Set, SetType),
295		Res = not_equal(Set,b(empty_set,SetType,[])).
296		cleanup_pre(less(Integer0,Card),pred,I,Res,pred,I,multi/replace_card_0_with_neq_empty,[],[]) :-
297		% 0 < card(S) --> S /= {}
298		Card = b(card(Set),integer,_),
299		(Integer0 = b(integer(0),integer,_); Integer0 = b(value(int(0)),integer,_)),
300		!,
301		get_texpr_type(Set, SetType),
302		Res = not_equal(Set,b(empty_set,SetType,[])).
303		cleanup_pre(not_equal(Card,Integer0),pred,I,Res,pred,I,multi/replace_card_0_with_neq_empty,[],[]) :-
304		% card(S) /= 0 --> S /= {}
305		Card = b(card(Set),integer,_),
306		(Integer0 = b(integer(0),integer,_); Integer0 = b(value(int(0)),integer,_)),
307		!,
308		get_texpr_type(Set, SetType),
309		Res = not_equal(Set,b(empty_set,SetType,[])).
310		cleanup_pre(not_equal(Integer0,Card),pred,I,Res,pred,I,multi/replace_card_0_with_neq_empty,[],[]) :-
311		% 0 /= card(S) --> S /= {}
312		Card = b(card(Set),integer,_),
313		(Integer0 = b(integer(0),integer,_); Integer0 = b(value(int(0)),integer,_)),
314		!,
315		get_texpr_type(Set, SetType),
316		Res = not_equal(Set,b(empty_set,SetType,[])).
317		cleanup_pre(equal(Card,Integer0),pred,I,Res,pred,I,multi/replace_card_0_with_eq_empty,[],[]) :-
318		% card(S) = 0 --> S = {}
319		Card = b(card(Set),integer,_),
320		(Integer0 = b(integer(0),integer,_); Integer0 = b(value(int(0)),integer,_)),
321		!,
322		get_texpr_type(Set, SetType),
323		Res = equal(Set,b(empty_set,SetType,[])).
324		cleanup_pre(equal(Integer0,Card),pred,I,Res,pred,I,multi/replace_card_0_with_eq_empty,[],[]) :-
325		% 0 = card(S) --> S = {}
326		Card = b(card(Set),integer,_),
327		(Integer0 = b(integer(0),integer,_); Integer0 = b(value(int(0)),integer,_)),
328		!,
329		get_texpr_type(Set, SetType),
330		Res = equal(Set,b(empty_set,SetType,[])).
331		cleanup_pre(FiniteCardConstraint,pred,I,Res,pred,I,multi/RuleDescr,[],[]) :-
332	?	rewrite_finite_card(FiniteCardConstraint, Res, RuleDescr).
333		cleanup_pre(member(A,B),pred,I,Out,pred,I,multi/replace_member_interval,[],[]) :-
334		is_interval(B,Low,Up),
335		!, % A:Low..Up <==> A>=Low & A<=Up % important for e.g. :z3-cns mxint = 500 & goal : -mxint ..mxint
336		Out = conjunct(b(greater_equal(A,Low),pred,[]),b(greater_equal(Up,A),pred,[])).
337		cleanup_pre(member(A,B),pred,I,Out,pred,I,multi/replace_member_pow1_or_fin1,[],[]) :-
338	?	is_pow1_subset(B,Set),
339		get_texpr_type(Set, SetType),
340		!, % A:POW1(Set) <==> A <: Set & A /= {}
341		Out = conjunct(b(subset(A,Set),pred,[]),b(not_equal(A,b(set_extension([]),SetType,[])),pred,[])).
342		cleanup_pre(member(A,B),pred,I,Out,pred,I,multi/replace_member_pow_or_fin,[],[]) :-
343	?	is_pow_subset(B,Set),
344		!, % A:POW(Set) <==> A <: Set
345		% A/:POW(Set) <==> A /<: Set ; does not really seem to be necessary as negation rewritten before
346		Out = subset(A,Set).
347		cleanup_pre(member(A,B),pred,I,Disj,pred,I,multi/replace_finite_member_by_disj,[],[]) :-
348		% rewrite finite set membership to disjunction of equalities
349		B = b(value(avl_set(AvlSet)),set(InnerType),_),
350		!,
351		avl_to_list(AvlSet, EnumValueList),
352		findall(Equality, (member(EnumValue-_, EnumValueList), Equality = b(equal(A,b(value(EnumValue),InnerType,[])),pred,[])), Equalities),
353		disjunct_predicates(Equalities, DisjAst),
354		DisjAst = b(Disj,_,_).
355		cleanup_pre(not_subset(A,B),pred,I,negation(Subset),pred,[],multi/replace_not_subset,[],[]) :-
356		create_texpr(subset(A,B),pred,I,Subset).
357		% replace subset_strict by subset and not_equal
358		cleanup_pre(subset_strict(A,B),pred,I,conjunct(NotEqual,Subset),pred,[],multi/replace_not_member,[],[]) :-
359		create_texpr(subset(A,B),pred,I,Subset),
360		create_texpr(not_equal(A,B),pred,I,NotEqual).
361		cleanup_pre(equal(R,S),pred,I,POut,pred,I,multi/replace_struct_equality,[],[]) :-
362		% e.g., rewrite Dom = struct(f1:{1,2},f2:{1,2}) to Dom = {rec(f1:1,f2:1),rec(f1:1,f2:2),rec(f1:2,f2:1),rec(f1:2,f2:2)}
363		S = b(value(closure(['_zzzz_unary'],[record(_)],_)),_,_),
364		get_texpr_expr(R, identifier(IdName)),
365		get_texpr_type(R, set(record(FieldTypes))),
366		solver_interface:solve_predicate(b(equal(R,S),pred,I), Bindings, _),
367		member(bind(IdName,Set), Bindings),
368		% only for finite records
369		Set \= closure(_,_,_),
370		!,
371		POut = equal(R,b(value(Set),set(record(FieldTypes)),[])).
372		% replace membership in struct by equalities to avoid powerset construction
373		cleanup_pre(member(R,S),pred,I,POut,pred,I,multi/replace_struct_membership,[],[]) :-
374		% rewrite ProB closures introduced by b_compile/6
375		get_texpr_expr(R,identifier(_)),
376		S = b(value(ProBClosure),_,_),
377		replace_prob_closure(ProBClosure, ClosureExpr),
378		ClosureExpr = struct(Proto),
379		Proto = b(value(rec(Fields)),_,_),
380		( maplist(replace_prob_closure_record_field, Fields, TFields)
381		-> NFields = TFields
382		; NFields = Fields
383		),
384		!,
385		maplist(rewrite_struct_ids(R),NFields,Constraints),
386		conjunct_predicates(Constraints,Conj),
387		get_texpr_expr(Conj,POut).
388		cleanup_pre(member(R,S),pred,I,POut,pred,I,multi/replace_struct_membership,[],[]) :-
389		get_texpr_expr(R,identifier(_)),
390		get_texpr_expr(S,struct(Proto)),
391		get_texpr_expr(Proto,value(rec(Fields))),
392		maplist(rewrite_struct_ids(R),Fields,Constraints),
393		conjunct_predicates(Constraints,Conj),
394		get_texpr_expr(Conj,POut).
395		cleanup_pre(member(E,S),pred,I,disjunct(M1,M2),pred,I,multi/split_union_in_member,[],[]) :-
396		get_texpr_expr(S,union(S1,S2)),
397		create_texpr(member(E,S1),pred,I,M1),
398		create_texpr(member(E,S2),pred,I,M2).
399		cleanup_pre(member(E,S),pred,I,conjunct(M1,M2),pred,I,multi/split_intersection_in_member,[],[]) :-
400		get_texpr_expr(S,intersection(S1,S2)),
401		create_texpr(member(E,S1),pred,I,M1),
402		create_texpr(member(E,S2),pred,I,M2).
403		cleanup_pre(member(E,S),pred,I,conjunct(M1,NotM2),pred,I,multi/split_set_subtraction_in_member,[],[]) :-
404		get_texpr_expr(S,set_subtraction(S1,S2)),
405		create_texpr(member(E,S1),pred,I,M1),
406		create_texpr(member(E,S2),pred,I,M2),
407		create_negation(M2,NotM2).
408		cleanup_pre(member(E,F),pred,I,C,pred,I,multi/rewrite_member_of_function,[],[]) :-
409		%translation_type(axiomatic),
410	?	rewrite_member_of_function(E,F,C).
411		cleanup_pre(member(E,S),pred,I,C,pred,I,multi/rewrite_member_to_disequalities,[],[]) :-
412		get_texpr_type(E,integer),
413		get_texpr_type(S,set(integer)),
414		rewrite_member_to_ge_le(E,S,C).
415		cleanup_pre(equal(S,GlobalIntSet),pred,I,C,pred,I,multi/rewrite_equal_to_disequalities,[],[]) :-
416		get_texpr_type(S,set(integer)),
417		get_texpr_expr(GlobalIntSet,integer_set(_)),
418		rewrite_equal_to_ge_le(S,GlobalIntSet,C).
419		cleanup_pre(subset(Sub,Super),pred,I,C,pred,I,multi/rewrite_subset_of_integer_set_or_interval,[],[]) :-
420		get_texpr_type(Sub,set(integer)),
421		(get_texpr_expr(Super,integer_set(_)) ; get_texpr_expr(Super,interval(_,_))),
422		rewrite_subset_of_integer_set(Sub,Super,C).
423		% if there are still interval nodes after the former rule, try to replace them by constants
424		cleanup_pre(interval(From,To),set(integer),I,NExpr,set(integer),I,multi/rewrite_constant_interval,[],[]) :-
425		precompute_values(b(interval(From,To),set(integer),I), [instantiate_quantifier_limit(0)], Precomputed),
426		Precomputed = b(TExpr,_,_),
427		TExpr \= interval(From,To),
428		!,
429		NExpr = TExpr.
430		% remaining intervals have to be rewritten to set comprehensions (introduced forall)
431		cleanup_pre(interval(From,To),set(integer),I,comprehension_set([UIdD],Pred),set(integer),I,multi/rewrite_interval_to_set_comprehension,[],[]) :-
432		translation_type(axiomatic),
433		unique_typed_id("_smt_tmp",integer,UIdD),
434		create_texpr(greater_equal(UIdD,From),pred,[],Pred1),
435		create_texpr(less_equal(UIdD,To),pred,[],Pred2),
436		conjunct_predicates([Pred1,Pred2],Pred).
437		% rewrite some operators to set comprehensions
438		% later rules will rewrite them again and introduce foralls
439		cleanup_pre(pow_subset(Set),set(set(T)),I,comprehension_set([UIdD],Pred),set(set(T)),I,multi/rewrite_pow_subset,[],[]) :-
440		translation_type(axiomatic),
441		unique_typed_id("_smt_tmp",set(T),UIdD),
442		create_texpr(subset(UIdD,Set),pred,[],Pred).
443		cleanup_pre(pow1_subset(Set),set(set(T)),I,comprehension_set([UIdD],Pred),set(set(T)),I,multi/rewrite_pow1_subset,[],[]) :-
444		translation_type(axiomatic),
445		unique_typed_id("_smt_tmp",set(T),UIdD),
446		create_texpr(subset(UIdD,Set),pred,[],PredSubset),
447		create_texpr(empty_set,set(T),[],EmptySet),
448		create_texpr(not_equal(UIdD,EmptySet),pred,[],PredNotEqual),
449		conjunct_predicates([PredSubset,PredNotEqual],Pred).
450		cleanup_pre(fin_subset(Set),set(set(T)),I,comprehension_set([UIdD],Pred),set(set(T)),I,multi/rewrite_fin_subset,[],[]) :-
451		unique_typed_id("_smt_tmp",set(T),UIdD),
452		create_texpr(subset(UIdD,Set),pred,[],Pred1),
453		create_texpr(finite(Set),pred,[],Pred2),
454		conjunct_predicates([Pred1,Pred2],Pred).
455		cleanup_pre(fin1_subset(Set),set(set(T)),I,comprehension_set([UIdD],Pred),set(set(T)),I,multi/rewrite_fin1_subset,[],[]) :-
456		unique_typed_id("_smt_tmp",set(T),UIdD),
457		create_texpr(subset(UIdD,Set),pred,[],PredSubset),
458		create_texpr(empty_set,set(T),[],EmptySet),
459		create_texpr(not_equal(UIdD,EmptySet),pred,[],PredNotEqual),
460		create_texpr(finite(Set),pred,[],PredIsFinite),
461		conjunct_predicates([PredSubset,PredNotEqual,PredIsFinite],Pred).
462		/*cleanup_pre(relations(SetA,SetB),Type,I,pow_subset(Cart),Type,I,multi/rewrite_relations,[],[]) :-
463		Type = set(IT),
464		Cart = b(cartesian_product(SetA,SetB),IT,[]).
465		cleanup_pre(partial_function(SetA,SetB),Type,I,comprehension_set([IdR],Body),Type,I,multi/rewrite_partial_function,[],[]) :-
466		translation_type(constructive),
467		Type = set(set(IT)),
468		unique_typed_id("_r", set(IT), IdR),
469		IT = couple(TA,TB),
470		get_texpr_type(SetB, TSetB),
471		TSetB = set(InnerSetTypeB),
472		Member = b(member(IdR,b(pow_subset(b(cartesian_product(SetA,SetB),set(IT),[])),set(set(IT)),[])),pred,[]),
473		Comp = b(composition(b(reverse(IdR),set(couple(TB,TA)),[]),IdR),set(couple(InnerSetTypeB,InnerSetTypeB)),[]),
474		Subset = b(subset(Comp,b(identity(SetB),set(couple(InnerSetTypeB,InnerSetTypeB)),[])),pred,[]),
475		Body = b(conjunct(Member,Subset),pred,[]).*/
476		% TO DO: rewrite all functions? -> problems with model translation; probably not worth it though
477		cleanup_pre(direct_product(SetA,SetB),Type,I,comprehension_set([UIdE,UIdF,UIdG],Pred),Type,I,multi/rewrite_direct_product,[],[]) :-
478		translation_type(axiomatic),
479		Type = set(couple(E,couple(F,G))),
480		% TODO: the typing of the comprehension set ids creates a set of couples with a different nesting !!
481		% {x,y,z|(x,y):a & (x,z):b} is not type compatible with a >< b
482		% this is corrected by the translation later to quantifiers
483		unique_typed_id("_smt_tmp",E,UIdE),
484		unique_typed_id("_smt_tmp",F,UIdF),
485		unique_typed_id("_smt_tmp",G,UIdG),
486		create_texpr(couple(UIdE,UIdF),couple(E,F),[],CEF),
487		create_texpr(couple(UIdE,UIdG),couple(E,G),[],CEG),
488		create_texpr(member(CEF,SetA),pred,[],M1),
489		create_texpr(member(CEG,SetB),pred,[],M2),
490		conjunct_predicates([M1,M2],Pred).
491		cleanup_pre(parallel_product(SetA,SetB),Type,I,comprehension_set([UIdE,UIdG,UIdF,UIdH],Pred),Type,I,multi/rewrite_parallel_product,[],[]) :-
492		translation_type(axiomatic),
493		Type = set(couple(couple(E,G),couple(F,H))),
494		% TODO: the typing of the comprehension set ids creates a set of couples with a different nesting !!
495		unique_typed_id("_smt_tmp",E,UIdE),
496		unique_typed_id("_smt_tmp",F,UIdF),
497		unique_typed_id("_smt_tmp",G,UIdG),
498		unique_typed_id("_smt_tmp",H,UIdH),
499		create_texpr(couple(UIdE,UIdF),couple(E,F),[],CEF),
500		create_texpr(couple(UIdG,UIdH),couple(G,H),[],CGH),
501		create_texpr(member(CEF,SetA),pred,[],M1),
502		create_texpr(member(CGH,SetB),pred,[],M2),
503		conjunct_predicates([M1,M2],Pred).
504		cleanup_pre(composition(Rel1,Rel2),set(couple(TD,TR)),I,comprehension_set([UIdD,UIdR],Pred),set(couple(TD,TR)),I,multi/rewrite_composition,[],[]) :-
505		% change in Z3: lambda inside recursive functions was declared unsupported until proper support is provided (see https://github.com/Z3Prover/z3/issues/5813)
506		% see mk_op_iteration_func_decl in /extensions/z3interface/src/cpp/main.cpp
507		%translation_type(axiomatic),
508		get_texpr_type(Rel1,set(couple(TD,TI))),
509		unique_typed_id("_smt_tmp",TD,UIdD),
510		unique_typed_id("_smt_tmp",TR,UIdR),
511		unique_typed_id("_smt_tmp",TI,UIdI),
512		create_texpr(couple(UIdD,UIdI),couple(TD,TI),[],CoupleDomToI),
513		create_texpr(couple(UIdI,UIdR),couple(TI,TR),[],CoupleIToRan),
514		create_texpr(member(CoupleDomToI,Rel1),pred,[],Member1),
515		create_texpr(member(CoupleIToRan,Rel2),pred,[],Member2),
516		conjunct_predicates([Member1,Member2],Inner),
517		create_exists([UIdI],Inner,Pred).
518		cleanup_pre(domain_restriction(Set,Rel),set(couple(TD,TR)),I,comprehension_set([UIdD,UIdR],Pred),set(couple(TD,TR)),I,multi/rewrite_domain_restriction,[],[]) :-
519		translation_type(axiomatic),
520		unique_typed_id("_smt_tmp",TD,UIdD),
521		unique_typed_id("_smt_tmp",TR,UIdR),
522		create_texpr(couple(UIdD,UIdR),couple(TD,TR),[],Couple),
523		create_texpr(member(Couple,Rel),pred,[],MemberOfRel),
524		create_texpr(member(UIdD,Set),pred,[],MemberOfSet),
525		conjunct_predicates([MemberOfRel,MemberOfSet],Pred).
526		cleanup_pre(domain_subtraction(Set,Rel),set(couple(TD,TR)),I,comprehension_set([UIdD,UIdR],Pred),set(couple(TD,TR)),I,multi/rewrite_domain_subtraction,[],[]) :-
527		translation_type(axiomatic),
528		unique_typed_id("_smt_tmp",TD,UIdD),
529		unique_typed_id("_smt_tmp",TR,UIdR),
530		create_texpr(couple(UIdD,UIdR),couple(TD,TR),[],Couple),
531		create_texpr(member(Couple,Rel),pred,[],MemberOfRel),
532		create_texpr(member(UIdD,Set),pred,[],MemberOfSet),
533		create_negation(MemberOfSet,NotMemberOfSet),
534		conjunct_predicates([MemberOfRel,NotMemberOfSet],Pred).
535		cleanup_pre(range_restriction(Rel,Set),set(couple(TD,TR)),I,comprehension_set([UIdD,UIdR],Pred),set(couple(TD,TR)),I,multi/rewrite_range_restriction,[],[]) :-
536		translation_type(axiomatic),
537		unique_typed_id("_smt_tmp",TD,UIdD),
538		unique_typed_id("_smt_tmp",TR,UIdR),
539		create_texpr(couple(UIdD,UIdR),couple(TD,TR),[],Couple),
540		create_texpr(member(Couple,Rel),pred,[],MemberOfRel),
541		create_texpr(member(UIdR,Set),pred,[],MemberOfSet),
542		conjunct_predicates([MemberOfRel,MemberOfSet],Pred).
543		cleanup_pre(range_subtraction(Rel,Set),set(couple(TD,TR)),I,comprehension_set([UIdD,UIdR],Pred),set(couple(TD,TR)),I,multi/rewrite_range_subtraction,[],[]) :-
544		translation_type(axiomatic),
545		unique_typed_id("_smt_tmp",TD,UIdD),
546		unique_typed_id("_smt_tmp",TR,UIdR),
547		create_texpr(couple(UIdD,UIdR),couple(TD,TR),[],Couple),
548		create_texpr(member(Couple,Rel),pred,[],MemberOfRel),
549		create_texpr(member(UIdR,Set),pred,[],MemberOfSet),
550		create_negation(MemberOfSet,NotMemberOfSet),
551		conjunct_predicates([MemberOfRel,NotMemberOfSet],Pred).
552		cleanup_pre(overwrite(Set1,Set2),set(couple(TD,TR)),I,union(Set2,DomSub),set(couple(TD,TR)),I,multi/rewrite_overwrite,[],[]) :-
553		create_texpr(domain(Set2),set(TD),[],DomainSet2),
554		create_texpr(domain_subtraction(DomainSet2,Set1),set(couple(TD,TR)),[],DomSub).
555		cleanup_pre(reverse(Set),set(couple(TA,TB)),I,UnwrappedId,set(couple(TA,TB)),I,multi/reverse_to_forall,[AC],[UId]) :-
556		translation_type(axiomatic),
557		% the reverse is replaced by an identifier (uid)
558		unique_typed_id("_smt_tmp",set(couple(TA,TB)),UId),
559		get_texpr_expr(UId,UnwrappedId),
560		% the identifer carries an additional constraint:
561		% !(ida,idb).((ida,idb) : set <-> (idb,ida) : uid)
562		unique_typed_id("_smt_tmp",TA,UIdA),
563		unique_typed_id("_smt_tmp",TB,UIdB),
564		create_texpr(couple(UIdA,UIdB),couple(TA,TB),[],CoupleAB),
565		create_texpr(couple(UIdB,UIdA),couple(TB,TA),[],CoupleBA),
566
567		create_texpr(member(CoupleAB,UId),pred,[],MemberA),
568		create_texpr(member(CoupleBA,Set),pred,[],MemberB),
569		create_implication(MemberA,MemberB,Direction1),
570		create_implication(MemberB,MemberA,Direction2),
571		% use two foralls instead of equivalence!
572		create_forall([UIdA,UIdB],Direction1,AC1),
573		create_forall([UIdA,UIdB],Direction2,AC2),
574		conjunct_predicates([AC1,AC2],AC).
575		cleanup_pre(cartesian_product(SetA,SetB),set(couple(TR,TD)),I,comprehension_set([UIdR,UIdD],Pred),set(couple(TR,TD)),I,multi/cartesian_product_to_set_comprehension,[],[]) :-
576		translation_type(axiomatic),
577		unique_typed_id("_smt_tmp",TD,UIdD),
578		unique_typed_id("_smt_tmp",TR,UIdR),
579		create_texpr(member(UIdR,SetA),pred,[],MemberOf1),
580		create_texpr(member(UIdD,SetB),pred,[],MemberOf2),
581		conjunct_predicates([MemberOf1,MemberOf2],Pred).
582		cleanup_pre(Input,pred,I,C,pred,I2,multi/function_application_in_predicate_position_1,[],[]) :-
583		Input =.. [Pred,E,Arg],
584		\+ is_list(E), % avoids quantifiers
585		is_texpr(E), is_texpr(Fun),
586		get_texpr_expr(E,function(Fun,Elem)),
587		get_texpr_type(Fun,set(couple(RanT,DomT))),
588		unique_typed_id("_smt_tmp",DomT,UId),
589		create_texpr(couple(Elem,UId),couple(RanT,DomT),[],Couple),
590		create_texpr(member(Couple,Fun),pred,[],CoupleInFun),
591		Output =.. [Pred,UId,Arg],
592		create_texpr(Output,pred,I,UIdInS),
593		conjunct_predicates([CoupleInFun,UIdInS],Inner),
594		create_exists([UId],Inner,b(C,pred,I2)).
595		cleanup_pre(Input,pred,I,C,pred,I2,multi/function_application_in_predicate_position_2,[],[]) :-
596		Input =.. [Pred,E,Arg],
597		\+ is_list(Arg), % avoids quantifiers
598		is_texpr(Arg), is_texpr(Fun),
599		get_texpr_expr(Arg,function(Fun,Elem)),
600		get_texpr_type(Fun,set(couple(RanT,DomT))),
601		unique_typed_id("_smt_tmp",DomT,UId),
602		create_texpr(couple(Elem,UId),couple(RanT,DomT),[],Couple),
603		create_texpr(member(Couple,Fun),pred,[],CoupleInFun),
604		Output =.. [Pred,E,UId],
605		create_texpr(Output,pred,I,UIdInS),
606		conjunct_predicates([CoupleInFun,UIdInS],Inner),
607		create_exists([UId],Inner,b(C,pred,I2)).
608		/*cleanup_pre(Expr,Type,I,NExpr,Type,I,multi/precompute_values,[],[]) :-
609		precompute_values_e(Expr, TNExpr),
610		Expr \= TNExpr,
611		!,
612		NExpr = TNExpr.*/
613		% in case the former two rules have not removed a function/2
614		cleanup_pre(function(F,X),Type,I,UnwrappedId,Type,I,multi/function_application_to_membership,[AC],[UId]) :-
615		unique_typed_id("_smt_tmp",Type,UId),
616		get_texpr_expr(UId,UnwrappedId),
617		get_texpr_type(F,set(FunType)),
618		create_texpr(couple(X,UId),FunType,[],CoupleInFunction),
619		create_texpr(member(CoupleInFunction,F),pred,[],AC).
620
621		% ----------------------------------------------------------------------------
622		% the following rules introduce new identifiers and quantifiers to define them
623		% thus, they should be the last rules executed and be avoided if possible
624		% some of the expressions that are rewritten here can be removed if they
625		% occur in another context, i.e. f(x) in the predicate f(x) : S
626		% see rules above
627		% ----------------------------------------------------------------------------
628		cleanup_pre(integer_set('INTEGER'),set(integer),I,UnwrappedId,set(integer),I,multi/rewrite_integer_set_if_above_fails,[AC],[UId]) :-
629		% the integer set is replaced by an identifier (uid)
630		unique_typed_id("_smt_tmp",set(integer),UId),
631		get_texpr_expr(UId,UnwrappedId),
632
633		% the identifer carries an additional constraint:
634		% !(id).(id : uid)
635		unique_typed_id("_smt_tmp",integer,IdToQuantify),
636
637		create_texpr(member(IdToQuantify,UId),pred,[],MemberIn),
638
639		create_forall([IdToQuantify],MemberIn,AC).
640		cleanup_pre(min_real(Set),real,I,UnwrappedId,real,I,multi/min_real_to_definition,Args,Ids) :-
641		cleanup_pre(min(Set),real,I,UnwrappedId,real,I,_,Args,Ids).
642		cleanup_pre(max_real(Set),real,I,UnwrappedId,real,I,multi/max_real_to_definition,Args,Ids) :-
643		cleanup_pre(max(Set),real,I,UnwrappedId,real,I,_,Args,Ids).
644		cleanup_pre(min(Set),IntOrReal,I,UnwrappedId,IntOrReal,I,multi/min_to_definition,[AC1,AC2],[UId]) :-
645		(IntOrReal == integer; IntOrReal == real),
646		unique_typed_id("_smt_tmp",IntOrReal,UId),
647		get_texpr_expr(UId,UnwrappedId),
648		% two axioms:
649		% !(x).(x : Set => uid <= x)
650		% #(x).(x : Set & uid = x)
651
652		unique_typed_id("_smt_tmp",IntOrReal,QuantifiedVar),
653
654		create_texpr(less_equal(UId,QuantifiedVar),pred,[],LessEqual),
655		create_texpr(equal(UId,QuantifiedVar),pred,[],Equal),
656		create_texpr(member(QuantifiedVar,Set),pred,[],QuantifiedInSet),
657
658		conjunct_predicates([QuantifiedInSet,Equal],ExistsInner),
659		create_implication(QuantifiedInSet,LessEqual,ForallInner),
660
661		create_exists([QuantifiedVar],ExistsInner,AC1),
662
663		create_forall([QuantifiedVar],ForallInner,AC2).
664		cleanup_pre(max(Set),IntOrReal,I,UnwrappedId,IntOrReal,I,multi/max_to_definition,[AC1,AC2],[UId]) :-
665		(IntOrReal == integer; IntOrReal == real),
666		unique_typed_id("_smt_tmp",IntOrReal,UId),
667		get_texpr_expr(UId,UnwrappedId),
668		% two axioms:
669		% !(x).(x : Set => uid >= x)
670		% #(x).(x : Set & uid = x)
671
672		unique_typed_id("_smt_tmp",IntOrReal,QuantifiedVar),
673
674		create_texpr(greater_equal(UId,QuantifiedVar),pred,[],GreaterEqual),
675		create_texpr(equal(UId,QuantifiedVar),pred,[],Equal),
676		create_texpr(member(QuantifiedVar,Set),pred,[],QuantifiedInSet),
677
678		conjunct_predicates([QuantifiedInSet,Equal],ExistsInner),
679		create_implication(QuantifiedInSet,GreaterEqual,ForallInner),
680
681		create_exists([QuantifiedVar],ExistsInner,AC1),
682
683		create_forall([QuantifiedVar],ForallInner,AC2).
684		cleanup_pre(card(Set),integer,I,UnwrappedId,integer,I,multi/card_to_exists,[AC1,AC2],[UId]) :-
685		unique_typed_id("_smt_tmp",integer,UId),
686		get_texpr_expr(UId,UnwrappedId),
687		get_texpr_type(Set,set(SetT)),
688		unique_typed_id("_smt_tmp",set(couple(integer,SetT)),ForExists),
689		create_texpr(interval(b(integer(1),integer,[]),UId),set(integer),[],Interval),
690		create_texpr(total_bijection(Interval,Set),set(set(couple(integer,SetT))),[],Bijection),
691		create_texpr(member(ForExists,Bijection),pred,[],MemberOf),
692		create_exists([ForExists],MemberOf,AC1),
693		% without the following constraint, the empty set could have any (negative) cardinality
694		create_texpr(greater_equal(UId,b(integer(0),integer,[])),pred,[],AC2).
695		cleanup_pre(finite(Set),pred,I,ExistsExpr,pred,I,multi/finite_to_forall,[],[]) :-
696		% #(b,f).(b:NATURAL & f: Set --> 0..b)
697		get_texpr_type(Set,set(ST)),
698		unique_typed_id("_smt_tmp",integer,IDB),
699		create_texpr(interval(b(integer(0),integer,[]),IDB),set(integer),[],Interval0ToB),
700		unique_typed_id("_smt_tmp",set(couple(ST,integer)),IDFun),
701		create_texpr(total_injection(Set,Interval0ToB),set(set(couple(ST,integer))),[],Functions),
702		create_texpr(member(IDFun,Functions),pred,[],Member),
703		create_exists([IDB,IDFun],Member,Exists),
704		get_texpr_expr(Exists,ExistsExpr).
705		cleanup_pre(comprehension_set(Identifiers,Pred),set(X),I,UnwrappedId,set(X),I,multi/comprehension_set_to_forall,[AC],[UId]) :-
706		% NOTE: currently the comprehension sets generated are not valid according to B typing rules
707		% expr_list_to_couple_expr corrects this
708		%(
709		translation_type(axiomatic),
710		%; translation_type(constructive), % we use Z3's lambda for constructive translation
711		% \+ (member(b(_,_,LambdaIdInfo), Identifiers), member(lambda_result(_), LambdaIdInfo))
712		%),
713		%print(X),nl, print(Identifiers),nl,
714		( expr_list_to_couple_expr(Identifiers,X,IDCouple)
715		-> true
716		; add_message(cleanup_pre, 'Could not transform comprehension_set into quantifiers:~n ', b(comprehension_set(Identifiers,Pred),set(X),I))
717		),
718		% the set comprehension is replaced by an identifier (uid)
719		unique_typed_id("_smt_tmp",set(X),UId),
720		get_texpr_expr(UId,UnwrappedId),
721		% the identifer carries an additional constraint:
722		% !(id).(Pred(id) <-> id : uid)
723		create_texpr(member(IDCouple,UId),pred,[],MemberInComprehension),
724		create_implication(Pred,MemberInComprehension,Direction1),
725		create_implication(MemberInComprehension,Pred,Direction2),
726		% use two foralls instead of equivalence!
727
728		create_forall(Identifiers,Direction1,AC1),
729		create_forall(Identifiers,Direction2,AC2),
730		conjunct_predicates([AC1,AC2],AC).
731		/* doesn't seem to be correct, see :z3-double-check rx:BOOL <-> BOOL & not(( id(BOOL) ; rx) = rx)
732		cleanup_pre(identity(Set),set(couple(SetT,SetT)),I,UnwrappedId,set(couple(SetT,SetT)),I,multi/identity_to_forall,[AC],[UId]) :-
733		translation_type(axiomatic),
734		% the identity is replaced by an identifier (uid)
735		unique_typed_id("_smt_tmp",set(couple(SetT,SetT)),UId),
736		get_texpr_expr(UId,UnwrappedId),
737		% the identifer carries an additional constraint:
738		% !(id).(id : set <-> (id,id) : uid)
739		unique_typed_id("_smt_tmp",SetT,UIdInSet),
740		create_texpr(couple(UIdInSet,UIdInSet),couple(SetT,SetT),[],IdCouple),
741		create_texpr(member(UIdInSet,Set),pred,[],MemberInSet),
742		create_texpr(member(IdCouple,UId),pred,[],MemberInIdentity),
743		create_implication(MemberInIdentity,MemberInSet,Direction1),
744		create_implication(MemberInSet,MemberInIdentity,Direction2),
745		% use two foralls instead of equivalence!
746
747		create_forall([UIdInSet],Direction1,AC1),
748		create_forall([UIdInSet],Direction2,AC2),
749		conjunct_predicates([AC1,AC2],AC).*/
750		cleanup_pre(domain(Set),set(TD),I,UnwrappedId,set(TD),I,multi/domain_to_forall,[AC],[UId]) :-
751		translation_type(axiomatic),
752		% the alternative translation of domain and range using lambda is not supported by the incremental solver
753		% because an existential quantification is used in the body of the lambda ("internalization of exists is not supported")
754		% we thus rewrite these operators here if the incremental solver is used, otherwise they are translated in z3interface/../main.cpp
755		% the domain is replaced by an identifier (uid)
756		get_texpr_type(Set,set(couple(TD,TR))),
757		unique_typed_id("_smt_tmp",set(TD),UId),
758		get_texpr_expr(UId,UnwrappedId),
759		% the identifer carries an additional constraint:
760		% !(id).(id : uid <-> #(idr) : (id,idr) : set)
761		unique_typed_id("_smt_tmp",TD,UIdInDomain),
762		unique_typed_id("_smt_tmp",TR,UIdInRange),
763
764		create_texpr(couple(UIdInDomain,UIdInRange),couple(TD,TR),[],CoupleDR),
765		create_texpr(member(CoupleDR,Set),pred,[],CoupleInSet),
766		create_exists([UIdInRange],CoupleInSet,ExistsRanElement),
767
768		create_texpr(member(UIdInDomain,UId),pred,[],MemberInDomain),
769
770		create_implication(ExistsRanElement,MemberInDomain,Direction1),
771		create_implication(MemberInDomain,ExistsRanElement,Direction2),
772		% use two foralls instead of equivalence!
773
774		create_forall([UIdInDomain],Direction1,AC1),
775		create_forall([UIdInDomain],Direction2,AC2),
776		conjunct_predicates([AC1,AC2],AC).
777		cleanup_pre(range(Set),set(TR),I,UnwrappedId,set(TR),I,multi/range_to_forall,[AC],[UId]) :-
778		(member(no_lambda_translation, I); translation_type(axiomatic)),
779		% the range is replaced by an identifier (uid)
780		get_texpr_type(Set,set(couple(TD,TR))),
781		unique_typed_id("_smt_tmp",set(TR),UId),
782		get_texpr_expr(UId,UnwrappedId),
783		% the identifer carries an additional constraint:
784		% !(id).(id : uid <-> #(idd) : (idd,id) : set)
785		unique_typed_id("_smt_tmp",TD,UIdInDomain),
786		unique_typed_id("_smt_tmp",TR,UIdInRange),
787
788		create_texpr(couple(UIdInDomain,UIdInRange),couple(TD,TR),[],CoupleDR),
789		create_texpr(member(CoupleDR,Set),pred,[],CoupleInSet),
790		create_exists([UIdInDomain],CoupleInSet,ExistsDomElement),
791
792		create_texpr(member(UIdInRange,UId),pred,[],MemberInRange),
793		create_implication(ExistsDomElement,MemberInRange,Direction1),
794		create_implication(MemberInRange,ExistsDomElement,Direction2),
795		% use two foralls instead of equivalence!
796
797		create_forall([UIdInRange],Direction1,AC1),
798		create_forall([UIdInRange],Direction2,AC2),
799		conjunct_predicates([AC1,AC2],AC).
800		cleanup_pre(image(Function,Set),set(TR),I,UnwrappedId,set(TR),I,multi/image_to_forall,[AC],[UId]) :-
801		translation_type(axiomatic),
802		% the image is replaced by an identifier (uid)
803		get_texpr_type(Function,set(couple(TD,TR))),
804		unique_typed_id("_smt_tmp",set(TR),UId),
805		get_texpr_expr(UId,UnwrappedId),
806		% the identifer carries an additional constraint:
807		% !(idr).(idr : uid <-> #(idd) : idd:set & (idd,idr) : function)
808		unique_typed_id("_smt_tmp",TD,UIdInDomain),
809		unique_typed_id("_smt_tmp",TR,UIdInRange),
810
811		create_texpr(couple(UIdInDomain,UIdInRange),couple(TD,TR),[],CoupleDR),
812		create_texpr(member(CoupleDR,Function),pred,[],CoupleInFunction),
813		create_texpr(member(UIdInDomain,Set),pred,[],DomElementInSet),
814		conjunct_predicates([CoupleInFunction,DomElementInSet],ExistsInner),
815		create_exists([UIdInDomain],ExistsInner,RHS),
816
817		create_texpr(member(UIdInRange,UId),pred,[],LHS),
818
819		create_implication(LHS,RHS,Direction1),
820		create_implication(RHS,LHS,Direction2),
821		% use two foralls instead of equivalence!
822
823		create_forall([UIdInRange],Direction1,AC1),
824		create_forall([UIdInRange],Direction2,AC2),
825		conjunct_predicates([AC1,AC2],AC).
826		cleanup_pre(external_pred_call('LEQ_SYM',_),pred,I,truth,pred,I,multi/remove_leq_sym,[],[]) :-
827		debug_println(19,'Ignoring LEQ_SYM predicate').
828
829		cleanup_post_with_path(OExpr,OType,OInfo,NExpr,NType,NInfo,Mode/Rule,_Path,[],[]) :-
830		cleanup_post(OExpr,OType,OInfo,NExpr,NType,NInfo,Mode/Rule).
831		% remove membership / subset if only used for typing
832		cleanup_post(subset(A,B),pred,I,truth,pred,[was(subset(A,B))|I],multi/remove_type_subset) :-
833		is_just_type(B), !.
834		cleanup_post(member(X,B),pred,I,truth,pred,[was(member(X,B))|I],multi/remove_type_member) :-
835		is_just_type(B), !.
836		cleanup_post(not_member(X,B),pred,I,falsity,pred,[was(not_member(X,B))|I],multi/remove_type_not_member) :-
837		is_just_type(B), !.
838
839		% using create_couple would be much easier:
840		%expr_list_to_couple_expr(Exprs,TypeOfCoupleExpr,Result) :- !, bsyntaxtree:create_couple(Exprs,Result).
841		% but we seem to need this more complex version due to the fact that some translation rules
842		% like for parallel or direct_product generate incorrect comprehension sets
843		expr_list_to_couple_expr(Exprs,TypeOfCoupleExpr,Result) :-
844		expr_list_to_couple_expr(Exprs,TypeOfCoupleExpr,[],Result).
845		expr_list_to_couple_expr([T],_Type,[],R) :- !, T=R.
846		expr_list_to_couple_expr([E|Es],couple(TA,TR),Rest,R) :-
847		get_texpr_type(E,TA),!, % type is matching
848		expr_list_to_couple_expr(Es,TR,Rest,RHS),
849		get_texpr_type(RHS,RHST), get_texpr_type(E,ET),
850		create_texpr(couple(E,RHS),couple(ET,RHST),[],R).
851		expr_list_to_couple_expr(Es,couple(TA,TR),Rest,R) :-
852		TA = couple(SA,SB),
853		expr_list_to_couple_expr(Es,SA,TRest,LHS),
854		!,
855		expr_list_to_couple_expr(TRest,SB,TRest2,RHS),
856		get_texpr_type(RHS,RHST), get_texpr_type(LHS,LHST),
857		create_texpr(couple(LHS,RHS),couple(LHST,RHST),[],R1),
858		expr_list_to_couple_expr(TRest2,TR,Rest,R2),
859		!,
860		get_texpr_type(R1,R1T), get_texpr_type(R2,R2T),
861		create_texpr(couple(R1,R2),couple(R1T,R2T),[],R).
862		expr_list_to_couple_expr([T|Ts],_Type,Ts,R) :- !, T=R.
863
864		is_interval(BT,Low,Up) :-
865		get_texpr_expr(BT,B),
866		( B = interval(Low,Up) -> true
867		; B = value(Val), nonvar(Val),
868		is_interval_closure(Val,L,U) ->
869		Low = b(integer(L),integer,[]),
870		Up = b(integer(U),integer,[])).
871
872
873		rewrite_subset_of_integer_set(Sub,Super,COut) :-
874		unique_typed_id("_smt_tmp",integer,ForAllVar),
875		create_texpr(member(ForAllVar,Sub),pred,[],LHS),
876		create_texpr(member(ForAllVar,Super),pred,[],RHS), % will be replaced by another rule
877		create_implication(LHS,RHS,Inner),
878		create_forall([ForAllVar],Inner,C),
879		get_texpr_expr(C,COut).
880
881		rewrite_struct_ids(Record,field(Id,TPowerset),Constraint) :-
882		% b_compile/6 might have transformed ASTs to values
883		TPowerset \= b(_,_,_),
884		!,
885		get_texpr_type(Record,record([field(_,IdType)|_])),
886		Powerset = b(value(TPowerset),set(IdType),[]),
887		create_texpr(record_field(Record,Id),IdType,[],TheField),
888		create_texpr(member(TheField,Powerset),pred,[],Constraint).
889		rewrite_struct_ids(Record,field(Id,Powerset),Constraint) :-
890		get_texpr_type(Powerset,set(IdType)),
891		create_texpr(record_field(Record,Id),IdType,[],TheField),
892		create_texpr(member(TheField,Powerset),pred,[],Constraint).
893
894		% relations
895		rewrite_member_of_function(ID,Function,TypeConstraintOut) :-
896		get_texpr_expr(Function,relations(Dom,Ran)),
897		get_texpr_type(Function,set(set(couple(DomT,RanT)))),
898		% relations: only typing constraint !(x,y).((x,y) : ID => x : Dom & y : Ran)
899		unique_typed_id("_smt_tmp",DomT,UIdDom),
900		unique_typed_id("_smt_tmp",RanT,UIdRan),
901		create_texpr(couple(UIdDom,UIdRan),couple(DomT,RanT),[],UIdCouple),
902		create_texpr(member(UIdCouple,ID),pred,[],LHS),
903		create_texpr(member(UIdDom,Dom),pred,[],RHS1),
904		create_texpr(member(UIdRan,Ran),pred,[],RHS2),
905		conjunct_predicates([RHS1,RHS2],RHS),
906		create_implication(LHS,RHS,TypeConsInner),
907
908		create_forall([UIdDom,UIdRan],TypeConsInner,TypeConstraint),
909		get_texpr_expr(TypeConstraint,TypeConstraintOut).
910		rewrite_member_of_function(ID,Function,ConstraintOut) :-
911		get_texpr_expr(Function,total_relation(Dom,Ran)),
912		get_texpr_type(Function,set(set(couple(DomT,RanT)))),
913		% total_relation: relation & !(x).(x : Dom => #(y).(y : Ran & (x,y):Id))
914		unique_typed_id("_smt_tmp",DomT,UIdDom),
915		unique_typed_id("_smt_tmp",RanT,UIdRan),
916		create_texpr(couple(UIdDom,UIdRan),couple(DomT,RanT),[],UIdCouple),
917		create_texpr(member(UIdCouple,ID),pred,[],CoupleInID),
918		create_exists([UIdRan],CoupleInID,RHS),
919		create_texpr(member(UIdDom,Dom),pred,[],LHS),
920		create_implication(LHS,RHS,FunConsInner),
921		create_forall([UIdDom],FunConsInner,FunConstraint),
922		create_texpr(relations(Dom,Ran),set(set(couple(DomT,RanT))),[],Relations),
923		create_texpr(member(ID,Relations),pred,[],IsRelation),
924		ConstraintOut = conjunct(IsRelation,FunConstraint).
925		rewrite_member_of_function(ID,Function,ConstraintOut) :-
926		get_texpr_expr(Function,surjection_relation(Dom,Ran)),
927		get_texpr_type(Function,set(set(couple(DomT,RanT)))),
928		% surjection_relation: relation & ran = T
929		create_texpr(range(ID),set(RanT),[],Range),
930		create_texpr(equal(Range,Ran),pred,[],FunConstraint),
931		create_texpr(relations(Dom,Ran),set(set(couple(DomT,RanT))),[],Relations),
932		create_texpr(member(ID,Relations),pred,[],IsRelation),
933		ConstraintOut = conjunct(IsRelation,FunConstraint).
934		rewrite_member_of_function(ID,Function,ConstraintOut) :-
935		get_texpr_expr(Function,total_surjection_relation(Dom,Ran)),
936		get_texpr_type(Function,set(set(couple(DomT,RanT)))),
937		% total_surjection_relation: total_relation & surjection_relation
938		create_texpr(total_relation(Dom,Ran),set(set(couple(DomT,RanT))),[],TotalRelations),
939		create_texpr(member(ID,TotalRelations),pred,[],IsTotalRelation),
940		create_texpr(surjection_relation(Dom,Ran),set(set(couple(DomT,RanT))),[],SurjectionRelations),
941		create_texpr(member(ID,SurjectionRelations),pred,[],IsSurjectionRelation),
942		ConstraintOut = conjunct(IsTotalRelation,IsSurjectionRelation).
943		% functions
944		rewrite_member_of_function(ID,Function,ConstraintOut) :-
945		get_texpr_expr(Function,partial_function(Dom,Ran)),
946		get_texpr_type(Function,set(set(couple(DomT,RanT)))),
947		% partial_function: relation & !(x,y,z).((x,y) : ID & (x,z) : ID => y = z)
948		unique_typed_id("_smt_tmp",DomT,UIdDom),
949		unique_typed_id("_smt_tmp",RanT,UIdRan),
950		unique_typed_id("_smt_tmp",RanT,UIdRan2),
951		create_texpr(couple(UIdDom,UIdRan),couple(DomT,RanT),[],UIdCouple),
952		create_texpr(couple(UIdDom,UIdRan2),couple(DomT,RanT),[],UIdCouple2),
953		create_texpr(member(UIdCouple,ID),pred,[],C1InID),
954		create_texpr(member(UIdCouple2,ID),pred,[],C2InID),
955		create_texpr(equal(UIdRan,UIdRan2),pred,[],RHS),
956		conjunct_predicates([C1InID,C2InID],LHS),
957		create_implication(LHS,RHS,FunConsInner),
958
959		create_forall([UIdDom,UIdRan,UIdRan2],FunConsInner,FunConstraint),
960		% add typing: is a relation
961		create_texpr(relations(Dom,Ran),set(set(couple(DomT,RanT))),[],Relations),
962		create_texpr(member(ID,Relations),pred,[],IsRelation),
963		ConstraintOut = conjunct(IsRelation,FunConstraint).
964		rewrite_member_of_function(ID,Function,ConstraintOut) :-
965		get_texpr_expr(Function,total_function(Dom,Ran)),
966		get_texpr_type(Function,set(set(couple(DomT,RanT)))),
967		% total_function: partial_function & !(x).(x : Dom => #(y).(y : Ran & (x,y):Id))
968		unique_typed_id("_smt_tmp",DomT,UIdDom),
969		unique_typed_id("_smt_tmp",RanT,UIdRan),
970		create_texpr(couple(UIdDom,UIdRan),couple(DomT,RanT),[],UIdCouple),
971		create_texpr(member(UIdCouple,ID),pred,[],CoupleInID),
972		create_exists([UIdRan],CoupleInID,RHS),
973		create_texpr(member(UIdDom,Dom),pred,[],LHS),
974		create_implication(LHS,RHS,FunConsInner),
975		create_forall([UIdDom],FunConsInner,FunConstraint),
976		% add typing: is a partial_function
977		create_texpr(partial_function(Dom,Ran),set(set(couple(DomT,RanT))),[],PFunctions),
978		create_texpr(member(ID,PFunctions),pred,[],IsPFunction),
979		ConstraintOut = conjunct(IsPFunction,FunConstraint).
980		% injections
981		rewrite_member_of_function(ID,Function,ConstraintOut) :-
982		get_texpr_expr(Function,partial_injection(Dom,Ran)),
983		get_texpr_type(Function,set(set(couple(DomT,RanT)))),
984		% partial_injection: partial_function & !(x1,x2,y).((x1,y) : ID & (x2,y) : ID => x1 = x2)
985		unique_typed_id("_smt_tmp",DomT,UIdDom1),
986		unique_typed_id("_smt_tmp",DomT,UIdDom2),
987		unique_typed_id("_smt_tmp",RanT,UIdRan),
988		create_texpr(couple(UIdDom1,UIdRan),couple(DomT,RanT),[],UIdCouple),
989		create_texpr(couple(UIdDom2,UIdRan),couple(DomT,RanT),[],UIdCouple2),
990		create_texpr(member(UIdCouple,ID),pred,[],C1InID),
991		create_texpr(member(UIdCouple2,ID),pred,[],C2InID),
992		create_texpr(equal(UIdDom1,UIdDom2),pred,[],RHS),
993		conjunct_predicates([C1InID,C2InID],LHS),
994		create_implication(LHS,RHS,FunConsInner),
995
996		create_forall([UIdDom1,UIdDom2,UIdRan],FunConsInner,FunConstraint),
997		% add typing: is a partial_function
998		create_texpr(partial_function(Dom,Ran),set(set(couple(DomT,RanT))),[],PartialFunctions),
999		create_texpr(member(ID,PartialFunctions),pred,[],IsPartialFunction),
1000		ConstraintOut = conjunct(IsPartialFunction,FunConstraint).
1001		rewrite_member_of_function(ID,Function,ConstraintOut) :-
1002		get_texpr_expr(Function,total_injection(Dom,Ran)),
1003		get_texpr_type(Function,set(set(couple(DomT,RanT)))),
1004		% total_injection: total_function & partial_injection
1005		create_texpr(total_function(Dom,Ran),set(set(couple(DomT,RanT))),[],TotalFunctions),
1006		create_texpr(member(ID,TotalFunctions),pred,[],IsTotalFunction),
1007		create_texpr(partial_injection(Dom,Ran),set(set(couple(DomT,RanT))),[],PartialInjections),
1008		create_texpr(member(ID,PartialInjections),pred,[],IsPartialInjection),
1009		ConstraintOut = conjunct(IsTotalFunction,IsPartialInjection).
1010		% surjections
1011		rewrite_member_of_function(ID,Function,ConstraintOut) :-
1012		get_texpr_expr(Function,partial_surjection(Dom,Ran)),
1013		get_texpr_type(Function,set(set(couple(DomT,RanT)))),
1014		% partial_surjection: partial_function & ran = T
1015		create_texpr(range(ID),set(RanT),[],TRange),
1016		% TO DO: there is a bug when translating this range as a lambda function, happens for card, possible bug in Z3
1017		add_texpr_infos(TRange, [no_lambda_translation], Range),
1018		create_texpr(equal(Range,Ran),pred,[],FunConstraint),
1019		% add typing: is a partial_function
1020		create_texpr(partial_function(Dom,Ran),set(set(couple(DomT,RanT))),[],PFunctions),
1021		create_texpr(member(ID,PFunctions),pred,[],IsPFunction),
1022		ConstraintOut = conjunct(IsPFunction,FunConstraint).
1023		rewrite_member_of_function(ID,Function,ConstraintOut) :-
1024		get_texpr_expr(Function,total_surjection(Dom,Ran)),
1025		get_texpr_type(Function,set(set(couple(DomT,RanT)))),
1026		% total_surjection: total_function & partial_surjection
1027		create_texpr(total_function(Dom,Ran),set(set(couple(DomT,RanT))),[],TotalFunctions),
1028		create_texpr(member(ID,TotalFunctions),pred,[],IsTotalFunction),
1029		create_texpr(partial_surjection(Dom,Ran),set(set(couple(DomT,RanT))),[],PartialSurjections),
1030		create_texpr(member(ID,PartialSurjections),pred,[],IsPartialSurjection),
1031		ConstraintOut = conjunct(IsTotalFunction,IsPartialSurjection).
1032		% bijections
1033		rewrite_member_of_function(ID,Function,ConstraintOut) :-
1034		get_texpr_expr(Function,partial_bijection(Dom,Ran)),
1035		get_texpr_type(Function,set(set(couple(DomT,RanT)))),
1036		% partial_bijection: partial_surjection & partial_injection
1037		create_texpr(partial_surjection(Dom,Ran),set(set(couple(DomT,RanT))),[],PartialSurjections),
1038		create_texpr(member(ID,PartialSurjections),pred,[],IsPartialSurjection),
1039		create_texpr(partial_injection(Dom,Ran),set(set(couple(DomT,RanT))),[],PartialInjections),
1040		create_texpr(member(ID,PartialInjections),pred,[],IsPartialInjection),
1041		ConstraintOut = conjunct(IsPartialSurjection,IsPartialInjection).
1042		rewrite_member_of_function(ID,Function,ConstraintOut) :-
1043		get_texpr_expr(Function,total_bijection(Dom,Ran)),
1044		get_texpr_type(Function,set(set(couple(DomT,RanT)))),
1045		% total_bijection: total_surjection & total_injection
1046		create_texpr(total_surjection(Dom,Ran),set(set(couple(DomT,RanT))),[],TotalSurjections),
1047		create_texpr(member(ID,TotalSurjections),pred,[],IsTotalSurjection),
1048		create_texpr(total_injection(Dom,Ran),set(set(couple(DomT,RanT))),[],TotalInjections),
1049		create_texpr(member(ID,TotalInjections),pred,[],IsTotalInjection),
1050		ConstraintOut = conjunct(IsTotalSurjection,IsTotalInjection).
1051
1052		rewrite_equal_to_ge_le(ID,GlobalSet,Constraint) :-
1053		unique_typed_id("_smt_tmp",integer,UId),
1054		create_texpr(member(UId,ID),pred,[],UIdInSet),
1055		rewrite_member_to_ge_le(UId,GlobalSet,GeLeConstraints),
1056		create_texpr(GeLeConstraints,pred,[],GeLeTexpr),
1057		create_implication(UIdInSet,GeLeTexpr,Direction1),
1058		create_implication(GeLeTexpr,UIdInSet,Direction2),
1059
1060		create_forall([UId],Direction1,FA1),
1061		create_forall([UId],Direction2,FA2),
1062		Constraint = conjunct(FA1,FA2).
1063
1064		rewrite_global_set_nat_or_int_value(b(value(global_set('NATURAL')),set(integer),Info), Out) :-
1065		!,
1066		Out = b(integer_set('NATURAL'),set(integer),Info).
1067		rewrite_global_set_nat_or_int_value(b(value(global_set('NATURAL1')),set(integer),Info), Out) :-
1068		!,
1069		Out = b(integer_set('NATURAL1'),set(integer),Info).
1070		rewrite_global_set_nat_or_int_value(b(value(global_set('NAT')),set(integer),Info), Out) :-
1071		!,
1072		Out = b(integer_set('NAT'),set(integer),Info).
1073		rewrite_global_set_nat_or_int_value(b(value(global_set('NAT1')),set(integer),Info), Out) :-
1074		!,
1075		Out = b(integer_set('NAT1'),set(integer),Info).
1076		rewrite_global_set_nat_or_int_value(b(value(global_set('INT')),set(integer),Info), Out) :-
1077		!,
1078		Out = b(integer_set('INT'),set(integer),Info).
1079		rewrite_global_set_nat_or_int_value(In, In).
1080
1081		rewrite_member_to_ge_le(ID,Set,Constraint) :-
1082		get_texpr_expr(Set,interval(Low,High)),
1083		create_texpr(greater_equal(ID,Low),pred,[],Lower),
1084		create_texpr(greater_equal(High,ID),pred,[],Higher),
1085		Constraint = conjunct(Lower,Higher).
1086		rewrite_member_to_ge_le(ID,Set,Constraint) :-
1087		rewrite_global_set_nat_or_int_value(Set, NSet),
1088		get_texpr_expr(NSet,integer_set(Kind)), % no cut here see rule below
1089		bzero(BZero), bone(BOne), bminint(MinInt), bmaxint(MaxInt),
1090		create_texpr(greater_equal(ID,LowerBound),pred,[],Lower),
1091		create_texpr(greater_equal(UpperBound,ID),pred,[],Higher),
1092		Constraint = conjunct(Lower,Higher),
1093		(Kind = 'NAT' -> LowerBound = BZero, UpperBound = MaxInt ;
1094		Kind = 'NAT1' -> LowerBound = BOne, UpperBound = MaxInt ;
1095		Kind = 'INT' -> LowerBound = MinInt, UpperBound = MaxInt).
1096		rewrite_member_to_ge_le(ID,Set,Constraint) :-
1097		rewrite_global_set_nat_or_int_value(Set, NSet),
1098		get_texpr_expr(NSet,integer_set(Kind)), !,
1099		bzero(BZero), bone(BOne),
1100		(Kind = 'NATURAL' -> Constraint = greater_equal(ID,BZero) ;
1101		Kind = 'NATURAL1' -> Constraint = greater_equal(ID,BOne)).
1102
1103		bzero(b(integer(0),integer,[])).
1104		bone(b(integer(1),integer,[])).
1105		bminint(b(min_int,integer,[])).
1106		bmaxint(b(max_int,integer,[])).