a2/src/1c.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                                         (>= a$((i-1)) 29)
  41                                         (= l$i 1)
  42                                         (<= d$i (+ 29 (- $AMAX a$((i-1)))))
  43                                         (= a$i (+ (- a$((i-1)) 29) d$i))
  44
  45                                         (= b$i (- b$((i-1)) 29))
  46                                         (= c$i (- c$((i-1)) 29))
  47
  48                                         (= t$i (- t$((i-1)) d$i))
  49                                 ) (and ; now in B
  50                                         (>= b$((i-1)) 21)
  51                                         (= l$i 2)
  52                                         (<= d$i (+ 21 (- $BMAX b$((i-1)))))
  53                                         (= b$i (+ (- b$((i-1)) 21) d$i))
  54
  55                                         (= a$i (- a$((i-1)) 21))
  56                                         (= c$i (- c$((i-1)) 21))
  57
  58                                         (= t$i (- t$((i-1)) d$i))
  59                                 )
  60                         )
  61                 )
  62                 (and ;-- WAS IN A
  63                         (= l$((i-1)) 1)
  64                         (or
  65                                 (and ; now in S
  66                                         (= l$i 0)
  67                                         (= d$i 0)
  68
  69                                         (= a$i (- a$((i-1)) 29))
  70                                         (= b$i (- b$((i-1)) 29))
  71                                         (= c$i (- c$((i-1)) 29))
  72
  73                                         (= t$i $TMAX)
  74                                 ) (and ; now in B
  75                                         (>= b$((i-1)) 17)
  76                                         (= l$i 2)
  77                                         (<= d$i (+ 17 (- $BMAX b$((i-1)))))
  78                                         (= b$i (+ (- b$((i-1)) 17) d$i))
  79
  80                                         (= a$i (- a$((i-1)) 17))
  81                                         (= c$i (- c$((i-1)) 17))
  82
  83                                         (= t$i (- t$((i-1)) d$i))
  84                                 ) (and ; now in C
  85                                         (>= c$((i-1)) 32)
  86                                         (= l$i 3)
  87
  88                                         (<= d$i (+ 32 (- $CMAX c$((i-1)))))
  89                                         (= c$i (+ (- c$((i-1)) 32) d$i))
  90
  91                                         (= a$i (- a$((i-1)) 32))
  92                                         (= b$i (- b$((i-1)) 32))
  93
  94                                         (= t$i (- t$((i-1)) d$i))
  95                                 )
  96                         )
  97                 )
  98                 (and ;-- WAS IN B
  99                         (= l$((i-1)) 2)
 100                         (or
 101                                 (and ; now in S
 102                                         (= l$i 0)
 103                                         (= d$i 0)
 104
 105                                         (= a$i (- a$((i-1)) 21))
 106                                         (= b$i (- b$((i-1)) 21))
 107                                         (= c$i (- c$((i-1)) 21))
 108
 109                                         (= t$i $TMAX)
 110                                 ) (and ; now in A
 111                                         (>= a$((i-1)) 17)
 112                                         (= l$i 1)
 113                                         (<= d$i (+ 17 (- $AMAX a$((i-1)))))
 114                                         (= a$i (+ (- a$((i-1)) 17) d$i))
 115
 116                                         (= b$i (- b$((i-1)) 17))
 117                                         (= c$i (- c$((i-1)) 17))
 118
 119                                         (= t$i (- t$((i-1)) d$i))
 120                                 ) (and ; now in C
 121                                         (>= c$((i-1)) 37)
 122                                         (= l$i 3)
 123                                         (<= d$i (+ 37 (- $CMAX c$((i-1)))))
 124                                         (= c$i (+ (- c$((i-1)) 37) d$i))
 125
 126                                         (= a$i (- a$((i-1)) 37))
 127                                         (= b$i (- b$((i-1)) 37))
 128
 129                                         (= t$i (- t$((i-1)) d$i))
 130                                 )
 131                         )
 132                 )
 133                 (and ;-- WAS IN C
 134                         (= l$((i-1)) 3)
 135                         (or
 136                                 (and ; now in A
 137                                         (>= a$((i-1)) 32)
 138                                         (= l$i 1)
 139                                         (<= d$i (+ 32 (- $AMAX a$((i-1)))))
 140                                         (= a$i (+ (- a$((i-1)) 32) d$i))
 141
 142                                         (= b$i (- b$((i-1)) 32))
 143                                         (= c$i (- c$((i-1)) 32))
 144
 145                                         (= t$i (- t$((i-1)) d$i))
 146                                 ) (and ; now in B
 147                                         (>= b$((i-1)) 37)
 148                                         (= l$i 2)
 149                                         (<= d$i (+ 37 (- $BMAX b$((i-1)))))
 150                                         (= b$i (+ (- b$((i-1)) 37) d$i))
 151
 152                                         (= a$i (- a$((i-1)) 37))
 153                                         (= c$i (- c$((i-1)) 37))
 154
 155                                         (= t$i (- t$((i-1)) d$i))
 156                                 )
 157                         )
 158                 )
 159         )
 160 GEN
 161         done
 162         echo "(or"
 163         for i in $(seq 0 $ITERATIONS); do
 164                 for j in $(seq $((i+1)) $ITERATIONS); do
 165                         echo "(and (= t$i t$j) (= l$i l$j) (= a$i a$j) (= b$i b$j) (= c$i c$j))"
 166                 done
 167         done
 168         echo ")"
 169         echo "))"
 170 }
 171 it=1
 172 while generate $it 318 | $YICES -m | pee sort "grep -q \"^unsat\""
 173 do
 174         echo $((it++))
 175 done