/*
:- type be(VN)
   ---> f
      | t
      | v(VN)
      | n(be(VN))
      | a(be(VN),be(VN))
      | o(be(VN),be(VN))
      | i(be(VN),be(VN))
      | e(be(VN),be(VM)).

:- type robdd(VN)
   ---> ff
      | tt
      | if(VN,robdd(VN),robdd(VN)).

:- pred robdd(be(VN)::in, robdd(VN)::out) is det <= ord(VN).
:- pred opposite(be(VN)::in, robdd(VN)::out) is det <= ord(VN).
:- pred and_merge(robdd(VN)::in,robdd(VN)::in,robdd(VN)::out)is det<=ord(VN).
:- pred ior_merge(robdd(VN)::in,robdd(VN)::in,robdd(VN)::out)is det<=ord(VN).
:- pred imp_merge(robdd(VN)::in,robdd(VN)::in,robdd(VN)::out)is det<=ord(VN).
:- pred eqv_merge(robdd(VN)::in,robdd(VN)::in,robdd(VN)::out)is det<=ord(VN).
:- pred mk_if(VN::in, robdd(VN)::in, robdd(VN)::in, robdd(VN)::out)
        is det <= ord(VN).
*/

robdd(f, ff).
robdd(t, tt).
robdd(v(N), if(N,tt,ff)).
robdd(n(E), R) :- robdd(E, X), opposite(X, R).
robdd(a(E,F), R) :- robdd(E, X), robdd(F, Y), and_merge(X, Y, R).
robdd(o(E,F), R) :- robdd(E, X), robdd(F, Y), ior_merge(X, Y, R).
robdd(i(E,F), R) :- robdd(E, X), robdd(F, Y), imp_merge(X, Y, R).
robdd(e(E,F), R) :- robdd(E, X), robdd(F, Y), eqv_merge(X, Y, R).

opposite(ff, tt).
opposite(tt, ff).
opposite(if(V,E,F), if(V,X,Y)) :- opposite(E, X), opposite(F, Y).

mk_if(V, X, Y, R) :- ( X = Y -> R = X ; R = if(V,X,Y) ).

and_merge(ff, _, ff) :- !.
and_merge(_, ff, ff) :- !.
and_merge(tt, Y, Y ) :- !.
and_merge(X, tt, X ) :- !.
and_merge(X, X,  X ) :- !.
and_merge(X, Y,  if(W,E1,E2)) :-
    X = if(U,A,B), Y = if(V,C,D),
    ( U @< V ->
	W = U, and_merge(A, Y, E1), and_merge(B, Y, E2)
    ; V @< U ->
	W = V, and_merge(X, C, E1), and_merge(X, D, E2)
    ; /* V = U */
	W = U, and_merge(A, C, E1), and_merge(B, D, E2)
    ).


ior_merge(ff, Y, Y ) :- !.
ior_merge(X, ff, X ) :- !.
ior_merge(tt, _, tt) :- !.
ior_merge(_, tt, tt) :- !.
ior_merge(X, X,  X ) :- !.
ior_merge(X, Y,  if(W,E1,E2)) :-
    X = if(U,A,B), Y = if(V,C,D),
    ( U @< V ->
	W = U, ior_merge(A, Y, E1), ior_merge(B, Y, E2)
    ; V @< U ->
	W = V, ior_merge(X, C, E1), ior_merge(X, D, E2)
    ; /* V = U */
	W = U, ior_merge(A, C, E1), ior_merge(B, D, E2)
    ).

imp_merge(ff, _, tt) :- !.
imp_merge(X, ff, R)  :- !, opposite(X, R).
imp_merge(tt, Y, Y ) :- !.
imp_merge(_, tt, tt) :- !.
imp_merge(X, X,  tt) :- !.
imp_merge(X, Y,  if(W,E1,E2)) :-
    X = if(U,A,B), Y = if(V,C,D),
    ( U @< V ->
	W = U, imp_merge(A, Y, E1), imp_merge(B, Y, E2)
    ; V @< U ->
	W = V, imp_merge(X, C, E1), imp_merge(X, D, E2)
    ; /* V = U */
	W = U, imp_merge(A, C, E1), imp_merge(B, D, E2)
    ).

