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 = 22;
    private static final int NR_OF_PRITTLES_B = 19;
    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 final int OFFSET_NUZZLES = 0;
    private static final int OFFSET_SKIPPLES = OFFSET_NUZZLES + NR_OF_NUZZLES;
    private static final int OFFSET_CROTTLES = OFFSET_SKIPPLES + NR_OF_SKIPPLES;
    private static final int OFFSET_DUPPLES = OFFSET_CROTTLES + NR_OF_CROTTLES;
    private static final int OFFSET_PRITTLES = OFFSET_DUPPLES + NR_OF_DUPPLES;

    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 (and ");
        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 (and ");
        print_formula(NR_OF_PRITTLES_B);
        print_formula_b(NR_OF_PRITTLES_B);
        System.out.println("))");
    }

    private static void print_predicates(int prittles) {
        System.out.print("(N Int Int) ");
        System.out.print("(Ns Int Int) ");
        System.out.print("(P Int Int) ");
        System.out.print("(Ps Int Int) ");
        System.out.print("(S Int Int) ");
        System.out.print("(Ss Int Int) ");
        System.out.print("(C Int Int) ");
        System.out.print("(Cs Int Int) ");
        System.out.print("(D Int Int) ");
        System.out.print("(Ds Int Int) ");
        System.out.print("(Trucks Int Int Int) ");
        System.out.print("(Weight Int Int)");
    }

    private static void print_formula(int prittles) {
        /* valid truck assignment */
        System.out.println("(<= " + (NR_OF_NUZZLES + prittles + NR_OF_SKIPPLES + NR_OF_CROTTLES + NR_OF_DUPPLES) + " " + (NR_OF_TRUCKS * TRUCK_PALLET_CAPACITY) + ")");
        for(int i = 1; i <= NR_OF_NUZZLES; i++) {
            System.out.print("(<= (N " + i + ") " + NR_OF_TRUCKS +") (> (N " + i + ") 0) ");
            System.out.print("(<= (Ns " + i + ") " + TRUCK_PALLET_CAPACITY +") (> (Ns " + i + ") 0) ");
            System.out.print("(= (Weight " + (OFFSET_NUZZLES + i) + ") " + NUZZLES_WEIGHT + ")");
        }
        System.out.println();
        for(int i = 1; i <= prittles; i++) {
            System.out.print("(<= (P " + i + ") " + NR_OF_TRUCKS +") (> (P " + i + ") 0) ");
            System.out.print("(<= (Ps " + i + ") " + TRUCK_PALLET_CAPACITY +") (> (Ps " + i + ") 0) ");
            System.out.print("(= (Weight " + (OFFSET_PRITTLES + i) + ") " + PRITTLES_WEIGHT + ")");
        }
        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.print("(<= (Ss " + i + ") " + TRUCK_PALLET_CAPACITY +") (> (Ss " + i + ") 0) ");
            System.out.print("(= (Weight " + (OFFSET_SKIPPLES + i) + ") " + SKIPPLES_WEIGHT + ")");
        }
        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.print("(<= (Cs " + i + ") " + TRUCK_PALLET_CAPACITY +") (> (Cs " + i + ") 0) ");
            System.out.print("(= (Weight " + (OFFSET_CROTTLES + i) + ") " + CROTTLES_WEIGHT + ")");
        }
        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.print("(<= (Ds " + i + ") " + TRUCK_PALLET_CAPACITY +") (> (Ds " + i + ") 0) ");
            System.out.print("(= (Weight " + (OFFSET_DUPPLES + i) + ") " + DUPPLES_WEIGHT + ")");
        }
        System.out.println();

        /* assignment constraints */
        for(int j = 1; j <= NR_OF_TRUCKS; j++) {
            System.out.println("(<= (+ ");
            for (int i = 1; i <= TRUCK_PALLET_CAPACITY; i++) {
                System.out.print("(Weight (Trucks " + j + " " + i + "))");
            }
            System.out.println(") " + TRUCK_CAPACITY + ")");
        }

        for(int i = 1; i <= NR_OF_TRUCKS; i++) {
            for(int j = 1; j <= TRUCK_PALLET_CAPACITY; j++) {
                System.out.println("(<= (Trucks " + i + " " + j + ") " + (OFFSET_PRITTLES + prittles) + ")");
                System.out.println("(>= (Trucks " + i + " " + j + ") 0)");
            }
        }
        System.out.println("(= (Weight 0) 0)");

        /**** NEEDS REWRITING ****/
        for(int i = 1; i <= NR_OF_NUZZLES; i++) {
            System.out.println("(= (Trucks (N " + i + ") (Ns " + i + ")) " + (OFFSET_NUZZLES + i) + ") ");
        }
        for(int i = 1; i <= prittles; i++) {
            System.out.println("(= (Trucks (P " + i + ") (Ps " + i + ")) " + (OFFSET_PRITTLES + i) + ") ");
        }
        for (int i = 1; i <= NR_OF_SKIPPLES; i++) {
            System.out.println("(= (Trucks (S " + i + ") (Ss " + i + ")) " + (OFFSET_SKIPPLES + i) + ") ");
        }
        for (int i = 1; i <= NR_OF_CROTTLES; i++) {
            System.out.println("(= (Trucks (C " + i + ") (Cs " + i + ")) " + (OFFSET_CROTTLES + i) + ") ");
        }
        for (int i = 1; i <= NR_OF_DUPPLES; i++) {
            System.out.println("(= (Trucks (D " + i + ") (Ds " + i + ")) " + (OFFSET_DUPPLES + i) + ") ");
        }
        /**** NEEDS REWRITING ****/

        System.out.print("(distinct");
        for(int i = 1; i <= NR_OF_NUZZLES; i++) {
            System.out.print(" (N " + i + ")");
        }
        System.out.println(")");
    }

    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;
        }
    }
}