1		% (c) 2009-2024 Lehrstuhl fuer Softwaretechnik und Programmiersprachen,
2		% Heinrich Heine Universitaet Duesseldorf
3		% This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html)
4
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,[Union|Constraints]) :-
493		findall(Scope:E,
494		( member(NodeList,ElemNodes), memberchk(Scope:E,NodeList)),
495		AllElemNodes),
496		Union = constraint(AllElemNodes,[SeqNode],union),
497		% for set extensions like { min(0..7) } this generates an empty list AllElemenNodes; TO DO: fix
498		findall(constraint([SeqNode],[E],id), member(E,AllElemNodes), Constraints).
499
500		extract_extension_nodes([],_NodeEnv,[],[],X,X).
501		extract_extension_nodes([Elem|Rest],NodeEnv,[ElemNodes|RestNodes],[NElem|NRest],In,Out) :-
502		extract_nodes(Elem,NodeEnv,ElemNodes,_Mode,NElem,In,Inter),
503		extract_extension_nodes(Rest,NodeEnv,RestNodes,NRest,Inter,Out).
504
505
506		texpr_add_node_infos(TExpr,NodeId,NTExpr,In,Out) :-
507		get_texpr_expr(TExpr,Expr),
508		get_texpr_type(TExpr,Type),
509		get_texpr_info(TExpr,Info),
510		add_node_infos(Info,NodeId,NewInfo,In,Inter),
511		create_texpr(Expr,Type,NewInfo,NTExpr),
512		add_existing_constraints(Info,NodeId,Inter,Out).
513		add_node_infos(OldInfo,NodeId,NewInfos,
514		(Constraints,[infonode(NodeId,NewInfos,OldInfo)|Out]),
515		(Constraints,Out)).
516
517		add_all([],In,In).
518		add_all([E|Rest],([E|In],Infonodes),Out) :-
519		add_all(Rest,(In,Infonodes),Out).
520		extract_nodes_l([],_,[],[],[],In,In).
521		extract_nodes_l([TExpr|ERest],NodeEnv,[Node|NRest],[Mode|MRest],[NTExpr|NTRest],In,Out) :-
522		extract_nodes(TExpr,NodeEnv,Node,Mode,NTExpr,In,Inter),
523		extract_nodes_l(ERest,NodeEnv,NRest,MRest,NTRest,Inter,Out).
524		choose_one([],[],[],[]).
525		choose_one([List1|L1Rest],[List2|L2Rest],[Elem1|E1Rest],[Elem2|E2Rest]) :-
526	?	choose_one2(List1,List2,Elem1,Elem2),
527	?	choose_one(L1Rest,L2Rest,E1Rest,E2Rest).
528		choose_one2(NodeList,NodeListRO,Elem,ElemRO) :-
529	?	(Elem == (*) -> true ; nth1(N,NodeList,Elem), nth1(N,NodeListRO,ElemRO)).
530		ignore_readonly_nodes([],[],[]).
531		ignore_readonly_nodes([Mode|MRest],[InNodes|InRest],[OutNodes|OutRest]) :-
532		ignore_readonly_nodes2(Mode,InNodes,OutNodes),
533		ignore_readonly_nodes(MRest,InRest,OutRest).
534		ignore_readonly_nodes2(ro,Nodes,Ignored) :- ignore_readonly_nodes3(Nodes,Ignored).
535		ignore_readonly_nodes2(rw,Nodes,Nodes).
536		ignore_readonly_nodes3([],[]).
537		ignore_readonly_nodes3([Scope:_Node|NRest],[Scope:ignored|IRest]) :-
538		ignore_readonly_nodes3(NRest,IRest).
539
540		nodes_for_general_sum_or_mult(Rule,TId,TPred,TExpr,TOrig,NodeEnv,Nodes,TNew,In,Out) :-
541		identifier_nodes_readonly(NodeEnv,SubEnv1),
542		create_identifier_nodes2([TId],[NTId],SubEnv1,SubEnv,In,Inter1),
543		extract_nodes_l([TId,TPred,TExpr],SubEnv,[IdNodes,_PredNodes,ExprNodes],_Modes,
544		[NTId,NTPred,NTExpr],Inter1,Inter2),
545		get_texpr_info(TOrig,Info),
546		memberchk(interval:ExprNodeId,ExprNodes),
547		memberchk(possible_values:IdId,IdNodes),
548		new_node_scope(integer,NodeId,Nodes),
549		add_node_infos(Info,NodeId,NInfo,Inter2,Inter3),
550		add_all([constraint([possible_values:IdId,interval:ExprNodeId],
551		[interval:NodeId],Rule)],
552		Inter3,Out),
553		get_texpr_expr(TOrig,OrigExpr),functor(OrigExpr,Functor,_),
554		NExpr =.. [Functor,[NTId],NTPred,NTExpr],
555		create_texpr(NExpr,integer,NInfo,TNew).
556
557		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
558		% extract constraints from syntax elements
559		% extract(NExpr,NodeId,InputNodes,OrigOutputNodes,Transition)
560
561		extract(Expr,R,X,Y,Op) :-
562	?	extract_symmetric(Expr,R,X1,Y1,Op1),
563	?	symmetric_constraint(Op1,Op2),
564		( Op=Op1,X=X1,Y=Y1
565		; Op=Op2,X=Y1,Y=X1).
566
567		extract(integer(I),R,[],[interval:R],constant(irange(I,I))).
568		extract(value(IV),R,[],[interval:R],constant(irange(I,I))) :- nonvar(IV), IV = int(I). % TO DO: other vals
569		extract(interval(interval:A,interval:B),R,[interval:A,interval:B],[card:R],interval_card).
570		extract(member(S:A,elem(S):B),_,[elem(S):B],[S:A],id).
571		extract(subset(elem(S):A,elem(S):B),_,[elem(S):B],[elem(S):A],id).
572		extract(subset_strict(elem(S):A,elem(S):B),_,[elem(S):B],[elem(S):A],id).
573	?	extract(add(interval:A,interval:B),R,I,O,C) :- addition_constraint(interval:A,interval:B,interval:R,I,O,C).
574	?	extract(minus(interval:A,interval:B),R,I,O,C) :- addition_constraint(interval:B,interval:R,interval:A,I,O,C).
575		extract(minus(interval:A,interval:B),R,[interval:R,interval:B],[interval:A],add).
576		extract(minus(interval:A,interval:B),R,[interval:A,interval:R],[interval:B],sub).
577		extract(multiplication(interval:A,interval:B),R,[interval:A,interval:B],[interval:R],mult).
578		extract(div(interval:A,interval:B),R,[interval:A,interval:B],[interval:R],divrange).
579		extract(floored_div(interval:A,interval:B),R,[interval:A,interval:B],[interval:R],divrange). % TO DO: provide proper treatment of floored_div
580		extract(modulo(*,interval:B),R,[interval:B],[interval:R],lt).
581		extract(modulo(*,*),R,[],[interval:R],constant(irange(0,inf))).
582		extract(power_of(interval:Base,interval:Exp),R,[interval:Base,interval:Exp],[interval:R],power).
583		extract(integer_set(Set),R,[],[elem(interval):R],constant(irange(Min,Max))) :-
584	?	compute_integer_set(Set,Min,Max).
585		extract(bool_set,R,[],[card:R],constant(irange(2,2))).
586		extract(pow1_subset(*),R,[],[elem(card):R],constant(irange(1,inf))).
587		extract(fin_subset(A),R,AL,RL,Op) :- extract(pow_subset(A),R,AL,RL,Op).
588		extract(fin1_subset(A),R,AL,RL,Op) :- extract(pow1_subset(A),R,AL,RL,Op).
589	?	extract(partial_function(A,B),R,AL,RL,Op) :- extract(relations(A,B),R,AL,RL,Op).
590	?	extract(total_function(A,B),R,AL,RL,Op) :- extract(relations(A,B),R,AL,RL,Op).
591	?	extract(partial_injection(A,B),R,AL,RL,Op) :- extract(partial_function(A,B),R,AL,RL,Op).
592	?	extract(total_injection(A,B),R,AL,RL,Op) :- extract(total_function(A,B),R,AL,RL,Op).
593	?	extract(partial_surjection(A,B),R,AL,RL,Op) :- extract(partial_function(A,B),R,AL,RL,Op).
594	?	extract(total_surjection(A,B),R,AL,RL,Op) :- extract(total_function(A,B),R,AL,RL,Op).
595	?	extract(total_bijection(A,B),R,AL,RL,Op) :- extract(total_function(A,B),R,AL,RL,Op).
596	?	extract(partial_bijection(A,B),R,AL,RL,Op) :- extract(partial_function(A,B),R,AL,RL,Op).
597		extract(cartesian_product(card:A,card:B),R,[card:A,card:B],[card:R],mult).
598		extract(cartesian_product(card:A,card:B),R,[card:R,card:A],[card:B],cart_div).
599		extract(cartesian_product(card:A,card:B),R,[card:R,card:B],[card:A],cart_div).
600		extract(set_subtraction(elem(S):A,*),R,[elem(S):A],[elem(S):R],id).
601		extract(image(elem(right(S)):A,*),R,[elem(right(S)):A],[elem(S):R],id).
602	?	extract(intersection(S:A,*),R,I,O,C) :- is_subset_extract(S:R,S:A,I,O,C).
603	?	extract(intersection(*,S:B),R,I,O,C) :- is_subset_extract(S:R,S:B,I,O,C).
604		extract(union(elem(S):A,elem(S):B),R,[elem(S):A,elem(S):B],[elem(S):R],union).
605	?	extract(union(S:A,*),R,I,O,C) :- is_subset_extract(S:A,S:R,I,O,C).
606	?	extract(union(*,S:B),R,I,O,C) :- is_subset_extract(S:B,S:R,I,O,C).
607		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
608	?	extract(domain_restriction(*,S:B),R,I,O,C) :- is_subset_extract(S:R,S:B,I,O,C).
609	?	extract(domain_subtraction(*,S:B),R,I,O,C) :- is_subset_extract(S:R,S:B,I,O,C).
610		extract(range_restriction(*,S:B),R,I,O,C) :- is_subset_extract(right(S):R,S:B,I,O,C). % ALWAYS FAILS !!!!!
611	?	extract(range_restriction(S:A,*),R,I,O,C) :- is_subset_extract(S:R,S:A,I,O,C).
612	?	extract(range_subtraction(S:A,*),R,I,O,C) :- is_subset_extract(S:R,S:A,I,O,C).
613		extract(closure(elem(S):A),R,[elem(S):A],[elem(S):R],id).
614		extract(composition(elem(left(S)):A,*),R,I,O,C) :- is_subset_extract(elem(left(S)):R,elem(left(S)):A,I,O,C).
615		extract(composition(*,elem(right(S)):B),R,I,O,C) :- is_subset_extract(elem(right(S)):R,elem(right(S)):B,I,O,C).
616		extract(function(elem(right(S)):A,*),R,[elem(right(S)):A],[S:R],id).
617		extract(concat(card:A,card:B),R,I,O,C) :- addition_constraint(card:A,card:B,card:R,I,O,C).
618		extract(concat(Right:A,Right:B),R,[Right:A,Right:B],[Right:R],union) :- Right=elem(right(_)).
619		extract(concat(S:A,*),R,I,O,C) :- S=elem(right(_)),is_subset_extract(S:A,S:R,I,O,C).
620		extract(concat(*,S:B),R,I,O,C) :- S=elem(right(_)),is_subset_extract(S:B,S:R,I,O,C).
621		extract(concat(LI:A,LI:B),R,[LI:A,LI:B],[LI:R],concat_index) :- LI=elem(left(interval)). % TODO: More rules like addition
622		extract(seq(*),R,[],[elem(elem(left(interval))):R],constant(irange(1,inf))).
623		extract(seq1(A),R,I,O,C) :- extract(seq(A),R,I,O,C).
624		extract(seq1(*),R,[],[elem(card):R],constant(irange(1,inf))).
625		extract(size(A),R,I,O,C) :- extract(card(A),R,I,O,C).
626
627		addition_constraint(A,B,R,[A,B],[R],add).
628		addition_constraint(A,B,R,[R,B],[A],sub).
629		addition_constraint(A,B,R,[R,A],[B],sub).
630
631	?	is_subset_extract(A,B,I,O,C) :- extract(subset(A,B),_,I,O,C).
632
633		extract_symmetric(equal(S:A,S:B),_,[S:A],[S:B],id).
634		extract_symmetric(subset(card:A,card:B),_,[card:A],[card:B],gte).
635		extract_symmetric(subset_strict(card:A,card:B),_,[card:A],[card:B],gt).
636		extract_symmetric(less(interval:A,interval:B),_,[interval:B],[interval:A],lt).
637		extract_symmetric(less_equal(interval:A,interval:B),_,[interval:B],[interval:A],lte).
638		extract_symmetric(greater(interval:A,interval:B),_,[interval:B],[interval:A],gt).
639		extract_symmetric(greater_equal(interval:A,interval:B),_,[interval:B],[interval:A],gte).
640		extract_symmetric(unary_minus(interval:X),R,[interval:X],[interval:R],negate).
641		extract_symmetric(card(card:X),R,[card:X],[interval:R],id).
642		extract_symmetric(cartesian_product(elem(S):A,*),R,[elem(S):A],[elem(left(S)):R],id).
643		extract_symmetric(cartesian_product(*,elem(S):B),R,[elem(S):B],[elem(right(S)):R],id).
644		extract_symmetric(couple(S:A,*),R,[S:A],[left(S):R],id).
645		extract_symmetric(couple(*,S:B),R,[S:B],[right(S):R],id).
646		extract_symmetric(pow_subset(elem(S):A),R,[elem(S):A],[elem(elem(S)):R],id).
647		extract_symmetric(pow_subset(card:A),R,[card:A],[elem(card):R],lte).
648		extract_symmetric(pow1_subset(S),R,[A],[B],C) :- extract_symmetric(pow_subset(S),R,[A],[B],C).
649		extract_symmetric(seq(A),R,[elem(S):A],[elem(elem(right(S))):R],id).
650		extract_symmetric(relations(elem(S):A,*),R,[elem(S):A],[elem(elem(left(S))):R],id).
651		extract_symmetric(relations(*,elem(S):B),R,[elem(S):B],[elem(elem(right(S))):R],id).
652		extract_symmetric(interval(interval:A,interval:_),R,[interval:A],[elem(interval):R],gte).
653		extract_symmetric(interval(interval:_,interval:B),R,[interval:B],[elem(interval):R],lte).
654		extract_symmetric(partial_function(card:A,card:_),R,[card:A],[elem(card):R],lte).
655		extract_symmetric(total_function(card:A,card:_),R,[card:A],[elem(card):R],id).
656		extract_symmetric(partial_injection(card:_,card:B),R,[card:B],[elem(card):R],lte).
657		extract_symmetric(total_injection(card:_,card:B),R,[card:B],[elem(card):R],lte).
658		extract_symmetric(total_surjection(card:_,card:B),R,[card:B],[elem(card):R],gte).
659		extract_symmetric(total_bijection(card:A,card:_),R,[card:A],[elem(card):R],id).
660		extract_symmetric(total_bijection(card:_,card:B),R,[card:B],[elem(card):R],id).
661		extract_symmetric(domain(elem(left(S)):A),R,[elem(left(S)):A],[elem(S):R],id).
662		extract_symmetric(range(elem(right(S)):A),R,[elem(right(S)):A],[elem(S):R],id).
663		extract_symmetric(reverse(elem(left(S)):A),R,[elem(left(S)):A],[elem(right(S)):R],id).
664		extract_symmetric(reverse(elem(right(S)):A),R,[elem(right(S)):A],[elem(left(S)):R],id).
665		extract_symmetric(reverse(card:A),R,[card:A],[card:R],id).
666		extract_symmetric(set_subtraction(card:A,*),R,[card:A],[card:R],lte). % was erroneously gte, see test 2410
667		extract_symmetric(closure(elem(left(S)):A),R,[elem(left(S)):A],[elem(left(S)):R],id).
668		extract_symmetric(closure(elem(right(S)):A),R,[elem(right(S)):A],[elem(right(S)):R],id).
669		extract_symmetric(closure(card:A),R,[card:A],[card:R],gte).
670		extract_symmetric(image(card:A,*),R,[card:R],[card:A],gte).
671		extract_symmetric(first_of_pair(left(S):A),R,[left(S):A],[S:R],id).
672		extract_symmetric(second_of_pair(right(S):A),R,[right(S):A],[S:R],id).
673
674		symmetric_constraint(A,B) :- symmetric_constraint2(A,B),!.
675	?	symmetric_constraint(A,B) :- symmetric_constraint2(B,A).
676		symmetric_constraint2(id,id).
677		symmetric_constraint2(lt,gt).
678		symmetric_constraint2(lte,gte).
679		symmetric_constraint2(negate,negate).
680
681
682		% this seems to take up most of the time:
683		create_constraint_tree(Constraints,Nodes,Tree) :-
684		empty_avl(EmptyTree),
685		sort(Constraints,SConstraints), % for SAT_Generator sorting reduces runtime from 22 sec to 18 sec for n=8; TO DO: investigate
686		(debug:debug_mode(on) -> length(Constraints,Len), format('Processing ~w constraints~n',[Len]) ; true),
687		create_constraint_tree1(SConstraints,[],UnsortedNodes,EmptyTree,Tree),
688		(debug:debug_mode(on) -> length(UnsortedNodes,Len2), format('Sorting ~w nodes~n',[Len2]) ; true),
689		sort(UnsortedNodes,Nodes),
690		(debug:debug_mode(on) -> length(Nodes,Len3), format('Done sorting ~w nodes~n',[Len3]) ; true).
691		%,set_prolog_flag(profiling,off),print_profile.
692
693		create_constraint_tree1([],Nodes,Nodes,Tree,Tree).
694		create_constraint_tree1([C|CRest],InNodes,OutNodes,InTree,OutTree) :-
695		create_constraint_tree2(C,InNodes,InterNodes,InTree,InterTree),
696		create_constraint_tree1(CRest,InterNodes,OutNodes,InterTree,OutTree).
697
698		create_constraint_tree2(Constraint,InNodes,OutNodes,InTree,OutTree) :-
699		Constraint = constraint(Input,Output,_Rule),
700		( all_nodes_ignored(Output) ->
701		InTree = OutTree, InNodes=OutNodes
702		;
703		add_all_to_constraint_tree(Input,Constraint,InTree,OutTree),
704		%ord_union(Input,InNodes,Nodes),ord_union(Output,Nodes,OutNodes) % this can be very expensive !
705		append(Input,InNodes,Nodes), append(Output,Nodes,OutNodes) % just append the nodes and sort them later
706		).
707
708		add_all_to_constraint_tree([],_,Tree,Tree).
709		add_all_to_constraint_tree([Node|NRest],Constraint,InTree,OutTree) :-
710		( avl_change(Node,InTree,Old,InterTree,[Constraint|Old]) ->
711		true
712		;
713		avl_store(Node,InTree,[Constraint],InterTree)),
714		add_all_to_constraint_tree(NRest,Constraint,InterTree,OutTree).
715
716		all_nodes_ignored([]).
717		all_nodes_ignored([_:ignored|Rest]) :-
718		all_nodes_ignored(Rest).
719
720
721		create_initial_information(Nodes,InitEnv) :-
722		empty_avl(Empty),
723		foldl(create_initial_information2,Nodes,Empty,InitEnv).
724		create_initial_information2(Scope:Node,In,Out) :-
725		get_scope_top(Scope,Top),
726		avl_store(Scope:Node,In,Top,Out).
727
728		apply_start_constraints(Constraints,ChangedNodes,In,Out) :-
729		find_start_constraints(Constraints,Start),
730		writetodot(1,[],Start,In),
731		compute_constraints(Start,ChangedNodes1,[],In,Out),
732		list_to_ord_set(ChangedNodes1,ChangedNodes).
733		find_start_constraints(Constraints,Start) :-
734		findall(constraint([],Output,Rule),
735		member(constraint([],Output,Rule),Constraints),
736		Start).
737
738		do_analysis([],Counter,_MaxIter,_CTree,Values,Values) :-
739		!,writetodot(Counter,[],[],Values).
740		do_analysis([ChangedNode|CNRest],Counter,MaxIter,CTree,In,Out) :-
741		Counter < MaxIter,!,
742		(avl_fetch(ChangedNode,CTree,Constraints) -> true ; Constraints = []),
743		writetodot(Counter,[ChangedNode|CNRest],Constraints,In),
744	?	compute_constraints(Constraints,ChangedNodes1,[],In,Inter),
745		list_to_ord_set(ChangedNodes1,ChangedNodes),
746		ord_union(CNRest,ChangedNodes,NewChangedNodes),
747		Counter2 is Counter+1,
748	?	do_analysis(NewChangedNodes,Counter2,MaxIter,CTree,Inter,Out).
749		do_analysis(_ChangedNodes,Counter,MaxIter,_CTree,Values,Values) :-
750		Counter >= MaxIter.
751		compute_constraints([],Changed,Changed,Values,Values).
752		compute_constraints([Constraint|CRest],Cin,Cout,Vin,Vout) :-
753	?	compute_constraint(Constraint,Cin,Cinter,Vin,Vinter),
754	?	compute_constraints(CRest,Cinter,Cout,Vinter,Vout).
755		compute_constraint(constraint(Input,Output,Rule),Cin,Cout,Vin,Vout) :-
756		get_input_values(Input,Vin,InValues),
757		same_length(Output,OutValues),
758	?	call_rule(Rule,InValues,OutValues),
759		apply_output(Output,OutValues,Cin,Cout,Vin,Vout).
760		get_input_values([],_,[]).
761		get_input_values([Node|NRest],Values,[Value|VRest]) :-
762		avl_fetch(Node,Values,Value),
763		get_input_values(NRest,Values,VRest).
764		call_rule(Rule,InValues,OutValues) :-
765		append_arguments(Rule,InValues,CallRule),
766	?	if(rule(CallRule,OutValues), true,
767		(add_warning(predicate_analysis,'No rule for: ',CallRule),fail)).
768		apply_output([],[],Changed,Changed,Values,Values).
769		apply_output([Node|NRest],[Value|VRest],Cin,Cout,Vin,Vout) :-
770		( Node = _:ignored ->
771		Vin = Vinter, Cin=Cinter
772		;
773		avl_change(Node,Vin,OldValue,Vinter,NewValue),
774		info_conjunct(OldValue,Value,NewValue),
775		( has_more_information(NewValue,OldValue) ->
776		Cin = [Node|Cinter]
777		;
778		Cin = Cinter)),
779		apply_output(NRest,VRest,Cinter,Cout,Vinter,Vout).
780
781		append_arguments(Orig,Args,Result) :-
782		Orig =.. FA,
783		append_arguments2(FA,Args,AllArgs),
784		Result =.. AllArgs.
785		append_arguments2([F|FA],Args,AllArgs) :-
786		multi_rule(F),!,
787		append([F|FA],[Args],AllArgs).
788		append_arguments2(FA,Args,AllArgs) :-
789		append(FA,Args,AllArgs).
790
791
792		create_add_list_constraints([],_Result,Constraints) :- !,Constraints=[].
793		create_add_list_constraints([Node],Result,Constraints) :- !,
794		Constraints = [constraint([Node],[Result],id),constraint([Result],[Node],id)].
795		create_add_list_constraints(Nodes,Result,Constraints) :- !,
796		create_add_list_constraints2(Nodes,Result,Constraints,[]).
797		create_add_list_constraints2([A,B],Result) --> !,
798		findall(constraint(I,O,C),addition_constraint(A,B,Result,I,O,C)).
799		create_add_list_constraints2([A|Nodes],Result) -->
800		{new_node_scope(integer,NodeId,_Nodes)},
801		findall(constraint(I,O,C),addition_constraint(A,interval:NodeId,Result,I,O,C)),
802		create_add_list_constraints2(Nodes,interval:NodeId).
803
804
805
806		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
807		% compute a single constraint
808
809		rule(id(Info),[Info]).
810		rule(constant(Info),[Info]).
811		rule(add(A,B),[C]) :- interval_addition(A,B,C).
812		rule(sub(A,B),[C]) :- interval_subtraction(A,B,C).
813		rule(mult(A,B),[C]) :- interval_multiplication(A,B,C).
814		rule(power(Base,Exp),[Result]) :-
815		(power_rule(Base,Exp,Result) -> true ; Result = irange(-inf,inf)).
816		rule(cart_div(irange(Cm,CM2),irange(Am,AM2)),[irange(Bm,BM2)]) :- % propagates C = A * B
817		( CM2 = inf -> % C can be infinite
818		BM2 = inf
819		; Am = 0, % the set A can be empty
820		number(Cm),Cm<1 -> % set C can be empty
821		BM2 = inf % B can be arbitrarily larger and still yield an empty A*B
822		; Am = 0 -> % case: set C cannot be empty, actually Am is 1
823		BM2 = CM2 % B can be as large as the maximum size of C
824		; Am = inf -> % A is infinite
825		BM2 = 0 % as CM2 is not inf, C cannot be infinite, only solution is B to be empty
826		;
827		BM2 infis (CM2+Am-1) // Am % e.g., for CM2=3 and Am=2 we obtain 2 ?? Shouldnt we use CM2 // Am ??
828		),
829		( number(Cm),Cm<1 -> % set C can be empty
830		Bm = 0 % B can also be empty
831		; AM2 = 0 -> % A has to be empty; this means C is empty and we have a contradiction
832		Bm is -1 % try force contradiction
833		; AM2 = inf -> % A can be infinite, but C is definitely not empty
834		Bm = 1 % B must have at least one element
835		; Cm = inf -> Bm = inf % C has to be infinite, but A is finite
836		; AM2 > Cm -> Bm = 1 % B must have at least one element, as C is not empty
837		;
838		Bm infis Cm // AM2). % minimal size of B is C divided by maximal size of A
839		% 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
840		% print(rule_result(cart_div(irange(Cm,CM2),irange(Am,AM2)),[irange(Bm,BM2)])),nl.
841		rule(negate(A),[C]) :- interval_negation(A,C).
842		rule(lt(irange(_,AM2)),[irange(-inf,CM2)]) :- CM2 infis AM2-1.
843		rule(lte(irange(_,AM2)),[irange(-inf,AM2)]).
844		rule(gt(irange(Am,_)),[irange(Cm,inf)]) :- Cm infis Am+1.
845		rule(gte(irange(Am,_)),[irange(Am,inf)]).
846		rule(interval_card(irange(Am,AM2),irange(Bm,BM2)),[irange(Cm,CM2)]) :-
847		Cm infis max(Bm-AM2+1,0), CM2 infis max(BM2-Am+1,0).
848		rule(interval_possibilities(irange(Am,AM2)),[irange(0,M)]) :-
849		M infis max(AM2-Am+1,0).
850		rule(union([A|Rest]),[C]) :- union2(Rest,A,C).
851		rule(union([]),[irange(-inf,inf)]) :- print(empty_kodkod_union_constraint),nl. % TO DO: check if ok !!
852		% happens e.g., for set extensions like { min(0..7) } ; should not occur
853		rule(divrange(irange(Am,AM2),irange(Bm,BM2)),[C]) :- C = irange(MinC,MaxC),
854		div_rule(Am,AM2,Bm,BM2,MinC,MaxC),
855		format('Division propagation: ~w..~w / ~w..~w ---> ~w~n',[Am,AM2,Bm,BM2,C]).
856		rule(concat_index(irange(_,AM2),irange(_,BM2)),[irange(1,CM2)]) :-
857		(number(AM2),number(BM2) -> CM2 is AM2+BM2 ; CM2 = inf).
858
859
860		:- assert_must_succeed((div_rule(1,100,1,2,MinC,MaxC), MinC == 0, MaxC == 100)).
861		:- assert_must_succeed((div_rule(100,200,1,50,MinC,MaxC), MinC == 2, MaxC == 200)).
862		:- assert_must_succeed((div_rule(-2,100,1,50,MinC,MaxC), MinC == -2, MaxC == 100)).
863		:- assert_must_succeed((div_rule(-2,100,0,50,MinC,MaxC), MinC == -2, MaxC == 100)). % with try_find_abort we would get:
864		% :- assert_must_succeed((div_rule(-2,100,0,50,MinC,MaxC), MinC == -inf, MaxC == inf)). % above with try_find_abort
865
866		% propagate division Am..AM2 / Bm..BM2 --> C
867		div_rule(Am,AM2,Bm,BM2,MinC,MaxC) :- number(Bm), Bm >= 0,!, % division by positive number
868		(Am = -inf -> MinC = -inf
869		; 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
870		; Am < 0 -> MinC is Am // Bm % a possible lowest value is obtained by the largest absolute (neg) value
871		; BM2=inf -> MinC is 0 % Am is positive ; we can divide Am by an arbitrarily large number to reach 0
872		; MinC is Am // BM2 % minimum is dividing min of A by maximum of B
873		),
874		(AM2 = inf -> MaxC = inf
875		; BM2=inf, AM2<0 -> MinC is 0 % Am is positive ; we can divide Am by an arbitrarily large number to reach 0
876		; AM2 < 0 -> MaxC is AM2 // BM2 % a possible max value is obtained by the smallest absolute (neg) value
877		; Bm=0 -> MaxC = AM2 % if try_find_abort is true we could set MaxC to inf
878		; MaxC is AM2 // Bm % maximum is dividing max of A by min of B
879		).
880		div_rule(Am,AM2,_Bm,_BM2,MinC,MaxC) :- number(Am),number(AM2), !, % TODO: improve and check
881		M is max(abs(Am),abs(AM2)), % if try_find_abort is true we could divide by 0 and set to -inf .. inf
882		MinC is -M, MaxC = M.
883		div_rule(_,_,_,_,-inf,inf).
884
885		union2([],Acc,R) :- !,Acc=R.
886		union2([H|T],Acc,R) :- info_disjunct(H,Acc,I),union2(T,I,R).
887
888		power_rule(irange(Basem,BaseM2),irange(Expm,ExpM2),irange(Rm,RM2)) :-
889		number(Basem),Basem > 0,
890		number(Expm),Expm >= 0,
891		Rm is floor( Basem ** Expm),
892		((BaseM2=inf; ExpM2=inf) -> RM2=inf ; RM2 is floor(BaseM2 ** ExpM2)).
893
894		multi_rule(union).
895
896
897		insert_info(Infonodes,Values) :-
898		create_info_lookup_table(Values,ValueTable),
899		insert_info2(Infonodes,ValueTable).
900		insert_info2([],_).
901		insert_info2([infonode(Node,New,Old)|Rest],Values) :-
902		find_all_node_information(Node,Values,Info),
903		add_info(Info,Old,New),
904		insert_info2(Rest,Values).
905
906		:- load_files(library(system), [when(compile_time), imports([environ/2])]).
907		:- if(environ(prob_safe_mode,true)).
908		find_all_node_information(Node,_,_) :- \+ ground(Node), add_internal_error('Non-ground node: ',Node),fail.
909		:- endif.
910		find_all_node_information(Node,Values,Info) :-
911		( avl_fetch(Node,Values,RawInfos) -> filter_tops(RawInfos,Info) % used to call avl_member; but Node is ground
912		; Info = []).
913
914		filter_tops([],[]).
915		filter_tops([Scope:RI|RRest],Result) :-
916		get_scope_top(Scope,Top),
917		( has_more_information(RI,Top) -> Result = [Scope:RI|RestResult]
918		; Result = RestResult),
919		filter_tops(RRest,RestResult).
920
921		add_info([],Old,Old) :- !.
922		add_info(Info,Old,[analysis(Info)|Old]).
923
924		create_info_lookup_table(Values,Nodes) :-
925		avl_to_list(Values,ValueList),
926		empty_avl(Empty),
927		create_info_lookup_table2(ValueList,Empty,Nodes).
928		create_info_lookup_table2([],Nodes,Nodes).
929		create_info_lookup_table2([(Scope:Node)-I|Rest],In,Out) :-
930		(avl_fetch(Node,In,Old) -> true ; Old = []),
931		avl_store(Node,In,[Scope:I|Old],Inter),
932		create_info_lookup_table2(Rest,Inter,Out).
933
934		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
935		% dot output
936
937		writetodot(Counter,ChangedNodes,ActiveConstraints,Values) :-
938		debugging_enabled,!,
939		debug_constraints(Constraints),
940		writetodot(Counter,Constraints,ChangedNodes,ActiveConstraints,Values).
941		writetodot(_Counter,_ChangedNodes,_ActiveConstraints,_Values).
942
943		writetodot(Counter,Constraints,ChangedNodes,ActiveConstraints,Values) :-
944		printnulls(3,Counter,CStr),
945		ajoin(['debug-constraint-anim/constraints-',CStr,'.dot'],Filename),
946		debug_format(19,'Writing Kodkod constraints to dot file: ~w~n',[Filename]),
947		open(Filename,write,S),
948		write(S,'digraph constraints {\n'),
949		get_nodes(Constraints,INodes,CNodes),
950		write_inodes(INodes,ChangedNodes,Values,S),
951		write_cnodes(CNodes,INodes,ActiveConstraints,S),
952		write(S,'}\n'),
953		close(S).
954		get_nodes(Constraints,INodes,RNodes) :-
955		findall(CN,
956		(member(constraint(I,O,_),Constraints),
957		(member(CN,I);member(CN,O))),
958		Nodes1),
959		sort(Nodes1,Nodes2),
960		number_nodes(Nodes2,1,INodes),
961		number_nodes(Constraints,1,RNodes).
962		number_nodes([],_,[]).
963		number_nodes([N|Rest],Nr,[node(Nr,N)|RRest]) :-
964		Nr2 is Nr+1,
965		number_nodes(Rest,Nr2,RRest).
966		write_inodes([],_,_,_).
967		write_inodes([node(Nr,N)|Rest],ChangedNodes,Values,S) :-
968		write(S,' i'),write(S,Nr),write(S,'[shape=box,'),
969		( ChangedNodes = [N|_] ->
970		!,write(S,'fillcolor=green,style=filled,')
971		; member(N,ChangedNodes) ->
972		!,write(S,'fillcolor=yellow,style=filled,')
973		; true),
974		write(S,'label=\"'),
975		write(S,N),write(S,'\\n'),
976		( debug_node(N,TExpr) ->
977		translate_bexpression(TExpr,Text)
978		;
979		Text = ('?')),
980		write(S,Text),write(S,'\\n'),
981		( avl_fetch(N,Values,Value) ->
982		write(S,Value)
983		; write(S,'?')),
984		write(S,'\"];\n'),
985		write_inodes(Rest,ChangedNodes,Values,S).
986		write_cnodes([],_,_,_).
987		write_cnodes([node(Nr,constraint(In,Out,R))|Rest],INodes,ActiveConstraints,S) :-
988		write(S,' c'),write(S,Nr),write(S,'[shape=diamond,'),
989		( member(constraint(In,Out,R),ActiveConstraints) ->
990		!,write(S,'fillcolor=lightblue,style=filled,')
991		; true),
992		write(S,'label=\"'),
993		write(S,R),write(S,'\"];\n'),
994		write_inputs(In,INodes,Nr,S),
995		write_outputs(Out,INodes,Nr,S),
996		write_cnodes(Rest,INodes,ActiveConstraints,S).
997		write_inputs([],_,_,_).
998		write_inputs([I|Rest],INodes,RNr,S) :-
999		member(node(INr,I),INodes),!,
1000		write(S,' i'),write(S,INr),write(S,' -> '),
1001		write(S,' c'),write(S,RNr),write(S,';\n'),
1002		write_inputs(Rest,INodes,RNr,S).
1003		write_outputs([],_,_,_).
1004		write_outputs([O|Rest],INodes,RNr,S) :-
1005		member(node(ONr,O),INodes),!,
1006		write(S,' c'),write(S,RNr),write(S,' -> '),
1007		write(S,' i'),write(S,ONr),write(S,';\n'),
1008		write_outputs(Rest,INodes,RNr,S).
1009
1010		printnulls(N,Number,Str) :-
1011		number_codes(Number,NCodes),
1012		length(NCodes,L),
1013		R is N-L,
1014		fillnulls(R,NCodes,Codes),
1015		atom_codes(Str,Codes).
1016		fillnulls(R,Codes,Codes) :- R =< 0,!.
1017		fillnulls(R,NCodes,[48|Codes]) :-
1018		R2 is R-1,
1019		fillnulls(R2,NCodes,Codes).
1020
1021
1022		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1023
1024		:- dynamic debug_predicate_analysis/0.
1025		% assert this fact to enable dot visualization using writetodot below
1026
1027		store_debug_info(I,T) :- debug_predicate_analysis,!,store_debug_info2(I,T).
1028		store_debug_info(_,_).
1029
1030		store_debug_info2([],_).
1031		store_debug_info2([Node|Rest],TExpr) :-
1032		assertz(debug_node(Node,TExpr)),
1033		store_debug_info2(Rest,TExpr).
1034
1035
1036		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1037		% test case specification for predicate analysis
1038
1039		:- use_module(probsrc(junit_tests)).
1040
1041		test_predicate_analysis :-
1042		b_machine_has_constants,
1043		b_get_machine_constants(Constants),
1044		b_get_properties_from_machine(Properties),
1045		b_get_static_assertions_from_machine(Assertions),
1046		Assertions = [_|_],!,
1047		test_predicate_analysis2(Constants,Properties,Assertions,Junits),
1048		b_machine_name(MachineName),
1049		print_junit([predicate_analysis,MachineName], Junits).
1050		test_predicate_analysis :-
1051		add_error(predicate_analysis,
1052		'Machine must have constants and assertions to be a valid predicate analysis test case.'),
1053		fail.
1054		test_predicate_analysis2(Constants,Properties,Assertions,Junits) :-
1055	?	predicate_analysis_with_global_sets(Properties,[],Constants,TaggedConstants,_TaggedProperties),!,
1056		test_predicate_analysis3(Assertions,TaggedConstants,Junits).
1057		test_predicate_analysis2(_,_,_,[Junit]) :-
1058		in_junit_mode,!,
1059		pa_junit(setup,error('Predicate analysis failed'),Junit).
1060		test_predicate_analysis2(_,_,_,_) :-
1061		add_error(predicate_analysis, 'Predicate analysis of properties failed'),
1062		fail.
1063		test_predicate_analysis3([],_Constants,[]).
1064		test_predicate_analysis3([Assertion|Arest],Constants,[Junit|Jrest]) :-
1065		test_predicate_analysis_testcase(Assertion,Constants,Junit),
1066		test_predicate_analysis3(Arest,Constants,Jrest).
1067
1068		test_predicate_analysis_testcase(TAssertion,Constants,Junit) :-
1069		translate_bexpression(TAssertion,Name),
1070	?	( catch( ( test_predicate_analysis_testcase1(TAssertion,Constants),
1071		pa_junit(Name,pass,Junit)),
1072		junit(Msg),
1073		handle_error(Name,Msg,Junit)) -> true
1074		;
1075		pa_junit(Name,error('Test failed.'),Junit)).
1076		handle_error(Name,Msg,Junit) :-
1077		in_junit_mode,!,
1078		pa_junit(Name,error(Msg),Junit).
1079		handle_error(Name,Msg,_Junit) :-
1080		add_error(predicate_analysis, Name, Msg), fail.
1081
1082		test_predicate_analysis_testcase1(TAssertion,Constants) :-
1083	?	extract_predicate_analysis_testcases(TAssertion,[],Testcases),
1084		maplist(run_testcase(Constants),Testcases).
1085		run_testcase(Constants,pa_testcase(Id,Scope,ExpectedValue)) :-
1086		formatsilent('Predicate analysis testcase: check if "~w" of "~w" is ~w~N', [Scope,Id,ExpectedValue]),
1087		expected_value_is_top(ExpectedValue,Scope,IsTop),
1088		extract_analysis(Id,Constants,Scope,FoundValue,IsTop),
1089		( FoundValue == ExpectedValue -> true
1090		;
1091		ajoin(['unexpected information for constant ',Id,': expected ', ExpectedValue,
1092		', but was ', FoundValue],Msg),
1093		throw(junit(Msg))).
1094		expected_value_is_top(ExpectedValue,Scope,true) :-
1095		ground(ExpectedValue),get_scope_top(Scope,ExpectedValue),!.
1096		expected_value_is_top(_ExpectedValue,_Scope,false).
1097
1098		extract_predicate_analysis_testcases(TExpr,QRefs,Testcases) :-
1099		get_texpr_expr(TExpr,Expr),
1100	?	extract_predicate_analysis_testcases2(Expr,QRefs,Testcases).
1101		extract_predicate_analysis_testcases2(forall(Ids,TPre,Cond),QRefs,Testcases) :-
1102		get_texpr_expr(TPre,Pre),introduce_qrefs(Pre,Ids,QRefs,SubQRefs),
1103	?	extract_predicate_analysis_testcases(Cond,SubQRefs,Testcases).
1104		extract_predicate_analysis_testcases2(equal(Ref,Spec),QRefs,[pa_testcase(Constant,Scope,irange(Value,Value))]) :- !,
1105		extract_test_reference(Ref,QRefs,Constant,Scope),
1106		extract_integer(Spec,Value).
1107		extract_predicate_analysis_testcases2(less_equal(Ref,Spec),QRefs,[pa_testcase(Constant,Scope,irange(-inf,Value))]) :- !,
1108		extract_test_reference(Ref,QRefs,Constant,Scope),
1109		extract_integer(Spec,Value).
1110		extract_predicate_analysis_testcases2(greater_equal(Ref,Spec),QRefs,[pa_testcase(Constant,Scope,irange(Value,inf))]) :- !,
1111		extract_test_reference(Ref,QRefs,Constant,Scope),
1112		extract_integer(Spec,Value).
1113		extract_predicate_analysis_testcases2(member(Ref,TSpec),QRefs,[pa_testcase(Constant,Scope,Info)]) :-
1114		get_texpr_expr(TSpec,Spec),
1115		extract_test_reference(Ref,QRefs,Constant,Scope),
1116		integer_interval_membership(Spec,Scope,Info),!.
1117		extract_predicate_analysis_testcases2(not_member(Ref,TSpec),QRefs,[pa_testcase(Constant,Scope,Top)]) :-
1118		get_texpr_expr(TSpec,empty_set),
1119		extract_test_reference(Ref,QRefs,Constant,Scope),
1120		get_scope_top(Scope,Top).
1121		extract_predicate_analysis_testcases2(conjunct(A,B),QRefs,Testcases) :- !,
1122	?	extract_predicate_analysis_testcases(A,QRefs,TestcasesA),
1123	?	extract_predicate_analysis_testcases(B,QRefs,TestcasesB),
1124		append(TestcasesA,TestcasesB,Testcases).
1125		extract_predicate_analysis_testcases2(_Expr,_QRefs,_Testcases) :-
1126		throw(junit('Unsupported test case pattern')).
1127
1128		integer_interval_membership(empty_set,Scope,Bottom) :- get_scope_bottom(Scope,Bottom).
1129		integer_interval_membership(interval(Min,Max),_Scope,irange(VMin,VMax)) :-
1130		extract_integer(Min,VMin),extract_integer(Max,VMax).
1131		integer_interval_membership(integer_set(I),_Scope,irange(Min,Max)) :-
1132		compute_integer_set(I,Min,Max).
1133
1134		introduce_qrefs(member(E2,Ref),Ids,QRefs,NewQRefs) :-
1135		lookup_ref(Ref,QRefs,Path,Constant),append(Path,[elem],Path2),
1136		couple_pathes(E2,Path2,Constant,Ids,NewQRefs,QRefs).
1137		introduce_qrefs(equal(E2,Ref),Ids,QRefs,NewQRefs) :-
1138		lookup_ref(Ref,QRefs,Path,Constant),
1139		couple_pathes(E2,Path,Constant,Ids,NewQRefs,QRefs).
1140
1141		couple_pathes(TExpr,Path,Constant,TIdentifiers) -->
1142		{get_texpr_ids(TIdentifiers,Identifiers)},
1143		couple_pathes2(TExpr,Path,Constant,Identifiers).
1144		couple_pathes2(TExpr,Path,Constant,Identifiers) -->
1145		{get_texpr_expr(TExpr,Expr)},couple_pathes3(Expr,TExpr,Path,Constant,Identifiers).
1146		couple_pathes3(identifier(Id),_,Path,Constant,Identifiers) -->
1147		{memberchk(Id,Identifiers),!},[Id-ref(Path,Constant)].
1148		couple_pathes3(couple(A,B),_,Path,Constant,Identifiers) --> !,
1149		{append(Path,[left],PathA),append(Path,[right],PathB)},
1150		couple_pathes2(A,PathA,Constant,Identifiers),
1151		couple_pathes2(B,PathB,Constant,Identifiers).
1152		couple_pathes3(_,TExpr,_Path,_Constant,_Identifiers,_,_) :-
1153		translate_bexpression(TExpr,String),
1154		atom_concat('Expected quantified identifier or couple in test specification, but was: ',
1155		String,Msg),
1156		throw(junit(Msg)).
1157
1158
1159		lookup_ref(Expr,QRefs,Path,Constant) :-
1160		get_texpr_id(Expr,Id),
1161		memberchk(Id-ref(Path1,Constant1),QRefs),!,
1162		Path1=Path,Constant1=Constant.
1163		lookup_ref(Expr,_QRefs,[],Id) :-
1164		get_texpr_id(Expr,Id).
1165
1166		extract_analysis(Id,Constants,Scope,FoundValue,IsTop) :-
1167		get_texpr_id(Constant,Id),
1168		( memberchk(Constant,Constants) ->
1169		get_texpr_info(Constant,Info),
1170		(memberchk(analysis(Analysis),Info) -> true ; Analysis=[]),
1171		( memberchk(Scope:FoundValue,Analysis) -> true
1172		; IsTop == true -> get_scope_top(Scope,FoundValue) /* no information expected */
1173		;
1174		ajoin(['No analysis information found for constant ',Id,', scope ',Scope],Msg),
1175		print(extract_analysis(Id,Constants,Scope,FoundValue,IsTop)),nl,
1176		throw(junit(Msg)))
1177		;
1178		ajoin(['Constant ',Id,' not found'],Msg),
1179		throw(junit(Msg))).
1180
1181		extract_test_reference(TRef,QRefs,Id,Scope) :-
1182		get_texpr_expr(TRef,Ref),
1183		extract_test_reference2(Ref,QRefs,BaseScope,Id,ScopeList),
1184		construct_scope(ScopeList,BaseScope,Scope),!.
1185		extract_test_reference(TRef,_QRefs,_Id,_Scope) :-
1186		translate_bexpression(TRef,String),
1187		atom_concat('Unsupported reference on left side: ', String,Msg),
1188		throw(junit(Msg)).
1189		extract_test_reference2(card(TRef),QRefs,card,Id,Scope) :-
1190		!,get_texpr_expr(TRef,Ref),Ref=identifier(_),
1191		extract_test_reference2(Ref,QRefs,_,Id,Scope).
1192		extract_test_reference2(identifier(Id),QRefs,interval,Constant,Scope) :-
1193		memberchk(Id-ref(Scope,Constant),QRefs),!.
1194		extract_test_reference2(identifier(Id),_QRefs,interval,Id,[]) :- !.
1195
1196
1197		:- assert_must_succeed(( construct_scope([elem,right],interval,S),
1198		S==elem(right(interval)) )).
1199		construct_scope([],Scope,Scope).
1200		construct_scope([F|Rest],Base,Scope) :-
1201		functor(Scope,F,1),arg(1,Scope,Subscope),
1202		construct_scope(Rest,Base,Subscope).
1203
1204		extract_integer(Spec,Value) :-
1205		( get_texpr_expr(Spec,integer(Value)) -> true
1206		; get_texpr_expr(Spec,unary_minus(Spec2)) ->
1207		extract_integer(Spec2,Value2),Value is -Value2
1208		;
1209		throw(junit('Integer value expected in right side of assertion'))).
1210
1211		in_junit_mode :-
1212		junit_mode(_),!.
1213
1214		pa_junit(Name,Verdict,Junit) :-
1215		create_junit_result(Name,0,Verdict,Junit).