6 echo "(benchmark a4.smt"
11 for i
in $
(seq 2 $
((NUMA-1
))); do
12 for n
in $
(seq 0 $1); do
21 echo "(= a$NUMA $NUMA)"
22 for i
in $
(seq 2 $
((NUMA-1
))); do
26 for n
in $
(seq 1 $1); do
28 for i
in $
(seq 2 $
((NUMA-1
))); do
30 [ $i = 2 ] && prev
=1 || prev
="i$((n-1))a$((i-1))"
31 [ $i = $
((NUMA-1
)) ] && next
=7 || next
="i$((n-1))a$((i+1))"
32 echo "(= i${n}a$i (+ $prev $next)) "
33 for j
in $
(seq 2 $
((NUMA-1
))); do
35 echo "(= i${n}a$j i$((n-1))a$j)"
44 for i
in $
(seq 2 $
((NUMA-1
))); do
46 echo "(>= i${1}a$i 50)"
48 for j
in $
(seq 2 $
((NUMA-1
))); do
50 echo "(= i${1}a$i i${1}a$j)"
59 while [ $
(generate
$i | yices-smt
) = "unsat" ]; do
60 echo "N=$i is still unsat"
63 echo "N=$i is sat thus minimum N=$i"
64 generate
$i | yices-smt
-m | python src
/a4.py
> $1