#! /bin/bash

INST=${INST:=''}
RESULTSTRING=${RESULTSTRING:=''}
MODELCHECK=${MODELCHECK:='modelcheck.asp'}
VALIDITYENC=${VALIDITYENC:='validity.asp'}
UNSATENC=${UNSATENC:='unsatisfiable.asp'}
EQCHECKENC=${EQCHECKENC:='eq.asp'}
GRINGO=${GRINGO:='gringo'}
CLASPD=${CLASPD:='claspD-1.1.2'}
ITERATIONS=${ITERATIONS:='5'}
CURITER=${CURITER:='0'}
TMPFILE_REMAININGARGS=${TMPFILE_REMAININGARGS:=''}
TMPFILE_UNDECARGS=${TMPFILE_UNDECARGS:=''}
ACCEPTEDARGS=${ACCEPTEDARGS:=''}
REJECTEDARGS=${REJECTEDARGS:=''}
RESULT=${RESULT:=''}
CHANGE=${CHANGE:='0'}
TMPACC=${TMPACC:=''}
TMPREJ=${TMPREJ:=''}
WORKINGDIR=${WORKINGDIR:=''}

accrej() {
if [ "$ACCEPTEDARGS" == "" ]; then
  TMPACC=""
else
  TMPACC="assigned_true($ACCEPTEDARGS)."
fi

if [ "$REJECTEDARGS" == "" ]; then
  TMPREJ=""
else
  TMPREJ="assigned_false($REJECTEDARGS)."
fi

}

WORKINGDIR=`dirname $0`

# get instance/result file
INST=$1
RESULTSTRING=$2

if [ "$INST" == "" ]; then
  echo "usage ./" $0 " instancefile resultstring"
  echo "Note: resultstring may be empty."
  exit 1
fi

# get number of iterations (i.e. the number of statements in the adf)
ITERATIONS=`grep "ac" $INST  | wc -l`

# write all statements to temp file, 
TMPFILE_REMAININGARGS=`mktemp`
TMPFILE_UNDECARGS=`mktemp`
grep "ac" $INST  | awk -F "[(,)]" '{print $2}' > $TMPFILE_REMAININGARGS

# for number of its
while [ $CURITER -lt $ITERATIONS ]
do

  # set to initial state
  tail $TMPFILE_UNDECARGS > $TMPFILE_UNDECARGS
  CHANGE=0

  # read all remaining args
  while read ARG
  do
    # echo testing for: $ARG

    # VALIDITY check
    accrej
    RESULT=`grep "ac($ARG," $INST | $WORKINGDIR/$GRINGO - $WORKINGDIR/$MODELCHECK $WORKINGDIR/$VALIDITYENC <(echo $TMPACC $TMPREJ) 2> /dev/null | $WORKINGDIR/$CLASPD -q | grep "Models" | awk '{print $3}'`
    
    # ac is valid
    if [ "$RESULT" == "1" ]; then
#       echo "VALID"

      # add to accepted args
      if [ "$ACCEPTEDARGS" == "" ]; then
	ACCEPTEDARGS=$ARG
      else
	ACCEPTEDARGS=$ACCEPTEDARGS";"$ARG
      fi

      # found a new accepted arg => continue after this iteration
      CHANGE=1
      continue
    fi

    # UNSATISFIABILE check
    accrej
    RESULT=`grep "ac($ARG," $INST | $WORKINGDIR/$GRINGO - $WORKINGDIR/$MODELCHECK $WORKINGDIR/$UNSATENC <(echo $TMPACC $TMPREJ) 2> /dev/null | $WORKINGDIR/$CLASPD -q | grep "Models" | awk '{print $3}'`
    
    # ac is unsat
    if [ "$RESULT" == "1" ]; then
#       echo "UNSAT"

      # add to rejected args
      if [ "$REJECTEDARGS" == "" ]; then
	REJECTEDARGS=$ARG
      else
	REJECTEDARGS=$REJECTEDARGS";"$ARG
      fi

      # found a new rejected arg => continue after this iteration
      CHANGE=1
      continue
    fi

    # still undecided
    echo $ARG >> $TMPFILE_UNDECARGS

  done < $TMPFILE_REMAININGARGS

  # copy undecided to remaining
  cat $TMPFILE_UNDECARGS > $TMPFILE_REMAININGARGS

  # check for changes
  if [ "$CHANGE" == "0" ]; then
    break
  fi

  # advance iteration
  CURITER=$[$CURITER+1]
done

DEBUGMODE="no"
if [ "$DEBUGMODE" == "yes" ]; then
# test output
echo accepted: $ACCEPTEDARGS
echo rejected: $REJECTEDARGS
echo undecided: 
cat $TMPFILE_REMAININGARGS
fi

# check with given solution
# echo "comparison with given solution"
accrej
if [ "$TMPACC" == "" ]; then
  TMPACC=""
fi
if [ "$TMPREJ" == "" ]; then
  TMPREJ=""
fi

# make an asp call that checks equality
RESULT=`$WORKINGDIR/$GRINGO $WORKINGDIR/$EQCHECKENC $INST <(echo $RESULTSTRING $TMPACC $TMPREJ) 2> /dev/null | $WORKINGDIR/$CLASPD | grep "cost" | awk -F"[,()]" '{print $2"@2 "$3"@1"}'`

rm $TMPFILE_REMAININGARGS
rm $TMPFILE_UNDECARGS

# output result
if [ "$RESULT" != "" ]; then
  echo "OK $RESULT"
  exit 0
else
  echo "NOK"
  exit 0
fi
