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 preamble
  22 print('(benchmark a4.smt')
  23 print(':logic QF_UFLIA')
  24
  25 # Print variables
  26 print(':extrafuns (')
  27 for i in J:
  28     print('(j{} Int)'.format(i), end=' ')
  29 print('\n)')
  30
  31 print(':formula')
  32 print('(and')
  33 for i in J:
  34     # Make sure the times are positive and within the bound
  35     print('(> j{0} 0) (<= (+ j{0} {0}) {1})'.format(i, maxjobstart))
  36     # Make sure the dependencies are done when a task is scheduled
  37     for k in pi.get(i, {}):
  38         print('(>= j{0} (+ j{1} {1}))'.format(i, k))
  39 # Make sure the shared resources are not used by two tasks at once
  40 for i in Jprime:
  41     for k in Jprime:
  42         if i != k:
  43             print('(or (>= j{0} (+ j{1} {1}))'.format(i, k), end=' ')
  44             print('(<= (+ j{0} {0}) j{1}))'.format(i, k))
  45
  46 # Close the and,benchmark parenthesis
  47 print('))')