a2/src/1.bak

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