1#!/bin/sh 2 3echo "checking for assert/signal/error/terminate fail" 4xzgrep --color -i -e "assert.*fail" -e "floating" -e "signal" -e "error" -e "terminate" *.out.xz | tee issues.csv 5echo "checking for signal 4" 6xzgrep "signal 4" issues.csv 7 8# 1500 cutoff 9echo "Getting solveTimes" 10xzgrep "CPU time" *.out.xz | awk '{print $5 " "$1}' | sed 's/:c.*$//' > solveTimes_xz.csv 11echo "Getting problems solved under 1500" 12awk '{if ($1 < 1500) {print $2}}' solveTimes_xz.csv | sort > solved_under_1500_full_list_xz.csv 13awk '{print $2}' solveTimes_xz.csv | sort > solved_xz.csv 14sed 's/.gz.*/.gz/' solved_xz.csv > solved.csv 15sed 's/.gz.*/.gz/' solveTimes_xz.csv | sort -n > solveTimes.csv 16ls -- *.out.xz > allFiles_xz.csv 17ls -- *.out.xz | sed "s/.gz.*/.gz/" > allFiles.csv 18 19# for normal 20echo "Getting SAT & UNSAT" 21xzgrep "^s UNSATISFIABLE" $(cat solved_xz.csv) | sed 's/:s.*$//' | sed 's/.gz.*/.gz/' | sort > solvedUNSAT.csv 22xzgrep "^s SATISFIABLE" $(cat solved_xz.csv) | sed 's/:s.*$//' | sed 's/.gz.*/.gz/' | sort > solvedSAT.csv 23 24# adjusting solved.csv, solveTimes.csv, solveTimes_rev.csv 25echo "Getting solveTimes_rev.csv" 26sed "s/^/\^/" solved.csv | sed "s/$/\$/" > solved_filtering.csv 27grep -v -f solved_filtering.csv allFiles.csv | sed "s/.gz.*/.gz/" > unsolved.csv 28rm solved_filtering.csv 29grep -v -f solved_xz.csv allFiles_xz.csv > unsolved_xz.csv 30cat unsolved.csv | awk '{print "5000.00 " $1}' >> solveTimes.csv 31awk '{print $2 " " $1}' solveTimes.csv | sort > solveTimes_rev.csv 32 33# memory out 34echo "Getting memout..." 35xzgrep "what.*bad.*alloc" $(cat unsolved_xz.csv) | sed "s/.gz.*/.gz/" | sort > memout.csv 36sed "s/^/\^/" memout.csv | sed "s/$/\$/" > memout_filtering.csv 37grep -v -f memout_filtering.csv allFiles.csv | sed "s/.gz/.gz OK/" > memout2.csv 38rm memout_filtering.csv 39cat memout.csv | sed "s/.gz/.gz BAD/" >> memout2.csv 40sort memout2.csv > memout3.csv 41rm memout.csv memout2.csv 42mv memout3.csv memout.csv 43 44# 1500 cutoff 45echo "Getting 1500 UNSAT" 46xzgrep "^s UNSATISFIABLE" $(cat solved_under_1500_full_list_xz.csv) | sed 's/:s.*$//' | sed 's/.gz.*/.gz/' | sort > solvedUNSAT1500.csv 47echo "Getting 1500 SAT" 48xzgrep "^s SATISFIABLE" $(cat solved_under_1500_full_list_xz.csv) | sed 's/:s.*$//' | sed 's/.gz.*/.gz/' | sort > solvedSAT1500.csv 49rm -f solved1500.csv 50cat solvedUNSAT1500.csv > solved1500.csv 51cat solvedSAT1500.csv >> solved1500.csv 52 53cat solvedSAT.csv | awk '{print $1 " SAT"}' > solved_sol.csv 54cat solvedUNSAT.csv | awk '{print $1 " UNSAT"}' >> solved_sol.csv 55cat unsolved.csv | awk '{print $1 " UNKN"}' >> solved_sol.csv 56sort solved_sol.csv > solved_sol2.csv 57rm solved_sol.csv 58mv solved_sol2.csv solved_sol.csv 59 60 61xzgrep signal *.timeout.xz | sed -E "s/.timeout.*signal (.*)/ \1/" > signals.csv 62xzgrep signal *.timeout.xz | sed -E "s/.timeout.*signal (.*)//" > signals_files.csv 63sed "s/^/\^/" signals_files.csv | sed "s/$/\$/" > signals_files_filtering.csv 64grep -v -f signals_files_filtering.csv allFiles.csv | awk '{print $1 " -1"}' >> signals.csv 65rm signals_files_filtering.csv 66sort signals.csv > signals_sorted.csv 67rm signals.csv signals_files.csv 68mv signals_sorted.csv signals.csv 69grep " 11" signals.csv 70awk '{if ($1=="5000.00") {x+=10000} else {x += $1};} END {printf "%d\n", x}' solveTimes.csv > PAR2score 71echo "PAR2 score is: " `cat PAR2score` 72 73xzgrep "ASSIGNMENT FOUND" *.out.xz | sed "s/.out.*//" > walksat_sat.csv 74grep -v -f walksat_sat.csv allFiles.csv | sed "s/.gz/.gz FALL/" > walksat_nosat.csv 75sed "s/$/ WALK/" walksat_sat.csv > walksat_sat2.csv 76cat walksat_sat2.csv walksat_nosat.csv | sort > walksat.csv 77 78 79 80../concat_files.py > combined.csv 81