ostrich-client

#!/bin/sh

dotfilebase="/tmp/.ostrich"

JAVA=java
JAVA_OPTS="-Xss20000k -Xmx1500m"

me=`whoami`
portfile="$dotfilebase"_"$me"
errfile="$dotfilebase"_debug_"$me"

if [ $(uname) = "Linux" ]; then
    pathCmd="readlink -f"
elif [ $(uname) = "Darwin" ]; then
    pathCmd="stat -f %N"
else
    pathCmd="realpath"
fi

################################################################################

startDaemon() {
    lockfile="$dotfilebase"_lock_"$me"

    while [ -f "$lockfile" ] && \
          [ $(( `date +%s` - `date -r "$lockfile" +%s` )) -le 10 ]; do
        # apparently a concurrent script is starting up the daemon
        # already
        echo "waiting ..."
        sleep 1
    done
        
    if [ ! -f "$portfile" ]; then
        touch "$lockfile"

        BASEDIR=`dirname $($pathCmd $0)`
        TARGET=`echo $BASEDIR/target/scala-*/ostrich-assembly*.jar`

        tempportfile=`mktemp`
        touch "$tempportfile"
        chmod go-rwx "$tempportfile"

	$JAVA $JAVA_OPTS -cp $TARGET ap.ServerMain >"$tempportfile" &

        ostrichId=$!

        sleep 1
        while [ `wc -l "$tempportfile" | awk '{ printf $1 }'` -lt 2 ]; do
	    if ps -p $ostrichId >/dev/null; then
		sleep 1
	    else
		echo "Could not start server"
		exit 1
	    fi
        done

        mv "$tempportfile" "$portfile"
        rm "$lockfile"

        # Make sure that the daemon knows about the string portfolios; for
        # this, we have to start solving some initial string problem

        $BASEDIR/ostrich-client -timeout=0 $BASEDIR/tests/1234.corecstrs.readable.smt2 >/dev/null
    fi
}

################################################################################

stdintoexitstatus() {
  read exitstatus
  return $exitstatus
}

if [ ! -f "$portfile" ]; then
    startDaemon
fi

mainProcess=$$

outputlogfile=`mktemp`

success=1
until [ $success -eq 0 ]; do

    port=`head -n1 "$portfile"`

    (
        # send the ticket
        tail -n1 "$portfile"

        # command line arguments
        ostrichSolver=ostrich.OstrichStringTheory
        ostrichParams=""

        for var; do
	    case "$var" in
                [+-]eager | [+-]forward | -length=* | [+-]minimizeAutomata | [+-]parikh | -regexTranslator=* | [+-]forwardPropagation | [+-]backwardPropagation | [+-]nielsenSplitter)
                    if [ x"$ostrichParams" = x"" ]; then
                        ostrichParams=$var
                    else
                        ostrichParams=$ostrichParams,$var
                    fi
                    ;;
                -cea)
                    ostrichSolver=ostrich.OstrichStringTheory
                    ;;
                +cea)
                    ostrichSolver=ostrich.cesolver.stringtheory.CEStringTheory
                    ;;
		-*|+*)
		    echo "$var"
		    ;;
		*)
		    echo `$pathCmd "$var"`
		    ;;
	    esac
        done

        echo "-stringSolver=$ostrichSolver:$ostrichParams"

        echo "PROVE_AND_EXIT"

        # ping the daemon every second, to show that we are still
        # alive
        {
            sleep 1
            while ps -p $mainProcess >/dev/null; do
                echo "PING"
                sleep 1
            done
        } &
    ) | (((( nc localhost $port; echo $? >&3 ) | \
      tee $outputlogfile >&4) 3>&1) | stdintoexitstatus) 4>&1

    success=$?

    if [ $success -ne 0 ]; then
        rm "$portfile"
        startDaemon
    else if grep -q '^ERROR:' $outputlogfile; then
	rm $outputlogfile
	exit 1
    fi; fi

done

rm $outputlogfile