//==============================================================================
//	
//	Copyright (c) 2002-
//	Authors:
//	* Dave Parker <david.parker@comlab.ox.ac.uk> (University of Oxford, formerly University of Birmingham)
//	
//------------------------------------------------------------------------------
//	
//	This file is part of PRISM.
//	
//	PRISM is free software; you can redistribute it and/or modify
//	it under the terms of the GNU General Public License as published by
//	the Free Software Foundation; either version 2 of the License, or
//	(at your option) any later version.
//	
//	PRISM is distributed in the hope that it will be useful,
//	but WITHOUT ANY WARRANTY; without even the implied warranty of
//	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
//	GNU General Public License for more details.
//	
//	You should have received a copy of the GNU General Public License
//	along with PRISM; if not, write to the Free Software Foundation,
//	Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
//	
//==============================================================================

package jdd;

public class JDDTest
{
	public static void main(String[] args)
	{
		JDDNode a, b, c;
		JDDVars vars;		
		
		System.out.println("\nTest program for JDD\n====================");
		
		// initialise cudd
		JDD.InitialiseCUDD();
		
		// set up some variables
		vars = new JDDVars();
		vars.addVar(JDD.Var(0));
		vars.addVar(JDD.Var(2));
		
		// blank dd
		a = JDD.Create();
		System.out.println("\nCreate()");
		JDD.PrintVector(a, vars);
		JDD.Deref(a);
		
		// constant
		a = JDD.Constant(1.5);
		System.out.println("\nConstant(1.5)");
		JDD.PrintVector(a, vars);
		JDD.Deref(a);
		
		// plus infinity
		a = JDD.PlusInfinity();
		System.out.println("\nPlusInfinity()");
		JDD.PrintVector(a, vars);
		JDD.Deref(a);
		
		// minus infinity
		a = JDD.MinusInfinity();
		System.out.println("\nMinusInfinity()");
		JDD.PrintVector(a, vars);
		JDD.Deref(a);
		
		// var
		a = JDD.Var(0);
		System.out.println("\nVar(0)");
		JDD.PrintVector(a, vars);
		JDD.Deref(a);
				
		a = JDD.Var(0);
		b = JDD.Var(2);
		System.out.print("\na: ");
		JDD.PrintVector(a, vars);
		System.out.print("b: ");
		JDD.PrintVector(b, vars);

		// not
		JDD.Ref(a);
		c = JDD.Not(a);
		System.out.println("\nNot(a)");
		JDD.PrintVector(c, vars);
		JDD.Deref(c);
		
		// or
		JDD.Ref(a);
		JDD.Ref(b);
		c = JDD.Or(a, b);
		System.out.println("\nOr(a, b)");
		JDD.PrintVector(c, vars);
		JDD.Deref(c);
		
		// and
		JDD.Ref(a);
		JDD.Ref(b);
		c = JDD.And(a, b);
		System.out.println("\nAnd(a, b)");
		JDD.PrintVector(c, vars);
		JDD.Deref(c);
		
		// xor
		JDD.Ref(a);
		JDD.Ref(b);
		c = JDD.Xor(a, b);
		System.out.println("\nXor(a, b)");
		JDD.PrintVector(c, vars);
		JDD.Deref(c);
		
		// implies
		JDD.Ref(a);
		JDD.Ref(b);
		c = JDD.Implies(a, b);
		System.out.println("\nImplies(a, b)");
		JDD.PrintVector(c, vars);
		JDD.Deref(c);
		
		JDD.Deref(a);
		JDD.Deref(b);
		
		a = JDD.Create();
		a = JDD.SetVectorElement(a, vars, 0, 1);
		a = JDD.SetVectorElement(a, vars, 1, 2);
		a = JDD.SetVectorElement(a, vars, 2, 3);
		a = JDD.SetVectorElement(a, vars, 3, 4);
		b = JDD.Create();
		b = JDD.SetVectorElement(b, vars, 0, 0);
		b = JDD.SetVectorElement(b, vars, 1, 2);
		b = JDD.SetVectorElement(b, vars, 2, 4);
		b = JDD.SetVectorElement(b, vars, 3, 6);
		System.out.print("\na: ");
		JDD.PrintVector(a, vars);
		System.out.print("b: ");
		JDD.PrintVector(b, vars);
		
		// apply
		JDD.Ref(a);
		JDD.Ref(b);
		c = JDD.Apply(JDD.PLUS, a, b);
		System.out.println("\nApply(+, a, b)");
		JDD.PrintVector(c, vars);
		JDD.Deref(c);
		JDD.Ref(a);
		JDD.Ref(b);
		c = JDD.Apply(JDD.MINUS, a, b);
		System.out.println("\nApply(-, a, b)");
		JDD.PrintVector(c, vars);
		JDD.Deref(c);
		JDD.Ref(a);
		JDD.Ref(b);
		c = JDD.Apply(JDD.TIMES, a, b);
		System.out.println("\nApply(*, a, b)");
		JDD.PrintVector(c, vars);
		JDD.Deref(c);
		JDD.Ref(a);
		JDD.Ref(b);
		c = JDD.Apply(JDD.DIVIDE, a, b);
		System.out.println("\nApply(/, a, b)");
		JDD.PrintVector(c, vars);
		JDD.Deref(c);
		
		
		JDD.Deref(a);
		JDD.Deref(b);

		// dereference variables
		vars.derefAll();
		
		// close down cudd
		JDD.CloseDownCUDD();
		System.out.println();
	}
}

//------------------------------------------------------------------------------