a2/src/1b.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         (or ;-- ITERATION $i
  32                 (and ;-- SPECIAL CASE FOR STATE S(0)
  33                         (= l$i 0)
  34                         (= d$i 0)
  35                         (= t$i $TMAX)
  36                         (or
  37                                 (and ;-- CAME FROM A
  38                                         (= l$((i-1)) 1)
  39                                         (= a$i (- a$((i-1)) 29))
  40                                         (= b$i (- b$((i-1)) 29))
  41                                         (= c$i (- c$((i-1)) 29))
  42                                 )
  43                                 (and ;-- CAME FROM B
  44                                         (= l$((i-1)) 2)
  45                                         (= a$i (- a$((i-1)) 21))
  46                                         (= b$i (- b$((i-1)) 21))
  47                                         (= c$i (- c$((i-1)) 21))
  48                                 )
  49                         )
  50                 )
  51                 (and ;-- CASE FOR STATE A(1)
  52                         (= l$i 1)
  53                         (>= d$i 0) (<= d$i t$((i-1))) (<= d$i (- $AMAX a$((i-1))))
  54                         (= t$i (- t$((i-1)) d$i)) (= a$i (+ a$((i-1)) d$i))
  55
  56                         (or
  57                                 (and  ;-- CAME FROM S(0)
  58                                         (= l$((i-1)) 0)
  59                                         (= b$i (- b$((i-1)) 29))
  60                                         (= c$i (- c$((i-1)) 29))
  61                                 ) (and  ;-- CAME FROM B(2)
  62                                         (= l$((i-1)) 2)
  63                                         (= b$i (- b$((i-1)) 17))
  64                                         (= c$i (- c$((i-1)) 17))
  65                                 ) (and ;-- CAME FROM C(3)
  66                                         (= l$((i-1)) 3)
  67                                         (= b$i (- b$((i-1)) 32))
  68                                         (= c$i (- c$((i-1)) 32))
  69                                 )
  70                         )
  71                 )
  72                 (and ;-- CASE FOR STATE B(2)
  73                         (= l$i 2)
  74                         (>= d$i 0) (<= d$i t$((i-1))) (<= d$i (- $BMAX b$((i-1))))
  75                         (= t$i (- t$((i-1)) d$i)) (= b$i (+ b$((i-1)) d$i))
  76
  77                         (or
  78                                 (and  ;-- CAME FROM S(0)
  79                                         (= l$((i-1)) 0)
  80                                         (= a$i (- a$((i-1)) 21))
  81                                         (= c$i (- c$((i-1)) 21))
  82                                 ) (and  ;-- CAME FROM A(1)
  83                                         (= l$((i-1)) 1)
  84                                         (= a$i (- a$((i-1)) 17))
  85                                         (= c$i (- c$((i-1)) 17))
  86                                 ) (and ;-- CAME FROM C(3)
  87                                         (= l$((i-1)) 3)
  88                                         (= a$i (- a$((i-1)) 37))
  89                                         (= c$i (- c$((i-1)) 37))
  90                                 )
  91                         )
  92                 )
  93                 (and ;-- CASE FOR STATE C(3)
  94                         (= l$i 3)
  95                         (>= d$i 0) (<= d$i t$((i-1))) (<= d$i (- $CMAX c$((i-1))))
  96                         (= t$i (- t$((i-1)) d$i)) (= c$i (+ c$((i-1)) d$i))
  97
  98                         (or
  99                                 (and  ;-- CAME FROM A(1)
 100                                         (= l$((i-1)) 1)
 101                                         (= a$i (- a$((i-1)) 32))
 102                                         (= b$i (- b$((i-1)) 32))
 103                                 ) (and ;-- CAME FROM B(2)
 104                                         (= l$((i-1)) 2)
 105                                         (= a$i (- a$((i-1)) 37))
 106                                         (= b$i (- b$((i-1)) 37))
 107                                 )
 108                         )
 109                 )
 110         )
 111 GEN
 112         done
 113         echo "(or"
 114         for i in $(seq 0 $ITERATIONS); do
 115                 for j in $(seq $((i+1)) $ITERATIONS); do
 116                         echo "(and (= t$i t$j) (= l$i l$j) (= a$i a$j) (= b$i b$j) (= c$i c$j))"
 117                 done
 118         done
 119         echo ")))"
 120 }
 121
 122 it=1
 123 while generate $it 320 | $YICES -m | pee sort "grep unsat"
 124 do
 125         it=$((it+1))
 126 done
 127 echo $it