#!/bin/bash
# enter a bash shell

# This script will enable you to run the 'sbv -n MAX 'program 
# for repeated values of MAX
#
# Note that this script is rather ugly (but it avoids some annoying
# data parsing).  It might also exceed the MAXTIME for a run due
# softness issues in the timing.
#
# Edit the parameters as your need to.
#
# NOTE: IF YOUR PROGRAM HAS OUTPUT, IT WILL MAKE THE OUTPUT A MESS



# Set formatting for time
TIMEFORMAT=%U

# initial value for MAX
MAX=1 

# maximum number of nodes to be tested
MAXNODES=32768

# set maximum core dump size to 1
ulimit -Sc 0

# When the limit on CPU time is reached, a core file is created
while [ $MAX -le $MAXNODES ]; do

  # output value of MAX and the time sbv takes using method AND1
  echo -n "MAX= $MAX   TIME= "

  # The time builtin wants to write to the standard error stream (file
  # descriptor 2).  But we really would like it to write to the
  # standard output stream (file descriptor 1).  Luckily, Bourne-style
  # shells allow us to manipulate file descriptors at will.

  # First, we "save the old value" of file descriptor 2.  We do that
  # by making file descriptor 3, which is normally unused, be a copy
  # of file descriptor 2.
  exec 3>&2

  # Then, we make file descriptor 2 be a copy of file descriptor 1 (so
  # anything written to the standard error stream ends up being output
  # to the standard output stream).
  exec 2>&1

  # Then, we run the time command -- now that we tricked it into
  # writing to the standard output stream.
  time ./sbv AND2 -n $MAX

  # Then, we "restore the old value" of file descriptor 2.
  exec 2>&3

  # Finally, we close the file descriptor 3, as it's no longer needed.
  exec 3>&-

  # ??? It might be better to move this file descriptor manipulations
  # ??? outside the loop.

  sleep 1

  let "MAX=MAX*2"
  
done

# Clean up the script's mess
unset TIMEFORMAT
ulimit -c unlimited