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