1 :- module(kodkod_annotator, [annotate_kodkod_constraints/3,
2 contains_higher_order_or_int_ast/1,
3 preferred_by_kodkod/1]).
4
5 :- use_module(probsrc(bsyntaxtree), [find_typed_identifier_uses/3, get_texpr_type/2]).
6
7 :- use_module(probsrc(module_information),[module_info/2]).
8 :- module_info(group,kodkod).
9 :- module_info(description,'Annotate specific constraints within a typed B or Event-B AST with external predicate calls to be solved by Kodkod.').
10
11 %% join_using_couples(+Ids, -Couples).
12 %
13 % Join a non-empty list of identifiers to a single (possibly nested) couple.
14 join_using_couples([Id|T], Couples) :-
15 join_using_couples(T, Id, Couples).
16
17 join_using_couples([], Couples, Couples).
18 join_using_couples([Id|T], Acc, Couples) :-
19 get_texpr_type(Id, Type1),
20 get_texpr_type(Acc, Type2),
21 NewAcc = b(couple(Id, Acc), couple(Type1, Type2), []),
22 join_using_couples(T, NewAcc, Couples).
23
24 %% annotate_kodkod_constraints(+AnnotationType, +Ast, -AnnotatedAst).
25 %
26 % AnnotationType is either 'greedy' (send all possible constraints to Kodkod) or
27 % 'preferred' (only send preferred constraints to Kodkod, see preferred_by_kodkod/1).
28 % Annotate specific constraints to be solved by Kodkod.
29 % Currently preferred by Kodkod: implication, equal, not_equal, card
30 % Exclude: Operations on integers and higher-order quantification.
31 annotate_kodkod_constraints(_, Ast, AnnotatedAst) :-
32 Ast = b(kodkod(_,_),_,_),
33 !,
34 AnnotatedAst = Ast.
35 annotate_kodkod_constraints(AnnotationType, Ast, AnnotatedAst) :-
36 annotate_kodkod_constraints(AnnotationType, Ast, [], NewVarsAcc, TAnnotatedAst),
37 NewVarsAcc = [CoupledVars],
38 EmptySet = b(empty_set,set(any),[]),
39 KodkodSolve = b(external_pred_call('KODKOD_SOLVE',[b(integer(1),integer,[]), CoupledVars, EmptySet]),pred,[]),
40 AnnotatedAst = b(conjunct(TAnnotatedAst, KodkodSolve),pred,[]).
41 annotate_kodkod_constraints(_, Ast, Ast).
42
43 %% annotate_kodkod_constraints(AnnotationType, +Ast, +VarsAcc, -NewVarsAcc, -AnnotatedAst).
44 %
45 % AnnotationType is either greedy (use Kodkod wherever possible)
46 % or preferred (see preferred_by_kodkod/1).
47 % True if NewVarsAcc is a singleton list containing a couple of local identifiers of annotated constraints,
48 % and AnnotatedAst the equivalent ast with Kodkod annotations.
49 annotate_kodkod_constraints(greedy, b(Node,Type,Info), VarsAcc, NewVarsAcc, AnnotatedAst) :-
50 functor(Node, _, Arity),
51 Arity == 2,
52 arg(1, Node, Lhs),
53 arg(2, Node, Rhs),
54 \+contains_higher_order_or_int_ast([Lhs]),
55 \+contains_higher_order_or_int_ast([Rhs]),
56 !,
57 annotate_constraint_for_kodkod(b(Node,Type,Info), VarsAcc, NewVarsAcc, AnnotatedAst).
58 annotate_kodkod_constraints(preferred, b(Node,Type,Info), VarsAcc, NewVarsAcc, AnnotatedAst) :-
59 functor(Node, Functor, _),
60 preferred_by_kodkod(Functor),
61 !,
62 annotate_constraint_for_kodkod(b(Node,Type,Info), VarsAcc, NewVarsAcc, AnnotatedAst).
63 annotate_kodkod_constraints(AnnotationType, b(Node,Type,Info), VarsAcc, NewVarsAcc, AnnotatedAst) :-
64 functor(Node, Functor, Arity),
65 Arity == 2,
66 arg(1, Node, Lhs),
67 arg(2, Node, Rhs),
68 !,
69 annotate_kodkod_constraints(AnnotationType, Lhs, VarsAcc, VarsAcc1, ALhs),
70 annotate_kodkod_constraints(AnnotationType, Rhs, VarsAcc1, NewVarsAcc, ARhs),
71 NNode =.. [Functor, ALhs, ARhs],
72 AnnotatedAst = b(NNode,Type,Info).
73 annotate_kodkod_constraints(greedy, b(forall(Ids, Lhs, Rhs),pred,Info), VarsAcc, NewVarsAcc, AnnotatedAst) :-
74 \+contains_higher_order_or_int_ast([Ids]),
75 \+contains_higher_order_or_int_ast([Lhs]),
76 \+contains_higher_order_or_int_ast([Rhs]),
77 !,
78 annotate_kodkod_constraints(greedy, Lhs, VarsAcc, VarsAcc1, ALhs),
79 annotate_kodkod_constraints(greedy, Rhs, VarsAcc1, NewVarsAcc, ARhs),
80 AnnotatedAst = b(forall(Ids, ALhs, ARhs),pred,Info).
81 annotate_kodkod_constraints(greedy, b(exists(Ids, Pred),pred,Info), VarsAcc, NewVarsAcc, AnnotatedAst) :-
82 \+contains_higher_order_or_int_ast([Ids]),
83 \+contains_higher_order_or_int_ast([Pred]),
84 !,
85 annotate_kodkod_constraints(greedy, Pred, VarsAcc, NewVarsAcc, APred),
86 AnnotatedAst = b(exists(Ids, APred),pred,Info).
87 % Note: skips let etc. if on the top-level
88 annotate_kodkod_constraints(_, Ast, VarsAcc, VarsAcc, Ast).
89
90 annotate_constraint_for_kodkod(Ast, VarsAcc, [CoupledVars], AnnotatedAst) :-
91 AstAsBool = b(convert_bool(Ast),boolean,[]),
92 find_typed_identifier_uses(Ast, [], LocalIds),
93 join_using_couples(LocalIds, CoupledLocalIds),
94 join_using_couples([CoupledLocalIds|VarsAcc], CoupledVars),
95 EmptySet = b(empty_set,set(any),[]),
96 AnnotatedAst = b(external_pred_call('KODKOD',[b(integer(1),integer,[]), CoupledLocalIds, EmptySet, AstAsBool]),pred,[]).
97
98 %% contains_higher_order_or_int_ast(+ListOfAst).
99 %
100 % True if list contains an ast of type integer or a higher order quantification.
101 contains_higher_order_or_int_ast([b(Node,Type,Info)|_]) :-
102 get_texpr_type(b(Node,Type,Info), Type),
103 ( Type == integer
104 ; Type = set(A),
105 set_or_seq(A)
106 ; Type = seq(A),
107 set_or_seq(A)
108 ),
109 !.
110 contains_higher_order_or_int_ast([Ast|T]) :-
111 Ast =.. [_|Args],
112 ( contains_higher_order_or_int_ast(Args),
113 !
114 ; contains_higher_order_or_int_ast(T)).
115
116 set_or_seq(set(_)).
117 set_or_seq(seq(_)).
118
119 % TO DO: find more suitable operators for Kodkod annotations
120 preferred_by_kodkod(equal).
121 preferred_by_kodkod(not_equal).
122 preferred_by_kodkod(not_member).
123 preferred_by_kodkod(member).
124 preferred_by_kodkod(subset).
125 preferred_by_kodkod(not_subset).
126 preferred_by_kodkod(subset_strict).
127 preferred_by_kodkod(not_subset_strict).
128 preferred_by_kodkod(exists).
129 preferred_by_kodkod(forall).
130 preferred_by_kodkod(pow_subset).
131 preferred_by_kodkod(pow1_subset).
132 preferred_by_kodkod(fin_subset).
133 preferred_by_kodkod(fin1_subset).