kodkod_printer

dput_char(S,C) :- put_char(S,C).

dwrite(S,I) :- write(S,I).

flatten_subexpressions(Expr,Op) -->
    {functor(Expr,Op,2),!,arg(1,Expr,A),arg(2,Expr,B)},
    flatten_subexpressions(A,Op), flatten_subexpressions(B,Op).

flatten_subexpressions(Expr,_) --> [Expr].

flatten_subformulas(F,Args) :- flatten_subformulas2(F,Args,[]).

flatten_subformulas2(and(A,B)) -->
    !,flatten_subformulas2(A),flatten_subformulas2(B).

flatten_subformulas2(F) --> [F].

kkp_decl(decl(V,Arity,Mult,Expr)) :-
    !, kprint([popen,id(V),space,t(Arity),space,t(Mult)]),
    kkp_expression(Expr),kprint(pclose).

kkp_decls(Decls) :- kprint(popen),kkp_decls2(Decls),kprint(pclose).

kkp_decls2([]).

kkp_decls2([D|Drest]) :- kkp_decl(D),kkp_decls2(Drest).

kkp_expression(E) :- kprint(popen), kkp_expression2(E), kprint(pclose).

kkp_expression2(empty) :- !,kkp_opexpr(empty,[]).

kkp_expression2(iden) :- !,kkp_opexpr(iden,[]).

kkp_expression2(univ) :- !,kkp_opexpr(univ,[]).

kkp_expression2(transpose(E)) :- !,kkp_opexpr(transpose,[E]).

kkp_expression2(closure(E)) :- !,kkp_opexpr(closure,[E]).

kkp_expression2(reflexive_closure(E)) :-!,kkp_opexpr(reflexive_closure,[E]).

kkp_expression2(union(A,B)) :- !,kkp_fopexpr(union,union(A,B)).

kkp_expression2(intersection(A,B)) :- !,kkp_fopexpr(intersection,intersection(A,B)).

kkp_expression2(difference(A,B)) :- !,kkp_opexpr(difference,[A,B]).

kkp_expression2(join(A,B)) :- !,kkp_opexpr(join,[A,B]).

kkp_expression2(product(A,B)) :- !,kkp_fopexpr(product,product(A,B)).

kkp_expression2(overwrite(A,B)) :- !,kkp_opexpr(overwrite,[A,B]).

kkp_expression2(relref(I)) :- !,kprint([t('relref '),id(I)]).

kkp_expression2(varref(I)) :- !,kprint([t('varref '),id(I)]).

kkp_expression2(comp(Decls,Formula)) :- !,kkp_quantifier(comp, Decls, Formula).

kkp_expression2(prj(Is,Expr)) :- !,kprint(t(prj)),kkp_ints(Is),kkp_expression(Expr).

kkp_expression2(int2pow2(E)) :- !,kkp_opexpr(int2pow2,[E]).

kkp_expression2(int2intset(E)) :- !,kkp_opexpr(int2intset,[E]).

kkp_expression2(if(Cond,Then,Else)) :- !,kprint(t(if)),kkp_formula(Cond),kkp_expression_l([Then,Else]).

kkp_expression2(card(E)) :- !,kkp_opexpr(card,[E]).

kkp_expression2(add(A,B)) :- !,kkp_opexpr(add,[A,B]).

kkp_expression2(sub(A,B)) :- !,kkp_opexpr(sub,[A,B]).

kkp_expression2(mul(A,B)) :- !,kkp_opexpr(mul,[A,B]).

kkp_expression2(div(A,B)) :- !,kkp_opexpr(div,[A,B]).

kkp_expression2(floored_div(A,B)) :- !, add_warning(kodkod_printer,'Translating floored division as truncated division: ',div(A,B)),
    kkp_opexpr(div,[A,B]).

kkp_expression2(mod(A,B)) :- !,kkp_opexpr(mod,[A,B]).

kkp_expression2(sum(E)) :- !,kkp_opexpr(expr2int,[E]).

kkp_expression2(expr2int(E)) :- !,kkp_opexpr(expr2int,[E]).

kkp_expression2(int(I)) :- !,kprint(t(I)).

kkp_expression2(E) :- throw(unknown_construct(expression,E)).

kkp_expression_l([]).

kkp_expression_l([E|Erest]) :-
    kkp_expression(E),kkp_expression_l(Erest).

kkp_fopexpr(Op,Expr) :-
    flatten_subexpressions(Expr,Op,Subs,[]),
    kkp_opexpr(Op,Subs).

