a2/src/1.bash

   1 #!/bin/bash
   2 AI=40
   3 BI=30
   4 CI=145
   5 TI=300
   6 AMAX=120
   7 BMAX=120
   8 CMAX=200
   9 TMAX=300
  10
  11 ITERATIONS=1
  12
  13 function generate {
  14         cat<<GEN
  15 (benchmark a1.smt
  16 :logic QF_UFLIA
  17 :extrafuns (
  18 $(      for i in $(seq 0 $ITERATIONS); do
  19                 echo -e "\t(a$i Int) (b$i Int) (c$i Int) (t$i Int) (l$i Int) (d$i Int)"
  20         done)
  21 )
  22 :formula
  23 (and
  24         -- PRECONDITION
  25         (and (= a0 $AI) (= b0 $BI) (= c0 $CI) (= t0 $TI) (= l0 0) (= d0 0))
  26 GEN
  27         for i in $(seq 1 $ITERATIONS); do
  28                 cat<<GEN
  29         -- SPECIAL CASE FOR STATE S(0)
  30         (= l$i 0) (= d$i 0) (= t$i $TMAX)
  31         (or
  32                 (and -- Comes from A
  33                         (= l$((i-1)) 1)
  34                         (= a$i (- a$((i-1)) 29)
  35                         (= b$i (- b$((i-1)) 29)
  36                         (= c$i (- c$((i-1)) 29)
  37                 )
  38                 (and -- Comes from B
  39                         (= l$((i-1)) 2)
  40                         (= a$i (- a$((i-1)) 21)
  41                         (= b$i (- b$((i-1)) 21)
  42                         (= c$i (- c$((i-1)) 21)
  43                 )
  44         )
  45 GEN
  46         done
  47         echo "))"
  48 }
  49 #time generate | yices-smt -m | python3 src/a2.py > $1
  50 generate