#!/bin/bash

if [ $# -ne 2 ] 
then
    echo "usage: ./run.sh BENCHMARK TMPDIR" 
    exit 1
fi

TMPDIR=$2
SATELITE=./SatElite
REVIVAL=./revival
MINISAT=./minisat  

TMP=bench
TMP_1=${TMPDIR}/bench.viv.cnf
TMP_2=${TMPDIR}/bench.viv.sat.cnf

echo -n "c revival is preprocessing the formula..."
$REVIVAL $1 500 > $TMP_1 #&> /dev/null
echo "done !"


echo "c Now, SatElite..."
$SATELITE $TMP_1 $TMP_2 ${TMPDIR}/$TMP.vmap ${TMPDIR}/$TMP.elim
X=$?
if [ $X == 0 ]; then
  #SatElite terminated correctly
    echo "c SatElite is done !"
    echo "c Calling MINISAT"
    $MINISAT $TMP_2 ${TMPDIR}/$TMP.result "$@"
    X=$?
    if [ $X == 20 ]; then
    	echo "s UNSATISFIABLE"
	exit 20
    #Don't call SatElite for model extension.
    elif [ $X != 10 ]; then
    #timeout/unknown, nothing to do, just clean up and exit.
	exit $X
    fi 
    
  #SATISFIABLE, call SatElite for model extension
    echo "c SatElite Model extension..."
    $SATELITE +ext $TMP_1 ${TMPDIR}/$TMP.result ${TMPDIR}/$TMP.vmap ${TMPDIR}/$TMP.elim $@
    X=$?
    
elif [ $X == 11 ]; then
  #SatElite died, RSat must take care of the rest
    echo "SatElite died... trying RSAT..."
    $MINISAT $TMP_1 "$@" -s #but we must force rsat to print out result here!!!
    X=$?
elif [ $X == 12 ]; then
  #SatElite prints out usage message
  #There is nothing to do here.
    X=0
fi

exit $X
