a2/src/1.bash

   1 #!/bin/bash
   2 AINIT=40
   3 BINIT=30
   4 CINIT=145
   5 AMAX=120
   6 BMAX=120
   7 CMAX=200
   8 TMAX=300
   9 TINIT=300
  10 TLOC=0
  11
  12 PLACES=s a b c
  13 STATES=5
  14
  15 function generate {
  16         local i j
  17         cat<<GEN
  18 (benchmark a1.smt
  19 :logic QF_UFLIA
  20 :extrafuns (
  21 GEN
  22         for i in $(seq 0 $STATES); do
  23                 echo "(a$i Int) (b$i Int) (c$i Int) (t$i Int) (l$i Int)"
  24         done
  25         cat <<GEN
  26 )
  27 :formula
  28 (and
  29         (and (= a0 $AINIT) (= b0 $BINIT) (= c0 $CINIT) (= t0 $TINIT) (= l0 0))
  30 GEN
  31         for i in $(seq $STATES); do
  32                 j=$((i-1))
  33                 echo $i $j
  34                 echo "(or"
  35
  36                 #Truck is in S
  37                 echo "(and"
  38                 echo "(= l$j 0)"
  39                 echo "(> dump
  40                 echo ")"
  41                 #Truck is in A
  42                 echo "(and"
  43                 echo "(= l$j 0)"
  44                 echo ")"
  45                 #Truck is in B
  46                 echo "(and"
  47                 echo "(= l$j 0)"
  48                 echo ")"
  49                 #Truck is in C
  50                 echo "(and"
  51                 echo "(= l$j 0)"
  52                 echo ")"
  53
  54                 echo ")"
  55         done
  56         echo "))"
  57 }
  58 #time generate | yices-smt -m | python3 src/a2.py > $1
  59 generate