From 8c3efd1ed40f51115a3766248dcff62cf9e3f12d Mon Sep 17 00:00:00 2001 From: Koen van der Heijden Date: Sun, 11 Dec 2016 17:16:19 +0100 Subject: Correct format, just runs too slow... --- .gitignore | 1 + chip_design.z3 | 0 chip_design/chip_design.z3 | 0 integer_sum_from_neighbours.z3 | 0 .../integer_sum_from_neighbours.z3 | 0 job_scheduling.z3 | 0 job_scheduling/job_scheduling.z3 | 0 packing_pallets_in_trucks.z3 | 0 .../src/nl/tue/PackingPallets.java | 180 +++++++++++++++++++++ 9 files changed, 181 insertions(+) delete mode 100644 chip_design.z3 create mode 100644 chip_design/chip_design.z3 delete mode 100644 integer_sum_from_neighbours.z3 create mode 100644 integer_sum_from_neighbours/integer_sum_from_neighbours.z3 delete mode 100644 job_scheduling.z3 create mode 100644 job_scheduling/job_scheduling.z3 delete mode 100644 packing_pallets_in_trucks.z3 create mode 100644 packing_pallets_in_trucks/src/nl/tue/PackingPallets.java 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.z3 deleted file mode 100644 index e69de29..0000000 diff --git a/chip_design/chip_design.z3 b/chip_design/chip_design.z3 new file mode 100644 index 0000000..e69de29 diff --git a/integer_sum_from_neighbours.z3 b/integer_sum_from_neighbours.z3 deleted file mode 100644 index e69de29..0000000 diff --git a/integer_sum_from_neighbours/integer_sum_from_neighbours.z3 b/integer_sum_from_neighbours/integer_sum_from_neighbours.z3 new file mode 100644 index 0000000..e69de29 diff --git a/job_scheduling.z3 b/job_scheduling.z3 deleted file mode 100644 index e69de29..0000000 diff --git a/job_scheduling/job_scheduling.z3 b/job_scheduling/job_scheduling.z3 new file mode 100644 index 0000000..e69de29 diff --git a/packing_pallets_in_trucks.z3 b/packing_pallets_in_trucks.z3 deleted file mode 100644 index e69de29..0000000 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; + } + } +} -- cgit v1.2.1