eqv_merge(ff, Y, R ) :- !, opposite(Y, R).
eqv_merge(X, ff, R ) :- !, opposite(X, R).
eqv_merge(tt, Y, Y ) :- !.
eqv_merge(X, tt, X ) :- !.
eqv_merge(X, X,  tt) :- !.
eqv_merge(X, Y,  if(W,E1,E2)) :-
    X = if(U,A,B), Y = if(V,C,D),
    ( U @< V ->
	W = U, eqv_merge(A, Y, E1), eqv_merge(B, Y, E2)
    ; V @< U ->
	W = V, eqv_merge(X, C, E1), eqv_merge(X, D, E2)
    ; /* V = U */
	W = U, eqv_merge(A, C, E1), eqv_merge(B, D, E2)
    ).

model(BE, M) :-
    robdd(BE, R),
    model(R, [], M).

model(tt, M0, M) :-
    reverse(M0, M).
model(if(X,A,B), M0, M) :-
    (   model(A, [X=t|M0], M)
    ;   model(B, [X=f|M0], M)
    ).

counter_model(BE, M) :-
    robdd(BE, R),
    counter_model(R, [], M).

counter_model(ff, M0, M) :-
    reverse(M0, M).
counter_model(if(X,A,B), M0, M) :-
    (   counter_model(A, [X=t|M0], M)
    ;   counter_model(B, [X=f|M0], M)
    ).

mm(N) :-
    tc(N, BE), model(BE, M), write(M), nl.

cm(N) :-
    tc(N, BE), counter_model(BE, M), write(M), nl.

/* Here are some test cases */
N/R :- tc(N, X), robdd(X, R).

:- op(10, fx, v).
tc(1, v 1).
tc(2, o(v 1,v 1)).
tc(3, e(i(v 1,v 2),o(n(v 1),v 2))).
tc(4, e(a(v 1,v 1),v 1)).
tc(5, a(a(a(e(v 13,o(a(f,v 1),o(a(f,v 5),a(v 1,v 5)))),e(v 9,e(e(f,n(v
    1)), n(v 5)))),a(a(e(v 14,o(a(v 13,v 2),o(a(v 13,v 6),a(v 2,v
    6)))),e(v 10, e(e(v 13,n(v 2)),n(v 6)))),a(a(e(v 15,o(a(v 14,v
    3),o(a(v 14,v 7),a(v 3, v 7)))),e(v 11,e(e(v 14,n(v 3)),n(v
    7)))),a(e(v 16,o(a(v 15,v 4), o(a(v 15,v 8),a(v 4,v 8)))),e(v
    12,e(e(v 15,n(v 4)),n(v 8))))))), a(a(a(e(v 17,o(a(n(f),a(v 1,v
    5)),a(f,o(v 1,v 5)))),e(v 9,o(a(f,a(v 1, v 5)),o(a(f,a(n(v 1),n(v
    5))),o(a(n(f),a(v 1,n(v 5))),a(n(f),a(n(v 1), v 5))))))),a(a(e(v
    18,o(a(n(v 17),a(v 2,v 6)),a(v 17,o(v 2,v 6)))), e(v 10,o(a(v 17,a(v
    2,v 6)),o(a(v 17,a(n(v 2),n(v 6))),o(a(n(v 17),a(v 2, n(v 6))),a(n(v
    17),a(n(v 2),v 6))))))),a(a(e(v 19,o(a(n(v 18),a(v 3, v 7)),a(v
    18,o(v 3,v 7)))),e(v 11,o(a(v 18,a(v 3,v 7)),o(a(v 18,a(n(v 3), n(v
    7))),o(a(n(v 18),a(v 3,n(v 7))),a(n(v 18),a(n(v 3),v 7))))))), a(e(v
    20,o(a(n(v 19),a(v 4,v 8)),a(v 19,o(v 4,v 8)))),e(v 12,o(a(v 19, a(v
    4,v 8)),o(a(v 19,a(n(v 4),n(v 8))),o(a(n(v 19),a(v 4,n(v 8))), a(n(v
    19),a(n(v 4),v 8)))))))))),e(v 16,v 20)))).
