final ar

[master.git] / ar / assignment1 / src / a3.bash

diff --git a/ar/assignment1/src/a3.bash b/ar/assignment1/src/a3.bash
index 0a21dee..5b16adc 100644 (file)
--- a/ar/assignment1/src/a3.bash
+++ b/ar/assignment1/src/a3.bash
@@ -1,7 +1,50 @@
+#!/bin/bash
+JOBS=12
+J=$(seq 1 $JOBS)
+JPRIME="5 7 10"
+
+function pi {
+       case $1 in
+               3) echo 1 2;;
+               5) echo 3 4;;
+               7) echo 3 4 6;;
+               9) echo 5 8;;
+               11) echo 10;;
+               12) echo 9 11;;
+               *);;
+       esac
+}
+
+function generate {
+       local i j
+       echo "(benchmark a4.smt"
+       echo ":logic QF_UFLIA"
+       echo ":extrafuns ("
+       for i in $J; do
+               echo "(j$i Int)"
+       done
+       echo ")"
+       echo ":formula"
+       echo "(and"
+       for i in $J; do
+               echo "(> j$i 0) (<= (+ j$i $i) $1)"
+               for j in $(pi $i); do
+                       echo "(>= j$i (+ j$j $j))"
+               done
+       done
+       for i in $JPRIME; do
+               for j in $JPRIME; do
+                       if [ $i != $j ]; then
+                               echo "(or (>= j$i (+ j$j $j))"
+                               echo "    (<= (+ j$i $i) j$j))"
+                       fi
+               done
+       done
+       echo "))"
+}
+
 i=1
-while [ $(python3 a3.py $i | yices-smt) = "unsat" ]; do
-       echo "T=$i is still unsat"
-       i=$((i+1))
+while [ $(generate $i | yices-smt) = "unsat" ]; do
+       echo "T=$((i++)) is still unsat"
 done
 echo "T=$i is sat thus the minimum T=$i"
-python3 a3.py $i | yices-smt -m