ar/assignments/src/2.py

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