1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
|
#!/bin/bash
dir="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )"
boolector=$dir/../../../../build/bin/boolector
mmcomm=$dir/../../../../build/bin/examples/matrixmultcomm
numbits=32
for ((size=2;size<=12;size+=1))
do
header=1
if [[ $size -lt 10 ]]; then
sizestring=0$size
else
sizestring=$size
fi
filename=matrixmultcomm$sizestring".smt2"
$mmcomm $numbits $size | $boolector -rwl 0 -ds | while read line
do
if [[ $header -eq 1 ]]; then
echo "(set-info :source |" >> $filename
echo -n "This benchmark shows that matrix multiplication" >> $filename
echo "is not commutative in general." >> $filename
echo "We try to show that A x B = B x A, which is generally not the case". >> $filename
echo -n "The matrices have $size * $size fields of " >> $filename
echo "bit-width $numbits," >> $filename
echo "and are respectively represented by a one-dimensional array." >> $filename
echo "" >> $filename
echo -n "Contributed by Robert Brummayer " >> $filename
echo "(robert.brummayer@gmail.com)." >> $filename
echo "|)" >> $filename
echo "(set-info :status sat)" >> $filename
echo "(set-info :category crafted)" >> $filename
header=0
else
echo $line >> $filename
fi
done
done
|
