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