ar finished

[master.git] / ar / assignment1 / src / a3.py

diff --git a/ar/assignment1/src/a3.py b/ar/assignment1/src/a3.py
new file mode 100644 (file)
index 0000000..7d79135
--- /dev/null
+++ b/ar/assignment1/src/a3.py
@@ -0,0 +1,47 @@
+#!/usr/bin/env python3
+import sys
+
+if len(sys.argv) != 2:
+    print('usage: {} maxjobstart'.format(sys.argv[0]))
+    exit()
+
+maxjobstart = sys.argv[1]
+jobs = 12
+J = range(1, jobs+1)
+Jprime = {5, 7, 10}
+pi = {
+    3: {1, 2},
+    5: {3, 4},
+    7: {3, 4, 6},
+    9: {5, 8},
+    11: {10},
+    12: {9, 11}
+}
+
+# Print preamble
+print('(benchmark a4.smt')
+print(':logic QF_UFLIA')
+
+# Print variables
+print(':extrafuns (')
+for i in J:
+    print('(j{} Int)'.format(i), end=' ')
+print('\n)')
+
+print(':formula')
+print('(and')
+for i in J:
+    # Make sure the times are positive and within the bound
+    print('(> j{0} 0) (<= (+ j{0} {0}) {1})'.format(i, maxjobstart))
+    # Make sure the dependencies are done when a task is scheduled
+    for k in pi.get(i, {}):
+        print('(>= j{0} (+ j{1} {1}))'.format(i, k))
+# Make sure the shared resources are not used by two tasks at once
+for i in Jprime:
+    for k in Jprime:
+        if i != k:
+            print('(or (>= j{0} (+ j{1} {1}))'.format(i, k), end=' ')
+            print('(<= (+ j{0} {0}) j{1}))'.format(i, k))
+
+# Close the and,benchmark parenthesis
+print('))')