src/a4.bash

   1 #!/usr/bin/env python3
   2 NUMA=7
   3
   4 function generate {
   5         local i n j
   6         echo "(benchmark a4.smt"
   7         echo ":logic QF_UFLIA"
   8         echo ":extrafuns ("
   9         echo "(a1 Int)"
  10         echo "(a$NUMA Int)"
  11         for i in $(seq 2 $((NUMA-1))); do
  12                 for n in $(seq 0 $1); do
  13                         echo "(i${n}a$i Int)"
  14                 done
  15         done
  16         echo ")"
  17         echo ":formula"
  18         echo "(and"
  19
  20         echo "(= a1 1)"
  21         echo "(= a$NUMA $NUMA)"
  22         for i in $(seq 2 $((NUMA-1))); do
  23                 echo "(= i0a$i $i)"
  24         done
  25
  26         for n in $(seq 1 $1); do
  27                 echo "(or"
  28                 for i in $(seq 2 $((NUMA-1))); do
  29                         echo "(and"
  30                         [ $i = 2 ] && prev=1 || prev="i$((n-1))a$((i-1))"
  31                         [ $i = $((NUMA-1)) ] && next=7 || next="i$((n-1))a$((i+1))"
  32                         echo "(= i${n}a$i (+ $prev $next)) "
  33                         for j in $(seq 2 $((NUMA-1))); do
  34                                 if [ $i != $j ]; then
  35                                         echo "(= i${n}a$j i$((n-1))a$j)"
  36                                 fi
  37                         done
  38                         echo ")"
  39                 done
  40                 echo ")"
  41         done
  42
  43         echo "(or"
  44         for i in $(seq 2 $((NUMA-1))); do
  45                 echo "(and"
  46                 echo "(>= i${1}a$i 50)"
  47                 echo "(or"
  48                 for j in $(seq 2 $((NUMA-1))); do
  49                         if [ $i != $j ]; then
  50                                 echo "(= i${1}a$i i${1}a$j)"
  51                         fi
  52                 done
  53                 echo "))"
  54         done
  55         echo ")))"
  56 }
  57
  58 i=1
  59 while [ $(generate $i | yices-smt) = "unsat" ]; do
  60         echo "N=$i is still unsat"
  61         i=$((i+1))
  62 done
  63 echo "N=$i is sat thus minimum N=$i"