public class JobScheduling {

    private static int NR_OF_JOBS = 12;

    private static int MINIMIZE_A = 59;
    private static int MINIMIZE_B = 65;

    private static void assignmentA() {
        System.out.println("(benchmark job_scheduling_a.smt");
        System.out.println(":logic QF_UFLIA");
        System.out.println(":extrafuns (");
        print_predicates();
        System.out.println(")");
        System.out.println(":formula (and ");
        print_formula(MINIMIZE_A);
        System.out.println("))");
    }

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

    private static void print_predicates() {
        for(int i = 1; i <= NR_OF_JOBS; i++) {
            System.out.println("(j" + i + " Int)");
        }
    }

    private static void print_formula(int minimize) {
        for(int i = 1; i <= NR_OF_JOBS; i++) {
            System.out.println("(<= (+ j" + i + " " + (i + 5) + ") " + minimize + ")");
        }

        for(int i = 1; i <= NR_OF_JOBS; i++) {
            System.out.println("(>= j" + i + " 0)");
        }
        System.out.println("(and (>= j3 (+ j1 6)) (>= j3 (+ j2 7)))");
        System.out.println("(and (>= j5 (+ j3 8)) (>= j5 (+ j4 9)))");
        System.out.println("(and (>= j7 (+ j3 8)) (>= j7 (+ j4 9)) (>= j7 (+ j6 11)))");
        System.out.println("(>= j8 j5)");
        System.out.println("(and (>= j9 (+ j5 10)) (>= j9 (+ j8 13)))");
        System.out.println("(>= j11 (+ j10 15))");
        System.out.println("(and (>= j12 (+ j9 14)) (>= j12 (+ j11 16)))");

        /* 5,7 and 10 resource thingy */
        int[] smallset = {5, 7, 10};
        for(int i : smallset) {
            for(int j : smallset) {
                if(i == j) continue;
                System.out.println("(=> (<= j" + i + " j" + j + ") (<= (+ j" + i + " " + (i + 5) + ") j" + j + "))");
            }
        }
    }

    private static void print_formula_b() {
        System.out.println("(>= j6 j12)");
        System.out.println("(<= (+ j6 11) (+ j12 17))");
    }

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