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(probsrc(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		; otherwise ->
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(TExpr) :-
58		get_texpr_info(TExpr,Info),
59		memberchk(analysis(Analysis),Info),
60		member(_:IRange,Analysis),
61		is_inconsistent_intrange(IRange),!.
62
63		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
64		% unique identifier
65		:- dynamic unique_counter/1, debug_identifier/0.
66
67
68		unique_identifier(Prefix,Name,Id) :-
69		( debug_identifier ->
70		increase_counter(C),
71		ajoin([Prefix,C,'_',Name],Id)
72		; otherwise ->
73		unique_identifier(Prefix,Id)).
74		unique_identifier(Prefix,Id) :-
75		increase_counter(C),
76		ajoin([Prefix,C],Id).
77		unique_identifier(Id) :-
78		unique_identifier(tmpid__,Id).
79		increase_counter(C2) :-
80		( retract(unique_counter(C)) -> true; C=0 ),
81		C2 is C+1,
82		assert(unique_counter(C2)).
83
84		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
85		% merge two integer ranges
86		merge_integer_info(none,A,A) :- !.
87		merge_integer_info(A,none,A) :- !.
88		merge_integer_info(IRangeA,IRangeB,IRange) :-
89		info_disjunct(IRangeA,IRangeB,IRange).
90
91
92		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
93		% combining Kodkod expressions
94
95		kodkod_conjunction(List,Result) :-
96		findall(E,(member(E,List),E \= true),L2),
97		kodkod_conjunction2(L2,Result).
98		kodkod_conjunction2([],true).
99		kodkod_conjunction2([F],F) :- !.
100		kodkod_conjunction2([A,B|R],and(A,F)) :- kodkod_conjunction2([B|R],F).
101
102		kodkod_implication(true,Formula,Formula) :- !.
103		kodkod_implication(false,_,true) :- !.
104		kodkod_implication(F1,F2,implies(F1,F2)).
105
106		disassemble_conjunction(Formula,Result) :-
107		disassemble_conjunction2(Formula,Result,[]),!.
108		disassemble_conjunction2(and(A,B)) -->
109		disassemble_conjunction2(A),
110		disassemble_conjunction2(B).
111		disassemble_conjunction2(X) --> {X\=and(_,_)},[X].