ar/assignments/src/1.smt

   1 (benchmark a1.smt
   2 :logic QF_UFLIA
   3 :extrafuns (
   4         (t1p Int) (t1n Int) (t1s Int) (t1c Int) (t1d Int)
   5         (t2p Int) (t2n Int) (t2s Int) (t2c Int) (t2d Int)
   6         (t3p Int) (t3n Int) (t3s Int) (t3c Int) (t3d Int)
   7         (t4p Int) (t4n Int) (t4s Int) (t4c Int) (t4d Int)
   8         (t5p Int) (t5n Int) (t5s Int) (t5c Int) (t5d Int)
   9         (t6p Int) (t6n Int) (t6s Int) (t6c Int) (t6d Int)
  10 )
  11 :formula
  12 (and
  13         (>= t1p 0) (>= t1n 0) (>= t1s 0) (>= t1c 0) (>= t1d 0)
  14         (>= t2p 0) (>= t2n 0) (>= t2s 0) (>= t2c 0) (>= t2d 0)
  15         (>= t3p 0) (>= t3n 0) (>= t3s 0) (>= t3c 0) (>= t3d 0)
  16         (>= t4p 0) (>= t4n 0) (>= t4s 0) (>= t4c 0) (>= t4d 0)
  17         (>= t5p 0) (>= t5n 0) (>= t5s 0) (>= t5c 0) (>= t5d 0)
  18         (>= t6p 0) (>= t6n 0) (>= t6s 0) (>= t6c 0) (>= t6d 0)
  19
  20         (<= (+ t1p t1n t1s t1c t1d) 8)
  21         (<= (+ t2p t2n t2s t2c t2d) 8)
  22         (<= (+ t3p t3n t3s t3c t3d) 8)
  23         (<= (+ t4p t4n t4s t4c t4d) 8)
  24         (<= (+ t5p t5n t5s t5c t5d) 8)
  25         (<= (+ t6p t6n t6s t6c t6d) 8)
  26
  27         (<= (+ (* t1n 700) (* t1p 800) (* t1s 1000) (* t1c 1500) (* t1d 100)) 7800)
  28         (<= (+ (* t2n 700) (* t2p 800) (* t2s 1000) (* t2c 1500) (* t2d 100)) 7800)
  29         (<= (+ (* t3n 700) (* t3p 800) (* t3s 1000) (* t3c 1500) (* t3d 100)) 7800)
  30         (<= (+ (* t4n 700) (* t4p 800) (* t4s 1000) (* t4c 1500) (* t4d 100)) 7800)
  31         (<= (+ (* t5n 700) (* t5p 800) (* t5s 1000) (* t5c 1500) (* t5d 100)) 7800)
  32         (<= (+ (* t6n 700) (* t6p 800) (* t6s 1000) (* t6c 1600) (* t6d 100)) 7800)
  33
  34         (= (+ t1n t2n t3n t4n t5n t6n) 4)
  35         (= (+ t1s t2s t3s t4s t5s t6s) 8)
  36         (= (+ t1c t2c t3c t4c t5c t6c) 10)
  37         (= (+ t1d t2d t3d t4d t5d t6d) 5)
  38
  39         (or (= 0 t1p) (= 0 t1c))
  40         (or (= 0 t2p) (= 0 t2c))
  41         (or (= 0 t3p) (= 0 t3c))
  42         (or (= 0 t4p) (= 0 t4c))
  43         (or (= 0 t5p) (= 0 t5c))
  44         (or (= 0 t6p) (= 0 t6c))
  45
  46         (= t3s 0)
  47         (= t4s 0)
  48         (= t5s 0)
  49         (= t6s 0)
  50
  51         (<= t1d 1)
  52         (<= t2d 1)
  53         (<= t3d 1)
  54         (<= t4d 1)
  55         (<= t5d 1)
  56         (<= t6d 1)
  57
  58         (>= (+ t1p t2p t3p t4p t5p t6p) <REP>)
  59 )
  60 )