import java.applet.Applet;
import java.awt.*;
import java.awt.event.*;
import java.applet.*;
import java.awt.geom.*;
import java.math.*;


/*This file does calculation 4*/


public class ProofCalc4 {

    public static void main(Manager M) {
	for(int i=0;i<8;++i) M.C.MESSAGE[i]="";
	M.C.MESSAGE[0]="start calc 4";
	M.C.MESSAGE[1]="start order-2 test";
	M.C.repaint();
	test1();
	M.C.MESSAGE[1]="order-2 test done";

	M.C.MESSAGE[2]="start main test";
	M.C.repaint();
	test2(M);
	M.C.MESSAGE[5]="main  test done";
	M.C.MESSAGE[6]="calc 4 done";
	M.C.repaint();

    }

    public static void fail() {
	throw new ProofException("calc 4 fails");
    }



    /*Here is 6 times the 420-scaled volume of the trivial tile
      from 1/2 to 3/4. This is computed in the VolumeComputer file.*/

    public static long volumeTrivial() {
	return(157437000);
    }

    public static LongPolyhedron phi(LongPolyhedron P) {
	long x=0;
	for(int i=0;i<P.count;++i) x=x+P.V[i].x[0];
	int hand=0;
	if(x>0) hand=1;
	LongPolyhedron Q=new LongPolyhedron(P);
	for(int i=0;i<Q.count;++i) Q.V[i]=phi(hand,P.V[i]);
	Q.SCALE=P.SCALE;
	Q.FACE=P.FACE;
	return(Q);
    }

    public static LongVector phi(int hand,LongVector V) {
	LongVector W=new LongVector(V);
	W.x[2]=420-V.x[2];
	long u=420-2*V.x[2];
	if(hand==0) {
            W.x[0]=V.x[0]-u;
	    W.x[1]=V.x[1]-u;
	}
	if(hand==1) {
	    W.x[0]=V.x[0]+u;
	    W.x[1]=V.x[1]+u;
	}
	return(W);
    }

/*Checks the order 2 tile on the interval [3/4,1].
  We precompute the desired polyhedron separately in this case.*/
    public static void test1() {
        LongPolyhedron Q1=DataPartitionExtra.order2A();
        LongPolyhedron Q2=ProofSupport.F2(Q1);
        boolean test1=isOutside(Q1);
        LongPolyhedron Q3=ProofSupport.F2(Q2);
        boolean test2=isOutside(Q2);
        boolean test3=LongPolyCombinatorics.isSubset(Q3,Q1);
	if(test1==false) fail();
	if(test2==false) fail();
	if(test3==false) fail();
    }




    /*The target is the volume of the domain from 1/2 to 3/4.
      This is the bulk of the calculation.*/

    public static void test2(Manager M) {
	long total=0;
	long target=277830000L;
	for(int i=1;i<19;++i) {
	    LongPolyhedron P0=DataPartition.poly(i);
	    LongPolyhedron P1=DataPartition.imagePoly(i);
	    int test=checkReturn(P0,P1);
	    total=total+test*DataPartition.volume(i);
	}

	total=total+volumeTrivial();  //vol of trivial tile in [1/2,3/4]
	if(total!=target) fail();
	Long T1=new Long(total);
	Long T2=new Long(target);
	M.C.MESSAGE[2]="volume check";
	M.C.MESSAGE[3]= T1.toString();
	M.C.MESSAGE[4]= T2.toString();
    }


    public static int checkReturn(LongPolyhedron P0,LongPolyhedron P1) {
	boolean test=false;
	int count=0;
	LongPolyhedron Q0=phi(P0);
	LongPolyhedron Q1=phi(P1);
	while(test==false) {    
	    ++count;
	    Q1=ProofSupport.F1(Q1);
	    boolean test1=isOutside(Q1);
	    boolean test2=LongPolyCombinatorics.isSubset(Q1,Q0);
	    if((test1==false)&&(test2==false)) System.out.println("fail");
	    if(test2==true) return(count);
	}
	return(-1);
    }

    public static boolean isOutside(LongPolyhedron P) {
	for(int i=1;i<19;++i) {
	    LongPolyhedron Q=phi(DataPartition.poly(i));
	    if(LongPolyCombinatorics.separate(10,P,Q)==false) return(false);
	}
	return(true);
    }


}