diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-10 23:17:14 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-10 23:17:14 +0200 |
| commit | 1f6cb381b91fc40d1e6b7c6ae1f022077f6091de (patch) | |
| tree | 3795bfb60eb28dfa62430d600986eb12fca25eb1 /test/monniaux/minisat | |
| parent | a3d856e24b2ac6577678a1535e4d15316cf0755c (diff) | |
| download | compcert-kvx-1f6cb381b91fc40d1e6b7c6ae1f022077f6091de.tar.gz compcert-kvx-1f6cb381b91fc40d1e6b7c6ae1f022077f6091de.zip | |
for running benchmarks on marte
Diffstat (limited to 'test/monniaux/minisat')
| -rw-r--r-- | test/monniaux/minisat/Makefile.on_marte | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/test/monniaux/minisat/Makefile.on_marte b/test/monniaux/minisat/Makefile.on_marte new file mode 100644 index 00000000..af7b9145 --- /dev/null +++ b/test/monniaux/minisat/Makefile.on_marte @@ -0,0 +1,16 @@ +EXE=minisat.ccomp.exe minisat.ccomp.trace-linearize.exe \ + minisat.gcc-O3.exe \ + minisat.ccomp.profiled.exe minisat.gcc-O3.profiled.exe + +LOG=$(EXE:.exe=.dat) + +all: $(LOG) + +%.log : %.exe + rm -f $@ + for i in `seq 1 1000` ; do ./$< sudoku.sat >> $@; done + +%.dat : %.log + grep 'time cycles: ' $< | sed -e 's/time cycles: //' | awk '{ total += $$1; count++ } END { print total/count }' > $@ + +.SECONDARY: |