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