a2/src/1a.bash

   1 #!/bin/bash
   2 YICES=~/projects/yices-2.4.2/bin/yices-smt
   3 AI=40
   4 BI=30
   5 CI=145
   6 AMAX=120
   7 BMAX=120
   8 CMAX=200
   9
  10 function generate {
  11         ITERATIONS=$1
  12         TMAX=$2
  13         cat<<GEN
  14 (benchmark a1.smt
  15 :logic QF_UFLIA
  16 :extrafuns (
  17 $(      for i in $(seq 0 $ITERATIONS); do
  18                 echo -e "\t(a$i Int) (b$i Int) (c$i Int) (t$i Int) (l$i Int) (d$i Int)"
  19         done)
  20 )
  21 :formula
  22 (and
  23         ;-- PRECONDITION
  24         (and (= a0 $AI) (= b0 $BI) (= c0 $CI) (= t0 $TMAX) (= l0 0) (= d0 0))
  25 GEN
  26         for i in $(seq 1 $ITERATIONS); do
  27                 cat<<GEN
  28         (> a$i 0)
  29         (> b$i 0)
  30         (> c$i 0)
  31         (>= d$i 0)
  32         (<= d$i $TMAX)
  33         (>= t$i 0)
  34         (<= t$i $TMAX)
  35         (or ;-- ITERATION $i
  36                 (and ;-- WAS IN S
  37                         (= l$((i-1)) 0)
  38                         (or
  39                                 (and ; now in A
  40                                         (= l$i 1)
  41                                         (<= d$i (+ 29 (- $AMAX a$((i-1)))))
  42                                         (= a$i (+ (- a$((i-1)) 29) d$i))
  43
  44                                         (= b$i (- b$((i-1)) 29))
  45                                         (= c$i (- c$((i-1)) 29))
  46
  47                                         (= t$i (- t$((i-1)) d$i))
  48                                 ) (and ; now in B
  49                                         (= l$i 2)
  50                                         (<= d$i (+ 21 (- $BMAX b$((i-1)))))
  51                                         (= b$i (+ (- b$((i-1)) 21) d$i))
  52
  53                                         (= a$i (- a$((i-1)) 21))
  54                                         (= c$i (- c$((i-1)) 21))
  55
  56                                         (= t$i (- t$((i-1)) d$i))
  57                                 )
  58                         )
  59                 )
  60                 (and ;-- WAS IN A
  61                         (= l$((i-1)) 1)
  62                         (or
  63                                 (and ; now in S
  64                                         (= l$i 0)
  65                                         (= d$i 0)
  66
  67                                         (= a$i (- a$((i-1)) 29))
  68                                         (= b$i (- b$((i-1)) 29))
  69                                         (= c$i (- c$((i-1)) 29))
  70
  71                                         (= t$i $TMAX)
  72                                 ) (and ; now in B
  73                                         (= l$i 2)
  74                                         (<= d$i (+ 17 (- $BMAX b$((i-1)))))
  75                                         (= b$i (+ (- b$((i-1)) 17) d$i))
  76
  77                                         (= a$i (- a$((i-1)) 17))
  78                                         (= c$i (- c$((i-1)) 17))
  79
  80                                         (= t$i (- t$((i-1)) d$i))
  81                                 ) (and ; now in C
  82                                         (= l$i 3)
  83
  84                                         (<= d$i (+ 32 (- $CMAX c$((i-1)))))
  85                                         (= c$i (+ (- c$((i-1)) 32) d$i))
  86
  87                                         (= a$i (- a$((i-1)) 32))
  88                                         (= b$i (- b$((i-1)) 32))
  89
  90                                         (= t$i (- t$((i-1)) d$i))
  91                                 )
  92                         )
  93                 )
  94                 (and ;-- WAS IN B
  95                         (= l$((i-1)) 2)
  96                         (or
  97                                 (and ; now in S
  98                                         (= l$i 0)
  99                                         (= d$i 0)
 100
 101                                         (= a$i (- a$((i-1)) 21))
 102                                         (= b$i (- b$((i-1)) 21))
 103                                         (= c$i (- c$((i-1)) 21))
 104
 105                                         (= t$i $TMAX)
 106                                 ) (and ; now in A
 107                                         (= l$i 1)
 108                                         (<= d$i (+ 17 (- $AMAX a$((i-1)))))
 109                                         (= a$i (+ (- a$((i-1)) 17) d$i))
 110
 111                                         (= b$i (- b$((i-1)) 17))
 112                                         (= c$i (- c$((i-1)) 17))
 113
 114                                         (= t$i (- t$((i-1)) d$i))
 115                                 ) (and ; now in C
 116                                         (= l$i 3)
 117                                         (<= d$i (+ 37 (- $CMAX c$((i-1)))))
 118                                         (= c$i (+ (- c$((i-1)) 37) d$i))
 119
 120                                         (= a$i (- a$((i-1)) 37))
 121                                         (= b$i (- b$((i-1)) 37))
 122
 123                                         (= t$i (- t$((i-1)) d$i))
 124                                 )
 125                         )
 126                 )
 127                 (and ;-- WAS IN C
 128                         (= l$((i-1)) 3)
 129                         (or
 130                                 (and ; now in A
 131                                         (= l$i 1)
 132                                         (<= d$i (+ 32 (- $AMAX a$((i-1)))))
 133                                         (= a$i (+ (- a$((i-1)) 32) d$i))
 134
 135                                         (= b$i (- b$((i-1)) 32))
 136                                         (= c$i (- c$((i-1)) 32))
 137
 138                                         (= t$i (- t$((i-1)) d$i))
 139                                 ) (and ; now in B
 140                                         (= l$i 2)
 141                                         (<= d$i (+ 37 (- $BMAX b$((i-1)))))
 142                                         (= b$i (+ (- b$((i-1)) 37) d$i))
 143
 144                                         (= a$i (- a$((i-1)) 37))
 145                                         (= c$i (- c$((i-1)) 37))
 146
 147                                         (= t$i (- t$((i-1)) d$i))
 148                                 )
 149                         )
 150                 )
 151         )
 152 GEN
 153         done
 154         echo "(or"
 155         for i in $(seq 0 $ITERATIONS); do
 156                 for j in $(seq $((i+1)) $ITERATIONS); do
 157                         echo "(and (= t$i t$j) (= l$i l$j) (= a$i a$j) (= b$i b$j) (= c$i c$j))"
 158                 done
 159         done
 160         echo ")))"
 161 }
 162 it=1
 163 while generate $it 318 | $YICES -m | pee sort "grep -q unsat"
 164 do
 165         echo $((it++))
 166 done