src/a2.bash

   1 #!/bin/bash
   2 MAXX=29
   3 MAXY=22
   4 PD=17
   5 PC="1 2 3"
   6 RC="4 5 6 7 8 9 10 11"
   7
   8 function wp {
   9         case $1 in
  10                 1) echo 3;;
  11                 2) echo 3;;
  12                 3) echo 3;;
  13                 4) echo 8;;
  14                 5) echo 11;;
  15                 6) echo 9;;
  16                 7) echo 17;;
  17                 8) echo 19;;
  18                 9) echo 9;;
  19                 10) echo 7;;
  20                 11) echo 9;;
  21                 *);;
  22         esac
  23 }
  24
  25 function hp {
  26         case $1 in
  27                 1) echo 1;;
  28                 2) echo 1;;
  29                 3) echo 1;;
  30                 4) echo 6;;
  31                 5) echo 5;;
  32                 6) echo 6;;
  33                 7) echo 4;;
  34                 8) echo 3;;
  35                 9) echo 5;;
  36                 10) echo 5;;
  37                 11) echo 7;;
  38                 *);;
  39         esac
  40 }
  41
  42 function generate {
  43         local i j
  44         echo "(benchmark a4.smt"
  45         echo ":logic QF_UFLIA"
  46         echo ":extrafuns ("
  47         for i in $PC $RC; do
  48                 echo "(c${i}x Int) (c${i}y Int) (c${i}w Int) (c${i}h Int)"
  49         done
  50         echo ")"
  51         echo ":formula"
  52         echo "(and"
  53         for i in $PC $RC; do
  54                 echo "(or"
  55                 echo "(and (= c${i}w $(wp $i)) (= c${i}h $(hp $i)))"
  56                 echo "(and (= c${i}w $(hp $i)) (= c${i}h $(wp $i)))"
  57                 echo ")"
  58
  59                 echo "(> c${i}x 0) (> c${i}y 0)"
  60                 echo "(<= (+ c${i}x c${i}w) $MAXX) (<= (+ c${i}y c${i}h) $MAXY)"
  61
  62                 for j in $PC $RC; do
  63                         if [ $i != $j ]; then
  64                                 echo "(or"
  65                                 echo "(> c${i}x (+ c${j}x c${j}w)) (< (+ c${i}x c${i}w) c${j}x)"
  66                                 echo "(> c${i}y (+ c${j}y c${j}h)) (< (+ c${i}y c${i}h) c${j}y)"
  67                                 echo ")"
  68                         fi
  69                 done
  70         done
  71
  72         for i in $PC; do
  73                 for j in $PC; do
  74                         if [ $i != $j ]; then
  75                                 echo "(or"
  76                                 echo "(> (- (+ c${i}x (/ c${i}w 2)) (+ c${j}x (/ c${j}w 2))) $PD)"
  77                                 echo "(> (- (+ c${j}x (/ c${j}w 2)) (+ c${i}x (/ c${i}w 2))) $PD)"
  78                                 echo "(> (- (+ c${i}y (/ c${i}h 2)) (+ c${j}y (/ c${j}h 2))) $PD)"
  79                                 echo "(> (- (+ c${j}y (/ c${j}h 2)) (+ c${i}y (/ c${i}h 2))) $PD)"
  80                                 echo ")"
  81                         fi
  82                 done
  83         done
  84
  85         for i in $RC; do
  86                 echo "(or"
  87                 for j in $PC; do
  88                         if [ $i != $j ]; then
  89                                 echo "(not (or "
  90                                 echo "(> c${i}x (+ c${j}x 1 c${j}w)) (< (+ c${i}x c${i}w) (- c${j}x 1))"
  91                                 echo "(> c${i}y (+ c${j}y 1 c${j}h)) (< (+ c${i}y c${i}h) (- c${j}y 1))"
  92                                 echo "))"
  93                         fi
  94                 done
  95                 echo ")"
  96         done
  97         echo "))"
  98 }
  99 time generate | yices-smt -m | python3 src/a2.py > $1