ar/assignment1/src/a2.py

   1 #!/usr/bin/env python3
   2 pc = [(4, 2), (4, 2), (4, 2)]
   3 rc = [(9, 7), (12, 6), (10, 7), (18, 5), (20, 4), (10, 6), (8, 6), (10, 8)]
   4 mx = 29
   5 my = 22
   6 pd = 17
   7
   8
   9 # Print variables and preamble
  10 print('(benchmark a4.smt')
  11 print(':logic QF_UFLIA')
  12 print(':extrafuns (')
  13 for i, (w, h) in enumerate(pc+rc, 1):
  14     print('(c{}x Int)'.format(i), end=' ')
  15     print('(c{}y Int)'.format(i), end=' ')
  16     print('(c{}w Int)'.format(i), end=' ')
  17     print('(c{}h Int)'.format(i))
  18 print(')')
  19
  20 print(':formula')
  21 print('(and')
  22
  23 # Print the PC and RC subformulas
  24 for i, (w, h) in enumerate(pc+rc, 1):
  25     # Print the width and height
  26     print(('(or '
  27            '(and (= c{0}w {1}) (= c{0}h {2})) '
  28            '(and (= c{0}w {2}) (= c{0}h {1})))').format(i, w-1, h-1))
  29     # Print the bounds of the coordinates
  30     print(('(> c{0}x 0) (> c{0}y 0)'
  31            '(<= (+ c{0}x c{0}w) {1}) (<= (+ c{0}y c{0}h) {2})'
  32            ).format(i, mx, my))
  33
  34     # Print the non overlap with others
  35     for j in range(1, 1+len(pc+rc)):
  36         if i != j:
  37             print((
  38                  '(or '
  39                  '(> c{0}x (+ c{1}x c{1}w)) (< (+ c{0}x c{0}w) c{1}x) '
  40                  '(> c{0}y (+ c{1}y c{1}h)) (< (+ c{0}y c{0}h) c{1}y)'
  41                  ')').format(i, j))
  42
  43 # Print the PC distance to eachother
  44 for i, _ in enumerate(pc, 1):
  45     for j, _ in enumerate(pc, 1):
  46         if i != j:
  47             print(('(or '
  48                    '(> (- (+ c{0}x (/ c{0}w 2)) (+ c{1}x (/ c{1}w 2))) {2}) '
  49                    '(> (- (+ c{1}x (/ c{1}w 2)) (+ c{0}x (/ c{0}w 2))) {2}) '
  50                    '(> (- (+ c{0}y (/ c{0}h 2)) (+ c{1}y (/ c{1}h 2))) {2}) '
  51                    '(> (- (+ c{1}y (/ c{1}h 2)) (+ c{0}y (/ c{0}h 2))) {2})'
  52                    ')').format(i, j, pd))
  53
  54             # Print the constraint that they have to be connected to a ps
  55 for i, _ in enumerate(rc, 1+len(pc)):
  56     print('(or')
  57     for j, _ in enumerate(pc, 1):
  58         print(('(not (or '
  59                '(> c{0}x (+ c{1}x 1 c{1}w)) (< (+ c{0}x c{0}w) (- c{1}x 1)) '
  60                '(> c{0}y (+ c{1}y 1 c{1}h)) (< (+ c{0}y c{0}h) (- c{1}y 1))'
  61                '))').format(i, j))
  62     print(')')
  63
  64 # Close the and,benchmark parenthesis
  65 print('))')