public class PackingPallets {

    private static final int NR_OF_TRUCKS = 8;
    private static final int NR_OF_COOLING_TRUCKS = 3;
    private static final int TRUCK_CAPACITY = 8000;
    private static final int TRUCK_PALLET_CAPACITY = 8;

    private static final int NR_OF_NUZZLES = 4;
    private static final int NUZZLES_WEIGHT = 700;

    private static final int NR_OF_PRITTLES_A = 32;
    private static final int NR_OF_PRITTLES_B = 32;
    private static final int PRITTLES_WEIGHT = 400;

    private static final int NR_OF_SKIPPLES = 8;
    private static final int SKIPPLES_WEIGHT = 1000;

    private static final int NR_OF_CROTTLES = 10;
    private static final int CROTTLES_WEIGHT = 2500;

    private static final int NR_OF_DUPPLES = 20;
    private static final int DUPPLES_WEIGHT = 200;

    private static void assignmentA() {
        System.out.println("(benchmark packing_pallets_a.smt");
        System.out.println(":logic QF_UFLIA");
        System.out.println(":extrafuns (");
        print_predicates(NR_OF_PRITTLES_A);
        System.out.println(")");
        System.out.print(":formula (");
        print_formula(NR_OF_PRITTLES_A);
        System.out.println("))");
    }

    private static void assignmentB() {
        System.out.println("(benchmark packing_pallets_b.smt");
        System.out.println(":logic QF_UFLIA");
        System.out.println(":extrafuns (");
        print_predicates(NR_OF_PRITTLES_B);
        System.out.println(")");
        System.out.print(":formula (");
        print_formula(NR_OF_PRITTLES_B);
        print_formula_b(NR_OF_PRITTLES_B);
        System.out.println("))");
    }

    private static void print_predicates(int prittles) {
        for(int i = 1; i <= NR_OF_NUZZLES; i++) {
            System.out.print("(n" + i + " Int) ");
        }
        System.out.println();
        for(int i = 1; i <= prittles; i++) {
            System.out.print("(p" + i + " Int) ");
        }
        System.out.println();
        for(int i = 1; i <= NR_OF_SKIPPLES; i++) {
            System.out.print("(s" + i + " Int) ");
        }
        System.out.println();
        for(int i = 1; i <= NR_OF_CROTTLES; i++) {
            System.out.print("(c" + i + " Int) ");
        }
        System.out.println();
        for(int i = 1; i <= NR_OF_DUPPLES; i++) {
            System.out.print("(d" + i + " Int) ");
        }
        System.out.println();
    }

    private static void print_formula(int prittles) {
        /* valid truck assignment */
        System.out.println("and ");
        for(int i = 1; i <= NR_OF_NUZZLES; i++) {
            System.out.print("(<= n" + i + " " + NR_OF_TRUCKS +") (> n" + i + " 0) ");
        }
        System.out.println();
        for(int i = 1; i <= prittles; i++) {
            System.out.print("(<= p" + i + " " + NR_OF_TRUCKS +") (> p" + i + " 0) ");
        }
        System.out.println();
        for(int i = 1; i <= NR_OF_SKIPPLES; i++) {
            System.out.print("(<= s" + i + " " + NR_OF_COOLING_TRUCKS +") (> s" + i + " 0) ");
        }
        System.out.println();
        for(int i = 1; i <= NR_OF_CROTTLES; i++) {
            System.out.print("(<= c" + i + " " + NR_OF_TRUCKS +") (> c" + i + " 0) ");
        }
        System.out.println();
        for(int i = 1; i <= NR_OF_DUPPLES; i++) {
            System.out.print("(<= d" + i + " " + NR_OF_TRUCKS +") (> d" + i + " 0) ");
        }
        System.out.println();

        /* assignment constraints */
        for(int j = 1; j <= NR_OF_TRUCKS; j++) {
            System.out.println("(< (+ ");
            for(int i = 1; i <= NR_OF_NUZZLES; i++) {
                System.out.print("(ite (= n" + i + " " + j + ") " + NUZZLES_WEIGHT + " 0)" );
            }
            System.out.println();
            for(int i = 1; i <= prittles; i++) {
                System.out.print("(ite (= p" + i + " " + j + ") " + PRITTLES_WEIGHT + " 0) ");
            }
            System.out.println();
            for(int i = 1; i <= NR_OF_SKIPPLES; i++) {
                System.out.print("(ite (= s" + i + " " + j + ") " + SKIPPLES_WEIGHT + " 0) ");
            }
            System.out.println();
            for(int i = 1; i <= NR_OF_CROTTLES; i++) {
                System.out.print("(ite (= c" + i + " " + j + ") " + CROTTLES_WEIGHT + " 0) ");
            }
            System.out.println();
            for(int i = 1; i <= NR_OF_DUPPLES; i++) {
                System.out.print("(ite (= d" + i + " " + j + ") " + DUPPLES_WEIGHT + " 0) ");
            }
            System.out.println(") " + TRUCK_CAPACITY + ")");
        }

        for(int j = 1; j <= NR_OF_TRUCKS; j++) {
            System.out.println("(< (+ ");
            for(int i = 1; i <= NR_OF_NUZZLES; i++) {
                System.out.print("(ite (= n" + i + " " + j + ") 1 0) ");
            }
            System.out.println();
            for(int i = 1; i <= prittles; i++) {
                System.out.print("(ite (= p" + i + " " + j + ") 1 0) ");
            }
            System.out.println();
            for(int i = 1; i <= NR_OF_SKIPPLES; i++) {
                System.out.print("(ite (= s" + i + " " + j + ") 1 0) ");
            }
            System.out.println();
            for(int i = 1; i <= NR_OF_CROTTLES; i++) {
                System.out.print("(ite (= c" + i + " " + j + ") 1 0) ");
            }
            System.out.println();
            for(int i = 1; i <= NR_OF_DUPPLES; i++) {
                System.out.print("(ite (= d" + i + " " + j + ") 1 0) ");
            }
            System.out.println(") " + TRUCK_PALLET_CAPACITY + ")");
        }

        for(int i = 1; i <= NR_OF_NUZZLES; i++) {
            for(int j = i + 1; j <= NR_OF_NUZZLES; j++ ) {
                System.out.println("(not (= n" + i + " n" + j +"))");
            }
        }
    }

    private static void print_formula_b(int prittles) {
        for(int i = 1; i <= NR_OF_TRUCKS; i++) {
            System.out.print("(=> (or ");
            for(int j = 1; j <= prittles; j++) {
                System.out.print("(= p" + j + " " + i + ") ");
            }
            System.out.print(") (not (or ");
            for(int j = 1; j <= NR_OF_CROTTLES; j++) {
                System.out.print("(= c" + j + " " + i + ") ");
            }
            System.out.println(")))");

            System.out.print("(=> (or ");
            for(int j = 1; j <= NR_OF_CROTTLES; j++) {
                System.out.print("(= c" + j + " " + i + ") ");
            }
            System.out.print(") (not (or ");
            for(int j = 1; j <= prittles; j++) {
                System.out.print("(= p" + j + " " + i + ") ");
            }
            System.out.println(")))");
        }
    }
	
	public static void main(String... args) {
        assert(args.length > 0);
        switch(args[0]) {
            case "a":
                assignmentA();
                break;
            case "b":
                assignmentB();
                break;
            default:
                System.err.println("Specify assignment a or b!");
                break;
        }
    }
}