Correct format, just runs too slow...

6 files changed, 181 insertions, 0 deletions

diff --git a/.gitignore b/.gitignore
index 14cf9c4..36f9ba7 100644
--- a/.gitignore
+++ b/.gitignore
@@ -8,3 +8,4 @@
 *.vrb
 .*.sw?
 *.pdf
+*.dvi
diff --git a/chip_design.z3 b/chip_design/chip_design.z3
index e69de29..e69de29 100644
--- a/chip_design.z3
+++ b/chip_design/chip_design.z3
diff --git a/integer_sum_from_neighbours.z3 b/integer_sum_from_neighbours/integer_sum_from_neighbours.z3
index e69de29..e69de29 100644
--- a/integer_sum_from_neighbours.z3
+++ b/integer_sum_from_neighbours/integer_sum_from_neighbours.z3
diff --git a/job_scheduling.z3 b/job_scheduling/job_scheduling.z3
index e69de29..e69de29 100644
--- a/job_scheduling.z3
+++ b/job_scheduling/job_scheduling.z3
diff --git a/packing_pallets_in_trucks.z3 b/packing_pallets_in_trucks.z3
deleted file mode 100644
index e69de29..0000000
--- a/packing_pallets_in_trucks.z3
+++ /dev/null
diff --git a/packing_pallets_in_trucks/src/nl/tue/PackingPallets.java b/packing_pallets_in_trucks/src/nl/tue/PackingPallets.java
new file mode 100644
index 0000000..0d2afc1
--- /dev/null
+++ b/packing_pallets_in_trucks/src/nl/tue/PackingPallets.java
@@ -0,0 +1,180 @@
+package nl.tue;
+
+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 = 5;
+    private static final int NR_OF_PRITTLES_B = 5;
+    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(")))");
+        }
+    }
+	
+	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;
+        }
+    }
+}