Newer
Older
#!/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