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
6		:- module(predicate_analysis,[predicate_analysis/5
7		,predicate_analysis_with_global_sets/5
8		,info_conjunct/3
9		,info_disjunct/3
10		,test_predicate_analysis/0
11		,max_type_cardinality/2
12		]).
13
14		:- use_module(library(lists)).
15		:- use_module(library(avl)).
16		:- use_module(library(ordsets)).
17		:- use_module(library(terms)).
18
19		:- use_module(probsrc(bsyntaxtree)).
20		:- use_module(probsrc(btypechecker)).
21		:- use_module(probsrc(preferences)).
22		:- use_module(probsrc(tools)).
23		:- use_module(probsrc(translate)).
24		:- use_module(probsrc(bmachine)).
25		:- use_module(probsrc(b_global_sets), [is_b_global_constant/3,b_global_set_cardinality/2]).
26
27		:- use_module(probsrc(error_manager)).
28		:- use_module(probsrc(self_check)).
29		:- use_module(probsrc(debug),[debug_println/2, formatsilent/2, debug_format/3]).
30
31		:- use_module(probsrc(inf_arith)).
32		:- use_module(kodkodsrc(interval_calc)).
33
34		% for interpreting value(...) components
35		:- use_module(probsrc(store), [empty_state/1]).
36		:- use_module(probsrc(b_interpreter), [b_compute_expression_nowf/6]).
37
38		:- use_module(probsrc(module_information),[module_info/2]).
39		:- module_info(group,kodkod).
40		:- module_info(description,'This is a module and plugin to extract information about expressions (e.g. integer bounds (aka intervals), cardinality) by static analysis. Used by Kodkod.').
41
42		:- dynamic debugging_enabled/0.
43		:- load_files(library(system), [when(compile_time), imports([environ/2])]).
44		% avl_apply
45		% similar to avl_fetch_pair: but checks whether we have a function
46		% and whether the function is defined for the key
47		:- if(environ(debug_kodkod,true)).
48		debugging_enabled. % commment in to have dot files written to debug-constraint-anim folder (interval analysis for kodkod)
49		:- endif.
50
51		% the following is called by kodkod:
52		predicate_analysis_with_global_sets(Tree,ROIdentifiers,Identifiers,NewIdentifiers,NewTree) :-
53		findall(X,
54		(bmachine_is_precompiled,
55		b_get_machine_set(Set),
56		b_global_set_cardinality(Set,Card),
57		create_texpr(identifier(Set),set(global(Set)),[analysis([card:irange(Card,Card)])],X)),
58		Sets),
59		findall(X,
60		(bmachine_is_precompiled,
61		is_b_global_constant(Set,_Index,Elem),
62		create_texpr(identifier(Elem),global(Set),[],X)),
63		Elements),
64		append([ROIdentifiers,Sets,Elements],ROIds2),
65	?	predicate_analysis(Tree,ROIds2,Identifiers,NewIdentifiers,NewTree).
66
67
68		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
69		% static analysis of integers
70
71		:- volatile nodecounter/1, debug_node/2, debug_constraints/1.
72		:- dynamic nodecounter/1, debug_node/2, debug_constraints/1.
73
74		predicate_analysis(Tree,ROIdentifiers,Identifiers,NewIdentifiers,NewTree) :-
75		reset_nodecounter,
76		debug_println(15,starting_predicate_analysis),
77		start_ms_timer(Timer1),
78		create_node_environment(ROIdentifiers,Identifiers,NewIdentifiers,NodeEnv,Infos1),
79		(debug:debug_mode(on) -> stop_ms_timer_with_msg(Timer1,create_node_environment) ; true),
80		start_ms_timer(Timer2),
81		extract_nodes(Tree,NodeEnv,_Node,_Mode,NewTree,(Constraints,Infos),Infos1),
82		(debug:debug_mode(on) -> stop_ms_timer_with_msg(Timer2,extract_nodes) ; true),
83		start_ms_timer(Timer3),
84		create_constraint_tree(Constraints,Nodes,CTree),
85		(debug:debug_mode(on) -> stop_ms_timer_with_msg(Timer3,create_constraint_tree) ; true),
86		retractall(debug_constraints(_)),assertz(debug_constraints(Constraints)),
87		create_initial_information(Nodes,Empty),
88		apply_start_constraints(Constraints,ChangedNodes,Empty,Initial),
89		compute_maximum_iterations(Nodes,MaxIter),
90		start_ms_timer(Timer4),
91	?	do_analysis(ChangedNodes,2,MaxIter,CTree,Initial,Values),
92		(debug:debug_mode(on) -> stop_ms_timer_with_msg(Timer4,do_analysis(MaxIter)) ; true),
93		start_ms_timer(Timer5),
94		insert_info(Infos,Values),
95		(debug:debug_mode(on) -> stop_ms_timer_with_msg(Timer5,insert_info) ; true).
96
97		create_node_environment(ROIdentifiers,Identifiers,NewIdentifiers,NodeEnv,Infos) :-
98		initial_node_env(InitNodeEnv),
99		create_identifier_nodes2(ROIdentifiers,_,InitNodeEnv,RONodeEnv1,Infos1,([],[])),
100		identifier_nodes_readonly(RONodeEnv1,RONodeEnv),
101		create_identifier_nodes2(Identifiers,NewIdentifiers,RONodeEnv,NodeEnv,Infos2,Infos1),
102		foldl(add_id_basic_constraint(NodeEnv),Identifiers,Infos,Infos2).
103		add_id_basic_constraint(NodeEnv,Identifier,In,Out) :-
104		get_texpr_id(Identifier,Id),
105		identifier_node_lookup(Id,NodeEnv,_NodeId,Nodes,_Mode),
106		add_type_constraints(Identifier,Nodes,In,Out).
107
108		% just a heuristic to avoid a non-terminating run
109		compute_maximum_iterations(Nodes,MaxIter) :-
110		length(Nodes,N), MaxIter is N*10.
111
112		reset_nodecounter :-
113		retractall(nodecounter(_)),assertz(nodecounter(1)),
114		retractall(debug_node(_,_)),
115		retractall(debug_constraints(_)).
116
117		% create a numbered node for each identifier
118		initial_node_env(NodeEnv) :- empty_avl(NodeEnv).
119
120		%create_identifier_nodes(Ids,NIds,Env,IIn,IOut) :-
121		% empty_avl(Start), create_identifier_nodes2(Ids,NIds,Start,Env,IIn,IOut).
122
123		create_identifier_nodes2([],[],Env,Env,Info,Info).
124		create_identifier_nodes2([TId|Rest],[NTId|NRest],In,Out,IIn,IOut) :-
125		create_identifier_nodes3(TId,NTId,In,Inter,IIn,IInter),
126		create_identifier_nodes2(Rest,NRest,Inter,Out,IInter,IOut).
127		create_identifier_nodes3(TId,NTId,In,Out,IIn,IOut) :-
128		get_texpr_id(TId,Id),
129		get_texpr_type(TId,Type),
130		new_node_scope(Type,NodeId,Nodes),
131		avl_store(Id,In,nodes(NodeId,Nodes,rw),Out),
132		texpr_add_node_infos(TId,NodeId,NTId,IIn,IOut).
133
134		% look up the node of an identifier
135		identifier_node_lookup(Id,Env,NodeId,Nodes,Mode) :-
136		(avl_fetch(Id,Env,nodes(NodeId,Nodes,Mode)) -> true
137		; add_warning(kodkod,'Could not lookup identifier: ',Id),fail).
138
139		% set the complete environment to read-only,
140		% read-only nodes are not used for output of constraint nodes
141		identifier_nodes_readonly(OldEnv,NewEnv) :-
142		avl_map(set_readonly,OldEnv,NewEnv).
143		set_readonly(nodes(Id,Nodes,_Mode),nodes(Id,Nodes,ro)).
144
145		compute_integer_set('INTEGER',-inf,inf).
146		compute_integer_set('NATURAL',0,inf).
147		compute_integer_set('NATURAL1',1,inf).
148		compute_integer_set('INT',Min,Max) :-
149		get_preference(minint,Min),
150		get_preference(maxint,Max).
151		compute_integer_set('NAT',0,Max) :-
152		get_preference(maxint,Max).
153		compute_integer_set('NAT1',1,Max) :-
154		get_preference(maxint,Max).
155
156		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
157		% computation on information
158
159		info_conjunct(irange(X,Y),irange(A,B),Result) :-
160		Max infis max(X,A), Min infis min(Y,B),
161		normalise_irange(irange(Max,Min),Result).
162		info_disjunct(irange(X,Y),irange(A,B),Result) :-
163		( is_bottom(irange(X,Y)) -> Result = irange(A,B)
164		; is_bottom(irange(A,B)) -> Result = irange(X,Y)
165		;
166		Min infis min(X,A), Max infis max(Y,B),
167		normalise_irange(irange(Min,Max),Result)).
168
169		normalise_irange(In,Result) :-
170		(is_bottom(In) -> Result=irange(0,-1) ; Result=In).
171		is_bottom(irange(A,B)) :- infless(B,A).
172
173
174		has_more_information(irange(X,_Y),irange(A,_B)) :- infless(A,X),!.
175		has_more_information(irange(_X,Y),irange(_A,B)) :- infless(Y,B),!.
176		has_more_information(set(A),elem(B)) :- has_more_information(A,B).
177		has_more_information(left(A),left(B)) :- has_more_information(A,B).
178		has_more_information(right(A),right(B)) :- has_more_information(A,B).
179
180		% what kind of information may be stored in a node of a certain data type
181		get_type_scopes(Type,Scopes) :-
182		findall(S,get_type_scope(Type,S),Scopes1),
183		sort([possible_values|Scopes1],Scopes).
184		get_type_scope(integer,interval).
185		get_type_scope(set(T),elem(S)) :-
186	?	get_type_scope(T,S).
187		get_type_scope(set(_),card).
188		get_type_scope(seq(S),T) :-
189		get_type_scope(set(couple(integer,S)),T).
190		get_type_scope(couple(A,_),left(S)) :-
191	?	get_type_scope(A,S).
192		get_type_scope(couple(_,B),right(S)) :-
193		get_type_scope(B,S).
194
195		% get the top element of a scope
196		get_scope_top(interval,irange(-inf,inf)).
197		get_scope_top(possible_values,irange(0,inf)).
198		get_scope_top(elem(S),T) :- get_scope_top(S,T).
199		get_scope_top(left(S),T) :- get_scope_top(S,T).
200		get_scope_top(right(S),T) :- get_scope_top(S,T).
201		get_scope_top(card,irange(0,inf)).
202
203		get_scope_bottom(interval,irange(0,-1)).
204		get_scope_bottom(possible_values,T) :- get_scope_bottom(interval,T).
205		get_scope_bottom(elem(S),T) :- get_scope_bottom(S,T).
206		get_scope_bottom(left(S),T) :- get_scope_bottom(S,T).
207		get_scope_bottom(right(S),T) :- get_scope_bottom(S,T).
208		get_scope_bottom(card,T) :- get_scope_bottom(interval,T).
209
210		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
211		% operations on possible infinite numbers
212		%irange_union(irange(Am,AM2),irange(Bm,BM2),irange(Cm,CM2)) :-
213		% Cm infis min(Am,Bm), CM2 infis max(AM2,BM2).
214
215		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
216		% new extract
217
218		new_node_scope(Type,Id,Nodes) :-
219		new_node2(Id),get_type_scopes(Type,Scopes),
220		findall(S:Id,member(S,Scopes),Nodes).
221
222		new_node2(Id):-
223		retract(nodecounter(Id)),
224		Id2 is Id+1, assertz(nodecounter(Id2)).
225
226		extract_nodes(TExpr,NodeEnv,Nodes,Mode,NTExpr,In,Out) :-
227		get_texpr_expr(TExpr,Expr),
228		extract_nodes2(Expr,TExpr,NodeEnv,Nodes,Mode,NTExpr,In,Inter),
229		add_type_constraints(TExpr,Nodes,Inter,Out),
230		store_debug_info(Nodes,TExpr).
231		extract_nodes2(identifier(Id),TExpr,NodeEnv,Nodes,Mode,NTExpr,In,Out) :- !,
232		identifier_node_lookup(Id,NodeEnv,NodeId,Nodes,Mode),!,
233		texpr_add_node_infos(TExpr,NodeId,NTExpr,In,Out).
234		extract_nodes2(conjunct(A,B),TExpr,NodeEnv,[],rw,NTExpr,In,Out) :- !,
235		get_texpr_info(TExpr,Infos),
236		create_texpr(conjunct(NA,NB),pred,Infos,NTExpr),
237		extract_nodes(A,NodeEnv,_NodesA,_ModeA,NA,In,Inter),
238		extract_nodes(B,NodeEnv,_NodesB,_ModeB,NB,Inter,Out).
239		extract_nodes2(forall(Ids,Pre,Cond),TExpr,NodeEnv,[],rw,NTExpr,In,Out) :- !,
240		get_texpr_info(TExpr,Info),
241		create_texpr(forall(NIds,NPre,NCond),pred,Info,NTExpr),
242		identifier_nodes_readonly(NodeEnv,SubEnv1),
243		create_identifier_nodes2(Ids,NIds,SubEnv1,SubEnv,In,Inter1),
244		extract_nodes(Pre,SubEnv,_NodesPre,_ModePre,NPre,Inter1,Inter2),
245		identifier_nodes_readonly(SubEnv,ROEnv),
246		extract_nodes(Cond,ROEnv,_NodesCond,_ModeCond,NCond,Inter2,Out).
247		extract_nodes2(exists(Ids,Cond),TExpr,NodeEnv,[],rw,NTExpr,In,Out) :- !,
248		get_texpr_info(TExpr,Info),
249		create_texpr(exists(NIds,NCond),pred,Info,NTExpr),
250		create_identifier_nodes2(Ids,NIds,NodeEnv,SubEnv,In,Inter1),
251		extract_nodes(Cond,SubEnv,_NodesCond,_ModeCond,NCond,Inter1,Out).
252		extract_nodes2(general_sum([TId],TPred,TExpr),TSigma,NodeEnv,Nodes,rw,NTSigma,In,Out) :- !,
253		nodes_for_general_sum_or_mult(mult,TId,TPred,TExpr,TSigma,NodeEnv,Nodes,NTSigma,In,Out).
254		extract_nodes2(general_product([TId],TPred,TExpr),TSigma,NodeEnv,Nodes,rw,NTSigma,In,Out) :- !,
255		nodes_for_general_sum_or_mult(power_rule,TId,TPred,TExpr,TSigma,NodeEnv,Nodes,NTSigma,In,Out).
256		extract_nodes2(comprehension_set(Ids,Cond),TExpr,NodeEnv,Nodes,rw,NTExpr,In,Out) :- !,
257		get_texpr_info(TExpr,Info),
258		get_texpr_type(TExpr,Type),
259		identifier_nodes_readonly(NodeEnv,SubEnv1),
260		create_identifier_nodes2(Ids,NIds,SubEnv1,SubEnv,In,Inter1),
261		extract_nodes(Cond,SubEnv,_NodesCond,_ModeCond,NCond,Inter1,Inter2),
262		new_node_scope(Type,NodeId,Nodes),
263		compset_constraints(Nodes,Ids,SubEnv,Constraints),
264		add_all(Constraints,Inter2,Inter3),
265		add_node_infos(Info,NodeId,NInfo,Inter3,Out),
266		create_texpr(comprehension_set(NIds,NCond),Type,NInfo,NTExpr).
267		extract_nodes2(set_extension(L),TExpr,NodeEnv,LocalNodes,rw,NTExpr,In,Out) :- !,
268		get_texpr_info(TExpr,Info),
269		get_texpr_type(TExpr,Type),
270		new_node_scope(Type,NodeId,LocalNodes),
271		extract_set_extension(L,NodeEnv,LocalNodes,NTSubs,In,Inter1),
272		CardNode = card:_, memberchk(CardNode,LocalNodes),
273		length(L,MaxCard),
274		add_all([constraint([],[CardNode],constant(irange(1,MaxCard)))],
275		Inter1,Inter2),
276		add_node_infos(Info,NodeId,NewInfo,Inter2,Out),
277		create_texpr(set_extension(NTSubs),Type,NewInfo,NTExpr).
278		extract_nodes2(value(Value),TExpr,NodeEnv,LocalNodes,RW,NTExpr,In,Out) :-
279		get_texpr_info(TExpr,Infos), member(was_identifier(ID),Infos),
280		\+ ground(Value),!,
281		%print(treating_value_as_id(Value,ID)),nl,
282		extract_nodes2(identifier(ID),TExpr,NodeEnv,LocalNodes,RW,NTExpr,In,Out).
283		extract_nodes2(value(Value),TExpr,_NodeEnv,LocalNodes,rw,NTExpr,In,Out) :- nonvar(Value),
284		!,
285		get_texpr_info(TExpr,Info),
286		get_texpr_type(TExpr,Type),
287		new_node_scope(Type,NodeId,LocalNodes),
288		findall(C,extract_constraint_for_value(Type,TExpr,LocalNodes,C),Constraints),
289		add_all(Constraints,In,Inter),
290		add_node_infos(Info,NodeId,NewInfo,Inter,Out),
291		create_texpr(value(Value),Type,NewInfo,NTExpr).
292		extract_nodes2(partition(S,Es),TExpr,NodeEnv,[],rw,NTExpr,In,Out) :- !,
293		extract_nodes_l([S|Es],NodeEnv,[SNodes|EsNodeLists],_Modes,[NS|NEs],In,Inter1),
294		% subset constraints
295		findall(constraint(CI,CO,CC),
296		(member(Scope:SId,SNodes),
297		member(NodeList,EsNodeLists),member(Scope:Elem,NodeList),
298		is_subset_extract(Scope:Elem,Scope:SId,CI,CO,CC)),
299		SubsetConstraints),
300		add_all(SubsetConstraints,Inter1,Inter2),
301		% cardinality constraints
302		memberchk(card:SNodeId,SNodes),
303		findall(card:Elem2,(member(NodeList2,EsNodeLists),member(card:Elem2,NodeList2)),
304		CardNodes),
305		create_add_list_constraints(CardNodes,card:SNodeId,CardConstraints),
306		add_all(CardConstraints,Inter2,Inter3),
307		% union constraints
308		findall(constraint(ElemNodes,[elem(Scope3):SId3],union),
309		( member(elem(Scope3):SId3,SNodes),
310		findall(elem(Scope3):Elem3,
311		(member(NodeList3,EsNodeLists),member(elem(Scope3):Elem3,NodeList3)),
312		ElemNodes)),
313		UnionConstraints),
314		add_all(UnionConstraints,Inter3,Out),
315		get_texpr_info(TExpr,Info),
316		create_texpr(partition(NS,NEs),pred,Info,NTExpr).
317		extract_nodes2(sequence_extension(L),TExpr,NodeEnv,LocalNodes,rw,NTExpr,In,Out) :- !,
318		get_texpr_info(TExpr,Info),
319		get_texpr_type(TExpr,Type),
320		new_node_scope(Type,NodeId,LocalNodes),
321		extract_seq_extension(L,NodeEnv,LocalNodes,NTSubs,In,Inter1),
322		CardNode = card:_, memberchk(CardNode,LocalNodes),
323		DomNode = elem(left(interval)):_, memberchk(DomNode,LocalNodes),
324		length(L,Card),
325		add_all([constraint([],[CardNode],constant(irange(Card,Card))),
326		constraint([],[DomNode], constant(irange(1, Card)))],
327		Inter1,Inter2),
328		add_node_infos(Info,NodeId,NewInfo,Inter2,Out),
329		create_texpr(sequence_extension(NTSubs),Type,NewInfo,NTExpr).
330		extract_nodes2(empty_set,TExpr,_NodeEnv,Nodes,rw,NTExpr,In,Out) :- !,
331		get_texpr_type(TExpr,Type), new_node_scope(Type,NodeId,Nodes),
332		texpr_add_node_infos(TExpr,NodeId,NTExpr,In,Inter),
333		get_type_scopes(Type,Scopes),
334		findall(constraint([],[elem(S):NodeId],constant(Bottom)),
335		(member(elem(S),Scopes),get_scope_bottom(S,Bottom)),
336		Bottoms),
337		add_all([constraint([],[card:NodeId],constant(irange(0,0)))|Bottoms],Inter,Out).
338		extract_nodes2(Expr,TExpr,NodeEnv,Nodes,rw,NTExpr,In,Out) :-
339		same_functor(Expr,Tmp),
340	?	extract(Tmp,_,_,_,_),!,
341		syntaxtransformation(Expr,Subs,[],NSubs,NExpr),
342		copy_term((NSubs,NExpr),(NSubsRO,NExprRO)),
343		copy_term((NSubs,NExpr),(NewSubs,NewExpr)),
344		extract_nodes_l(Subs,NodeEnv,SubNodeLists,Modes,NewSubs,In,Inter),
345		ignore_readonly_nodes(Modes,SubNodeLists,SubNodeListsRO),
346		get_texpr_info(TExpr,Info),
347		get_texpr_type(TExpr,Type),
348		new_node_scope(Type,NodeId,Nodes),
349		add_node_infos(Info,NodeId,NewInfos,Inter,Inter2),
350		create_texpr(NewExpr,Type,NewInfos,NTExpr),
351		findall(constraint(InputNodes,OutputNodes,Transition),
352		( extract(NExpr,NodeId,InputNodes,OrigOutputNodes,Transition),
353		copy_term(extract(NExpr,NodeId,InputNodes,OrigOutputNodes,Transition),
354		extract(NExprRO,NodeId,_,OutputNodes,Transition)),
355		choose_one(SubNodeLists,SubNodeListsRO,NSubs,NSubsRO)),
356		Constraints),
357		%error_manager:print_error_span(TExpr),nl,print(Constraints),nl,
358		add_all(Constraints,Inter2,Out).
359		extract_nodes2(Expr,TExpr,NodeEnv,[],rw,NTExpr,In,Out) :-
360		remove_bt(TExpr,_,NExpr,NTExpr),
361		syntaxtransformation(Expr,Subs,Names,NSubs,NExpr),
362		identifier_nodes_readonly(NodeEnv,SubEnv1),
363		create_identifier_nodes2(Names,_NIds,SubEnv1,SubEnv,In,Inter1),!,
364		extract_nodes_l(Subs,SubEnv,_SubNodeLists,_Modes,NSubs,Inter1,Out).
365		extract_nodes2(_,TExpr,_,_,_,_,_,_) :-
366		throw(failed_analysis(TExpr)).
367
368		add_type_constraints(TExpr,Nodes,In,Out) :-
369		get_texpr_type(TExpr,Type),
370		findall(C, type_constraint(Type,Nodes,C), Constraints),
371		add_all(Constraints,In,Out).
372
373		type_constraint(Type,Nodes,constraint([],[possible_values:N],constant(irange(1,Card)))) :-
374	?	member(possible_values:N,Nodes),
375		max_type_cardinality(Type,Card).
376		type_constraint(set(T),Nodes,constraint([],[card:N],constant(irange(0,Card)))) :-
377	?	member(card:N,Nodes),
378		max_type_cardinality(T,Card).
379		type_constraint(integer,Nodes,constraint([interval:N],[possible_values:N],interval_possibilities)) :-
380	?	member(interval:N,Nodes),member(possible_values:N,Nodes).
381
382		max_type_cardinality(global(G),Card) :-
383		% TODO: This should be switched off if we try to determine the cardinality of the deferred sets
384		b_global_set_cardinality(G,Card).
385		max_type_cardinality(boolean,2).
386		max_type_cardinality(set(T),Card) :-
387		max_type_cardinality(T,C1),
388		% catch/3 to avoid overflow errors
389		catch( Card is ceiling(2 ** C1),
390		error(_,_),
391		fail).
392		max_type_cardinality(couple(A,B),Card) :-
393		max_type_cardinality(A,CardA),
394		max_type_cardinality(B,CardB),
395		Card is CardA * CardB.
396
397		add_existing_constraints(Info,NodeId,In,Out) :-
398		memberchk(analysis(Analysis),Info),!,
399		findall( constraint([],[Scope:NodeId],constant(Value)),
400		member(Scope:Value,Analysis),
401		Constraints),
402		add_all(Constraints,In,Out).
403		add_existing_constraints(_Info,_NodeId,In,In).
404
405		extract_constraint_for_value(Type,Value,LocalNodes,constraint([],[NodeType:NodeId],Constant)) :-
406	?	extract_constraint_for_value2(Type,Value,NodeType,Constant),
407		memberchk(NodeType:NodeId,LocalNodes).
408		extract_constraint_for_value2(set(_Type),Value,card,Constant) :-
409		compute_integer(card(Value),Card),
410		Constant = constant(irange(Card,Card)).
411		extract_constraint_for_value2(set(integer),Value,elem(interval),constant(irange(Min,Max))) :-
412		compute_integer(min(Value),Min),
413		compute_integer(max(Value),Max).
414		extract_constraint_for_value2(set(couple(TA,_)),Value,elem(left(DN)),Constant) :-
415		compute_expression(domain(Value),set(TA),Dom),
416		create_texpr(value(Dom),set(TA),[],BDom),
417		extract_constraint_for_value2(set(TA),BDom,elem(DN),Constant).
418		extract_constraint_for_value2(set(couple(_,TB)),Value,elem(right(RN)),Constant) :-
419		compute_expression(range(Value),set(TB),Ran),
420		create_texpr(value(Ran),set(TB),[],BRan),
421		extract_constraint_for_value2(set(TB),BRan,elem(RN),Constant).
422
423		compute_integer(Expr,Result) :-
424		compute_expression(Expr,integer,int(Result)).
425		compute_expression(Expr,Type,Result) :-
426		empty_state(Empty),
427		create_texpr(Expr,Type,[],BExpr),
428		b_compute_expression_nowf(BExpr,Empty,Empty,Result,'predicate analysis',0).
429
430		compset_constraints(SetNodes,Ids,NodeEnv,Constraints) :-
431		lookup_identifier_nodes(Ids,NodeEnv,NodeLists),
432		findall( C,
433		(SetNode=elem(Scope):_SetNodeId, member(SetNode,SetNodes),
434		compset_constraint(Scope,NodeLists,ElemNode),
435		member(C, [constraint([SetNode],[ElemNode],id),
436		constraint([ElemNode],[SetNode],id)])),
437		Constraints).
438		compset_constraint(left(Scope),NodeLists,Node) :- !,
439		last(Begin,_,NodeLists),
440		compset_constraint(Scope,Begin,Node).
441		compset_constraint(right(Scope),NodeLists,Node) :- !,
442		last(_,Last,NodeLists),
443		compset_constraint(Scope,[Last],Node).
444		compset_constraint(Scope,[Nodes],Scope:NodeId) :-
445		memberchk(Scope:NodeId,Nodes).
446
447		lookup_identifier_nodes([],_Env,[]).
448		lookup_identifier_nodes([TId|Irest],Env,[Nodes|Nrest]) :-
449		get_texpr_id(TId,Id),
450		identifier_node_lookup(Id,Env,_NodeId,Nodes,_Mode),
451		lookup_identifier_nodes(Irest,Env,Nrest).
452
453		/*
454		extract_set_extension([L],NodeEnv,Nodes,[NTExpr],In,Out) :- !,
455		extract_nodes(L,NodeEnv,Nodes,_Mode,NTExpr,In,Out).
456		extract_set_extension([Elem|Rest],NodeEnv,TmpNodes,[NTExpr|NTrest],In,Out) :-
457		extract_nodes(Elem,NodeEnv,ElemNodes,_Mode,NTExpr,In,Inter1),
458		extract_set_extension(Rest,NodeEnv,RestNodes,NTrest,Inter1,Inter2),
459		%append([TmpNodes,ElemNodes,RestNodes],Nodes),
460		get_texpr_type(Elem,Type),
461		new_node_scope(Type,NodeId,TmpNodes),
462		add_node_infos([],NodeId,_,Inter2,Inter3),
463		findall(C,( EN = Scope:_,
464		RN = Scope:_,
465		ON = Scope:_,
466		member(EN,ElemNodes),
467		memberchk(RN,RestNodes),
468		memberchk(ON,TmpNodes),
469		member(C,[constraint([EN,RN],[ON],union),
470		constraint([ON],[EN],id),
471		constraint([ON],[RN],id)])),
472		Constraints),
473		add_all(Constraints,Inter3,Out).
474		*/
475		extract_set_extension(Elements,NodeEnv,SeqNodes,NElements,In,Out) :-
476		extract_extension_nodes(Elements,NodeEnv,ElemNodes,NElements,In,Inter),
477		findall(n(Scope,elem(Scope):N),member(elem(Scope):N,SeqNodes),Scopes),
478		extract_ext_nodes2(Scopes,ElemNodes,Constraints),
479		add_all(Constraints,Inter,Out).
480
481		extract_seq_extension(Elements,NodeEnv,SeqNodes,NElements,In,Out) :-
482		extract_extension_nodes(Elements,NodeEnv,ElemNodes,NElements,In,Inter),
483		findall(n(Scope,elem(right(Scope)):N),member(elem(right(Scope)):N,SeqNodes),Scopes),
484		extract_ext_nodes2(Scopes,ElemNodes,Constraints),
485		add_all(Constraints,Inter,Out).
486
487		extract_ext_nodes2([],_ElemNodes,[]).
488		extract_ext_nodes2([Scope|Srest],ElemNodes,Constraints) :-
489		extract_ext_nodes3(Scope,ElemNodes,C1),
490		append(C1,C2,Constraints),
491		extract_ext_nodes2(Srest,ElemNodes,C2).
492		extract_ext_nodes3(n(Scope,SeqNode),ElemNodes,Constraints) :-
493		findall(Scope:E,
494		( member(NodeList,ElemNodes), memberchk(Scope:E,NodeList)),
495		AllElemNodes),
496		findall(constraint([SeqNode],[E],id), member(E,AllElemNodes), IdConstraints),
497		( same_length(AllElemNodes,ElemNodes) ->
498		Constraints = [constraint(AllElemNodes,[SeqNode],union)|IdConstraints]
499		; % some elements have no node, e.g., for {min(t),y}; the union of the other elements
500		% would be an unsound restriction of the set extension
501		Constraints = IdConstraints).
502
503		extract_extension_nodes([],_NodeEnv,[],[],X,X).
504		extract_extension_nodes([Elem|Rest],NodeEnv,[ElemNodes|RestNodes],[NElem|NRest],In,Out) :-
505		extract_nodes(Elem,NodeEnv,ElemNodes,_Mode,NElem,In,Inter),
506		extract_extension_nodes(Rest,NodeEnv,RestNodes,NRest,Inter,Out).
507
508
509		texpr_add_node_infos(TExpr,NodeId,NTExpr,In,Out) :-
510		get_texpr_expr(TExpr,Expr),
511		get_texpr_type(TExpr,Type),
512		get_texpr_info(TExpr,Info),
513		add_node_infos(Info,NodeId,NewInfo,In,Inter),
514		create_texpr(Expr,Type,NewInfo,NTExpr),
515		add_existing_constraints(Info,NodeId,Inter,Out).
516		add_node_infos(OldInfo,NodeId,NewInfos,
517		(Constraints,[infonode(NodeId,NewInfos,OldInfo)|Out]),
518		(Constraints,Out)).
519
520		add_all([],In,In).
521		add_all([E|Rest],([E|In],Infonodes),Out) :-
522		add_all(Rest,(In,Infonodes),Out).
523		extract_nodes_l([],_,[],[],[],In,In).
524		extract_nodes_l([TExpr|ERest],NodeEnv,[Node|NRest],[Mode|MRest],[NTExpr|NTRest],In,Out) :-
525		extract_nodes(TExpr,NodeEnv,Node,Mode,NTExpr,In,Inter),
526		extract_nodes_l(ERest,NodeEnv,NRest,MRest,NTRest,Inter,Out).
527		choose_one([],[],[],[]).
528		choose_one([List1|L1Rest],[List2|L2Rest],[Elem1|E1Rest],[Elem2|E2Rest]) :-
529	?	choose_one2(List1,List2,Elem1,Elem2),
530	?	choose_one(L1Rest,L2Rest,E1Rest,E2Rest).
531		choose_one2(NodeList,NodeListRO,Elem,ElemRO) :-
532	?	(Elem == (*) -> true ; nth1(N,NodeList,Elem), nth1(N,NodeListRO,ElemRO)).
533		ignore_readonly_nodes([],[],[]).
534		ignore_readonly_nodes([Mode|MRest],[InNodes|InRest],[OutNodes|OutRest]) :-
535		ignore_readonly_nodes2(Mode,InNodes,OutNodes),
536		ignore_readonly_nodes(MRest,InRest,OutRest).
537		ignore_readonly_nodes2(ro,Nodes,Ignored) :- ignore_readonly_nodes3(Nodes,Ignored).
538		ignore_readonly_nodes2(rw,Nodes,Nodes).
539		ignore_readonly_nodes3([],[]).
540		ignore_readonly_nodes3([Scope:_Node|NRest],[Scope:ignored|IRest]) :-
541		ignore_readonly_nodes3(NRest,IRest).
542
543		nodes_for_general_sum_or_mult(Rule,TId,TPred,TExpr,TOrig,NodeEnv,Nodes,TNew,In,Out) :-
544		identifier_nodes_readonly(NodeEnv,SubEnv1),
545		create_identifier_nodes2([TId],[NTId],SubEnv1,SubEnv,In,Inter1),
546		extract_nodes_l([TId,TPred,TExpr],SubEnv,[IdNodes,_PredNodes,ExprNodes],_Modes,
547		[NTId,NTPred,NTExpr],Inter1,Inter2),
548		get_texpr_info(TOrig,Info),
549		memberchk(interval:ExprNodeId,ExprNodes),
550		memberchk(possible_values:IdId,IdNodes),
551		new_node_scope(integer,NodeId,Nodes),
552		add_node_infos(Info,NodeId,NInfo,Inter2,Inter3),
553		add_all([constraint([possible_values:IdId,interval:ExprNodeId],
554		[interval:NodeId],Rule)],
555		Inter3,Out),
556		get_texpr_expr(TOrig,OrigExpr),functor(OrigExpr,Functor,_),
557		NExpr =.. [Functor,[NTId],NTPred,NTExpr],
558		create_texpr(NExpr,integer,NInfo,TNew).
559
560		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
561		% extract constraints from syntax elements
562		% extract(NExpr,NodeId,InputNodes,OrigOutputNodes,Transition)
563
564		extract(Expr,R,X,Y,Op) :-
565	?	extract_symmetric(Expr,R,X1,Y1,Op1),
566	?	symmetric_constraint(Op1,Op2),
567		( Op=Op1,X=X1,Y=Y1
568		; Op=Op2,X=Y1,Y=X1).
569
570		extract(integer(I),R,[],[interval:R],constant(irange(I,I))).
571		extract(value(IV),R,[],[interval:R],constant(irange(I,I))) :- nonvar(IV), IV = int(I). % TO DO: other vals
572		extract(interval(interval:A,interval:B),R,[interval:A,interval:B],[card:R],interval_card).
573		% the elements of A..B lie between A and B; the reverse direction is only valid if A..B is not empty
574		% (e.g., x..y = {} does not imply x <= y)
575		extract(interval(interval:A,interval:_),R,[interval:A],[elem(interval):R],gte).
576		extract(interval(interval:_,interval:B),R,[interval:B],[elem(interval):R],lte).
577		extract(member(S:A,elem(S):B),_,[elem(S):B],[S:A],id).
578		extract(subset(elem(S):A,elem(S):B),_,[elem(S):B],[elem(S):A],id).
579		extract(subset_strict(elem(S):A,elem(S):B),_,[elem(S):B],[elem(S):A],id).
580	?	extract(add(interval:A,interval:B),R,I,O,C) :- addition_constraint(interval:A,interval:B,interval:R,I,O,C).
581	?	extract(minus(interval:A,interval:B),R,I,O,C) :- addition_constraint(interval:B,interval:R,interval:A,I,O,C).
582		extract(minus(interval:A,interval:B),R,[interval:R,interval:B],[interval:A],add).
583		extract(minus(interval:A,interval:B),R,[interval:A,interval:R],[interval:B],sub).
584		extract(multiplication(interval:A,interval:B),R,[interval:A,interval:B],[interval:R],mult).
585		extract(div(interval:A,interval:B),R,[interval:A,interval:B],[interval:R],divrange).
586		extract(floored_div(interval:A,interval:B),R,[interval:A,interval:B],[interval:R],floored_divrange).
587		extract(modulo(*,interval:B),R,[interval:B],[interval:R],lt).
588		extract(modulo(*,*),R,[],[interval:R],constant(irange(0,inf))).
589		extract(power_of(interval:Base,interval:Exp),R,[interval:Base,interval:Exp],[interval:R],power).
590		extract(integer_set(Set),R,[],[elem(interval):R],constant(irange(Min,Max))) :-
591		compute_integer_set(Set,Min,Max).
592		extract(bool_set,R,[],[card:R],constant(irange(2,2))).
593		extract(pow1_subset(*),R,[],[elem(card):R],constant(irange(1,inf))).
594		extract(fin_subset(A),R,AL,RL,Op) :- extract(pow_subset(A),R,AL,RL,Op).
595		extract(fin1_subset(A),R,AL,RL,Op) :- extract(pow1_subset(A),R,AL,RL,Op).
596	?	extract(partial_function(A,B),R,AL,RL,Op) :- extract(relations(A,B),R,AL,RL,Op).
597	?	extract(total_function(A,B),R,AL,RL,Op) :- extract(relations(A,B),R,AL,RL,Op).
598	?	extract(partial_injection(A,B),R,AL,RL,Op) :- extract(partial_function(A,B),R,AL,RL,Op).
599	?	extract(total_injection(A,B),R,AL,RL,Op) :- extract(total_function(A,B),R,AL,RL,Op).
600	?	extract(partial_surjection(A,B),R,AL,RL,Op) :- extract(partial_function(A,B),R,AL,RL,Op).
601	?	extract(total_surjection(A,B),R,AL,RL,Op) :- extract(total_function(A,B),R,AL,RL,Op).
602	?	extract(total_bijection(A,B),R,AL,RL,Op) :- extract(total_function(A,B),R,AL,RL,Op).
603		extract(partial_bijection(A,B),R,AL,RL,Op) :- extract(partial_function(A,B),R,AL,RL,Op).
604		extract(cartesian_product(card:A,card:B),R,[card:A,card:B],[card:R],mult).
605		extract(cartesian_product(card:A,card:B),R,[card:R,card:A],[card:B],cart_div).
606		extract(cartesian_product(card:A,card:B),R,[card:R,card:B],[card:A],cart_div).
607		extract(set_subtraction(elem(S):A,*),R,[elem(S):A],[elem(S):R],id).
608		extract(image(elem(right(S)):A,*),R,[elem(right(S)):A],[elem(S):R],id).
609	?	extract(intersection(S:A,*),R,I,O,C) :- is_subset_extract(S:R,S:A,I,O,C).
610	?	extract(intersection(*,S:B),R,I,O,C) :- is_subset_extract(S:R,S:B,I,O,C).
611		extract(union(elem(S):A,elem(S):B),R,[elem(S):A,elem(S):B],[elem(S):R],union).
612	?	extract(union(S:A,*),R,I,O,C) :- is_subset_extract(S:A,S:R,I,O,C).
613	?	extract(union(*,S:B),R,I,O,C) :- is_subset_extract(S:B,S:R,I,O,C).
614		extract(domain_restriction(S:A,*),R,I,O,C) :- is_subset_extract(left(S):R,S:A,I,O,C). % ALWAYS FAILS !!!!! SOMETHING IS WRONG HERE; TODO: fix
615	?	extract(domain_restriction(*,S:B),R,I,O,C) :- is_subset_extract(S:R,S:B,I,O,C).
616	?	extract(domain_subtraction(*,S:B),R,I,O,C) :- is_subset_extract(S:R,S:B,I,O,C).
617		extract(range_restriction(*,S:B),R,I,O,C) :- is_subset_extract(right(S):R,S:B,I,O,C). % ALWAYS FAILS !!!!!
618	?	extract(range_restriction(S:A,*),R,I,O,C) :- is_subset_extract(S:R,S:A,I,O,C).
619	?	extract(range_subtraction(S:A,*),R,I,O,C) :- is_subset_extract(S:R,S:A,I,O,C).
620		extract(closure(elem(S):A),R,[elem(S):A],[elem(S):R],id).
621		extract(composition(elem(left(S)):A,*),R,I,O,C) :- is_subset_extract(elem(left(S)):R,elem(left(S)):A,I,O,C).
622		extract(composition(*,elem(right(S)):B),R,I,O,C) :- is_subset_extract(elem(right(S)):R,elem(right(S)):B,I,O,C).
623		extract(function(elem(right(S)):A,*),R,[elem(right(S)):A],[S:R],id).
624		extract(concat(card:A,card:B),R,I,O,C) :- addition_constraint(card:A,card:B,card:R,I,O,C).
625		extract(concat(Right:A,Right:B),R,[Right:A,Right:B],[Right:R],union) :- Right=elem(right(_)).
626		extract(concat(S:A,*),R,I,O,C) :- S=elem(right(_)),is_subset_extract(S:A,S:R,I,O,C).
627		extract(concat(*,S:B),R,I,O,C) :- S=elem(right(_)),is_subset_extract(S:B,S:R,I,O,C).
628		extract(concat(LI:A,LI:B),R,[LI:A,LI:B],[LI:R],concat_index) :- LI=elem(left(interval)). % TODO: More rules like addition
629		extract(seq(*),R,[],[elem(elem(left(interval))):R],constant(irange(1,inf))).
630		extract(seq1(A),R,I,O,C) :- extract(seq(A),R,I,O,C).
631		extract(seq1(*),R,[],[elem(card):R],constant(irange(1,inf))).
632		extract(size(A),R,I,O,C) :- extract(card(A),R,I,O,C).
633
634		addition_constraint(A,B,R,[A,B],[R],add).
635		addition_constraint(A,B,R,[R,B],[A],sub).
636		addition_constraint(A,B,R,[R,A],[B],sub).
637
638	?	is_subset_extract(A,B,I,O,C) :- extract(subset(A,B),_,I,O,C).
639
640		extract_symmetric(equal(S:A,S:B),_,[S:A],[S:B],id).
641		extract_symmetric(subset(card:A,card:B),_,[card:A],[card:B],gte).
642		extract_symmetric(subset_strict(card:A,card:B),_,[card:A],[card:B],gt).
643		extract_symmetric(less(interval:A,interval:B),_,[interval:B],[interval:A],lt).
644		extract_symmetric(less_equal(interval:A,interval:B),_,[interval:B],[interval:A],lte).
645		extract_symmetric(greater(interval:A,interval:B),_,[interval:B],[interval:A],gt).
646		extract_symmetric(greater_equal(interval:A,interval:B),_,[interval:B],[interval:A],gte).
647		extract_symmetric(unary_minus(interval:X),R,[interval:X],[interval:R],negate).
648		extract_symmetric(card(card:X),R,[card:X],[interval:R],id).
649		extract_symmetric(cartesian_product(elem(S):A,*),R,[elem(S):A],[elem(left(S)):R],id).
650		extract_symmetric(cartesian_product(*,elem(S):B),R,[elem(S):B],[elem(right(S)):R],id).
651		extract_symmetric(couple(S:A,*),R,[S:A],[left(S):R],id).
652		extract_symmetric(couple(*,S:B),R,[S:B],[right(S):R],id).
653		extract_symmetric(pow_subset(elem(S):A),R,[elem(S):A],[elem(elem(S)):R],id).
654		extract_symmetric(pow_subset(card:A),R,[card:A],[elem(card):R],lte).
655		extract_symmetric(pow1_subset(S),R,[A],[B],C) :- extract_symmetric(pow_subset(S),R,[A],[B],C).
656		extract_symmetric(seq(A),R,[elem(S):A],[elem(elem(right(S))):R],id).
657		extract_symmetric(relations(elem(S):A,*),R,[elem(S):A],[elem(elem(left(S))):R],id).
658		extract_symmetric(relations(*,elem(S):B),R,[elem(S):B],[elem(elem(right(S))):R],id).
659		extract_symmetric(partial_function(card:A,card:_),R,[card:A],[elem(card):R],lte).
660		extract_symmetric(total_function(card:A,card:_),R,[card:A],[elem(card):R],id).
661		extract_symmetric(partial_injection(card:_,card:B),R,[card:B],[elem(card):R],lte).
662		extract_symmetric(total_injection(card:_,card:B),R,[card:B],[elem(card):R],lte).
663		extract_symmetric(total_surjection(card:_,card:B),R,[card:B],[elem(card):R],gte).
664		extract_symmetric(total_bijection(card:A,card:_),R,[card:A],[elem(card):R],id).
665		extract_symmetric(total_bijection(card:_,card:B),R,[card:B],[elem(card):R],id).
666		extract_symmetric(domain(elem(left(S)):A),R,[elem(left(S)):A],[elem(S):R],id).
667		extract_symmetric(range(elem(right(S)):A),R,[elem(right(S)):A],[elem(S):R],id).
668		extract_symmetric(reverse(elem(left(S)):A),R,[elem(left(S)):A],[elem(right(S)):R],id).
669		extract_symmetric(reverse(elem(right(S)):A),R,[elem(right(S)):A],[elem(left(S)):R],id).
670		extract_symmetric(reverse(card:A),R,[card:A],[card:R],id).
671		extract_symmetric(set_subtraction(card:A,*),R,[card:A],[card:R],lte). % was erroneously gte, see test 2410
672		extract_symmetric(closure(elem(left(S)):A),R,[elem(left(S)):A],[elem(left(S)):R],id).
673		extract_symmetric(closure(elem(right(S)):A),R,[elem(right(S)):A],[elem(right(S)):R],id).
674		extract_symmetric(closure(card:A),R,[card:A],[card:R],gte).
675		extract_symmetric(image(card:A,*),R,[card:R],[card:A],gte).
676		extract_symmetric(first_of_pair(left(S):A),R,[left(S):A],[S:R],id).
677		extract_symmetric(second_of_pair(right(S):A),R,[right(S):A],[S:R],id).
678
679		symmetric_constraint(A,B) :- symmetric_constraint2(A,B),!.
680	?	symmetric_constraint(A,B) :- symmetric_constraint2(B,A).
681		symmetric_constraint2(id,id).
682		symmetric_constraint2(lt,gt).
683		symmetric_constraint2(lte,gte).
684		symmetric_constraint2(negate,negate).
685
686
687		% this seems to take up most of the time:
688		create_constraint_tree(Constraints,Nodes,Tree) :-
689		empty_avl(EmptyTree),
690		sort(Constraints,SConstraints), % for SAT_Generator sorting reduces runtime from 22 sec to 18 sec for n=8; TO DO: investigate
691		(debug:debug_mode(on) -> length(Constraints,Len), format('Processing ~w constraints~n',[Len]) ; true),
692		create_constraint_tree1(SConstraints,[],UnsortedNodes,EmptyTree,Tree),
693		(debug:debug_mode(on) -> length(UnsortedNodes,Len2), format('Sorting ~w nodes~n',[Len2]) ; true),
694		sort(UnsortedNodes,Nodes),
695		(debug:debug_mode(on) -> length(Nodes,Len3), format('Done sorting ~w nodes~n',[Len3]) ; true).
696		%,set_prolog_flag(profiling,off),print_profile.
697
698		create_constraint_tree1([],Nodes,Nodes,Tree,Tree).
699		create_constraint_tree1([C|CRest],InNodes,OutNodes,InTree,OutTree) :-
700		create_constraint_tree2(C,InNodes,InterNodes,InTree,InterTree),
701		create_constraint_tree1(CRest,InterNodes,OutNodes,InterTree,OutTree).
702
703		create_constraint_tree2(Constraint,InNodes,OutNodes,InTree,OutTree) :-
704		Constraint = constraint(Input,Output,_Rule),
705		( all_nodes_ignored(Output) ->
706		InTree = OutTree, InNodes=OutNodes
707		;
708		add_all_to_constraint_tree(Input,Constraint,InTree,OutTree),
709		%ord_union(Input,InNodes,Nodes),ord_union(Output,Nodes,OutNodes) % this can be very expensive !
710		append(Input,InNodes,Nodes), append(Output,Nodes,OutNodes) % just append the nodes and sort them later
711		).
712
713		add_all_to_constraint_tree([],_,Tree,Tree).
714		add_all_to_constraint_tree([Node|NRest],Constraint,InTree,OutTree) :-
715		( avl_change(Node,InTree,Old,InterTree,[Constraint|Old]) ->
716		true
717		;
718		avl_store(Node,InTree,[Constraint],InterTree)),
719		add_all_to_constraint_tree(NRest,Constraint,InterTree,OutTree).
720
721		all_nodes_ignored([]).
722		all_nodes_ignored([_:ignored|Rest]) :-
723		all_nodes_ignored(Rest).
724
725
726		create_initial_information(Nodes,InitEnv) :-
727		empty_avl(Empty),
728		foldl(create_initial_information2,Nodes,Empty,InitEnv).
729		create_initial_information2(Scope:Node,In,Out) :-
730		get_scope_top(Scope,Top),
731		avl_store(Scope:Node,In,Top,Out).
732
733		apply_start_constraints(Constraints,ChangedNodes,In,Out) :-
734		find_start_constraints(Constraints,Start),
735		writetodot(1,[],Start,In),
736		compute_constraints(Start,ChangedNodes1,[],In,Out),
737		list_to_ord_set(ChangedNodes1,ChangedNodes).
738		find_start_constraints(Constraints,Start) :-
739		findall(constraint([],Output,Rule),
740		member(constraint([],Output,Rule),Constraints),
741		Start).
742
743		do_analysis([],Counter,_MaxIter,_CTree,Values,Values) :-
744		!,writetodot(Counter,[],[],Values).
745		do_analysis([ChangedNode|CNRest],Counter,MaxIter,CTree,In,Out) :-
746		Counter < MaxIter,!,
747		(avl_fetch(ChangedNode,CTree,Constraints) -> true ; Constraints = []),
748		writetodot(Counter,[ChangedNode|CNRest],Constraints,In),
749	?	compute_constraints(Constraints,ChangedNodes1,[],In,Inter),
750		list_to_ord_set(ChangedNodes1,ChangedNodes),
751		ord_union(CNRest,ChangedNodes,NewChangedNodes),
752		Counter2 is Counter+1,
753	?	do_analysis(NewChangedNodes,Counter2,MaxIter,CTree,Inter,Out).
754		do_analysis(_ChangedNodes,Counter,MaxIter,_CTree,Values,Values) :-
755		Counter >= MaxIter.
756		compute_constraints([],Changed,Changed,Values,Values).
757		compute_constraints([Constraint|CRest],Cin,Cout,Vin,Vout) :-
758	?	compute_constraint(Constraint,Cin,Cinter,Vin,Vinter),
759	?	compute_constraints(CRest,Cinter,Cout,Vinter,Vout).
760		compute_constraint(constraint(Input,Output,Rule),Cin,Cout,Vin,Vout) :-
761		get_input_values(Input,Vin,InValues),
762		same_length(Output,OutValues),
763	?	call_rule(Rule,InValues,OutValues),
764		apply_output(Output,OutValues,Cin,Cout,Vin,Vout).
765		get_input_values([],_,[]).
766		get_input_values([Node|NRest],Values,[Value|VRest]) :-
767		avl_fetch(Node,Values,Value),
768		get_input_values(NRest,Values,VRest).
769		call_rule(Rule,InValues,OutValues) :-
770		append_arguments(Rule,InValues,CallRule),
771	?	if(rule(CallRule,OutValues), true,
772		(add_warning(predicate_analysis,'No rule for: ',CallRule),fail)).
773		apply_output([],[],Changed,Changed,Values,Values).
774		apply_output([Node|NRest],[Value|VRest],Cin,Cout,Vin,Vout) :-
775		( Node = _:ignored ->
776		Vin = Vinter, Cin=Cinter
777		;
778		avl_change(Node,Vin,OldValue,Vinter,NewValue),
779		info_conjunct(OldValue,Value,NewValue),
780		( has_more_information(NewValue,OldValue) ->
781		Cin = [Node|Cinter]
782		;
783		Cin = Cinter)),
784		apply_output(NRest,VRest,Cinter,Cout,Vinter,Vout).
785
786		append_arguments(Orig,Args,Result) :-
787		Orig =.. FA,
788		append_arguments2(FA,Args,AllArgs),
789		Result =.. AllArgs.
790		append_arguments2([F|FA],Args,AllArgs) :-
791		multi_rule(F),!,
792		append([F|FA],[Args],AllArgs).
793		append_arguments2(FA,Args,AllArgs) :-
794		append(FA,Args,AllArgs).
795
796
797		create_add_list_constraints([],_Result,Constraints) :- !,Constraints=[].
798		create_add_list_constraints([Node],Result,Constraints) :- !,
799		Constraints = [constraint([Node],[Result],id),constraint([Result],[Node],id)].
800		create_add_list_constraints(Nodes,Result,Constraints) :- !,
801		create_add_list_constraints2(Nodes,Result,Constraints,[]).
802		create_add_list_constraints2([A,B],Result) --> !,
803		findall(constraint(I,O,C),addition_constraint(A,B,Result,I,O,C)).
804		create_add_list_constraints2([A|Nodes],Result) -->
805		{new_node_scope(integer,NodeId,_Nodes)},
806		findall(constraint(I,O,C),addition_constraint(A,interval:NodeId,Result,I,O,C)),
807		create_add_list_constraints2(Nodes,interval:NodeId).
808
809
810
811		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
812		% compute a single constraint
813
814		rule(id(Info),[Info]).
815		rule(constant(Info),[Info]).
816		rule(add(A,B),[C]) :- interval_addition(A,B,C).
817		rule(sub(A,B),[C]) :- interval_subtraction(A,B,C).
818		rule(mult(A,B),[C]) :- interval_multiplication(A,B,C).
819		rule(power(Base,Exp),[Result]) :-
820		(power_rule(Base,Exp,Result) -> true ; Result = irange(-inf,inf)).
821		rule(power_rule(PossibleValues,ExprRange),[Result]) :- % used for PI, see nodes_for_general_sum_or_mult
822		(general_product_rule(PossibleValues,ExprRange,Result) -> true ; Result = irange(-inf,inf)).
823		rule(cart_div(irange(Cm,CM2),irange(Am,AM2)),[irange(Bm,BM2)]) :- % propagates C = A * B
824		( CM2 = inf -> % C can be infinite
825		BM2 = inf
826		; Am = 0, % the set A can be empty
827		number(Cm),Cm<1 -> % set C can be empty
828		BM2 = inf % B can be arbitrarily larger and still yield an empty A*B
829		; Am = 0 -> % case: set C cannot be empty, actually Am is 1
830		BM2 = CM2 % B can be as large as the maximum size of C
831		; Am = inf -> % A is infinite
832		BM2 = 0 % as CM2 is not inf, C cannot be infinite, only solution is B to be empty
833		;
834		BM2 infis (CM2+Am-1) // Am % e.g., for CM2=3 and Am=2 we obtain 2 ?? Shouldnt we use CM2 // Am ??
835		),
836		( number(Cm),Cm<1 -> % set C can be empty
837		Bm = 0 % B can also be empty
838		; AM2 = 0 -> % A has to be empty; this means C is empty and we have a contradiction
839		Bm is -1 % try force contradiction
840		; AM2 = inf -> % A can be infinite, but C is definitely not empty
841		Bm = 1 % B must have at least one element
842		; Cm = inf -> Bm = inf % C has to be infinite, but A is finite
843		; AM2 > Cm -> Bm = 1 % B must have at least one element, as C is not empty
844		;
845		Bm infis Cm // AM2). % minimal size of B is C divided by maximal size of A
846		% TO DO: can be improved, e.g., for :kodkod A = {1,2} & avl = {1|->2, 1|->3, 2|->2, 2|->3, 4|->2} & avl = A*B
847		% print(rule_result(cart_div(irange(Cm,CM2),irange(Am,AM2)),[irange(Bm,BM2)])),nl.
848		rule(negate(A),[C]) :- interval_negation(A,C).
849		rule(lt(irange(_,AM2)),[irange(-inf,CM2)]) :- CM2 infis AM2-1.
850		rule(lte(irange(_,AM2)),[irange(-inf,AM2)]).
851		rule(gt(irange(Am,_)),[irange(Cm,inf)]) :- Cm infis Am+1.
852		rule(gte(irange(Am,_)),[irange(Am,inf)]).
853		rule(interval_card(irange(Am,AM2),irange(Bm,BM2)),[irange(Cm,CM2)]) :-
854		Cm infis max(Bm-AM2+1,0), CM2 infis max(BM2-Am+1,0).
855		rule(interval_possibilities(irange(Am,AM2)),[irange(0,M)]) :-
856		M infis max(AM2-Am+1,0).
857		rule(union([A|Rest]),[C]) :- union2(Rest,A,C).
858		rule(union([]),[irange(-inf,inf)]) :- debug_println(19,empty_kodkod_union_constraint). % TO DO: check if ok !!
859		% happens e.g., for set extensions like { min(0..7) } ; should not occur
860		rule(divrange(irange(Am,AM2),irange(Bm,BM2)),[irange(MinC,MaxC)]) :-
861		div_rule(truncated,Am,AM2,Bm,BM2,MinC,MaxC).
862		rule(floored_divrange(irange(Am,AM2),irange(Bm,BM2)),[irange(MinC,MaxC)]) :-
863		div_rule(floored,Am,AM2,Bm,BM2,MinC,MaxC).
864		rule(concat_index(irange(_,AM2),irange(_,BM2)),[irange(1,CM2)]) :-
865		(number(AM2),number(BM2) -> CM2 is AM2+BM2 ; CM2 = inf).
866
867
868		:- assert_must_succeed((div_rule(truncated,1,100,1,2,MinC,MaxC), MinC == 0, MaxC == 100)).
869		:- assert_must_succeed((div_rule(truncated,100,200,1,50,MinC,MaxC), MinC == 2, MaxC == 200)).
870		:- assert_must_succeed((div_rule(truncated,-2,100,1,50,MinC,MaxC), MinC == -2, MaxC == 100)).
871		:- assert_must_succeed((div_rule(truncated,-2,100,0,50,MinC,MaxC), MinC == -2, MaxC == 100)). % with try_find_abort we would get:
872		% :- assert_must_succeed((div_rule(truncated,-2,100,0,50,MinC,MaxC), MinC == -inf, MaxC == inf)). % above with try_find_abort
873		:- assert_must_succeed((div_rule(truncated,-7,-1,2,4,MinC,MaxC), MinC == -3, MaxC == 0)).
874		:- assert_must_succeed((div_rule(floored,-7,-1,2,4,MinC,MaxC), MinC == -4, MaxC == -1)).
875		:- assert_must_succeed((div_rule(truncated,-7,-1,2,inf,MinC,MaxC), MinC == -3, MaxC == 0)).
876		:- assert_must_succeed((div_rule(floored,-7,-1,2,inf,MinC,MaxC), MinC == -4, MaxC == -1)).
877
878		% propagate division Am..AM2 / Bm..BM2 --> C
879		% Kind is truncated (B's div) or floored (floored_div)
880		div_rule(Kind,Am,AM2,Bm,BM2,MinC,MaxC) :- number(Bm), Bm >= 0,!, % division by positive number
881		(Am = -inf -> MinC = -inf
882		; Am < 0, Bm=0 -> MinC = Am % if try_find_abort is true we could set MinC to -inf; here we suppose division by 0 will not occur or not produce a value
883		; Am < 0 -> int_div(Kind,Am,Bm,MinC) % a possible lowest value is obtained by the largest absolute (neg) value
884		; BM2=inf -> MinC is 0 % Am is positive ; we can divide Am by an arbitrarily large number to reach 0
885		; int_div(Kind,Am,BM2,MinC) % minimum is dividing min of A by maximum of B
886		),
887		(AM2 = inf -> MaxC = inf
888		; BM2=inf, AM2<0 -> (Kind=floored -> MaxC = -1 ; MaxC = 0) % we can divide AM2 by an arbitrarily large number
889		; AM2 < 0 -> int_div(Kind,AM2,BM2,MaxC) % a possible max value is obtained by the smallest absolute (neg) value
890		; Bm=0 -> MaxC = AM2 % if try_find_abort is true we could set MaxC to inf
891		; int_div(Kind,AM2,Bm,MaxC) % maximum is dividing max of A by min of B
892		).
893		div_rule(_,Am,AM2,_Bm,_BM2,MinC,MaxC) :- number(Am),number(AM2), !, % TODO: improve and check
894		M is max(abs(Am),abs(AM2)), % if try_find_abort is true we could divide by 0 and set to -inf .. inf
895		MinC is -M, MaxC = M.
896		div_rule(_,_,_,_,_,-inf,inf).
897
898		int_div(truncated,A,B,C) :- C is A // B.
899		int_div(floored,A,B,C) :- C is A div B.
900
901		union2([],Acc,R) :- !,Acc=R.
902		union2([H|T],Acc,R) :- info_disjunct(H,Acc,I),union2(T,I,R).
903
904		power_rule(irange(Basem,BaseM2),irange(Expm,ExpM2),irange(Rm,RM2)) :-
905		number(Basem),Basem > 0,
906		number(Expm),Expm >= 0,
907		Rm is floor( Basem ** Expm),
908		((BaseM2=inf; ExpM2=inf) -> RM2=inf ; RM2 is floor(BaseM2 ** ExpM2)).
909
910		% the product of at most N values in Em..EM
911		general_product_rule(irange(_,N),irange(Em,EM),irange(Rm,RM)) :-
912		number(N), number(Em), number(EM),
913		M is max(max(abs(Em),abs(EM)),1),
914		RM is M^N,
915		( Em >= 1 -> Rm = 1
916		; Em >= 0 -> Rm = 0
917		; Rm is -RM).
918
919		multi_rule(union).
920
921
922		insert_info(Infonodes,Values) :-
923		create_info_lookup_table(Values,ValueTable),
924		insert_info2(Infonodes,ValueTable).
925		insert_info2([],_).
926		insert_info2([infonode(Node,New,Old)|Rest],Values) :-
927		find_all_node_information(Node,Values,Info),
928		add_info(Info,Old,New),
929		insert_info2(Rest,Values).
930
931		:- load_files(library(system), [when(compile_time), imports([environ/2])]).
932		:- if(environ(prob_safe_mode,true)).
933		find_all_node_information(Node,_,_) :- \+ ground(Node), add_internal_error('Non-ground node: ',Node),fail.
934		:- endif.
935		find_all_node_information(Node,Values,Info) :-
936		( avl_fetch(Node,Values,RawInfos) -> filter_tops(RawInfos,Info) % used to call avl_member; but Node is ground
937		; Info = []).
938
939		filter_tops([],[]).
940		filter_tops([Scope:RI|RRest],Result) :-
941		get_scope_top(Scope,Top),
942		( has_more_information(RI,Top) -> Result = [Scope:RI|RestResult]
943		; Result = RestResult),
944		filter_tops(RRest,RestResult).
945
946		add_info([],Old,Old) :- !.
947		add_info(Info,Old,[analysis(Info)|Old]).
948
949		create_info_lookup_table(Values,Nodes) :-
950		avl_to_list(Values,ValueList),
951		empty_avl(Empty),
952		create_info_lookup_table2(ValueList,Empty,Nodes).
953		create_info_lookup_table2([],Nodes,Nodes).
954		create_info_lookup_table2([(Scope:Node)-I|Rest],In,Out) :-
955		(avl_fetch(Node,In,Old) -> true ; Old = []),
956		avl_store(Node,In,[Scope:I|Old],Inter),
957		create_info_lookup_table2(Rest,Inter,Out).
958
959		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
960		% dot output
961
962		writetodot(Counter,ChangedNodes,ActiveConstraints,Values) :-
963		debugging_enabled,!,
964		debug_constraints(Constraints),
965		writetodot(Counter,Constraints,ChangedNodes,ActiveConstraints,Values).
966		writetodot(_Counter,_ChangedNodes,_ActiveConstraints,_Values).
967
968		writetodot(Counter,Constraints,ChangedNodes,ActiveConstraints,Values) :-
969		printnulls(3,Counter,CStr),
970		ajoin(['debug-constraint-anim/constraints-',CStr,'.dot'],Filename),
971		debug_format(19,'Writing Kodkod constraints to dot file: ~w~n',[Filename]),
972		open(Filename,write,S),
973		write(S,'digraph constraints {\n'),
974		get_nodes(Constraints,INodes,CNodes),
975		write_inodes(INodes,ChangedNodes,Values,S),
976		write_cnodes(CNodes,INodes,ActiveConstraints,S),
977		write(S,'}\n'),
978		close(S).
979		get_nodes(Constraints,INodes,RNodes) :-
980		findall(CN,
981		(member(constraint(I,O,_),Constraints),
982		(member(CN,I);member(CN,O))),
983		Nodes1),
984		sort(Nodes1,Nodes2),
985		number_nodes(Nodes2,1,INodes),
986		number_nodes(Constraints,1,RNodes).
987		number_nodes([],_,[]).
988		number_nodes([N|Rest],Nr,[node(Nr,N)|RRest]) :-
989		Nr2 is Nr+1,
990		number_nodes(Rest,Nr2,RRest).
991		write_inodes([],_,_,_).
992		write_inodes([node(Nr,N)|Rest],ChangedNodes,Values,S) :-
993		write(S,' i'),write(S,Nr),write(S,'[shape=box,'),
994		( ChangedNodes = [N|_] ->
995		!,write(S,'fillcolor=green,style=filled,')
996		; member(N,ChangedNodes) ->
997		!,write(S,'fillcolor=yellow,style=filled,')
998		; true),
999		write(S,'label=\"'),
1000		write(S,N),write(S,'\\n'),
1001		( debug_node(N,TExpr) ->
1002		translate_bexpression(TExpr,Text)
1003		;
1004		Text = ('?')),
1005		write(S,Text),write(S,'\\n'),
1006		( avl_fetch(N,Values,Value) ->
1007		write(S,Value)
1008		; write(S,'?')),
1009		write(S,'\"];\n'),
1010		write_inodes(Rest,ChangedNodes,Values,S).
1011		write_cnodes([],_,_,_).
1012		write_cnodes([node(Nr,constraint(In,Out,R))|Rest],INodes,ActiveConstraints,S) :-
1013		write(S,' c'),write(S,Nr),write(S,'[shape=diamond,'),
1014		( member(constraint(In,Out,R),ActiveConstraints) ->
1015		!,write(S,'fillcolor=lightblue,style=filled,')
1016		; true),
1017		write(S,'label=\"'),
1018		write(S,R),write(S,'\"];\n'),
1019		write_inputs(In,INodes,Nr,S),
1020		write_outputs(Out,INodes,Nr,S),
1021		write_cnodes(Rest,INodes,ActiveConstraints,S).
1022		write_inputs([],_,_,_).
1023		write_inputs([I|Rest],INodes,RNr,S) :-
1024		member(node(INr,I),INodes),!,
1025		write(S,' i'),write(S,INr),write(S,' -> '),
1026		write(S,' c'),write(S,RNr),write(S,';\n'),
1027		write_inputs(Rest,INodes,RNr,S).
1028		write_outputs([],_,_,_).
1029		write_outputs([O|Rest],INodes,RNr,S) :-
1030		member(node(ONr,O),INodes),!,
1031		write(S,' c'),write(S,RNr),write(S,' -> '),
1032		write(S,' i'),write(S,ONr),write(S,';\n'),
1033		write_outputs(Rest,INodes,RNr,S).
1034
1035		printnulls(N,Number,Str) :-
1036		number_codes(Number,NCodes),
1037		length(NCodes,L),
1038		R is N-L,
1039		fillnulls(R,NCodes,Codes),
1040		atom_codes(Str,Codes).
1041		fillnulls(R,Codes,Codes) :- R =< 0,!.
1042		fillnulls(R,NCodes,[48|Codes]) :-
1043		R2 is R-1,
1044		fillnulls(R2,NCodes,Codes).
1045
1046
1047		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1048
1049		:- dynamic debug_predicate_analysis/0.
1050		% assert this fact to enable dot visualization using writetodot below
1051
1052		store_debug_info(I,T) :- debug_predicate_analysis,!,store_debug_info2(I,T).
1053		store_debug_info(_,_).
1054
1055		store_debug_info2([],_).
1056		store_debug_info2([Node|Rest],TExpr) :-
1057		assertz(debug_node(Node,TExpr)),
1058		store_debug_info2(Rest,TExpr).
1059
1060
1061		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1062		% test case specification for predicate analysis
1063
1064		:- use_module(probsrc(junit_tests)).
1065
1066		test_predicate_analysis :-
1067		b_machine_has_constants,
1068		b_get_machine_constants(Constants),
1069		b_get_properties_from_machine(Properties),
1070		b_get_static_assertions_from_machine(Assertions),
1071		Assertions = [_|_],!,
1072		test_predicate_analysis2(Constants,Properties,Assertions,Junits),
1073		b_machine_name(MachineName),
1074		full_junit_test_suite_name([predicate_analysis,MachineName], SuiteName),
1075		print_junit(SuiteName, Junits).
1076		test_predicate_analysis :-
1077		add_error(predicate_analysis,
1078		'Machine must have constants and assertions to be a valid predicate analysis test case.'),
1079		fail.
1080		test_predicate_analysis2(Constants,Properties,Assertions,Junits) :-
1081		predicate_analysis_with_global_sets(Properties,[],Constants,TaggedConstants,_TaggedProperties),!,
1082		test_predicate_analysis3(Assertions,TaggedConstants,Junits).
1083		test_predicate_analysis2(_,_,_,[Junit]) :-
1084		in_junit_mode,!,
1085		pa_junit(setup,error('Predicate analysis failed'),Junit).
1086		test_predicate_analysis2(_,_,_,_) :-
1087		add_error(predicate_analysis, 'Predicate analysis of properties failed'),
1088		fail.
1089		test_predicate_analysis3([],_Constants,[]).
1090		test_predicate_analysis3([Assertion|Arest],Constants,[Junit|Jrest]) :-
1091		test_predicate_analysis_testcase(Assertion,Constants,Junit),
1092		test_predicate_analysis3(Arest,Constants,Jrest).
1093
1094		test_predicate_analysis_testcase(TAssertion,Constants,Junit) :-
1095		translate_bexpression(TAssertion,Name),
1096		( catch( ( test_predicate_analysis_testcase1(TAssertion,Constants),
1097		pa_junit(Name,pass,Junit)),
1098		junit(Msg),
1099		handle_error(Name,Msg,Junit)) -> true
1100		;
1101		pa_junit(Name,error('Test failed.'),Junit)).
1102		handle_error(Name,Msg,Junit) :-
1103		in_junit_mode,!,
1104		pa_junit(Name,error(Msg),Junit).
1105		handle_error(Name,Msg,_Junit) :-
1106		add_error(predicate_analysis, Name, Msg), fail.
1107
1108		test_predicate_analysis_testcase1(TAssertion,Constants) :-
1109		extract_predicate_analysis_testcases(TAssertion,[],Testcases),
1110		maplist(run_testcase(Constants),Testcases).
1111		run_testcase(Constants,pa_testcase(Id,Scope,ExpectedValue)) :-
1112		formatsilent('Predicate analysis testcase: check if "~w" of "~w" is ~w~N', [Scope,Id,ExpectedValue]),
1113		expected_value_is_top(ExpectedValue,Scope,IsTop),
1114		extract_analysis(Id,Constants,Scope,FoundValue,IsTop),
1115		( FoundValue == ExpectedValue -> true
1116		;
1117		ajoin(['unexpected information for constant ',Id,': expected ', ExpectedValue,
1118		', but was ', FoundValue],Msg),
1119		throw(junit(Msg))).
1120		expected_value_is_top(ExpectedValue,Scope,true) :-
1121		ground(ExpectedValue),get_scope_top(Scope,ExpectedValue),!.
1122		expected_value_is_top(_ExpectedValue,_Scope,false).
1123
1124		extract_predicate_analysis_testcases(TExpr,QRefs,Testcases) :-
1125		get_texpr_expr(TExpr,Expr),
1126		extract_predicate_analysis_testcases2(Expr,QRefs,Testcases).
1127		extract_predicate_analysis_testcases2(forall(Ids,TPre,Cond),QRefs,Testcases) :-
1128		get_texpr_expr(TPre,Pre),introduce_qrefs(Pre,Ids,QRefs,SubQRefs),
1129		extract_predicate_analysis_testcases(Cond,SubQRefs,Testcases).
1130		extract_predicate_analysis_testcases2(equal(Ref,Spec),QRefs,[pa_testcase(Constant,Scope,irange(Value,Value))]) :- !,
1131		extract_test_reference(Ref,QRefs,Constant,Scope),
1132		extract_integer(Spec,Value).
1133		extract_predicate_analysis_testcases2(less_equal(Ref,Spec),QRefs,[pa_testcase(Constant,Scope,irange(-inf,Value))]) :- !,
1134		extract_test_reference(Ref,QRefs,Constant,Scope),
1135		extract_integer(Spec,Value).
1136		extract_predicate_analysis_testcases2(greater_equal(Ref,Spec),QRefs,[pa_testcase(Constant,Scope,irange(Value,inf))]) :- !,
1137		extract_test_reference(Ref,QRefs,Constant,Scope),
1138		extract_integer(Spec,Value).
1139		extract_predicate_analysis_testcases2(member(Ref,TSpec),QRefs,[pa_testcase(Constant,Scope,Info)]) :-
1140		get_texpr_expr(TSpec,Spec),
1141		extract_test_reference(Ref,QRefs,Constant,Scope),
1142		integer_interval_membership(Spec,Scope,Info),!.
1143		extract_predicate_analysis_testcases2(not_member(Ref,TSpec),QRefs,[pa_testcase(Constant,Scope,Top)]) :-
1144		get_texpr_expr(TSpec,empty_set),
1145		extract_test_reference(Ref,QRefs,Constant,Scope),
1146		get_scope_top(Scope,Top).
1147		extract_predicate_analysis_testcases2(conjunct(A,B),QRefs,Testcases) :- !,
1148		extract_predicate_analysis_testcases(A,QRefs,TestcasesA),
1149		extract_predicate_analysis_testcases(B,QRefs,TestcasesB),
1150		append(TestcasesA,TestcasesB,Testcases).
1151		extract_predicate_analysis_testcases2(_Expr,_QRefs,_Testcases) :-
1152		throw(junit('Unsupported test case pattern')).
1153
1154		integer_interval_membership(empty_set,Scope,Bottom) :- get_scope_bottom(Scope,Bottom).
1155		integer_interval_membership(interval(Min,Max),_Scope,irange(VMin,VMax)) :-
1156		extract_integer(Min,VMin),extract_integer(Max,VMax).
1157		integer_interval_membership(integer_set(I),_Scope,irange(Min,Max)) :-
1158		compute_integer_set(I,Min,Max).
1159
1160		introduce_qrefs(member(E2,Ref),Ids,QRefs,NewQRefs) :-
1161		lookup_ref(Ref,QRefs,Path,Constant),append(Path,[elem],Path2),
1162		couple_pathes(E2,Path2,Constant,Ids,NewQRefs,QRefs).
1163		introduce_qrefs(equal(E2,Ref),Ids,QRefs,NewQRefs) :-
1164		lookup_ref(Ref,QRefs,Path,Constant),
1165		couple_pathes(E2,Path,Constant,Ids,NewQRefs,QRefs).
1166
1167		couple_pathes(TExpr,Path,Constant,TIdentifiers) -->
1168		{get_texpr_ids(TIdentifiers,Identifiers)},
1169		couple_pathes2(TExpr,Path,Constant,Identifiers).
1170		couple_pathes2(TExpr,Path,Constant,Identifiers) -->
1171		{get_texpr_expr(TExpr,Expr)},couple_pathes3(Expr,TExpr,Path,Constant,Identifiers).
1172		couple_pathes3(identifier(Id),_,Path,Constant,Identifiers) -->
1173		{memberchk(Id,Identifiers),!},[Id-ref(Path,Constant)].
1174		couple_pathes3(couple(A,B),_,Path,Constant,Identifiers) --> !,
1175		{append(Path,[left],PathA),append(Path,[right],PathB)},
1176		couple_pathes2(A,PathA,Constant,Identifiers),
1177		couple_pathes2(B,PathB,Constant,Identifiers).
1178		couple_pathes3(_,TExpr,_Path,_Constant,_Identifiers,_,_) :-
1179		translate_bexpression(TExpr,String),
1180		atom_concat('Expected quantified identifier or couple in test specification, but was: ',
1181		String,Msg),
1182		throw(junit(Msg)).
1183
1184
1185		lookup_ref(Expr,QRefs,Path,Constant) :-
1186		get_texpr_id(Expr,Id),
1187		memberchk(Id-ref(Path1,Constant1),QRefs),!,
1188		Path1=Path,Constant1=Constant.
1189		lookup_ref(Expr,_QRefs,[],Id) :-
1190		get_texpr_id(Expr,Id).
1191
1192		extract_analysis(Id,Constants,Scope,FoundValue,IsTop) :-
1193		get_texpr_id(Constant,Id),
1194		( memberchk(Constant,Constants) ->
1195		get_texpr_info(Constant,Info),
1196		(memberchk(analysis(Analysis),Info) -> true ; Analysis=[]),
1197		( memberchk(Scope:FoundValue,Analysis) -> true
1198		; IsTop == true -> get_scope_top(Scope,FoundValue) /* no information expected */
1199		;
1200		ajoin(['No analysis information found for constant ',Id,', scope ',Scope],Msg),
1201		print(extract_analysis(Id,Constants,Scope,FoundValue,IsTop)),nl,
1202		throw(junit(Msg)))
1203		;
1204		ajoin(['Constant ',Id,' not found'],Msg),
1205		throw(junit(Msg))).
1206
1207		extract_test_reference(TRef,QRefs,Id,Scope) :-
1208		get_texpr_expr(TRef,Ref),
1209		extract_test_reference2(Ref,QRefs,BaseScope,Id,ScopeList),
1210		construct_scope(ScopeList,BaseScope,Scope),!.
1211		extract_test_reference(TRef,_QRefs,_Id,_Scope) :-
1212		translate_bexpression(TRef,String),
1213		atom_concat('Unsupported reference on left side: ', String,Msg),
1214		throw(junit(Msg)).
1215		extract_test_reference2(card(TRef),QRefs,card,Id,Scope) :-
1216		!,get_texpr_expr(TRef,Ref),Ref=identifier(_),
1217		extract_test_reference2(Ref,QRefs,_,Id,Scope).
1218		extract_test_reference2(identifier(Id),QRefs,interval,Constant,Scope) :-
1219		memberchk(Id-ref(Scope,Constant),QRefs),!.
1220		extract_test_reference2(identifier(Id),_QRefs,interval,Id,[]) :- !.
1221
1222
1223		:- assert_must_succeed(( construct_scope([elem,right],interval,S),
1224		S==elem(right(interval)) )).
1225		construct_scope([],Scope,Scope).
1226		construct_scope([F|Rest],Base,Scope) :-
1227		functor(Scope,F,1),arg(1,Scope,Subscope),
1228		construct_scope(Rest,Base,Subscope).
1229
1230		extract_integer(Spec,Value) :-
1231		( get_texpr_expr(Spec,integer(Value)) -> true
1232		; get_texpr_expr(Spec,unary_minus(Spec2)) ->
1233		extract_integer(Spec2,Value2),Value is -Value2
1234		;
1235		throw(junit('Integer value expected in right side of assertion'))).
1236
1237		in_junit_mode :-
1238		junit_mode(_),!.
1239
1240		pa_junit(Name,Verdict,Junit) :-
1241		create_junit_result(Name,0,Verdict,Junit).