tc(6, a(a(a(e(v 13,o(a(f,t),o(a(f,v 5),a(t,v 5)))), e(v
    9,e(e(f,n(t)),n(v 5)))),a(a(e(v 14,o(a(v 13,f),o(a(v 13,v 6),a(f, v
    6)))),e(v 10,e(e(v 13,n(f)),n(v 6)))),a(a(e(v 15,o(a(v 14,f), o(a(v
    14,v 7),a(f,v 7)))),e(v 11,e(e(v 14,n(f)),n(v 7)))),a(e(v 16, o(a(v
    15,t),o(a(v 15,v 8),a(t,v 8)))),e(v 12,e(e(v 15,n(t)), n(v
    8))))))),a(a(a(e(v 17,o(a(n(f),a(t,v 5)),a(f,o(t,v 5)))),e(v 9,
    o(a(f,a(t,v 5)),o(a(f,a(n(t),n(v 5))),o(a(n(f),a(t,n(v 5))),
    a(n(f),a(n(t),v 5))))))),a(a(e(v 18,o(a(n(v 17),a(f,v 6)),a(v
    17,o(f, v 6)))),e(v 10,o(a(v 17,a(f,v 6)),o(a(v 17,a(n(f),n(v
    6))),o(a(n(v 17), a(f,n(v 6))),a(n(v 17),a(n(f),v 6))))))),a(a(e(v
    19,o(a(n(v 18),a(f, v 7)),a(v 18,o(f,v 7)))),e(v 11,o(a(v 18,a(f,v
    7)),o(a(v 18,a(n(f), n(v 7))),o(a(n(v 18),a(f,n(v 7))),a(n(v
    18),a(n(f),v 7))))))),a(e(v 20, o(a(n(v 19),a(t,v 8)),a(v 19,o(t,v
    8)))),e(v 12,o(a(v 19,a(t,v 8)), o(a(v 19,a(n(t),n(v 8))),o(a(n(v
    19),a(t,n(v 8))),a(n(v 19),a(n(t), v 8)))))))))),e(v 16,v 20)))).
tc(7, e(n(a(v 1,a(v 2,a(v 3,a(v 4,a(v 5,a(v 6,a(v 7,a(v 8,a(v 9,a(v
    10,a(v 11, a(v 12,a(v 13,a(v 14,a(v 15,v 16)))))))))))))))),o(n(v
    1),o(n(v 2), o(n(v 3),o(n(v 4),o(n(v 5),o(n(v 6),o(n(v 7),o(n(v
    8),o(n(v 9),o(n(v 10), o(n(v 11),o(n(v 12),o(n(v 13),o(n(v 14),o(n(v
    15), n(v 16)))))))))))))))))).
tc(8, e(n(o(v 1,o(v 2,o(v 3,o(v 4,o(v 5,o(v 6,o(v 7,o(v 8,o(v 9,o(v
    10,o(v 11, o(v 12,o(v 13,o(v 14,o(v 15,v 16)))))))))))))))),a(n(v
    1),a(n(v 2), a(n(v 3),a(n(v 4),a(n(v 5),a(n(v 6),a(n(v 7),a(n(v
    8),a(n(v 9),a(n(v 10), a(n(v 11),a(n(v 12),a(n(v 13),a(n(v 14),a(n(v
    15),n(v 16)))))))))))))))))).
tc(9, e(n(o(v 1,o(v 2,o(v 3,o(v 4,o(v 5,o(v 6,o(v 7,o(v 8,o(v 9,
    o(v 10,o(v(11),o(v 12,o(v 13,o(v 14,o(v 15,v 16)))))))))))))))),
    a(n(v 1),a(n(v 2),a(n(v 3),a(n(v 4),a(n(v 5),a(n(v 6),a(n(v 7),
    a(n(v 8),a(n(v 9),a(n(v 10),a(n(v(11)),a(n(v 12),a(n(v 13),
    a(n(v 14),a(n(v 15),n(v 16)))))))))))))))))).
% Test cases 10 to 21 were provided by Jonathan Pengelly
tc(10, a(v 1,n(v 1))).
tc(11, o(a(v 1,n(v 2)),a(n(v 1),v 2))).
% Modus Ponens test
tc(12, a(a(v 1,i(v 1,v 2)),n(v 2))).
% Modus Tollens test
tc(13, a(a(n(v 2),i(v 1,v 2)),v 1)).
% Double negation test
tc(14, e(v 1,n(n(v 1)))).
% Associativity
tc(15, e(a(a(v 1,v 2),v 3),a(v 1,a(v 2,v 3)))).
% De Morgan's rules
tc(16, e(n(o(v 1,v 2)),a(n(v 1),n(v 2)))).
% Show that the following is not a tautology
tc(17, i(i(v 1,v 3),i(i(v 2,v 4),i(o(v 1,v 2),v 3)))).
% Unsatisfiable set of clauses
tc(18, a(a(a(o(o(v 1,v 2),n(v 3)),o(o(v 1,v 2),v 3)),o(v 1,n(v 2))),n(v 1))).
% Tautology
tc(19, i(v 1,i(v 2,v 1))).
tc(20, t).
tc(21, f).