%
%  Write a BDD.
%

:- module(bddwrite,
     [write_bdd/1,       % Write a BDD
      write_bdd/2]).     %  (optional) second arg
                         %    is predicate to write variable.

:- dynamic id/1, bddid/2.
%
%  The nodes are numbers by IDs.
%  id is used to generate node IDs.
%  bddid caches pairs (bdd, id):
%    if a subBDD appears again, write the previous ID
%

%
%  write_bdd(B, Write)         - write a bdd after clearing database.
%  write_bdd(B, indent, Write) - auxiliary predicate with indent count.
%    (1) If B has been encourtered just write the node id.
%    (2) For terminals, write the value, assign id and cache the node.
%    (3) For nonterminals, write the variable number,
%          assign id, cache the node and recurse.
%
%    The Write argument must be supplied with a predicate that is
%      used to write the variable numbered N.
%
write_bdd(B)  :-
  write_bdd(B, write_atom).

write_bdd(B, Write) :-
  retractall(bddid(_,_)),
  retractall(id(_)),
  write_bdd(B, 0, Write).

write_bdd(B, Indent, _) :- 
  bddid(B, ID), !, 
  tab(4+Indent),
  write_node(ID).

write_bdd(B, Indent, _) :-
  B = bdd(leaf, Val, _), !,
  generate_id(ID), 
  assert(bddid(B, ID)),
  write_node(ID),
  tab(Indent),
  write(Val).

write_bdd(B, Indent, Write) :-
  B = bdd(N, False, True),
  generate_id(ID),
  assert(bddid(B, ID)),
  write_node(ID),
  tab(Indent),
  call(Write,N), nl,         % Call Write predicate to write the variable
  Indent1 is Indent + 3,
  write_bdd(False,  Indent1, Write), nl,
  write_bdd(True,   Indent1, Write), nl.

%
%  write_node(N)        - write node id N.
%
write_node(ID) :-
  width(ID), write('['), write(ID), write('] ').

%
%  width(ID)            - write ID in field of width 3.
%
width(ID) :- ID < 100, !, write(' ').
width(ID) :- ID <  10, !, write(' ').
width(_).

%
%  generate_id(id(ID))  - increment the id.
%
generate_id(ID) :-
  retract(id(N)), !, ID is N + 1, assert(id(ID)).
generate_id(1)  :-
  assert(id(1)).

%
%  Default is write a variable as vN.
%
write_atom(N) :- write('v'), write(N).