final ar

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

diff --git a/ar/assignment1/src/a4.bash b/ar/assignment1/src/a4.bash
index 23abab8..7f9e0f9 100644 (file)
--- a/ar/assignment1/src/a4.bash
+++ b/ar/assignment1/src/a4.bash
@@ -1,7 +1,63 @@
+#!/usr/bin/env python3
+NUMA=7
+
+function generate {
+       local i n j
+       echo "(benchmark a4.smt"
+       echo ":logic QF_UFLIA"
+       echo ":extrafuns ("
+       echo "(a1 Int)"
+       echo "(a$NUMA Int)"
+       for i in $(seq 2 $((NUMA-1))); do
+               for n in $(seq 0 $1); do
+                       echo "(i${n}a$i Int)"
+               done
+       done
+       echo ")"
+       echo ":formula"
+       echo "(and"
+
+       echo "(= a1 1)"
+       echo "(= a$NUMA $NUMA)"
+       for i in $(seq 2 $((NUMA-1))); do
+               echo "(= i0a$i $i)"
+       done
+
+       for n in $(seq 1 $1); do
+               echo "(or"
+               for i in $(seq 2 $((NUMA-1))); do
+                       echo "(and"
+                       [ $i = 2 ] && prev=1 || prev="i$((n-1))a$((i-1))"
+                       [ $i = $((NUMA-1)) ] && next=7 || next="i$((n-1))a$((i+1))"
+                       echo "(= i${n}a$i (+ $prev $next)) "
+                       for j in $(seq 2 $((NUMA-1))); do
+                               if [ $i != $j ]; then
+                                       echo "(= i${n}a$j i$((n-1))a$j)"
+                               fi
+                       done
+                       echo ")"
+               done
+               echo ")"
+       done
+
+       echo "(or"
+       for i in $(seq 2 $((NUMA-1))); do
+               echo "(and"
+               echo "(>= i${1}a$i 50)"
+               echo "(or"
+               for j in $(seq 2 $((NUMA-1))); do
+                       if [ $i != $j ]; then
+                               echo "(= i${1}a$i i${1}a$j)"
+                       fi
+               done
+               echo "))"
+       done
+       echo ")))"
+}
+
 i=1
-while [ $(python3 a4.py $i | yices-smt) = "unsat" ]; do
+while [ $(generate $i | yices-smt) = "unsat" ]; do
        echo "N=$i is still unsat"
        i=$((i+1))
 done
 echo "N=$i is sat thus minimum N=$i"
-python3 a4.py $i | yices-smt -m