#!/bin/sh

# Top-level script for RSat SAT-2009 competition

# usage ./rsat.sh <cnf file> <tmp dir>

if [ "x$1" = "x" ]; then
  echo "USAGE: SatELiteGTI <input CNF>"
  exit 1
fi

tmp_dir=/tmp

if [ "$#" -gt 1 ]; then
    tmp_dir=$2;
fi

INPUT=$1;
name=${INPUT##*/}

pid=$$

TMP=$tmp_dir/SatElite_temp_"$name"_pid$pid #set this to the location of temporary files
SE=./SatElite           #set this to the executable of SatELite
RS=./rsat               #set this to the executable of RSat
shift 

$SE $INPUT $TMP.cnf $TMP.vmap $TMP.elim
X=$?

if [ "$X" = 0 ]; then
  #SatElite terminated correctly
  $RS $TMP.cnf -q -r $TMP.result "$@"
  X=$?
  if [ "$X" = 20 ]; then
    #RSat must not print out result!
    echo "s UNSATISFIABLE"
    rm -f $TMP.cnf $TMP.vmap $TMP.elim $TMP.result
    exit 20
    #Don't call SatElite for model extension.
  elif [ "$X" != 10 ]; then
    #timeout/unknown, nothing to do, just clean up and exit.
    rm -f $TMP.cnf $TMP.vmap $TMP.elim $TMP.result
    exit $X
  fi 
  
  #SATISFIABLE, call SatElite for model extension
  #echo c Calling SatELite for actual solution
  $SE +ext -s $INPUT $TMP.result $TMP.vmap $TMP.elim "$@"
  X=$?
elif [ "$X" = 11 ]; then
  #SatElite died, RSat must take care of the rest
  $RS $INPUT "$@" -s #but we must force rsat to print out result here!!!
  X=$?
fi    

rm -f $TMP.cnf $TMP.vmap $TMP.elim $TMP.result
exit $X
