diff options
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/Makefile.am | 5 | ||||
| -rwxr-xr-x | contrib/cut-release | 4 | ||||
| -rwxr-xr-x | contrib/get-abc | 8 | ||||
| -rwxr-xr-x | contrib/run-script-cascj7-fnt | 6 | ||||
| -rwxr-xr-x | contrib/run-script-cascj7-fof | 6 | ||||
| -rwxr-xr-x | contrib/run-script-cascj7-tff | 6 | ||||
| -rwxr-xr-x | contrib/run-script-smtcomp2014 | 3 |
7 files changed, 26 insertions, 12 deletions
diff --git a/contrib/Makefile.am b/contrib/Makefile.am index b707a9140..ad3b6f220 100644 --- a/contrib/Makefile.am +++ b/contrib/Makefile.am @@ -13,7 +13,10 @@ EXTRA_DIST = \ get-antlr-3.4 \ mac-build \ win32-build \ - run-script-smtcomp2012 \ + run-script-smtcomp2014 \ + run-script-cascj7-fnt \ + run-script-cascj7-fof \ + run-script-cascj7-tff \ theoryskel/kinds \ theoryskel/README.WHATS-NEXT \ theoryskel/theory_DIR.cpp \ diff --git a/contrib/cut-release b/contrib/cut-release index ed39da6e4..7f14a8d7e 100755 --- a/contrib/cut-release +++ b/contrib/cut-release @@ -183,11 +183,11 @@ if ! $SHELL -c '\ ./autogen.sh || echo "autoconf failed; does library_versions have something to match $version?"; \ mkdir "release-$version"; \ cd "release-$version"; \ - ../configure production-staticbinary --disable-shared --enable-unit-testing --with-readline --with-portfolio; \ + ../configure production-staticbinary --disable-shared --enable-unit-testing --with-portfolio --bsd; \ make dist "$@"; \ tar xf "cvc4-$version.tar.gz"; \ cd "cvc4-$version"; \ - ./configure production-staticbinary --disable-shared --enable-unit-testing --with-readline --with-portfolio; \ + ./configure production-staticbinary --disable-shared --enable-unit-testing --with-portfolio --bsd; \ make check "$@"; \ make distcheck "$@"; \ '; then diff --git a/contrib/get-abc b/contrib/get-abc index 8e04ca655..c60e403e6 100755 --- a/contrib/get-abc +++ b/contrib/get-abc @@ -42,6 +42,14 @@ cd alanmi-abc-$commit cp src/base/main/main.c src/base/main/main.c.orig sed 's,^// *#define ABC_LIB *$,#define ABC_LIB,' src/base/main/main.c.orig > src/base/main/main.c +# Strip out libSupport.c, it is in charge of loading extensions and we +# don't want different behavior based on ABC_LIB_PATH, or based on what +# .so is in the current directory! +cp src/base/main/module.make src/base/main/module.make.orig +grep -v 'libSupport\.c' src/base/main/module.make.orig > src/base/main/module.make +cp src/base/main/mainInit.c src/base/main/mainInit.c.orig +sed 's,\( *\)\(.*Libs_Init(\),\1//\2,;s,\( *\)\(.*Libs_End(\),\1//\2,' src/base/main/mainInit.c.orig > src/base/main/mainInit.c + # Build optimized, without readline, without pthreads. # These aren't necessary for our usage and we don't want the dependencies. make libabc.a OPTFLAGS=-O READLINE=0 PTHREADS=0 diff --git a/contrib/run-script-cascj7-fnt b/contrib/run-script-cascj7-fnt index 0d8642e67..e3ad1a2ff 100755 --- a/contrib/run-script-cascj7-fnt +++ b/contrib/run-script-cascj7-fnt @@ -1,6 +1,6 @@ #!/bin/bash -cvc4=cvc4 +cvc4=./cvc4 bench="$1" file=${bench##*/} @@ -15,7 +15,7 @@ echo "------- cvc4-fnt casc j7 : $bench at $2..." function trywith { limit=$1; shift; echo "--- Run $@ at $limit..."; - (ulimit -S -t "$limit";$cvc4 --no-checking --no-interactive --dump-models --produce-models --force-no-limit-cpu-while-dump "$@" $bench) 2>/dev/null | + (ulimit -S -t "$limit";$cvc4 --lang=tptp --no-checking --no-interactive --dump-models --produce-models --force-no-limit-cpu-while-dump "$@" $bench) 2>/dev/null | (read w1 w2 w3 result w4 w5; case "$result" in Satisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;; @@ -25,7 +25,7 @@ function trywith { } function finishwith { echo "--- Run $@..."; - $cvc4 --no-checking --no-interactive --dump-models --produce-models --force-no-limit-cpu-while-dump "$@" $bench + $cvc4 --lang=tptp --no-checking --no-interactive --dump-models --produce-models --force-no-limit-cpu-while-dump "$@" $bench } trywith 30 --finite-model-find --sort-inference --uf-ss-fair diff --git a/contrib/run-script-cascj7-fof b/contrib/run-script-cascj7-fof index 4cd222854..fb2ca33eb 100755 --- a/contrib/run-script-cascj7-fof +++ b/contrib/run-script-cascj7-fof @@ -1,6 +1,6 @@ #!/bin/bash -cvc4=cvc4 +cvc4=./cvc4 bench="$1" file=${bench##*/} @@ -15,7 +15,7 @@ echo "------- cvc4-fof casc j7 : $bench at $2..." function trywith { limit=$1; shift; echo "--- Run $@ at $limit..."; - (ulimit -S -t "$limit";$cvc4 --no-checking --no-interactive --dump-instantiations --inst-format=szs --force-no-limit-cpu-while-dump "$@" $bench) 2>/dev/null | + (ulimit -S -t "$limit";$cvc4 --lang=tptp --no-checking --no-interactive --dump-instantiations --inst-format=szs --force-no-limit-cpu-while-dump "$@" $bench) 2>/dev/null | (read w1 w2 w3 result w4 w5; case "$result" in Unsatisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;; @@ -25,7 +25,7 @@ function trywith { } function finishwith { echo "--- Run $@..."; - $cvc4 --no-checking --no-interactive --dump-instantiations --inst-format=szs --force-no-limit-cpu-while-dump "$@" $bench + $cvc4 --lang=tptp --no-checking --no-interactive --dump-instantiations --inst-format=szs --force-no-limit-cpu-while-dump "$@" $bench } trywith 15 --quant-cf --pre-skolem-quant --full-saturate-quant diff --git a/contrib/run-script-cascj7-tff b/contrib/run-script-cascj7-tff index 9422f8536..11350cd7e 100755 --- a/contrib/run-script-cascj7-tff +++ b/contrib/run-script-cascj7-tff @@ -1,6 +1,6 @@ #!/bin/bash -cvc4=cvc4 +cvc4=./cvc4 bench="$1" file=${bench##*/} @@ -15,7 +15,7 @@ echo "------- cvc4-tff casc j7 : $bench at $2..." function trywith { limit=$1; shift; echo "--- Run $@ at $limit..."; - (ulimit -t "$limit";$cvc4 --no-checking --no-interactive "$@" $bench) 2>/dev/null | + (ulimit -t "$limit";$cvc4 --lang=tptp --no-checking --no-interactive "$@" $bench) 2>/dev/null | (read w1 w2 w3 result w4 w5; case "$result" in Unsatisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;; @@ -25,7 +25,7 @@ function trywith { } function finishwith { echo "--- Run $@..."; - $cvc4 --no-checking --no-interactive "$@" $bench + $cvc4 --lang=tptp --no-checking --no-interactive "$@" $bench } trywith 15 --cbqi-recurse --full-saturate-quant diff --git a/contrib/run-script-smtcomp2014 b/contrib/run-script-smtcomp2014 index 55f274234..31ee4cf4d 100755 --- a/contrib/run-script-smtcomp2014 +++ b/contrib/run-script-smtcomp2014 @@ -69,6 +69,9 @@ QF_AUFBV) trywith 600 finishwith --decision=justification-stoponly ;; +QF_ABV) + finishwith --ite-simp --simp-with-care --repeat-simp + ;; QF_BV) exec ./pcvc4 -L smt2 --no-incremental --no-checking --no-interactive \ --threads 2 \ |