#!/bin/bash
#
# File:  runz3
# Author:  mikolas
# Created on:  Fri Dec 7 13:49:17 WET 2012
# Copyright (C) 2012, Mikolas Janota
#
# qcnf2z3.py and z3 need to be on the path
if [[ $# < 1 ]]; then
    echo "Usage: $0 instance [timeout]"
    exit 100;
fi


if [[ $# > 1 ]]; then TMA="-T:${2}"
else TMA=""
fi

TF=/tmp/runz3_${RANDOM}
file=$1
if [[ $file == *.gz ]]
then 
 CATCMD=zcat
else
 CATCMD=cat
fi
$CATCMD $file | qcnf2z3.py | z3 ${TMA} 'AUTO_CONFIG=false' -smt2 -in >$TF
if [ $? != 0 ]; then 
  echo "z3 did not run correctly"
  exit 400
fi

RETV=300
if grep -q -we '^unsat' $TF; then RETV=20;
elif grep -q -we '^sat' $TF; then RETV=10; fi
FIRST_QLINE=`$CATCMD $file | grep -m1 -e '^[ae] '`
if [ "${FIRST_QLINE:0:1}" == 'a' ]; then # swap result for formulas starting with FORALL
  if [ $RETV == 10 ]; then RETV=20
  elif [ $RETV == 20 ]; then RETV=10 
  fi
fi  
if [ $RETV == 10 ]; then echo 's cnf 1'; fi
if [ $RETV == 20 ]; then echo 's cnf 0'; fi
/bin/rm -f $TF
exit $RETV