1 | % (c) 2009-2022 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 | :- module(kodkod_printer,[kkp_problem/6 | |
6 | ,kkp_request/5 | |
7 | ,kkp_list/3]). | |
8 | ||
9 | :- use_module(library(lists)). | |
10 | ||
11 | :- use_module(probsrc(module_information),[module_info/2]). | |
12 | :- use_module(probsrc(tools),[print_message/1]). | |
13 | ||
14 | :- module_info(group,kodkod). | |
15 | :- module_info(description,'This module contains code to print the description of a Kodkod problem, used to send it to a seperate process.'). | |
16 | ||
17 | :- dynamic output_stream/1. | |
18 | ||
19 | set_stream(Stream) :- | |
20 | retractall(output_stream(_)), | |
21 | assertz(output_stream(Stream)). | |
22 | ||
23 | kkp_problem(Stream,Timeout,Symmetry,Solver,Id,P) :- | |
24 | set_stream(Stream), | |
25 | call_cleanup( (kkp_problem2(Timeout,Symmetry,Solver,Id,P),!), retractall(output_stream(_)) ). | |
26 | kkp_problem2(Timeout,Symmetry,Solver,Id,problem(Types,Relations,Formula,_,_IntRange)) :- | |
27 | problem_id(Id,PID), | |
28 | kprint([t('problem '),id(PID),space,t(Timeout),space,t(Symmetry),space,t(Solver)]), | |
29 | % will output something like "problem p2 2500 0 sat4j" | |
30 | kkp_types(Types), | |
31 | kkp_relations(Relations), | |
32 | kkp_formula(Formula), | |
33 | kprint(stop). | |
34 | ||
35 | kkp_types(Types) :- kprint(popen), kkp_types2(Types), kprint(pclose). | |
36 | kkp_types2([]). | |
37 | kkp_types2([Type|TRest]) :- kkp_type(Type), kkp_types2(TRest). | |
38 | kkp_type(type(Id,Size)) :- kprint([popen,id(Id),space,t(Size),pclose]). | |
39 | % TODO: Maybe it would be better to convert the problem to "falsity" instead | |
40 | kkp_type(inttype(PowName,PowMin,PowMax)) :- | |
41 | PowMax<PowMin,!, | |
42 | print_message('Translation to Kodkod: Inconsistent integer range: Relaxing to avoid exceptions'), | |
43 | kkp_type(inttype(PowName,PowMin,PowMin)). % relax in | |
44 | kkp_type(inttype(PowName,PowMin,PowMax)) :- | |
45 | kkp_inttype_part1(PowName,PowMin,PowMax),kkp_inttype_part2. | |
46 | kkp_type(inttype(PowName,PowMin,PowMax,IntsetName,Min,Max)) :- | |
47 | PowMax<PowMin,!, | |
48 | print_message('Translation to Kodkod: Inconsistent integer range: Relaxing to avoid exceptions'), | |
49 | kkp_type(inttype(PowName,PowMin,PowMin,IntsetName,Min,Max)). | |
50 | kkp_type(inttype(PowName,PowMin,PowMax,IntsetName,Min,Max)) :- | |
51 | Max<Min,!, | |
52 | print_message('Translation to Kodkod: Inconsistent integer range: Relaxing to avoid exceptions'), | |
53 | kkp_type(inttype(PowName,PowMin,PowMax,IntsetName,Min,Min)). | |
54 | kkp_type(inttype(PowName,PowMin,PowMax,IntsetName,Min,Max)) :- | |
55 | kkp_inttype_part1(PowName,PowMin,PowMax), | |
56 | kprint([popen,id(IntsetName),space,t(Min),space,t(Max),pclose]), | |
57 | kkp_inttype_part2. | |
58 | kkp_inttype_part1(PowName,PowMin,PowMax) :- | |
59 | kprint([popen,t(inttype),popen,id(PowName),space,t(PowMin),space,t(PowMax),pclose]). | |
60 | kkp_inttype_part2 :- | |
61 | kprint(pclose). | |
62 | ||
63 | kkp_relations(Relations) :- | |
64 | kprint(popen), kkp_relations2(Relations), kprint(pclose). | |
65 | kkp_relations2([]). | |
66 | kkp_relations2([Rel|Rrest]) :- | |
67 | kkp_relation(Rel), kkp_relations2(Rrest). | |
68 | kkp_relation(reldef(Id,Types,SetOrSingleton,SubsetExact,Set)) :- | |
69 | kprint([popen,id(Id),space]), | |
70 | ( SetOrSingleton==single -> kprint(t('singleton ')); true), | |
71 | kprint([t(SubsetExact)]),kkp_typerefs(Types), | |
72 | kkp_tupleset(Set), | |
73 | kprint(pclose). | |
74 | kkp_typerefs([]). | |
75 | kkp_typerefs([Type|Trest]) :- | |
76 | kprint([space,t(Type)]), | |
77 | kkp_typerefs(Trest). | |
78 | kkp_tupleset(full) :- !. | |
79 | kkp_tupleset(TupleSet) :- is_list(TupleSet),!, | |
80 | kprint(popen),kkp_tupleset2(TupleSet),kprint(pclose). | |
81 | kkp_tupleset2([]). | |
82 | kkp_tupleset2([tuple(Tuple)|Trest]) :- | |
83 | kprint(tuple(Tuple)),kkp_tupleset2(Trest). | |
84 | ||
85 | kkp_formula(F) :- kprint(popen), kkp_formula2(F), kprint(pclose). | |
86 | kkp_formula2(true) :- !,kprint(t(true)). | |
87 | kkp_formula2(false) :- !,kprint(t(false)). | |
88 | kkp_formula2(one(E)) :- !,kkp_formula_mult(one, E). | |
89 | kkp_formula2(some(E)) :- !,kkp_formula_mult(some,E). | |
90 | kkp_formula2(no(E)) :- !,kkp_formula_mult(no, E). | |
91 | kkp_formula2(lone(E)) :- !,kkp_formula_mult(lone,E). | |
92 | kkp_formula2(set(E)) :- !,kkp_formula_mult(set, E). | |
93 | kkp_formula2(in(A,B)) :- !,kkp_opexpr(in,[A,B]). | |
94 | kkp_formula2(equals(A,B)) :- !,kkp_opexpr(equals,[A,B]). | |
95 | kkp_formula2(not(F)) :- !,kkp_opform(not,[F]). | |
96 | kkp_formula2(and(A,B)) :- !,flatten_subformulas(and(A,B),Args), kkp_opform(and,Args). | |
97 | kkp_formula2(or(A,B)) :- !,kkp_opform(or, [A,B]). | |
98 | kkp_formula2(implies(A,B)) :- !,kkp_opform(implies,[A,B]). | |
99 | kkp_formula2(iff(A,B)) :- !,kkp_opform(iff,[A,B]). | |
100 | kkp_formula2(forall(Decls,Formula)) :- !,kkp_quantifier(all, Decls, Formula). | |
101 | kkp_formula2(exists(Decls,Formula)) :- !,kkp_quantifier(exists, Decls, Formula). | |
102 | kkp_formula2(gt(A,B)) :- !,kkp_opexpr(gt, [A,B]). | |
103 | kkp_formula2(gte(A,B)) :- !,kkp_opexpr(gte,[A,B]). | |
104 | kkp_formula2(lt(A,B)) :- !,kkp_opexpr(lt, [A,B]). | |
105 | kkp_formula2(lte(A,B)) :- !,kkp_opexpr(lte,[A,B]). | |
106 | kkp_formula2(pfunc(E,D,R)) :- !,kkp_opexpr(pfunc,[E,D,R]). | |
107 | kkp_formula2(func(E,D,R)) :- !,kkp_opexpr(func,[E,D,R]). | |
108 | kkp_formula2(F) :- throw(unknown_construct(formula,F)). | |
109 | ||
110 | flatten_subformulas(F,Args) :- flatten_subformulas2(F,Args,[]). | |
111 | flatten_subformulas2(and(A,B)) --> | |
112 | !,flatten_subformulas2(A),flatten_subformulas2(B). | |
113 | flatten_subformulas2(F) --> [F]. | |
114 | ||
115 | ||
116 | kkp_formula_l([]). | |
117 | kkp_formula_l([F|Rest]) :- kkp_formula(F),kkp_formula_l(Rest). | |
118 | ||
119 | kkp_formula_mult(M,E) :- kkp_opexpr(M,[E]). | |
120 | %kkp_formula_binlog(Op,A,B) :- kprint(t(Op)),kkp_formula(A),kkp_formula(B). | |
121 | ||
122 | kkp_opexpr(Op,Expressions) :- kprint(t(Op)),kkp_expression_l(Expressions). | |
123 | kkp_opform(Op,Formulas) :- kprint(t(Op)),kkp_formula_l(Formulas). | |
124 | ||
125 | kkp_quantifier(Type,Decls,Formula) :- | |
126 | kprint(id(Type)),kkp_decls(Decls),kkp_formula(Formula). | |
127 | kkp_decls(Decls) :- kprint(popen),kkp_decls2(Decls),kprint(pclose). | |
128 | kkp_decls2([]). | |
129 | kkp_decls2([D|Drest]) :- kkp_decl(D),kkp_decls2(Drest). | |
130 | kkp_decl(decl(V,Arity,Mult,Expr)) :- | |
131 | !, kprint([popen,id(V),space,t(Arity),space,t(Mult)]), | |
132 | kkp_expression(Expr),kprint(pclose). | |
133 | ||
134 | :- use_module(probsrc(error_manager),[add_warning/3]). | |
135 | /* expressions */ | |
136 | kkp_expression(E) :- kprint(popen), kkp_expression2(E), kprint(pclose). | |
137 | kkp_expression2(empty) :- !,kkp_opexpr(empty,[]). | |
138 | kkp_expression2(iden) :- !,kkp_opexpr(iden,[]). | |
139 | kkp_expression2(univ) :- !,kkp_opexpr(univ,[]). | |
140 | kkp_expression2(transpose(E)) :- !,kkp_opexpr(transpose,[E]). | |
141 | kkp_expression2(closure(E)) :- !,kkp_opexpr(closure,[E]). | |
142 | kkp_expression2(reflexive_closure(E)) :-!,kkp_opexpr(reflexive_closure,[E]). | |
143 | kkp_expression2(union(A,B)) :- !,kkp_fopexpr(union,union(A,B)). | |
144 | kkp_expression2(intersection(A,B)) :- !,kkp_fopexpr(intersection,intersection(A,B)). | |
145 | kkp_expression2(difference(A,B)) :- !,kkp_opexpr(difference,[A,B]). | |
146 | kkp_expression2(join(A,B)) :- !,kkp_opexpr(join,[A,B]). | |
147 | kkp_expression2(product(A,B)) :- !,kkp_fopexpr(product,product(A,B)). | |
148 | kkp_expression2(overwrite(A,B)) :- !,kkp_opexpr(overwrite,[A,B]). | |
149 | kkp_expression2(relref(I)) :- !,kprint([t('relref '),id(I)]). | |
150 | kkp_expression2(varref(I)) :- !,kprint([t('varref '),id(I)]). | |
151 | kkp_expression2(comp(Decls,Formula)) :- !,kkp_quantifier(comp, Decls, Formula). | |
152 | kkp_expression2(prj(Is,Expr)) :- !,kprint(t(prj)),kkp_ints(Is),kkp_expression(Expr). | |
153 | kkp_expression2(int2pow2(E)) :- !,kkp_opexpr(int2pow2,[E]). | |
154 | kkp_expression2(int2intset(E)) :- !,kkp_opexpr(int2intset,[E]). | |
155 | kkp_expression2(if(Cond,Then,Else)) :- !,kprint(t(if)),kkp_formula(Cond),kkp_expression_l([Then,Else]). | |
156 | /* integer expressions */ | |
157 | kkp_expression2(card(E)) :- !,kkp_opexpr(card,[E]). | |
158 | kkp_expression2(add(A,B)) :- !,kkp_opexpr(add,[A,B]). | |
159 | kkp_expression2(sub(A,B)) :- !,kkp_opexpr(sub,[A,B]). | |
160 | kkp_expression2(mul(A,B)) :- !,kkp_opexpr(mul,[A,B]). | |
161 | kkp_expression2(div(A,B)) :- !,kkp_opexpr(div,[A,B]). | |
162 | kkp_expression2(floored_div(A,B)) :- !, add_warning(kodkod_printer,'Translating floored division as truncated division: ',div(A,B)), | |
163 | kkp_opexpr(div,[A,B]). | |
164 | kkp_expression2(mod(A,B)) :- !,kkp_opexpr(mod,[A,B]). | |
165 | kkp_expression2(sum(E)) :- !,kkp_opexpr(expr2int,[E]). | |
166 | kkp_expression2(expr2int(E)) :- !,kkp_opexpr(expr2int,[E]). | |
167 | kkp_expression2(int(I)) :- !,kprint(t(I)). | |
168 | kkp_expression2(E) :- throw(unknown_construct(expression,E)). | |
169 | ||
170 | kkp_fopexpr(Op,Expr) :- | |
171 | flatten_subexpressions(Expr,Op,Subs,[]), | |
172 | kkp_opexpr(Op,Subs). | |
173 | flatten_subexpressions(Expr,Op) --> | |
174 | {functor(Expr,Op,2),!,arg(1,Expr,A),arg(2,Expr,B)}, | |
175 | flatten_subexpressions(A,Op), flatten_subexpressions(B,Op). | |
176 | flatten_subexpressions(Expr,_) --> [Expr]. | |
177 | ||
178 | kkp_expression_l([]). | |
179 | kkp_expression_l([E|Erest]) :- | |
180 | kkp_expression(E),kkp_expression_l(Erest). | |
181 | ||
182 | kkp_ints(Ints) :- kkp_ints2(Ints,P),kprint([popen|P]). | |
183 | kkp_ints2([],[pclose]). | |
184 | kkp_ints2([I|Irest],[t(I),space|Prest]) :- kkp_ints2(Irest,Prest). | |
185 | ||
186 | % send a problem request to Kodkod | |
187 | % MaxLength is the maximum number of solutions | |
188 | kkp_request(Id, Signum, MaxLength, Values, Stream) :- %print(kkp_request(Id, Signum, MaxLength, Values, Stream)),nl, | |
189 | set_stream(Stream), | |
190 | problem_id(Id,PID), | |
191 | kprint([t('request '),id(PID),space, | |
192 | t(MaxLength),space,t(Signum), | |
193 | space,popen]), | |
194 | kkp_values(Values), | |
195 | kprint([pclose,stop]). | |
196 | kkp_values([]). | |
197 | kkp_values([kout(Name,Value)|VRest]) :- | |
198 | kprint([popen,id(Name)]), | |
199 | kkp_tupleset2(Value), | |
200 | kprint(pclose), | |
201 | kkp_values(VRest). | |
202 | ||
203 | kkp_list(Id,MaxLength,Stream) :- | |
204 | set_stream(Stream), | |
205 | problem_id(Id,PID), | |
206 | kprint([t('list '),id(PID),space,t(MaxLength),stop]). | |
207 | ||
208 | :- use_module(probsrc(debug),[debug_mode/1]). | |
209 | kprint(Out) :- | |
210 | (debug_mode(on) -> kprint2(Out,user_output) ; true), | |
211 | output_stream(Stream), | |
212 | kprint2(Out,Stream). | |
213 | kprint2([],_Stream) :- !. | |
214 | kprint2([E|Rest],Stream) :- | |
215 | !,kprint2(E,Stream),kprint2(Rest,Stream). | |
216 | kprint2(E,S) :- kprint_trans(E,N),!,kprint2(N,S). | |
217 | kprint2(t(T),S) :- dwrite(S,T). | |
218 | kprint2(char(C),S) :- dput_char(S,C). | |
219 | kprint2(tuple(Ints),S) :- dput_char(S,'<'), | |
220 | kprint_ints(Ints,S),dput_char(S,'>'). | |
221 | ||
222 | kprint_trans(id(Id),t(Id)). | |
223 | kprint_trans(space,char(' ')). | |
224 | kprint_trans(popen,char('(')). | |
225 | kprint_trans(pclose,char(')')). | |
226 | kprint_trans(stop,t('.\n')). | |
227 | ||
228 | kprint_ints([],_). | |
229 | kprint_ints([I|Irest],S) :- | |
230 | dwrite(S,I),dput_char(S,' '), | |
231 | kprint_ints(Irest,S). | |
232 | ||
233 | ||
234 | %dwrite(S,I) :- write(I), write(S,I). | |
235 | %dput_char(S,C) :- put_char(C), put_char(S,C). | |
236 | dwrite(S,I) :- write(S,I). | |
237 | dput_char(S,C) :- put_char(S,C). | |
238 | ||
239 | ||
240 | problem_id(Num,Id) :- | |
241 | % don't know why the parser does not accept pure numbers | |
242 | number_codes(Num,Codes), | |
243 | % 112 is the ASCII code for p | |
244 | atom_codes(Id,[112|Codes]). |