blob: ebe8d009afe803babc84cc0778aa5ad0393c7e7d (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
|
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;
}
}
}
|
