diff options
author | Karel Kočí <cynerd@email.cz> | 2015-05-05 11:58:26 +0200 |
---|---|---|
committer | Karel Kočí <cynerd@email.cz> | 2015-05-05 11:58:26 +0200 |
commit | dfe47d067a70f9781e3b431f6a685090bf87ff40 (patch) | |
tree | 5151ba40cdd422e9f9bbbba0398b2a569ba88311 /scripts/picosat-959/configure | |
parent | 289b0ce128cdca79676307646eef3d56c25c6dd2 (diff) | |
download | linux-conf-perf-dfe47d067a70f9781e3b431f6a685090bf87ff40.tar.gz linux-conf-perf-dfe47d067a70f9781e3b431f6a685090bf87ff40.tar.bz2 linux-conf-perf-dfe47d067a70f9781e3b431f6a685090bf87ff40.zip |
Add picosat version 959
Diffstat (limited to 'scripts/picosat-959/configure')
-rwxr-xr-x | scripts/picosat-959/configure | 127 |
1 files changed, 127 insertions, 0 deletions
diff --git a/scripts/picosat-959/configure b/scripts/picosat-959/configure new file mode 100755 index 0000000..ca5ec77 --- /dev/null +++ b/scripts/picosat-959/configure @@ -0,0 +1,127 @@ +#!/bin/sh + +satcompetition=no + +log=no +debug=no +stats=undefined +trace=undefined +static=yes +shared=no +thirtytwobit=no +static=no + +while [ $# -gt 0 ] +do + case $1 in + -g|--debug) debug=yes;; + -O|--optimize) debug=no;; + -l|--log) log=yes;; + -s|--stats) stats=yes;; + -t|--trace) trace=yes;; + --no-stats) stats=no;; + --no-trace) trace=no;; + -32|--32|-m32) thirtytwobit=yes;; + -static|--static) static=yes;; + -shared|--shared) shared=yes;; + *) cat <<EOF +usage: ./configure [<option> ...] + +where <option> is one of the following: + + -g|--debug include debugging code and symbols + -O|--optimize optimized compilation (default) + -l|--log add low level logging code (default with '-g') + -s|--stats more expensive statististcs (default with '-g') + -t|--trace trace generation (more memory, default with '-g') + --no-stats disable expensive stats + --no-trace enable trace generation + -32|--32|-m32 compile for 32 bit machine even on 64 bit host + -static|--static produce static binary + -shared|--shared produce shared library +EOF +exit 1 +;; + esac +shift +done + +echo "version ... `cat VERSION`" + +if [ $satcompetition = yes ] +then + debug=no + stats=no + trace=no + thirtytwobit=yes + static=yes + shared=no +fi + +echo "debug ... $debug" +echo "log ... $log" + +[ $stats = undefined ] && stats=$debug +echo "stats ... $stats" + +[ $trace = undefined ] && trace=$debug +echo "trace ... $trace" + +echo "static ... $static" + +echo "shared ... $shared" + +[ "X$CC" = X ] && CC=gcc + +if [ X"$CFLAGS" = X ] +then + case X"$CC" in + *wine*|*mingw*) CFLAGS="-DNGETRUSAGE -DNALLSIGNALS";; + *);; + esac + [ $log = yes ] && CFLAGS="$CFLAGS -DLOGGING" + [ $stats = yes ] && CFLAGS="$CFLAGS -DSTATS" + [ $trace = yes ] && CFLAGS="$CFLAGS -DTRACE" + [ $static = yes ] && CFLAGS="$CFLAGS -static" + case X"$CC" in + X*gcc*) + CFLAGS="$CFLAGS -Wall -Wextra" + [ $thirtytwobit = yes ] && CFLAGS="$CFLAGS -m32" + if [ $debug = yes ] + then + CFLAGS="$CFLAGS -g3 -ggdb" + else + CFLAGS="$CFLAGS -DNDEBUG -O3" + fi + ;; + *) + if [ $debug = yes ] + then + CFLAGS="$CFLAGS -g" + else + CFLAGS="$CFLAGS -O" + fi + ;; + esac +fi + +TARGETS="picosat picomcs picomus picogcnf libpicosat.a" +if [ $shared = yes ] +then + TARGETS="$TARGETS libpicosat.so" + CFLAGS="$CFLAGS -fPIC" +fi +echo "targets ... $TARGETS" + +echo "cc ... $CC" + +echo "cflags ... $CFLAGS" + +printf "makefile ..." +rm -f makefile +sed \ + -e "s,@CC@,$CC," \ + -e "s,@CFLAGS@,$CFLAGS," \ + -e "s,@TARGETS@,$TARGETS," \ +makefile.in > makefile +echo " done" |