public class ChipDesign {

    private static final int CHIP_HEIGHT = 30;
    private static final int CHIP_WIDTH = 30;

    private static final int NR_OF_COMPONENTS = 10;

    private static final int X = 0;
    private static final int Y = 1;

    private static final int NR_OF_POWER_COMPONENTS = 4;
    private static final int[] POWER_COMPONENT = {4, 3};

    private static final int[][] COMPONENTS = {
            {4, 5},
            {4, 6},
            {5, 20},
            {6, 9},
            {6, 10},
            {6, 11},
            {7, 8},
            {7, 12},
            {10, 10},
            {10, 20}
    };

    private static void print_predicates() {
        for(int i = 0; i < NR_OF_COMPONENTS; i++) {
            System.out.println("(Cx" + i + " Int) (Cy" + i + " Int)");
            System.out.println("(Cr" + i + ")");
        }
        for(int i = 0; i < NR_OF_POWER_COMPONENTS; i++) {
            System.out.println("(PCx" + i + " Int) (PCy" + i + " Int)");
            System.out.println("(PCr" + i + ")");
        }
    }

    private static void print_formula() {
        for(int i = 0; i < NR_OF_COMPONENTS; i++) {
            System.out.println("(>= Cx" + i + " 0) (>= Cy" + i + " 0)");
            System.out.println("(<= (+ Cx" + i + " (ite (Cr" + i + ") " + COMPONENTS[i][Y] + " " + COMPONENTS[i][X] + ")) " + CHIP_WIDTH + ") (<= (+ Cy" + i + " (ite (Cr" + i + ") " + COMPONENTS[i][X] + " " + COMPONENTS[i][Y] + ")) " + CHIP_HEIGHT + ")");
        }
        for(int i = 0; i < NR_OF_POWER_COMPONENTS; i++) {
            System.out.println("(>= PCx" + i + " 0) (>= PCy" + i + " 0)");
            System.out.println("(<= (+ PCx" + i + " (ite (PCr" + i + ") " + COMPONENTS[i][Y] + " " + COMPONENTS[i][X] + ")) " + CHIP_WIDTH + ") (<= (+ PCy" + i + " (ite (PCr" + i + ") " + COMPONENTS[i][X] + " " + COMPONENTS[i][Y] + ")) " + CHIP_HEIGHT + ")");
        }

        /* Non-overlap constraint? It is not in the pdf, but it'd be weird if overlap was allowed */

        /* Power requirement (connected edge) */

        /* Heat production limit */
        for(int i = 0; i < NR_OF_POWER_COMPONENTS; i++) {
            for(int j = i + 1; j < NR_OF_POWER_COMPONENTS; j++) {
                if(i == j) continue;
                System.out.println("(or (> (- PCx" + i + " PCx" + j + ") 17) (> (- PCy" + i + " PCy" + j + ") 17) (> (- PCx" + j + " PCx" + i + ") 17) (> (- PCy" + j + " PCy" + i + ") 17))");
            }
        }
    }

	public static void main(String... args) {
		System.out.println("(benchmark chip_design.smt");
		System.out.println(":logic QF_UFLIA");
		System.out.println(":extrafuns (");
		print_predicates();
		System.out.println(")");
		System.out.println(":formula (and ");
		print_formula();
		System.out.println("))");
	}
}