hexiom/parse.sh

   1 #!/bin/bash
   2 source ../common.sh
   3 BEGIN=*"begin iteration"*
   4 EXECTIME=*"Program Execution Time"*
   5 SATCSOLVTIME=*"SAT Solving time"*
   6 SATTIME=*"c CPU time"*
   7
   8 row=""
   9 timeout=0
  10
  11
  12 while IFS='' read -r line || [[ -n "$line" ]]; do
  13         if [[ $line == $EXECTIME ]]; then
  14                 number=$(echo $line|grep -Eo '[+-]?[0-9]+([.][0-9]+)?')
  15                 if [[ $timeout == 0 ]]; then
  16                         row+=",-"
  17                 fi
  18                 timeout=0
  19                 row+=","$number
  20         fi
  21
  22         if [[ $line == $SATCSOLVTIME ]]; then
  23                 number=$(echo $line|grep -Eo '[+-]?[0-9]+([.][0-9]+)?')
  24                 row+=","$number
  25                 timeout=1
  26         fi
  27
  28         if [[ $line == $SATTIME ]]; then
  29                 number=$(echo $line|grep -Eo '[+-]?[0-9]+([.][0-9]+)?')
  30                 row+=","$number
  31         fi
  32
  33 done < "$1"
  34 echo "$2$row" >> $OFILE