import junit.framework.Assert;
import junit.framework.TestCase;
import java.io.BufferedInputStream;
import java.io.DataInputStream;
import java.io.File;
import java.io.FileInputStream;
import java.io.FileNotFoundException;
import java.io.IOException;

public class Test extends TestCase{


	
	/**

	 * This SIMPLE test should return satisfiable

	 * @param filename

	 */

	public void testSimpleSat()

	{
		ABMatrix m = new ABMatrix();
		m.matrix = new double[5][5];
		for (int i=0; i<5; i++)
			for (int j=0; j<5; j++)
			{
				m.matrix[i][j] = Double.NEGATIVE_INFINITY;
			}
		m.matrix[1][0] = 5; // x-y >= 5
		m.matrix[0][1] = -10; // -x+y >= -10
		m.M = 5;

		CdbTuple t = new CdbTuple(m, new String[] {"x", "y", "z", "x1", "z1"});
		boolean flag = t.satisfiable();
		Assert.assertTrue(flag);
	}

	

	public void testSimpleUnsat()
	{
		ABMatrix m = new ABMatrix();
		m.matrix = new double[5][5];
		for (int i=0; i<5; i++)
			for (int j=0; j<5; j++)
			{
				m.matrix[i][j] = Double.NEGATIVE_INFINITY;
			}
		m.matrix[1][0] = 12; // x-y >= 12
		m.matrix[0][1] = -10; // -x+y >= -10
		m.M = 5;
		
		CdbTuple t = new CdbTuple(m, new String[] {"x", "y", "z", "x1", "z1"});
		boolean flag = t.satisfiable();
		Assert.assertTrue(!flag);
	}

	public void testAddSat()
	{
		ABMatrix m = new ABMatrix();
		m.matrix = new double[5][5];
		m.M = 5;

		for (int i=0; i<5; i++)
			for (int j=0; j<5; j++)
			{
				m.matrix[i][j] = Double.NEGATIVE_INFINITY;
			}
		m.matrix[1][0] = 5; // x-y >= 5
		m.matrix[0][1] = -10; // x+y >= -10
		m.matrix[2][1] = 3; // -x-y >= -10
		m.matrix[2][3] = -5; // +x+y >= -10

		CdbTuple t = new CdbTuple(m, new String[] {"xp", "yp", "xn", "yn", "z1"});
		boolean flag = t.satisfiable();
		Assert.assertTrue(flag);
	}
	

}

