src/a3.bash

   1 #!/bin/bash
   2 JOBS=12
   3 J=$(seq 1 $JOBS)
   4 JPRIME="5 7 10"
   5
   6 function pi {
   7         case $1 in
   8                 3) echo 1 2;;
   9                 5) echo 3 4;;
  10                 7) echo 3 4 6;;
  11                 9) echo 5 8;;
  12                 11) echo 10;;
  13                 12) echo 9 11;;
  14                 *);;
  15         esac
  16 }
  17
  18 function generate {
  19         local i j
  20         echo "(benchmark a4.smt"
  21         echo ":logic QF_UFLIA"
  22         echo ":extrafuns ("
  23         for i in $J; do
  24                 echo "(j$i Int)"
  25         done
  26         echo ")"
  27         echo ":formula"
  28         echo "(and"
  29         for i in $J; do
  30                 echo "(> j$i 0) (<= (+ j$i $i) $1)"
  31                 for j in $(pi $i); do
  32                         echo "(>= j$i (+ j$j $j))"
  33                 done
  34         done
  35         for i in $JPRIME; do
  36                 for j in $JPRIME; do
  37                         if [ $i != $j ]; then
  38                                 echo "(or (>= j$i (+ j$j $j))"
  39                                 echo "    (<= (+ j$i $i) j$j))"
  40                         fi
  41                 done
  42         done
  43         echo "))"
  44 }
  45
  46 i=1
  47 while [ $(generate $i | yices-smt) = "unsat" ]; do
  48         echo "T=$((i++)) is still unsat"
  49 done
  50 echo "T=$i is sat thus the minimum T=$i"