1		:- module(kodkod_tools,[ extract_finite_integer_range/3
2		, unique_identifier/1
3		, unique_identifier/2
4		, unique_identifier/3
5		, merge_integer_info/3
6		, kodkod_conjunction/2
7		, kodkod_implication/3
8		, disassemble_conjunction/2
9
10		, pow2integer_relation_kodkod_name/1
11		, intset_relation_kodkod_name/1
12
13		, is_inconsistent_expression/1
14		]).
15
16		:- use_module(probsrc(tools), [ajoin/2]).
17		:- use_module(probsrc(module_information)).
18		:- use_module(probsrc(translate), [translate_bexpression/2]).
19		:- use_module(probsrc(bsyntaxtree)).
20		:- use_module(predicate_analysis, [info_disjunct/3]).
21
22		:- module_info(group,kodkod).
23		:- module_info(description,'This module contains helper predicates for the Kodkod translation part of ProB').
24
25		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
26		% constants
27		pow2integer_relation_kodkod_name(p2i).
28		intset_relation_kodkod_name(is).
29
30		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
31		% helper to extract the integer range of a type expression
32		extract_finite_integer_range(TExpr,ScopeList,IRange) :-
33		convert_scopelist_to_scope(ScopeList,interval,Scope),
34		extract_finite_integer_range2(TExpr,Scope,IRange).
35		convert_scopelist_to_scope([],Scope,Scope).
36		convert_scopelist_to_scope([Access|Rest],OScope,Scope) :-
37		functor(NScope,Access,1),arg(1,NScope,OScope),
38		convert_scopelist_to_scope(Rest,NScope,Scope).
39		extract_finite_integer_range2(TExpr,Scope,IRange) :-
40		get_texpr_info(TExpr,Info),
41		memberchk(analysis(Analysis),Info),
42		memberchk(Scope:IRange0,Analysis),
43		( is_inconsistent_intrange(IRange0) ->
44		IRange = irange(0,0) % throwing an exception is not really sensible, e.g.
45		% if we have an inconsistent range of a variable in a
46		% comprehension set - then the set would just be empty
47		% We can safely(?) assume a larger range (here 0..0)
48		;
49		is_finite(IRange0),IRange0=IRange),!.
50		extract_finite_integer_range2(TExpr,_Scope,_IRange) :-
51		translate_bexpression(TExpr,SExpr),
52		ajoin(['integer without upper and lower bound in: ', SExpr], Msg),
53		throw(kodkod(unsupported_int(Msg))).
54		is_finite(irange(Min,Max)) :- number(Min),number(Max).
55		is_inconsistent_intrange(irange(Min,Max)) :-
56		number(Min),number(Max),Max < Min.
57		is_inconsistent_expression(b(E,_,Info)) :-
58		memberchk(analysis(Analysis),Info),
59	?	member(Type:IRange,Analysis), % elem(interval)
60		Type \= elem(_), % otherwise, e.g., for elem(interval) we talk about possible elements, an inconsistency here simply means that the set is empty
61		is_inconsistent_intrange(IRange),!,
62		debug:debug_println(19,inconsistent_range(E,IRange)).
63
64		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
65		% unique identifier
66		:- dynamic unique_counter/1, debug_identifier/0.
67
68
69		unique_identifier(Prefix,Name,Id) :-
70		( debug_identifier ->
71		increase_counter(C),
72		ajoin([Prefix,C,'_',Name],Id)
73		;
74		unique_identifier(Prefix,Id)).
75		unique_identifier(Prefix,Id) :-
76		increase_counter(C),
77		ajoin([Prefix,C],Id).
78		unique_identifier(Id) :-
79		unique_identifier(tmpid__,Id).
80		increase_counter(C2) :-
81		( retract(unique_counter(C)) -> true; C=0 ),
82		C2 is C+1,
83		assertz(unique_counter(C2)).
84
85		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
86		% merge two integer ranges
87		merge_integer_info(none,A,A) :- !.
88		merge_integer_info(A,none,A) :- !.
89		merge_integer_info(IRangeA,IRangeB,IRange) :-
90		info_disjunct(IRangeA,IRangeB,IRange).
91
92
93		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
94		% combining Kodkod expressions
95
96		kodkod_conjunction(List,Result) :-
97		findall(E,(member(E,List),E \= true),L2),
98		kodkod_conjunction2(L2,Result).
99		kodkod_conjunction2([],true).
100		kodkod_conjunction2([F],F) :- !.
101		kodkod_conjunction2([A,B|R],and(A,F)) :- kodkod_conjunction2([B|R],F).
102
103		kodkod_implication(true,Formula,Formula) :- !.
104		kodkod_implication(false,_,true) :- !.
105		kodkod_implication(F1,F2,implies(F1,F2)).
106
107		disassemble_conjunction(Formula,Result) :-
108	?	disassemble_conjunction2(Formula,Result,[]),!.
109		disassemble_conjunction2(and(A,B)) -->
110	?	disassemble_conjunction2(A),
111	?	disassemble_conjunction2(B).
112		disassemble_conjunction2(X) --> {X\=and(_,_)},[X].