cleaned up old directory
[master.git] / ar / assignments / src / a3.py
diff --git a/ar/assignments/src/a3.py b/ar/assignments/src/a3.py
deleted file mode 100644 (file)
index a295c8d..0000000
+++ /dev/null
@@ -1,47 +0,0 @@
-#!/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("))")