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]. |