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