% http://www.cs.kuleuven.be/~dtai/events/ASP-competition/Benchmarks/GBIE.shtml
% by Neng-Fa Zhou, April 10, 2009

solve(As):-
    make_char_list(As,S,1),
    equation(S).

% fails if the sequence is not sorted by positions
make_char_list([],[],_).
make_char_list([char(C,P)|As],[C|S],P):-
    P1 is P+1,
    make_char_list(As,S,P1).

% <equation> -> <expression> <greater> <sign_1> <number>
equation(S0):-
    expression(S0,S1,Lhs),
    S1=[g|S2],  %'>'
    sign_1(S2,S3,SignR),
    number(S3,[],ValueR),
    (Lhs>=0->SignL=p,ValueL=Lhs;SignL=m,ValueL is -Lhs),
    (SignR=='m'->Rhs is -ValueR;Rhs is ValueR),
    (Lhs>Rhs->
     format("sol. values(~w,~w,~w,~w). ~n",[SignL,ValueL,SignR,ValueR]);
     format("UNSATISFIABLE~n")).

% <expression> -> <sign_1> <term> <term_1>
expression(S0,SR,Value):-
    sign_1(S0,S1,Sign),
    term(S1,S2,TermValue),
    term_1(S2,SR,TermLValue),
    (Sign==p->Value is  TermValue+TermLValue;
              Value is -TermValue+TermLValue).

% <term> -> <number> | <op_bracket> <expression> <cl_bracket>
term(S0,SR,Value):-
    number(S0,SR,Value), !.
term(S0,SR,Value):-
    S0=[o|S1],  % '('
    expression(S1,S2,Value),
    S2=[c|SR].  % ')'

% <term_1> -> <sign> <term> <term_1> | epsilon
% <sign> -> <plus> | <minus>
term_1(S0,SR,Value):-
    sign(S0,S1,Op), !,
    term(S1,S2,TermValue),
    term_1(S2,SR,TermLValue),
    (Op==m->Value is -TermValue+TermLValue;
            Value is  TermValue+TermLValue).
term_1(S,S,0).


sign([p|S],S,p) :- !.
sign([m|S],S,m).

% <sign_1> -> <sign> | epsilon
sign_1(S0,SR,Sign):-
     sign(S0,SR,Sign), !.
sign_1(S,S,p).

% <number> -> <digit> <number_1>
number(S0,SR,Value):-
    digit(S0,S1,D),
    number_1(S1,SR,D,Value).

%<number_1> -> <digit> <number_1> | epsilon
number_1(S0,SR,Value0,Value):-
    digit(S0,S1,D), !,
    Value1 is Value0*10+D,
    number_1(S1,SR,Value1,Value).
number_1(S,S,Value,Value).

digit([D|S],S,D):-
    is_digit(D).

is_digit(0).
is_digit(1).
is_digit(2).
is_digit(3).
is_digit(4).
is_digit(5).
is_digit(6).
is_digit(7).
is_digit(8).
is_digit(9).

test:-
   solve([char(9,1),char(m,2),char(o,3),char(3,4),char(p,5),char(o,6),char(4,7),char(m,8),char(2,9),char(c,10),char(p,11),char(1,12),char(c,13),char(g,14),char(m,15),char(1,16)]).