kkp_formula(F) :- kprint(popen), kkp_formula2(F), kprint(pclose).

kkp_formula2(true) :- !,kprint(t(true)).

kkp_formula2(false) :- !,kprint(t(false)).

kkp_formula2(one(E)) :- !,kkp_formula_mult(one, E).

kkp_formula2(some(E)) :- !,kkp_formula_mult(some,E).

kkp_formula2(no(E)) :- !,kkp_formula_mult(no, E).

kkp_formula2(lone(E)) :- !,kkp_formula_mult(lone,E).

kkp_formula2(set(E)) :- !,kkp_formula_mult(set, E).

kkp_formula2(in(A,B)) :- !,kkp_opexpr(in,[A,B]).

kkp_formula2(equals(A,B)) :- !,kkp_opexpr(equals,[A,B]).

kkp_formula2(not(F)) :- !,kkp_opform(not,[F]).

kkp_formula2(and(A,B)) :- !,flatten_subformulas(and(A,B),Args), kkp_opform(and,Args).

kkp_formula2(or(A,B)) :- !,kkp_opform(or, [A,B]).

kkp_formula2(implies(A,B)) :- !,kkp_opform(implies,[A,B]).

kkp_formula2(iff(A,B)) :- !,kkp_opform(iff,[A,B]).

kkp_formula2(forall(Decls,Formula)) :- !,kkp_quantifier(all, Decls, Formula).

kkp_formula2(exists(Decls,Formula)) :- !,kkp_quantifier(exists, Decls, Formula).

kkp_formula2(gt(A,B)) :- !,kkp_opexpr(gt, [A,B]).

kkp_formula2(gte(A,B)) :- !,kkp_opexpr(gte,[A,B]).

kkp_formula2(lt(A,B)) :- !,kkp_opexpr(lt, [A,B]).

kkp_formula2(lte(A,B)) :- !,kkp_opexpr(lte,[A,B]).

kkp_formula2(pfunc(E,D,R)) :- !,kkp_opexpr(pfunc,[E,D,R]).

kkp_formula2(func(E,D,R)) :- !,kkp_opexpr(func,[E,D,R]).

kkp_formula2(F) :- throw(unknown_construct(formula,F)).

kkp_formula_l([]).

kkp_formula_l([F|Rest]) :- kkp_formula(F),kkp_formula_l(Rest).

kkp_formula_mult(M,E) :- kkp_opexpr(M,[E]).

kkp_ints(Ints) :- kkp_ints2(Ints,P),kprint([popen|P]).

kkp_ints2([],[pclose]).

kkp_ints2([I|Irest],[t(I),space|Prest]) :- kkp_ints2(Irest,Prest).

kkp_inttype_part1(PowName,PowMin,PowMax) :-
    kprint([popen,t(inttype),popen,id(PowName),space,t(PowMin),space,t(PowMax),pclose]).

kkp_inttype_part2 :-
    kprint(pclose).

kkp_list(Id,MaxLength,Stream) :-
    set_stream(Stream),
    problem_id(Id,PID),
    kprint([t('list '),id(PID),space,t(MaxLength),stop]).

kkp_opexpr(Op,Expressions) :- kprint(t(Op)),kkp_expression_l(Expressions).

kkp_opform(Op,Formulas) :- kprint(t(Op)),kkp_formula_l(Formulas).

kkp_problem(Stream,Timeout,Symmetry,Solver,Id,P) :-
    set_stream(Stream),
    call_cleanup( (kkp_problem2(Timeout,Symmetry,Solver,Id,P),!), retractall(output_stream(_)) ).

kkp_problem2(Timeout,Symmetry,Solver,Id,problem(Types,Relations,Formula,_,_IntRange)) :-
    problem_id(Id,PID),
    kprint([t('problem '),id(PID),space,t(Timeout),space,t(Symmetry),space,t(Solver)]),
    % will output something like "problem p2 2500 0 sat4j"
    kkp_types(Types),
    kkp_relations(Relations),
    kkp_formula(Formula),
    kprint(stop).

kkp_quantifier(Type,Decls,Formula) :-
    kprint(id(Type)),kkp_decls(Decls),kkp_formula(Formula).

kkp_relation(reldef(Id,Types,SetOrSingleton,SubsetExact,Set)) :-
    kprint([popen,id(Id),space]),
    ( SetOrSingleton==single -> kprint(t('singleton ')); true),
    kprint([t(SubsetExact)]),kkp_typerefs(Types),
    kkp_tupleset(Set),
    kprint(pclose).

