/**
 * Listing a normal form from a binary decision diagram.
 *
 * Copyright 2012, XLOG Technologies GmbH, Switzerland
 * Jekejeke Prolog 0.9.7 (a fast and small prolog interpreter)
 */

:- op(900,xfx,=>).
:- op(900,xfx,<=>).
:- op(800,xfy,v).
:- op(700,xfy,&).
:- op(600,fy,~).

% convert(+Form, -Tree)
convert(A => B, R) :- !, convert(~A v B, R).
convert(A <=> B, R) :- !, convert((A => B) & (B => A), R).
convert(A v B, R) :- !, convert(A, X), convert(B, Y), union(X, Y, R).
convert(A & B, R) :- !, convert(A, X), convert(B, Y), inter(X, Y, R).
convert(~A, R) :- !, convert(A, X), invert(X, R).
convert(X, (X -> true;false)).

% cnf(+Tree, +List, -List)
cnf(false, L, L).
cnf((V -> S;_), L, R) :-
   cnf(S, [not(V)|L], R).
cnf((V -> _;T), L, R) :-
   cnf(T, [V|L], R).

% dnf(+Tree, +List, -List)
dnf(true, L, L).
dnf((V -> S;_), L, R) :-
  dnf(S, [V|L], R).
dnf((V -> _;T), L, R) :-
  dnf(T, [not(V)|L], R).