src/a1.bash

   1 function generate {
   2         cat<<GENERATE
   3 (benchmark a1.smt
   4 :logic QF_UFLIA
   5 :extrafuns (
   6         (t1p Int) (t1n Int) (t1s Int) (t1c Int) (t1d Int)
   7         (t2p Int) (t2n Int) (t2s Int) (t2c Int) (t2d Int)
   8         (t3p Int) (t3n Int) (t3s Int) (t3c Int) (t3d Int)
   9         (t4p Int) (t4n Int) (t4s Int) (t4c Int) (t4d Int)
  10         (t5p Int) (t5n Int) (t5s Int) (t5c Int) (t5d Int)
  11         (t6p Int) (t6n Int) (t6s Int) (t6c Int) (t6d Int)
  12 )
  13 :formula
  14 (and
  15         (>= t1p 0) (>= t1n 0) (>= t1s 0) (>= t1c 0) (>= t1d 0)
  16         (>= t2p 0) (>= t2n 0) (>= t2s 0) (>= t2c 0) (>= t2d 0)
  17         (>= t3p 0) (>= t3n 0) (>= t3s 0) (>= t3c 0) (>= t3d 0)
  18         (>= t4p 0) (>= t4n 0) (>= t4s 0) (>= t4c 0) (>= t4d 0)
  19         (>= t5p 0) (>= t5n 0) (>= t5s 0) (>= t5c 0) (>= t5d 0)
  20         (>= t6p 0) (>= t6n 0) (>= t6s 0) (>= t6c 0) (>= t6d 0)
  21
  22         (<= (+ t1p t1n t1s t1c t1d) 8)
  23         (<= (+ t2p t2n t2s t2c t2d) 8)
  24         (<= (+ t3p t3n t3s t3c t3d) 8)
  25         (<= (+ t4p t4n t4s t4c t4d) 8)
  26         (<= (+ t5p t5n t5s t5c t5d) 8)
  27         (<= (+ t6p t6n t6s t6c t6d) 8)
  28
  29         (<= (+ (* t1n 700) (* t1p 800) (* t1s 1000) (* t1c 1500) (* t1d 100)) 7800)
  30         (<= (+ (* t2n 700) (* t2p 800) (* t2s 1000) (* t2c 1500) (* t2d 100)) 7800)
  31         (<= (+ (* t3n 700) (* t3p 800) (* t3s 1000) (* t3c 1500) (* t3d 100)) 7800)
  32         (<= (+ (* t4n 700) (* t4p 800) (* t4s 1000) (* t4c 1500) (* t4d 100)) 7800)
  33         (<= (+ (* t5n 700) (* t5p 800) (* t5s 1000) (* t5c 1500) (* t5d 100)) 7800)
  34         (<= (+ (* t6n 700) (* t6p 800) (* t6s 1000) (* t6c 1600) (* t6d 100)) 7800)
  35
  36         (or (= 0 t1p) (= 0 t1c))
  37         (or (= 0 t2p) (= 0 t2c))
  38         (or (= 0 t3p) (= 0 t3c))
  39         (or (= 0 t4p) (= 0 t4c))
  40         (or (= 0 t5p) (= 0 t5c))
  41         (or (= 0 t6p) (= 0 t6c))
  42
  43         (<= t1d 1) (<= t2d 1) (<= t3d 1) (<= t4d 1) (<= t5d 1) (<= t6d 1)
  44
  45         (= t3s 0) (= t4s 0) (= t5s 0) (= t6s 0)
  46
  47         (= (+ t1n t2n t3n t4n t5n t6n) 4)
  48         (= (+ t1s t2s t3s t4s t5s t6s) 8)
  49         (= (+ t1c t2c t3c t4c t5c t6c) 10)
  50         (= (+ t1d t2d t3d t4d t5d t6d) 5)
  51
  52         (>= (+ t1p t2p t3p t4p t5p t6p) $1)
  53 )
  54 )
  55 GENERATE
  56 }
  57
  58 i=1
  59 while [ $(generate $i | yices-smt) = "sat" ]; do
  60         echo "n(p)=$i is still sat"
  61         i=$((i+1))
  62 done
  63 echo "n(p)=$i is unsat thus maximum n(p)=$((i-1))"
  64 generate $((i-1)) | yices-smt -m | python3 src/a1.py > $1