kkp_relations(Relations) :-
    kprint(popen), kkp_relations2(Relations), kprint(pclose).

kkp_relations2([]).

kkp_relations2([Rel|Rrest]) :-
    kkp_relation(Rel), kkp_relations2(Rrest).

kkp_request(Id, Signum, MaxLength, Values, Stream) :- %print(kkp_request(Id, Signum, MaxLength, Values, Stream)),nl,
    set_stream(Stream),
    problem_id(Id,PID),
    kprint([t('request '),id(PID),space,
    t(MaxLength),space,t(Signum),
    space,popen]),
    kkp_values(Values),
    kprint([pclose,stop]).

kkp_tupleset(full) :- !.

kkp_tupleset(TupleSet) :- is_list(TupleSet),!,
    kprint(popen),kkp_tupleset2(TupleSet),kprint(pclose).

kkp_tupleset2([]).

kkp_tupleset2([tuple(Tuple)|Trest]) :-
    kprint(tuple(Tuple)),kkp_tupleset2(Trest).

kkp_type(type(Id,Size)) :- kprint([popen,id(Id),space,t(Size),pclose]).

kkp_type(inttype(PowName,PowMin,PowMax)) :-
    PowMax<PowMin,!,
    print_message('Translation to Kodkod: Inconsistent integer range: Relaxing to avoid exceptions'),
    kkp_type(inttype(PowName,PowMin,PowMin)). % relax in

kkp_type(inttype(PowName,PowMin,PowMax)) :-
    kkp_inttype_part1(PowName,PowMin,PowMax),kkp_inttype_part2.

kkp_type(inttype(PowName,PowMin,PowMax,IntsetName,Min,Max)) :-
    PowMax<PowMin,!,
    print_message('Translation to Kodkod: Inconsistent integer range: Relaxing to avoid exceptions'),
    kkp_type(inttype(PowName,PowMin,PowMin,IntsetName,Min,Max)).

kkp_type(inttype(PowName,PowMin,PowMax,IntsetName,Min,Max)) :-
    Max<Min,!,
    print_message('Translation to Kodkod: Inconsistent integer range: Relaxing to avoid exceptions'),
    kkp_type(inttype(PowName,PowMin,PowMax,IntsetName,Min,Min)).

kkp_type(inttype(PowName,PowMin,PowMax,IntsetName,Min,Max)) :-
    kkp_inttype_part1(PowName,PowMin,PowMax),
    kprint([popen,id(IntsetName),space,t(Min),space,t(Max),pclose]),
    kkp_inttype_part2.

kkp_typerefs([]).

kkp_typerefs([Type|Trest]) :-
    kprint([space,t(Type)]),
    kkp_typerefs(Trest).

kkp_types(Types) :- kprint(popen), kkp_types2(Types), kprint(pclose).

kkp_types2([]).

kkp_types2([Type|TRest]) :- kkp_type(Type), kkp_types2(TRest).

kkp_values([]).

kkp_values([kout(Name,Value)|VRest]) :-
    kprint([popen,id(Name)]),
    kkp_tupleset2(Value),
    kprint(pclose),
    kkp_values(VRest).

kprint(Out) :-
    (debug_mode(on) -> kprint2(Out,user_output) ; true),
    output_stream(Stream),
    kprint2(Out,Stream).

kprint2([],_Stream) :- !.

kprint2([E|Rest],Stream) :-
    !,kprint2(E,Stream),kprint2(Rest,Stream).

kprint2(E,S) :- kprint_trans(E,N),!,kprint2(N,S).

kprint2(t(T),S) :- dwrite(S,T).

kprint2(char(C),S) :- dput_char(S,C).

kprint2(tuple(Ints),S) :- dput_char(S,'<'),
    kprint_ints(Ints,S),dput_char(S,'>').

kprint_ints([],_).

kprint_ints([I|Irest],S) :-
    dwrite(S,I),dput_char(S,' '),
    kprint_ints(Irest,S).

kprint_trans(id(Id),t(Id)).

kprint_trans(space,char(' ')).

kprint_trans(popen,char('(')).

kprint_trans(pclose,char(')')).

kprint_trans(stop,t('.\n')).

problem_id(Num,Id) :-
    % don't know why the parser does not accept pure numbers
    number_codes(Num,Codes),
    % 112 is the ASCII code for p
    atom_codes(Id,[112|Codes]).

set_stream(Stream) :-
    retractall(output_stream(_)),
    assertz(output_stream(Stream)).