import junit.framework.Assert;
import junit.framework.TestCase;
import csce913proj1.*;

public class Test extends TestCase{
	
	ABMatrix dm = new ABMatrix();
	ABMatrix am = new ABMatrix();
	ABMatrix mm = new ABMatrix();
	
	public void testSatSimple() {
		dm.matrix = new double[5][5];
		am.matrix = new double[5][5];
		mm.matrix = new double[5][5];
		dm.M = 5;
		am.M = 5;
		mm.M = 5;
		for (int i=0; i<5; i++) {
			for (int j=0; j<5; j++)
			{
				dm.matrix[i][j] = Double.POSITIVE_INFINITY;
			}
		}
		dm.matrix[1][0] = 5; // x-y >= 5
		dm.matrix[0][1] = -10; // -x+y >= -10
		dm.M = 5;
		
		csce913proj1.CdbTuple t = new csce913proj1.CdbTuple(dm, am, mm, new String[] {"x", "y", "z", "x1", "z1"});
		boolean flag = t.satisfiable();
		Assert.assertTrue(flag);
	}
	
	public void testUnsatSimple()
	{
		dm.matrix = new double[5][5];
		am.matrix = new double[5][5];
		mm.matrix = new double[5][5];
		dm.M = 5;
		am.M = 5;
		mm.M = 5;
		//unsat testing
		for (int i=0; i<5; i++)
			for (int j=0; j<5; j++)
			{
				dm.matrix[i][j] = Double.POSITIVE_INFINITY;
			}
		dm.matrix[1][0] = 12; // x-y >= 12
		dm.matrix[0][1] = -10; // -x+y >= -10
		dm.M = 5;
		
		CdbTuple t = new CdbTuple(dm, am, mm, new String[] {"x", "y", "z", "x1", "z1"});
		boolean flag = t.satisfiable();
		Assert.assertTrue(!flag);
	}
	
	public void testSat2() {
        dm.matrix = new double[5][5];
        am.matrix = new double[5][5];
        mm.matrix = new double[5][5];
        dm.M = 5;
        am.M = 5;
        mm.M = 5;
        // Initialize matrices with positive infinity weights
        for (int i=0; i<5; i++) {
            for (int j=0; j<5; j++) {
            dm.matrix[i][j] = Double.POSITIVE_INFINITY;
            am.matrix[i][j] = Double.POSITIVE_INFINITY;
            mm.matrix[i][j] = Double.POSITIVE_INFINITY;
            }
        }
        
        //Set of SATISFIABLE addition constraints
        dm.matrix[2][3] = 10;    // -x+y <= 10
        dm.matrix[4][2] = -5;    //  x-z <= -5
        dm.matrix[0][1] = 0;     //    w <= 0
        dm.matrix[1][0] = 3;     //   -w <= 3
        am.matrix[1][2] = 6;  //  w+x <= 6
        mm.matrix[4][3] = 0;  // -y-z <= 0
        
        
        
        CdbTuple t = new CdbTuple(dm, am, mm, new String[] {"0", "w", "x", "y", "z"});
        boolean flag = t.satisfiable();
        assert(flag==true);
	}
	
	public void testUnsat2() {
        dm.matrix = new double[5][5];
        am.matrix = new double[5][5];
        mm.matrix = new double[5][5];
        dm.M = 5;
        am.M = 5;
        mm.M = 5;
        // Initialize matrices with positive infinity weights
        for (int i=0; i<5; i++) {
            for (int j=0; j<5; j++) {
            dm.matrix[i][j] = Double.POSITIVE_INFINITY;
            am.matrix[i][j] = Double.POSITIVE_INFINITY;
            mm.matrix[i][j] = Double.POSITIVE_INFINITY;
            }
        }
        
        // Set of UNSATISFIABLE addition constraints
        dm.matrix[4][2] = -3;    // x-z <= -3
        dm.matrix[4][3] = 8;     // y-z <= 8
        dm.matrix[3][1] = 2;     // w-y <= 2
        dm.matrix[2][1] = -4;    // w-x <= -4
        dm.matrix[1][0] = -40;   // -w <= -40
        dm.matrix[0][4] = 20;    // z <= 20
        
        CdbTuple t = new CdbTuple(dm, am, mm, new String[] {"0", "w", "x", "y", "z"});
        boolean flag = t.satisfiable();
        assert(flag==true);
	}
	
	public void testSat3() {
		dm.matrix = new double[3][3];
       	am.matrix = new double[3][3];
	    mm.matrix = new double[3][3];
	    dm.M = 3;
	    am.M = 3;
	    mm.M = 3;
	    // Initialize matrices with positive infinity weights
	    for (int i=0; i<3; i++) {
	        for (int j=0; j<3; j++) {
	        dm.matrix[i][j] = Double.POSITIVE_INFINITY;
	        am.matrix[i][j] = Double.POSITIVE_INFINITY;
	        mm.matrix[i][j] = Double.POSITIVE_INFINITY;
	        }
	    }
	    
	    // Set of UNSATISFIABLE addition constraints
	    dm.matrix[2][1] = 10;    // x-y >= 10
	    dm.matrix[1][2] = -10;   // y-x >= -10
	    am.matrix[1][2] = 10;    // x+y >= 10
	    	    
	    CdbTuple t = new CdbTuple(dm, am, mm, new String[] {"0", "w", "x", "y", "z"});
	    boolean flag = t.satisfiable();
	    assert(flag==true);
	}

}
