ar finished

[master.git] / ar / assignment1 / src / a1.smt

diff --git a/ar/assignment1/src/a1.smt b/ar/assignment1/src/a1.smt
new file mode 100644 (file)
index 0000000..cf5342e
--- /dev/null
+++ b/ar/assignment1/src/a1.smt
@@ -0,0 +1,60 @@
+(benchmark a1.smt
+:logic QF_UFLIA
+:extrafuns (
+       (t1p Int) (t1n Int) (t1s Int) (t1c Int) (t1d Int)
+       (t2p Int) (t2n Int) (t2s Int) (t2c Int) (t2d Int)
+       (t3p Int) (t3n Int) (t3s Int) (t3c Int) (t3d Int)
+       (t4p Int) (t4n Int) (t4s Int) (t4c Int) (t4d Int)
+       (t5p Int) (t5n Int) (t5s Int) (t5c Int) (t5d Int)
+       (t6p Int) (t6n Int) (t6s Int) (t6c Int) (t6d Int)
+)
+:formula
+(and
+       (>= t1p 0) (>= t1n 0) (>= t1s 0) (>= t1c 0) (>= t1d 0)
+       (>= t2p 0) (>= t2n 0) (>= t2s 0) (>= t2c 0) (>= t2d 0)
+       (>= t3p 0) (>= t3n 0) (>= t3s 0) (>= t3c 0) (>= t3d 0)
+       (>= t4p 0) (>= t4n 0) (>= t4s 0) (>= t4c 0) (>= t4d 0)
+       (>= t5p 0) (>= t5n 0) (>= t5s 0) (>= t5c 0) (>= t5d 0)
+       (>= t6p 0) (>= t6n 0) (>= t6s 0) (>= t6c 0) (>= t6d 0)
+
+       (<= (+ t1p t1n t1s t1c t1d) 8)
+       (<= (+ t2p t2n t2s t2c t2d) 8)
+       (<= (+ t3p t3n t3s t3c t3d) 8)
+       (<= (+ t4p t4n t4s t4c t4d) 8)
+       (<= (+ t5p t5n t5s t5c t5d) 8)
+       (<= (+ t6p t6n t6s t6c t6d) 8)
+
+       (<= (+ (* t1n 700) (* t1p 800) (* t1s 1000) (* t1c 1500) (* t1d 100)) 7800)
+       (<= (+ (* t2n 700) (* t2p 800) (* t2s 1000) (* t2c 1500) (* t2d 100)) 7800)
+       (<= (+ (* t3n 700) (* t3p 800) (* t3s 1000) (* t3c 1500) (* t3d 100)) 7800)
+       (<= (+ (* t4n 700) (* t4p 800) (* t4s 1000) (* t4c 1500) (* t4d 100)) 7800)
+       (<= (+ (* t5n 700) (* t5p 800) (* t5s 1000) (* t5c 1500) (* t5d 100)) 7800)
+       (<= (+ (* t6n 700) (* t6p 800) (* t6s 1000) (* t6c 1600) (* t6d 100)) 7800)
+
+       (or (= 0 t1p) (= 0 t1c))
+       (or (= 0 t2p) (= 0 t2c))
+       (or (= 0 t3p) (= 0 t3c))
+       (or (= 0 t4p) (= 0 t4c))
+       (or (= 0 t5p) (= 0 t5c))
+       (or (= 0 t6p) (= 0 t6c))
+
+       (<= t1d 1)
+       (<= t2d 1)
+       (<= t3d 1)
+       (<= t4d 1)
+       (<= t5d 1)
+       (<= t6d 1)
+
+       (= t3s 0)
+       (= t4s 0)
+       (= t5s 0)
+       (= t6s 0)
+
+       (= (+ t1n t2n t3n t4n t5n t6n) 4)
+       (= (+ t1s t2s t3s t4s t5s t6s) 8)
+       (= (+ t1c t2c t3c t4c t5c t6c) 10)
+       (= (+ t1d t2d t3d t4d t5d t6d) 5)
+
+       (>= (+ t1p t2p t3p t4p t5p t6p) <REP>)
+)
+)