#!/bin/sh
CONF="true"
COLDIR=$(realpath $(dirname $0))
MEMLIMIT=3000
INTERPRETER="false"

GOAL="solve('smt_colibri.in')"

while test $# != 0; do
    case "$1" in
        "--version")
            cat $COLDIR/version
            exit 0
            ;;
        "--help")
            echo "COLIBRI SMTLIB2_FILE [OPTIONS]

--version   print version
--help      print this help
--memlimit  set memlimit in Megabyte (default 3000)
--conf      evaluate the prolog expression (default true)

Specific heuristics:
--per-call-simplex-timeout [sec]   timeout for each call of the rational simplex
--delay-simplex-deactivation [sec] stop delta and simplex algorithm after the given time (0 always activated)
--external-simplex [name]          use the specified external solver (QF_LRA) instead of internal simplex
                                   acceptable values are (z3, z3-debug -- prints z3 inputs outputs to /tmp/{input,output}.smt2)
"
            exit 0
            ;;
        "--memlimit")
            #Keep space for other stuff a fixed 300M and 10% of given argument
            MEMLIMIT=$(expr \( \( "$2" - 300 \) "*" 9 \) \/ 10)
            shift
            ;;
        "--conf")
            CONF="$CONF,$2"
            shift
            ;;
        "--per-call-simplex-timeout")
            CONF="$CONF,set_simplex_timeout($2)"
            shift
            ;;
        "--delay-simplex-deactivation")
            CONF="$CONF,setval(simplex_delay_deactivation,$2)"
            shift
            ;;
        "--external-simplex")
            export COLIBRI_USE_SOLVER=$2
            PATH=$COLDIR/qf_lra_solver/:$PATH
            shift
            ;;
        "--interpreter-mode")
            INTERPRETER="true"
            ;;
        *)
            GOAL="smt_solve('$1')"
    esac
    shift
done

# Repertoire ECLiPSe Prolog
ECLIPSEDIR=$COLDIR/ECLIPSE
FILTER_SMTLIB_FILE=$COLDIR/COLIBRI/filter_smtlib_file
# Architecture
ARCH="x86_64"
LD_LIBRARY_PATH=${ECLIPSEDIR}/lib/${ARCH}_linux:$LD_LIBRARY_PATH
export FILTER_SMTLIB_FILE ECLIPSEDIR ARCH LD_LIBRARY_PATH 

if $INTERPRETER; then
# Chargement/demarrage de test_colibri
exec ${ECLIPSEDIR}/lib/${ARCH}_linux/eclipse.exe \
     -b ${COLDIR}/COLIBRI/compile_flag -b ${COLDIR}/COLIBRI/col_solve \
     -g ${MEMLIMIT}M
else
# Chargement/demarrage de test_colibri
exec ${ECLIPSEDIR}/lib/${ARCH}_linux/eclipse.exe \
     -b ${COLDIR}/COLIBRI/compile_flag -b ${COLDIR}/COLIBRI/col_solve \
     -g ${MEMLIMIT}M -e "seed(0),${CONF},${GOAL}"
fi