ar/assignment1/src/a3.py

   1 #!/usr/bin/env python3
   2 import sys
   3
   4 if len(sys.argv) != 2:
   5     print('usage: {} maxjobstart'.format(sys.argv[0]))
   6     exit()
   7
   8 maxjobstart = sys.argv[1]
   9 jobs = 12
  10 J = range(1, jobs+1)
  11 Jprime = {5, 7, 10}
  12 pi = {
  13     3: {1, 2},
  14     5: {3, 4},
  15     7: {3, 4, 6},
  16     9: {5, 8},
  17     11: {10},
  18     12: {9, 11}
  19 }
  20
  21 # Print variables and preamble
  22 print('(benchmark a4.smt')
  23 print(':logic QF_UFLIA')
  24 print(':extrafuns (')
  25 for i in J:
  26     print('(j{} Int)'.format(i), end=' ')
  27 print('\n)')
  28
  29 print(':formula')
  30 print('(and')
  31 for i in J:
  32     # Make sure the times are positive and within the bound
  33     print('(> j{0} 0) (<= (+ j{0} {0}) {1})'.format(i, maxjobstart))
  34     # Make sure the dependencies are done when a task is scheduled
  35     for k in pi.get(i, {}):
  36         print('(>= j{0} (+ j{1} {1}))'.format(i, k))
  37 # Make sure the shared resources are not used by two tasks at once
  38 for i in Jprime:
  39     for k in Jprime:
  40         if i != k:
  41             print('(or (>= j{0} (+ j{1} {1}))'.format(i, k), end=' ')
  42             print('(<= (+ j{0} {0}) j{1}))'.format(i, k))
  43
  44 # Close the and,benchmark parenthesis
  45 print('))')