\end{itemize}
\subsection{SMT format solution}
-The formula is easily convertable via a Python script to SMT format by literal
-conversion and said script is listed in Listing~\ref{listing:a3.py}. The Python
+The formula is easily convertable via a script to SMT format by literal
+conversion and said script is listed in Listing~\ref{listing:a3.bash}. The
script optimizes a little bit from the original formula by leaving out the
shared resource checking for the same jobs. The minimization is done by
incrementing variable $T$ every time the current $T$ yields unsat with a bash
script shown in Listing~\ref{listing:3.bash}.
-\lstinputlisting[language=bash,
+\lstinputlisting[language=bash,firstline=46,
caption={Iteratively find the shortest solution for problem 3},
label={listing:3.bash}]{src/a3.bash}
\subsection{SMT format solution}
The formula is easily convertable via a Python script to SMT format by literal
-conversion and said script is listed in Listing~\ref{listing:a4.py}. The Python
-script optimizes a little bit from the original formula by leaving out the
-$i=j$ comparison in subformula 17 and 18 by removing them from the set looped
-over. The script also optimizes by not checking variables $a_0^n$ and $a_I^n$
-since they always stay the same anyways. The minimization is done by
+conversion and said script is listed in Listing~\ref{listing:a4.bash}. The
+Python script optimizes a little bit from the original formula by leaving out
+the $i=j$ comparison in subformula 17 and 18 by removing them from the set
+looped over. The script also optimizes by not checking variables $a_0^n$ and
+$a_I^n$ since they always stay the same anyways. The minimization is done by
incrementing variable $N$ every time the current $N$ yields unsat with a bash
script shown in Listing~\ref{listing:4.bash}.
-\lstinputlisting[language=bash,
+\lstinputlisting[language=bash,firstline=58,
caption={Iteratively find the shortest solution for problem 4},
label={listing:4.bash}]{src/a4.bash}
\subsection{Solution}
The bash script finds and shows the minimal solution in which the postcondition
-is satisfied for $N=11$. Finding this solution takes less then $75$ seconds and
+is satisfied for $N=10$. Finding this solution takes less then $75$ seconds and
is shown in Table~\ref{tab:s4}.
Every line in the table represents the iteration and the bold items represent
label={listing:a2.py}]{src/a2.py}
\newpage
-\lstinputlisting[language=python,caption={a3.py},
- label={listing:a3.py}]{src/a3.py}
+\lstinputlisting[language=python,caption={a3.bash},
+ label={listing:a3.py}]{src/a3.bash}
\newpage
-\lstinputlisting[language=python,caption={a4.py},
- label={listing:a4.py}]{src/a4.py}
+\lstinputlisting[language=python,caption={a4.bash},
+ label={listing:a4.bash}]{src/a4.bash}
i=$((i+1))
done
echo "n(p)=$i is unsat thus maximum n(p)=$((i-1))"
-sed "s/<REP>/$((i-1))/g" a1.smt | yices-smt -m
my = 22
pd = 17
-
# Print variables and preamble
print('(benchmark a4.smt')
print(':logic QF_UFLIA')
+#!/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
+++ /dev/null
-#!/usr/bin/env python3
-import sys
-
-if len(sys.argv) != 2:
- print('usage: {} maxjobstart'.format(sys.argv[0]))
- exit()
-
-maxjobstart = sys.argv[1]
-jobs = 12
-J = range(1, jobs+1)
-Jprime = {5, 7, 10}
-pi = {
- 3: {1, 2},
- 5: {3, 4},
- 7: {3, 4, 6},
- 9: {5, 8},
- 11: {10},
- 12: {9, 11}
-}
-
-# Print variables and preamble
-print('(benchmark a4.smt')
-print(':logic QF_UFLIA')
-print(':extrafuns (')
-for i in J:
- print('(j{} Int)'.format(i), end=' ')
-print('\n)')
-
-print(':formula')
-print('(and')
-for i in J:
- # Make sure the times are positive and within the bound
- print('(> j{0} 0) (<= (+ j{0} {0}) {1})'.format(i, maxjobstart))
- # Make sure the dependencies are done when a task is scheduled
- for k in pi.get(i, {}):
- print('(>= j{0} (+ j{1} {1}))'.format(i, k))
-# Make sure the shared resources are not used by two tasks at once
-for i in Jprime:
- for k in Jprime:
- if i != k:
- print('(or (>= j{0} (+ j{1} {1}))'.format(i, k), end=' ')
- print('(<= (+ j{0} {0}) j{1}))'.format(i, k))
-
-# Close the and,benchmark parenthesis
-print('))')
+#!/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
+++ /dev/null
-#!/usr/bin/env python3
-import sys
-if len(sys.argv) != 2:
- print("usage: {} maxiterations".format(sys.argv[0]))
- exit()
-
-iterations = int(sys.argv[1]) if len(sys.argv) > 1 else 11
-numa = 7
-
-# Print variables and preamble
-print("(benchmark a4.smt")
-print(":logic QF_UFLIA")
-print(":extrafuns (")
-print("(a{} Int)".format(1))
-print("(a{} Int)".format(numa))
-for i in range(iterations):
- for v in range(2, numa):
- print("(i{}a{} Int) ".format(i, v))
-print(")")
-
-# Print preconditions
-print(":formula")
-print("(and")
-print("(= a1 1)")
-print("(= a{0} {0})".format(numa, numa))
-for i in range(2, numa):
- print("(= i0a{0} {0})".format(i))
-
-# Print iterations
-for i in range(1, iterations):
- print("(or")
- for v in range(2, numa):
- print("(and")
- for ov in [k for k in range(2, numa) if k != v]:
- print("(= i{0}a{1} i{2}a{1})".format(i, ov, i-1))
- im1 = 'a1' if v == 2 else 'i{}a{}'.format(i, v-1)
- ip1 = 'a{}'.format(numa) if v == numa-1 else 'i{}a{}'.format(i-1, v+1)
- print("(= i{}a{} (+ {} {}))".format(i, v, im1, ip1))
- print(")")
- print(")")
-
-# Post conditions
-print("(or")
-for v in range(2, numa):
- print("(and (>= i{}a{} 50)".format(iterations-1, v))
- print("(or")
- for ov in [k for k in range(2, numa) if k != v]:
- print("(= i{0}a{1} i{0}a{2})".format(iterations-1, v, ov))
- print("))")
-print(")")
-
-# Close the and,benchmark parenthesis
-print("))")
repositories / master.git / commitdiff