1		% (c) 2009-2019 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(bsyntaxtree).
20		:- use_module(btypechecker).
21		:- use_module(preferences).
22		:- use_module(tools).
23		:- use_module(translate).
24		:- use_module(bmachine).
25		:- use_module(b_global_sets, [is_b_global_constant/3,b_global_set_cardinality/2]).
26
27		:- use_module(error_manager).
28		:- use_module(self_check).
29		:- use_module(debug,[debug_println/2]).
30
31		:- use_module(inf_arith).
32		:- use_module(interval_calc).
33
34		% for interpreting value(...) components
35		:- use_module(store, [empty_state/1]).
36		:- use_module(b_interpreter, [b_compute_expression_nowf/4]).
37
38		:- use_module(module_information,[module_info/2]).
39		:- module_info(group,analysis).
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(_)),assert(debug_constraints(Constraints)),
87		create_initial_information(Nodes,Empty),
88		apply_start_constraints(Constraints,ChangedNodes,Empty,Initial),
89		compute_maximum_iterations(Nodes,MaxIter),
90		debug_println(15,predicate_analysis:do_analysis(MaxIter)),
91		start_ms_timer(Timer4),
92		do_analysis(ChangedNodes,2,MaxIter,CTree,Initial,Values),
93		(debug:debug_mode(on) -> stop_ms_timer_with_msg(Timer4,do_analysis) ; true),
94		insert_info(Infos,Values).
95
96		create_node_environment(ROIdentifiers,Identifiers,NewIdentifiers,NodeEnv,Infos) :-
97		initial_node_env(InitNodeEnv),
98		create_identifier_nodes2(ROIdentifiers,_,InitNodeEnv,RONodeEnv1,Infos1,([],[])),
99		identifier_nodes_readonly(RONodeEnv1,RONodeEnv),
100		create_identifier_nodes2(Identifiers,NewIdentifiers,RONodeEnv,NodeEnv,Infos2,Infos1),
101		foldl(add_id_basic_constraint(NodeEnv),Identifiers,Infos,Infos2).
102		add_id_basic_constraint(NodeEnv,Identifier,In,Out) :-
103		get_texpr_id(Identifier,Id),
104		identifier_node_lookup(Id,NodeEnv,_NodeId,Nodes,_Mode),
105		add_type_constraints(Identifier,Nodes,In,Out).
106
107		% just a heuristic to avoid a non-terminating run
108		compute_maximum_iterations(Nodes,MaxIter) :-
109		length(Nodes,N), MaxIter is N*10.
110
111		reset_nodecounter :-
112		retractall(nodecounter(_)),assert(nodecounter(1)),
113		retractall(debug_node(_,_)),
114		retractall(debug_constraints(_)).
115
116		% create a numbered node for each identifier
117		initial_node_env(NodeEnv) :- empty_avl(NodeEnv).
118
119		%create_identifier_nodes(Ids,NIds,Env,IIn,IOut) :-
120		% empty_avl(Start), create_identifier_nodes2(Ids,NIds,Start,Env,IIn,IOut).
121
122		create_identifier_nodes2([],[],Env,Env,Info,Info).
123		create_identifier_nodes2([TId|Rest],[NTId|NRest],In,Out,IIn,IOut) :-
124		create_identifier_nodes3(TId,NTId,In,Inter,IIn,IInter),
125		create_identifier_nodes2(Rest,NRest,Inter,Out,IInter,IOut).
126		create_identifier_nodes3(TId,NTId,In,Out,IIn,IOut) :-
127		get_texpr_id(TId,Id),
128		get_texpr_type(TId,Type),
129		new_node_scope(Type,NodeId,Nodes),
130		avl_store(Id,In,nodes(NodeId,Nodes,rw),Out),
131		texpr_add_node_infos(TId,NodeId,NTId,IIn,IOut).
132
133		% look up the node of an identifier
134		identifier_node_lookup(Id,Env,NodeId,Nodes,Mode) :-
135		(avl_fetch(Id,Env,nodes(NodeId,Nodes,Mode)) -> true
136		; add_warning(kodkod,'Could not lookup identifier: ',Id),fail).
137
138		% set the complete environment to read-only,
139		% read-only nodes are not used for output of constraint nodes
140		identifier_nodes_readonly(OldEnv,NewEnv) :-
141		avl_map(set_readonly,OldEnv,NewEnv).
142		set_readonly(nodes(Id,Nodes,_Mode),nodes(Id,Nodes,ro)).
143
144		compute_integer_set('INTEGER',-inf,inf).
145		compute_integer_set('NATURAL',0,inf).
146		compute_integer_set('NATURAL1',1,inf).
147		compute_integer_set('INT',Min,Max) :-
148		get_preference(minint,Min),
149		get_preference(maxint,Max).
150		compute_integer_set('NAT',0,Max) :-
151		get_preference(maxint,Max).
152		compute_integer_set('NAT1',1,Max) :-
153		get_preference(maxint,Max).
154
155		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
156		% computation on information
157
158		info_conjunct(irange(X,Y),irange(A,B),Result) :-
159		Max infis max(X,A), Min infis min(Y,B),
160		normalise_irange(irange(Max,Min),Result).
161		info_disjunct(irange(X,Y),irange(A,B),Result) :-
162		( is_bottom(irange(X,Y)) -> Result = irange(A,B)
163		; is_bottom(irange(A,B)) -> Result = irange(X,Y)
164		; otherwise ->
165		Min infis min(X,A), Max infis max(Y,B),
166		normalise_irange(irange(Min,Max),Result)).
167
168		normalise_irange(In,Result) :-
169		( is_bottom(In) -> Result=irange(0,-1)
170		; otherwise -> 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,AM),irange(Bm,BM),irange(Cm,CM)) :-
213		% Cm infis min(Am,Bm), CM infis max(AM,BM).
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, assert(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).
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
530		; otherwise -> nth1(N,NodeList,Elem), nth1(N,NodeListRO,ElemRO)).
531		ignore_readonly_nodes([],[],[]).
532		ignore_readonly_nodes([Mode|MRest],[InNodes|InRest],[OutNodes|OutRest]) :-
533		ignore_readonly_nodes2(Mode,InNodes,OutNodes),
534		ignore_readonly_nodes(MRest,InRest,OutRest).
535		ignore_readonly_nodes2(ro,Nodes,Ignored) :- ignore_readonly_nodes3(Nodes,Ignored).
536		ignore_readonly_nodes2(rw,Nodes,Nodes).
537		ignore_readonly_nodes3([],[]).
538		ignore_readonly_nodes3([Scope:_Node|NRest],[Scope:ignored|IRest]) :-
539		ignore_readonly_nodes3(NRest,IRest).
540
541		nodes_for_general_sum_or_mult(Rule,TId,TPred,TExpr,TOrig,NodeEnv,Nodes,TNew,In,Out) :-
542		identifier_nodes_readonly(NodeEnv,SubEnv1),
543		create_identifier_nodes2([TId],[NTId],SubEnv1,SubEnv,In,Inter1),
544		extract_nodes_l([TId,TPred,TExpr],SubEnv,[IdNodes,_PredNodes,ExprNodes],_Modes,
545		[NTId,NTPred,NTExpr],Inter1,Inter2),
546		get_texpr_info(TOrig,Info),
547		memberchk(interval:ExprNodeId,ExprNodes),
548		memberchk(possible_values:IdId,IdNodes),
549		new_node_scope(integer,NodeId,Nodes),
550		add_node_infos(Info,NodeId,NInfo,Inter2,Inter3),
551		add_all([constraint([possible_values:IdId,interval:ExprNodeId],
552		[interval:NodeId],Rule)],
553		Inter3,Out),
554		get_texpr_expr(TOrig,OrigExpr),functor(OrigExpr,Functor,_),
555		NExpr =.. [Functor,[NTId],NTPred,NTExpr],
556		create_texpr(NExpr,integer,NInfo,TNew).
557
558		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
559		% extract constraints from syntax elements
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).
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).
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],gte).
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		; %otherwise ->
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		; %otherwise ->
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
743		; otherwise -> Constraints = []),
744		writetodot(Counter,[ChangedNode|CNRest],Constraints,In),
745		compute_constraints(Constraints,ChangedNodes1,[],In,Inter),
746		list_to_ord_set(ChangedNodes1,ChangedNodes),
747		ord_union(CNRest,ChangedNodes,NewChangedNodes),
748		Counter2 is Counter+1,
749		do_analysis(NewChangedNodes,Counter2,MaxIter,CTree,Inter,Out).
750		do_analysis(_ChangedNodes,Counter,MaxIter,_CTree,Values,Values) :-
751		Counter >= MaxIter.
752		compute_constraints([],Changed,Changed,Values,Values).
753		compute_constraints([Constraint|CRest],Cin,Cout,Vin,Vout) :-
754		compute_constraint(Constraint,Cin,Cinter,Vin,Vinter),
755		compute_constraints(CRest,Cinter,Cout,Vinter,Vout).
756		compute_constraint(constraint(Input,Output,Rule),Cin,Cout,Vin,Vout) :-
757		get_input_values(Input,Vin,InValues),
758		same_length(Output,OutValues),
759		call_rule(Rule,InValues,OutValues),
760		apply_output(Output,OutValues,Cin,Cout,Vin,Vout).
761		get_input_values([],_,[]).
762		get_input_values([Node|NRest],Values,[Value|VRest]) :-
763		avl_fetch(Node,Values,Value),
764		get_input_values(NRest,Values,VRest).
765		call_rule(Rule,InValues,OutValues) :-
766		append_arguments(Rule,InValues,CallRule),
767		if(rule(CallRule,OutValues), true,
768		(add_warning(predicate_analysis,'No rule for: ',CallRule),fail)).
769		apply_output([],[],Changed,Changed,Values,Values).
770		apply_output([Node|NRest],[Value|VRest],Cin,Cout,Vin,Vout) :-
771		( Node = _:ignored ->
772		Vin = Vinter, Cin=Cinter
773		; otherwise ->
774		avl_change(Node,Vin,OldValue,Vinter,NewValue),
775		info_conjunct(OldValue,Value,NewValue),
776		( has_more_information(NewValue,OldValue) ->
777		Cin = [Node|Cinter]
778		; otherwise ->
779		Cin = Cinter)),
780		apply_output(NRest,VRest,Cinter,Cout,Vinter,Vout).
781
782		append_arguments(Orig,Args,Result) :-
783		Orig =.. FA,
784		append_arguments2(FA,Args,AllArgs),
785		Result =.. AllArgs.
786		append_arguments2([F|FA],Args,AllArgs) :-
787		multi_rule(F),!,
788		append([F|FA],[Args],AllArgs).
789		append_arguments2(FA,Args,AllArgs) :-
790		append(FA,Args,AllArgs).
791
792
793		create_add_list_constraints([],_Result,Constraints) :- !,Constraints=[].
794		create_add_list_constraints([Node],Result,Constraints) :- !,
795		Constraints = [constraint([Node],[Result],id),constraint([Result],[Node],id)].
796		create_add_list_constraints(Nodes,Result,Constraints) :- !,
797		create_add_list_constraints2(Nodes,Result,Constraints,[]).
798		create_add_list_constraints2([A,B],Result) --> !,
799		findall(constraint(I,O,C),addition_constraint(A,B,Result,I,O,C)).
800		create_add_list_constraints2([A|Nodes],Result) -->
801		{new_node_scope(integer,NodeId,_Nodes)},
802		findall(constraint(I,O,C),addition_constraint(A,interval:NodeId,Result,I,O,C)),
803		create_add_list_constraints2(Nodes,interval:NodeId).
804
805
806
807		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
808		% compute a single constraint
809
810		rule(id(Info),[Info]).
811		rule(constant(Info),[Info]).
812		rule(add(A,B),[C]) :- interval_addition(A,B,C).
813		rule(sub(A,B),[C]) :- interval_subtraction(A,B,C).
814		rule(mult(A,B),[C]) :- interval_multiplication(A,B,C).
815		rule(power(Base,Exp),[Result]) :-
816		( power_rule(Base,Exp,Result) -> true
817		; otherwise -> Result = irange(-inf,inf)).
818		rule(cart_div(irange(Cm,CM),irange(Am,AM)),[irange(Bm,BM)]) :-
819		( CM = inf ->
820		BM = inf
821		; Am = 0 ->
822		BM = inf
823		; otherwise ->
824		BM infis (CM+Am-1) // Am),
825		( AM = 0 -> Bm = inf
826		; AM = inf -> Bm = inf
827		; otherwise ->
828		Bm infis Cm // AM).
829		rule(negate(A),[C]) :- interval_negation(A,C).
830		rule(lt(irange(_,AM)),[irange(-inf,CM)]) :- CM infis AM-1.
831		rule(lte(irange(_,AM)),[irange(-inf,AM)]).
832		rule(gt(irange(Am,_)),[irange(Cm,inf)]) :- Cm infis Am+1.
833		rule(gte(irange(Am,_)),[irange(Am,inf)]).
834		rule(interval_card(irange(Am,AM),irange(Bm,BM)),[irange(Cm,CM)]) :-
835		Cm infis max(Bm-AM+1,0), CM infis max(BM-Am+1,0).
836		rule(interval_possibilities(irange(Am,AM)),[irange(0,M)]) :-
837		M infis max(AM-Am+1,0).
838		rule(union([A|Rest]),[C]) :- union2(Rest,A,C).
839		rule(union([]),[irange(-inf,inf)]) :- print(empty_kodkod_union_constraint),nl. % TO DO: check if ok !!
840		% happens e.g., for set extensions like { min(0..7) } ; should not occur
841		rule(divrange(irange(Am,AM),irange(Bm,_BM)),[C]) :-
842		% rough approximation to division
843		( number(Bm),Bm>=0 ->
844		C = irange(Am,AM)
845		; number(Am),number(AM) ->
846		M is max(abs(Am),abs(AM)),
847		C = irange(-M,M)
848		; otherwise ->
849		C = irange(-inf,inf)).
850		rule(concat_index(irange(_,AM),irange(_,BM)),[irange(1,CM)]) :-
851		( number(AM),number(BM) -> CM is AM+BM
852		; otherwise -> CM = inf).
853
854
855		union2([],Acc,R) :- !,Acc=R.
856		union2([H|T],Acc,R) :- info_disjunct(H,Acc,I),union2(T,I,R).
857
858		power_rule(irange(Basem,BaseM),irange(Expm,ExpM),irange(Rm,RM)) :-
859		number(Basem),Basem > 0,
860		number(Expm),Expm >= 0,
861		Rm is floor( Basem ** Expm),
862		( (BaseM=inf; ExpM=inf) -> RM=inf
863		; otherwise -> RM is floor(BaseM ** ExpM)).
864
865		multi_rule(union).
866
867
868		insert_info(Infonodes,Values) :-
869		create_info_lookup_table(Values,ValueTable),
870		insert_info2(Infonodes,ValueTable).
871		insert_info2([],_).
872		insert_info2([infonode(Node,New,Old)|Rest],Values) :-
873		find_all_node_information(Node,Values,Info),
874		add_info(Info,Old,New),
875		insert_info2(Rest,Values).
876		find_all_node_information(Node,Values,Info) :-
877		( avl_member(Node,Values,RawInfos) -> filter_tops(RawInfos,Info)
878		; otherwise -> Info = []).
879		filter_tops([],[]).
880		filter_tops([Scope:RI|RRest],Result) :-
881		get_scope_top(Scope,Top),
882		( has_more_information(RI,Top) -> Result = [Scope:RI|RestResult]
883		; otherwise -> Result = RestResult),
884		filter_tops(RRest,RestResult).
885		add_info([],Old,Old) :- !.
886		add_info(Info,Old,[analysis(Info)|Old]).
887
888		create_info_lookup_table(Values,Nodes) :-
889		avl_to_list(Values,ValueList),
890		empty_avl(Empty),
891		create_info_lookup_table2(ValueList,Empty,Nodes).
892		create_info_lookup_table2([],Nodes,Nodes).
893		create_info_lookup_table2([(Scope:Node)-I|Rest],In,Out) :-
894		( avl_fetch(Node,In,Old) -> true
895		; otherwise -> Old = []),
896		avl_store(Node,In,[Scope:I|Old],Inter),
897		create_info_lookup_table2(Rest,Inter,Out).
898
899		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
900		% dot output
901
902		writetodot(Counter,ChangedNodes,ActiveConstraints,Values) :-
903		debugging_enabled,!,
904		debug_constraints(Constraints),
905		writetodot(Counter,Constraints,ChangedNodes,ActiveConstraints,Values).
906		writetodot(_Counter,_ChangedNodes,_ActiveConstraints,_Values).
907
908		writetodot(Counter,Constraints,ChangedNodes,ActiveConstraints,Values) :-
909		printnulls(3,Counter,CStr),
910		ajoin(['debug-constraint-anim/constraints-',CStr,'.dot'],Filename),
911		open(Filename,write,S),
912		write(S,'digraph constraints {\n'),
913		get_nodes(Constraints,INodes,CNodes),
914		write_inodes(INodes,ChangedNodes,Values,S),
915		write_cnodes(CNodes,INodes,ActiveConstraints,S),
916		write(S,'}\n'),
917		close(S).
918		get_nodes(Constraints,INodes,RNodes) :-
919		findall(CN,
920		(member(constraint(I,O,_),Constraints),
921		(member(CN,I);member(CN,O))),
922		Nodes1),
923		sort(Nodes1,Nodes2),
924		number_nodes(Nodes2,1,INodes),
925		number_nodes(Constraints,1,RNodes).
926		number_nodes([],_,[]).
927		number_nodes([N|Rest],Nr,[node(Nr,N)|RRest]) :-
928		Nr2 is Nr+1,
929		number_nodes(Rest,Nr2,RRest).
930		write_inodes([],_,_,_).
931		write_inodes([node(Nr,N)|Rest],ChangedNodes,Values,S) :-
932		write(S,' i'),write(S,Nr),write(S,'[shape=box,'),
933		( ChangedNodes = [N|_] ->
934		!,write(S,'fillcolor=green,style=filled,')
935		; member(N,ChangedNodes) ->
936		!,write(S,'fillcolor=yellow,style=filled,')
937		; otherwise -> true),
938		write(S,'label=\"'),
939		write(S,N),write(S,'\\n'),
940		( debug_node(N,TExpr) ->
941		translate_bexpression(TExpr,Text)
942		; otherwise ->
943		Text = ('?')),
944		write(S,Text),write(S,'\\n'),
945		( avl_fetch(N,Values,Value) ->
946		write(S,Value)
947		; otherwise -> write(S,'?')),
948		write(S,'\"];\n'),
949		write_inodes(Rest,ChangedNodes,Values,S).
950		write_cnodes([],_,_,_).
951		write_cnodes([node(Nr,constraint(In,Out,R))|Rest],INodes,ActiveConstraints,S) :-
952		write(S,' c'),write(S,Nr),write(S,'[shape=diamond,'),
953		( member(constraint(In,Out,R),ActiveConstraints) ->
954		!,write(S,'fillcolor=lightblue,style=filled,')
955		; otherwise -> true),
956		write(S,'label=\"'),
957		write(S,R),write(S,'\"];\n'),
958		write_inputs(In,INodes,Nr,S),
959		write_outputs(Out,INodes,Nr,S),
960		write_cnodes(Rest,INodes,ActiveConstraints,S).
961		write_inputs([],_,_,_).
962		write_inputs([I|Rest],INodes,RNr,S) :-
963		member(node(INr,I),INodes),!,
964		write(S,' i'),write(S,INr),write(S,' -> '),
965		write(S,' c'),write(S,RNr),write(S,';\n'),
966		write_inputs(Rest,INodes,RNr,S).
967		write_outputs([],_,_,_).
968		write_outputs([O|Rest],INodes,RNr,S) :-
969		member(node(ONr,O),INodes),!,
970		write(S,' c'),write(S,RNr),write(S,' -> '),
971		write(S,' i'),write(S,ONr),write(S,';\n'),
972		write_outputs(Rest,INodes,RNr,S).
973
974		printnulls(N,Number,Str) :-
975		number_codes(Number,NCodes),
976		length(NCodes,L),
977		R is N-L,
978		fillnulls(R,NCodes,Codes),
979		atom_codes(Str,Codes).
980		fillnulls(R,Codes,Codes) :- R =< 0,!.
981		fillnulls(R,NCodes,[48|Codes]) :-
982		R2 is R-1,
983		fillnulls(R2,NCodes,Codes).
984
985
986		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
987
988		:- dynamic debug_predicate_analysis/0.
989		% assert this fact to enable dot visualization using writetodot below
990
991		store_debug_info(I,T) :- debug_predicate_analysis,!,store_debug_info2(I,T).
992		store_debug_info(_,_).
993
994		store_debug_info2([],_).
995		store_debug_info2([Node|Rest],TExpr) :-
996		assert(debug_node(Node,TExpr)),
997		store_debug_info2(Rest,TExpr).
998
999
1000		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1001		% test case specification for predicate analysis
1002
1003		:- use_module(junit_tests).
1004
1005		test_predicate_analysis :-
1006		b_machine_has_constants,
1007		b_get_machine_constants(Constants),
1008		b_get_properties_from_machine(Properties),
1009		b_get_static_assertions_from_machine(Assertions),
1010		Assertions = [_|_],!,
1011		test_predicate_analysis2(Constants,Properties,Assertions,Junits),
1012		print_junit(Junits,predicate_analysis).
1013		test_predicate_analysis :-
1014		add_error(predicate_analysis,
1015		'Machine must have constants and assertions to be a valid predicate analysis test case.'),
1016		fail.
1017		test_predicate_analysis2(Constants,Properties,Assertions,Junits) :-
1018		predicate_analysis_with_global_sets(Properties,[],Constants,TaggedConstants,_TaggedProperties),!,
1019		test_predicate_analysis3(Assertions,TaggedConstants,Junits).
1020		test_predicate_analysis2(_,_,_,[Junit]) :-
1021		in_junit_mode,!,
1022		pa_junit(setup,error('Predicate analysis failed'),Junit).
1023		test_predicate_analysis2(_,_,_,_) :-
1024		add_error(predicate_analysis, 'Predicate analysis of properties failed'),
1025		fail.
1026		test_predicate_analysis3([],_Constants,[]).
1027		test_predicate_analysis3([Assertion|Arest],Constants,[Junit|Jrest]) :-
1028		test_predicate_analysis_testcase(Assertion,Constants,Junit),
1029		test_predicate_analysis3(Arest,Constants,Jrest).
1030
1031		test_predicate_analysis_testcase(TAssertion,Constants,Junit) :-
1032		translate_bexpression(TAssertion,Name),
1033		( catch( ( test_predicate_analysis_testcase1(TAssertion,Constants),
1034		pa_junit(Name,pass,Junit)),
1035		junit(Msg),
1036		handle_error(Name,Msg,Junit)) -> true
1037		; otherwise ->
1038		pa_junit(Name,error('Test failed.'),Junit)).
1039		handle_error(Name,Msg,Junit) :-
1040		in_junit_mode,!,
1041		pa_junit(Name,error(Msg),Junit).
1042		handle_error(Name,Msg,_Junit) :-
1043		add_error(predicate_analysis, Name, Msg), fail.
1044
1045		test_predicate_analysis_testcase1(TAssertion,Constants) :-
1046		extract_predicate_analysis_testcases(TAssertion,[],Testcases),
1047		maplist(run_testcase(Constants),Testcases).
1048		run_testcase(Constants,pa_testcase(Id,Scope,ExpectedValue)) :-
1049		format('Predicate analysis testcase: check if "~w" of "~w" is ~w~N', [Scope,Id,ExpectedValue]),
1050		expected_value_is_top(ExpectedValue,Scope,IsTop),
1051		extract_analysis(Id,Constants,Scope,FoundValue,IsTop),
1052		( FoundValue == ExpectedValue -> true
1053		; otherwise ->
1054		ajoin(['unexpected information for constant ',Id,': expected ', ExpectedValue,
1055		', but was ', FoundValue],Msg),
1056		throw(junit(Msg))).
1057		expected_value_is_top(ExpectedValue,Scope,true) :-
1058		ground(ExpectedValue),get_scope_top(Scope,ExpectedValue),!.
1059		expected_value_is_top(_ExpectedValue,_Scope,false).
1060
1061		extract_predicate_analysis_testcases(TExpr,QRefs,Testcases) :-
1062		get_texpr_expr(TExpr,Expr),
1063		extract_predicate_analysis_testcases2(Expr,QRefs,Testcases).
1064		extract_predicate_analysis_testcases2(forall(Ids,TPre,Cond),QRefs,Testcases) :-
1065		get_texpr_expr(TPre,Pre),introduce_qrefs(Pre,Ids,QRefs,SubQRefs),
1066		extract_predicate_analysis_testcases(Cond,SubQRefs,Testcases).
1067		extract_predicate_analysis_testcases2(equal(Ref,Spec),QRefs,[pa_testcase(Constant,Scope,irange(Value,Value))]) :- !,
1068		extract_test_reference(Ref,QRefs,Constant,Scope),
1069		extract_integer(Spec,Value).
1070		extract_predicate_analysis_testcases2(less_equal(Ref,Spec),QRefs,[pa_testcase(Constant,Scope,irange(-inf,Value))]) :- !,
1071		extract_test_reference(Ref,QRefs,Constant,Scope),
1072		extract_integer(Spec,Value).
1073		extract_predicate_analysis_testcases2(greater_equal(Ref,Spec),QRefs,[pa_testcase(Constant,Scope,irange(Value,inf))]) :- !,
1074		extract_test_reference(Ref,QRefs,Constant,Scope),
1075		extract_integer(Spec,Value).
1076		extract_predicate_analysis_testcases2(member(Ref,TSpec),QRefs,[pa_testcase(Constant,Scope,Info)]) :-
1077		get_texpr_expr(TSpec,Spec),
1078		extract_test_reference(Ref,QRefs,Constant,Scope),
1079		integer_interval_membership(Spec,Scope,Info),!.
1080		extract_predicate_analysis_testcases2(not_member(Ref,TSpec),QRefs,[pa_testcase(Constant,Scope,Top)]) :-
1081		get_texpr_expr(TSpec,empty_set),
1082		extract_test_reference(Ref,QRefs,Constant,Scope),
1083		get_scope_top(Scope,Top).
1084		extract_predicate_analysis_testcases2(conjunct(A,B),QRefs,Testcases) :- !,
1085		extract_predicate_analysis_testcases(A,QRefs,TestcasesA),
1086		extract_predicate_analysis_testcases(B,QRefs,TestcasesB),
1087		append(TestcasesA,TestcasesB,Testcases).
1088		extract_predicate_analysis_testcases2(_Expr,_QRefs,_Testcases) :-
1089		throw(junit('Unsupported test case pattern')).
1090
1091		integer_interval_membership(empty_set,Scope,Bottom) :- get_scope_bottom(Scope,Bottom).
1092		integer_interval_membership(interval(Min,Max),_Scope,irange(VMin,VMax)) :-
1093		extract_integer(Min,VMin),extract_integer(Max,VMax).
1094		integer_interval_membership(integer_set(I),_Scope,irange(Min,Max)) :-
1095		compute_integer_set(I,Min,Max).
1096
1097		introduce_qrefs(member(E2,Ref),Ids,QRefs,NewQRefs) :-
1098		lookup_ref(Ref,QRefs,Path,Constant),append(Path,[elem],Path2),
1099		couple_pathes(E2,Path2,Constant,Ids,NewQRefs,QRefs).
1100		introduce_qrefs(equal(E2,Ref),Ids,QRefs,NewQRefs) :-
1101		lookup_ref(Ref,QRefs,Path,Constant),
1102		couple_pathes(E2,Path,Constant,Ids,NewQRefs,QRefs).
1103
1104		couple_pathes(TExpr,Path,Constant,TIdentifiers) -->
1105		{get_texpr_ids(TIdentifiers,Identifiers)},
1106		couple_pathes2(TExpr,Path,Constant,Identifiers).
1107		couple_pathes2(TExpr,Path,Constant,Identifiers) -->
1108		{get_texpr_expr(TExpr,Expr)},couple_pathes3(Expr,TExpr,Path,Constant,Identifiers).
1109		couple_pathes3(identifier(Id),_,Path,Constant,Identifiers) -->
1110		{memberchk(Id,Identifiers),!},[Id-ref(Path,Constant)].
1111		couple_pathes3(couple(A,B),_,Path,Constant,Identifiers) --> !,
1112		{append(Path,[left],PathA),append(Path,[right],PathB)},
1113		couple_pathes2(A,PathA,Constant,Identifiers),
1114		couple_pathes2(B,PathB,Constant,Identifiers).
1115		couple_pathes3(_,TExpr,_Path,_Constant,_Identifiers,_,_) :-
1116		translate_bexpression(TExpr,String),
1117		atom_concat('Expected quantified identifier or couple in test specification, but was: ',
1118		String,Msg),
1119		throw(junit(Msg)).
1120
1121
1122		lookup_ref(Expr,QRefs,Path,Constant) :-
1123		get_texpr_id(Expr,Id),
1124		memberchk(Id-ref(Path1,Constant1),QRefs),!,
1125		Path1=Path,Constant1=Constant.
1126		lookup_ref(Expr,_QRefs,[],Id) :-
1127		get_texpr_id(Expr,Id).
1128
1129		extract_analysis(Id,Constants,Scope,FoundValue,IsTop) :-
1130		get_texpr_id(Constant,Id),
1131		( memberchk(Constant,Constants) ->
1132		get_texpr_info(Constant,Info),
1133		( memberchk(analysis(Analysis),Info) -> true
1134		; otherwise -> Analysis=[]),
1135		( memberchk(Scope:FoundValue,Analysis) -> true
1136		; IsTop == true -> get_scope_top(Scope,FoundValue) /* no information expected */
1137		; otherwise ->
1138		ajoin(['No analysis information found for constant ',Id,', scope ',Scope],Msg),
1139		print(extract_analysis(Id,Constants,Scope,FoundValue,IsTop)),nl,
1140		throw(junit(Msg)))
1141		; otherwise ->
1142		ajoin(['Constant ',Id,' not found'],Msg),
1143		throw(junit(Msg))).
1144
1145		extract_test_reference(TRef,QRefs,Id,Scope) :-
1146		get_texpr_expr(TRef,Ref),
1147		extract_test_reference2(Ref,QRefs,BaseScope,Id,ScopeList),
1148		construct_scope(ScopeList,BaseScope,Scope),!.
1149		extract_test_reference(TRef,_QRefs,_Id,_Scope) :-
1150		translate_bexpression(TRef,String),
1151		atom_concat('Unsupported reference on left side: ', String,Msg),
1152		throw(junit(Msg)).
1153		extract_test_reference2(card(TRef),QRefs,card,Id,Scope) :-
1154		!,get_texpr_expr(TRef,Ref),Ref=identifier(_),
1155		extract_test_reference2(Ref,QRefs,_,Id,Scope).
1156		extract_test_reference2(identifier(Id),QRefs,interval,Constant,Scope) :-
1157		memberchk(Id-ref(Scope,Constant),QRefs),!.
1158		extract_test_reference2(identifier(Id),_QRefs,interval,Id,[]) :- !.
1159
1160
1161		:- assert_must_succeed(( construct_scope([elem,right],interval,S),
1162		S==elem(right(interval)) )).
1163		construct_scope([],Scope,Scope).
1164		construct_scope([F|Rest],Base,Scope) :-
1165		functor(Scope,F,1),arg(1,Scope,Subscope),
1166		construct_scope(Rest,Base,Subscope).
1167
1168		extract_integer(Spec,Value) :-
1169		( get_texpr_expr(Spec,integer(Value)) -> true
1170		; get_texpr_expr(Spec,unary_minus(Spec2)) ->
1171		extract_integer(Spec2,Value2),Value is -Value2
1172		; otherwise ->
1173		throw(junit('Integer value expected in right side of assertion'))).
1174
1175		in_junit_mode :-
1176		junit_mode(_),!.
1177
1178		pa_junit(Name,Verdict,Junit) :-
1179		b_machine_name(MachineName),
1180		create_junit_result(Name,predicate_analysis,MachineName,0,Verdict,Junit).