--- /dev/null
+#!/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("))")