ar/assignments/src/2.py

   1 #!/usr/bin/env python3
   2
   3 pc = [(4, 22), (4, 22), (4, 22)]
   4 rc = [(9, 7), (12, 6), (10, 7), (18, 5), (20, 4), (10, 6), (8, 6), (10, 8)]
   5
   6 ##Print preamble
   7 print("(benchmark a4.smt")
   8 print(":logic QF_UFLIA")
   9
  10 ##Print variables
  11 print(":extrafuns (")
  12 for i, (w, h) in enumerate(pc+rc, 1):
  13     print("(c{:02d}x Int)".format(i), end=' ')
  14     print("(c{:02d}y Int)".format(i), end=' ')
  15     print("(c{:02d}w Int)".format(i), end=' ')
  16     print("(c{:02d}h Int)".format(i), end=' ')
  17 print(")")
  18
  19 ##Preamble2
  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((
  27         '\t(or '
  28         '(and (= c{0:02d}w {1}) (= c{0:02d}h {2})) '
  29         '(and (= c{0:02d}w {2}) (= c{0:02d}h {1}))'
  30         ')').format(i, w, h))
  31
  32     ##Print the bounds of the coordinates
  33     print((
  34         '\t(> c{0:02d}x 0) (> c{0:02d}y 0)\n'
  35         '\t(<= (+ c{0:02d}x c{0:02d}w) 29) (<= (+ c{0:02d}y c{0:02d}h) 22)\n'
  36         ).format(i, w, h))
  37
  38     ##Print the non overlap with others
  39     for j in range(1, 1+len(pc+rc)):
  40         print((
  41             '\t(or (= {0} {1})\n'
  42             '\t\t(> c{0:02d}x (+ c{1:02d}x c{1:02d}w)) '
  43             '(< (+ c{0:02d}x c{0:02d}w) c{1:02d}x)\n'
  44             '\t\t(> c{0:02d}y (+ c{1:02d}y c{1:02d}h)) '
  45             '(< (+ c{0:02d}y c{0:02d}h) c{1:02d}y)'
  46             ')').format(i, j))
  47
  48 ##Print the PC distance to eachother
  49 for i, _ in enumerate(pc, 1):
  50     for j, _ in enumerate(pc, 1):
  51         print((
  52             '\t(or (= {0} {1})\n'
  53             '\t\t(> (- (/ (+ c{0:02d}x c{0:02d}w) 2) (/ (+ c{1:02d}x c{1:02d}w) 2)) 17)\n'
  54             '\t\t(> (- (/ (+ c{1:02d}x c{1:02d}w) 2) (/ (+ c{0:02d}x c{0:02d}w) 2)) 17)\n'
  55             '\t\t(> (- (/ (+ c{0:02d}y c{0:02d}h) 2) (/ (+ c{1:02d}y c{1:02d}h) 2)) 17)\n'
  56             '\t\t(> (- (/ (+ c{1:02d}y c{1:02d}h) 2) (/ (+ c{0:02d}y c{0:02d}h) 2)) 17)'
  57             ')').format(i, j))
  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('\t(or')
  62     for j, _ in enumerate(pc, 1):
  63         print((
  64             '\t\t(= c{0:02d}x (+ c{1:02d}x c{1:02d}w 1))\n'
  65             '\t\t(= (+ c{0:02d}x c{0:02d}w 1) c{1:02d}x)\n'
  66             '\t\t(= c{0:02d}y (+ c{1:02d}y c{1:02d}h 1))\n'
  67             '\t\t(= (+ c{0:02d}y c{0:02d}h 1) c{1:02d}y)'
  68             ).format(i, j))
  69     print('\t)')
  70
  71 ## Close the and,benchmark parenthesis
  72 print("))")