update with dynamic solution for problem 1

[ar1516.git] / src / a1.bash

diff --git a/src/a1.bash b/src/a1.bash
index 339536f..5e71a17 100644 (file)
--- a/src/a1.bash
+++ b/src/a1.bash
@@ -1,6 +1,64 @@
+function generate {
+       cat<<GENERATE
+(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) $1)
+)
+)
+GENERATE
+}
+
 i=1
-while [ $(sed "s/<REP>/$i/g" a1.smt | yices-smt) = "sat" ]; do
+while [ $(generate $i | yices-smt) = "sat" ]; do
        echo "n(p)=$i is still sat"
        i=$((i+1))
 done
 echo "n(p)=$i is unsat thus maximum n(p)=$((i-1))"
+generate $((i-1)) | yices-smt -m | python3 src/a1.py > $1