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