// Digtech 2 im SS 2003 - Zusatzaufgabe zur Übung 1 (ab 19. 5. 2003)

import org.sf.javabdd.*;

public class Ausgeben {

    public static void BDDAusgebe(BDD x)
    	{
		//Gib BBD aus unter folgender Form:
		//      x0 hat linken Sohn x2 und rechten Sohn x1
		//      x2 hat linken Sohn EINS und rechten Sohn NULL
		//      x1 hat linken Sohn x2 und rechten Sohn EINS
		//      x2 hat linken Sohn EINS und rechten Sohn NULL

		// ACHTUNG! DIES REICHT NICHT AUS ZUR
		// EINDEUTIGEN BESTIMMUNG DES BAUMES!


		// werden für die Rekursion gebraucht
		boolean linksrunter=false, rechtsrunter=false;

		System.out.print("x" + x.var() + " hat linken Sohn ");

		// nach links absteigen
		if (x.low().equals(Manager.mgr.zero()))
			System.out.print("NULL");
		else if (x.low().equals(Manager.mgr.one()))
			System.out.print("EINS");
		else
			{
			System.out.print("x" + (x.low()).var());
			linksrunter=true;
			}

		System.out.print (" und rechten Sohn ");

		// nach rechts absteigen
		if (x.high().equals(Manager.mgr.zero()))
			System.out.print("NULL");
		else if (x.high().equals(Manager.mgr.one()))
			System.out.print("EINS");
		else
			{
			System.out.print("x" + (x.high()).var());
			rechtsrunter=true;
			}

		System.out.println();

		if (linksrunter==true)
			BDDAusgebe (x.low());

		if (rechtsrunter==true)
			BDDAusgebe (x.high());

		}


    public static void main(String[] args)
	    {
		Manager.mgr = BuDDyFactory.init(10000,1000);
		Manager.mgr.setVarNum(4);

		BDD x0 = Manager.mgr.ithVar(0);
		BDD x1 = Manager.mgr.ithVar(1);
		BDD x2 = Manager.mgr.ithVar(2);
		BDD x3 = Manager.mgr.ithVar(2);

		BDDAusgebe((x0.and(x1)).or(x2.not()));

		System.out.println();

		Manager.mgr.done();
		}

}