diff options
| -rw-r--r-- | configure.ac | 4 | ||||
| -rw-r--r-- | contrib/run-script-casc26-fnt | 2 | ||||
| -rw-r--r-- | contrib/run-script-casc26-fof | 5 | ||||
| -rw-r--r-- | contrib/run-script-casc26-tfa | 12 | ||||
| -rwxr-xr-x | contrib/run-script-sygusComp2017-INV | 27 | ||||
| -rwxr-xr-x | contrib/run-script-sygusComp2017-PBE_Strings | 2 | ||||
| -rw-r--r-- | src/main/util.cpp | 48 |
7 files changed, 64 insertions, 36 deletions
diff --git a/configure.ac b/configure.ac index e94733576..805a8daea 100644 --- a/configure.ac +++ b/configure.ac @@ -1035,6 +1035,10 @@ AC_CHECK_FUNC([ffs], [AC_DEFINE([HAVE_FFS], [1], AC_LIBOBJ([strtok_r ffs]) +# Check for sigaltstack (missing in emscripten and mingw) +AC_CHECK_FUNC([sigaltstack], [AC_DEFINE([HAVE_SIGALTSTACK], [1], + [Defined to 1 if sigaltstack() is supported by the platform.])]) + # Check for antlr C++ runtime (defined in config/antlr.m4) AC_LIB_ANTLR diff --git a/contrib/run-script-casc26-fnt b/contrib/run-script-casc26-fnt index bc37180a6..c3c12f937 100644 --- a/contrib/run-script-casc26-fnt +++ b/contrib/run-script-casc26-fnt @@ -7,7 +7,7 @@ bench="$1" file=${bench##*/} filename=${file%.*} -echo "------- cvc4-fnt casc j8 : $bench at $2..." +echo "------- cvc4-fnt casc 26 : $bench at $2..." # use: trywith [params..] # to attempt a run. If an SZS ontology result is printed, then diff --git a/contrib/run-script-casc26-fof b/contrib/run-script-casc26-fof index 77553a5ae..376d18b15 100644 --- a/contrib/run-script-casc26-fof +++ b/contrib/run-script-casc26-fof @@ -9,7 +9,7 @@ bench="$1" file=${bench##*/} filename=${file%.*} -echo "------- cvc4-fof casc j8 : $bench at $2..." +echo "------- cvc4-fof casc 26 : $bench at $2..." # use: trywith [params..] # to attempt a run. If an SZS ontology result is printed, then @@ -39,12 +39,11 @@ trywith 5 --multi-trigger-when-single --full-saturate-quant trywith 5 --trigger-sel=max --full-saturate-quant trywith 5 --multi-trigger-when-single --multi-trigger-priority --full-saturate-quant trywith 10 --multi-trigger-cache --full-saturate-quant -trywith 5 --no-multi-trigger-linear --full-saturate-quant -trywith 15 --finite-model-find --no-quant-cf --sort-inference --uf-ss-fair trywith 15 --prenex-quant=none --full-saturate-quant trywith 15 --fs-inst --decision=internal --full-saturate-quant trywith 15 --relevant-triggers --full-saturate-quant trywith 15 --finite-model-find --fmf-inst-engine --sort-inference --uf-ss-fair +trywith 30 --full-saturate-quant --macros-quant trywith 30 --fs-inst --full-saturate-quant trywith 30 --no-quant-cf --full-saturate-quant finishwith --qcf-vo-exp --full-saturate-quant diff --git a/contrib/run-script-casc26-tfa b/contrib/run-script-casc26-tfa index 9f6749ed6..aa65a938f 100644 --- a/contrib/run-script-casc26-tfa +++ b/contrib/run-script-casc26-tfa @@ -7,7 +7,7 @@ bench="$1" file=${bench##*/} filename=${file%.*} -echo "------- cvc4-tfa casc j8 : $bench at $2..." +echo "------- cvc4-tfa casc 26 : $bench at $2..." # use: trywith [params..] # to attempt a run. If an SZS ontology result is printed, then @@ -31,11 +31,9 @@ function finishwith { trywith 10 --decision=internal --full-saturate-quant trywith 10 --finite-model-find --decision=internal -trywith 10 --nl-ext --nl-ext-tplanes --decision=internal --full-saturate-quant -trywith 10 --purify-quant --full-saturate-quant +trywith 10 --nl-ext --nl-ext-tplanes --full-saturate-quant trywith 10 --partial-triggers --full-saturate-quant -trywith 10 --no-e-matching --full-saturate-quant -trywith 30 --cbqi-all --purify-triggers --full-saturate-quant -trywith 30 --nl-ext --fs-inst --full-saturate-quant -finishwith --nl-ext --nl-ext-tplanes --full-saturate-quant +trywith 15 --cbqi-all --purify-triggers --full-saturate-quant +trywith 15 --nl-ext --fs-inst --full-saturate-quant +finishwith --full-saturate-quant --macros-quant # echo "% SZS status" "GaveUp for $filename" diff --git a/contrib/run-script-sygusComp2017-INV b/contrib/run-script-sygusComp2017-INV index a25a5f5c8..a21792fb9 100755 --- a/contrib/run-script-sygusComp2017-INV +++ b/contrib/run-script-sygusComp2017-INV @@ -3,14 +3,31 @@ cvc4=./cvc4 bench="$1" +function runl { + limit=$1; shift; + ulimit -S -t "$limit";$cvc4 --lang=sygus --no-checking --no-interactive --dump-synth --default-dag-thresh=0 "$@" $bench +} + function trywith { - ($cvc4 --lang=sygus --no-checking --no-interactive --dump-synth --default-dag-thresh=0 "$@" $bench) 2>/dev/null | + sol=$(runl $@) + status=$? + if [ $status -ne 134 ]; then + echo $sol | + (read result w1; + case "$result" in + unsat) echo "$w1";cat;exit 0;; + esac; exit 1) + if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi + fi +} + +function finishwith { + $cvc4 --lang=sygus --no-checking --no-interactive --dump-synth --default-dag-thresh=0 "$@" $bench 2>/dev/null | (read result w1; case "$result" in unsat) echo "$w1";cat;exit 0;; - esac; exit 1) - if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi + esac) } -trywith --sygus-inv-templ=post - +trywith 60 --sygus-inv-templ=pre +finishwith --sygus-inv-templ=post diff --git a/contrib/run-script-sygusComp2017-PBE_Strings b/contrib/run-script-sygusComp2017-PBE_Strings index 0a845bd78..849835b28 100755 --- a/contrib/run-script-sygusComp2017-PBE_Strings +++ b/contrib/run-script-sygusComp2017-PBE_Strings @@ -12,5 +12,5 @@ function trywith { if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi } -trywith --cegqi-si=none --strings-exp +trywith --cegqi-si=none --sygus-fair=direct diff --git a/src/main/util.cpp b/src/main/util.cpp index 72f431b0d..2fd796d92 100644 --- a/src/main/util.cpp +++ b/src/main/util.cpp @@ -66,8 +66,10 @@ void print_statistics() { #ifndef __WIN32__ +#ifdef HAVE_SIGALTSTACK size_t cvc4StackSize; void* cvc4StackBase; +#endif /* HAVE_SIGALTSTACK */ /** Handler for SIGXCPU, i.e., timeout. */ void timeout_handler(int sig, siginfo_t* info, void*) { @@ -83,6 +85,7 @@ void sigint_handler(int sig, siginfo_t* info, void*) { abort(); } +#ifdef HAVE_SIGALTSTACK /** Handler for SIGSEGV (segfault). */ void segv_handler(int sig, siginfo_t* info, void* c) { uintptr_t extent = reinterpret_cast<uintptr_t>(cvc4StackBase) - cvc4StackSize; @@ -143,6 +146,7 @@ void segv_handler(int sig, siginfo_t* info, void* c) { abort(); #endif /* CVC4_DEBUG */ } +#endif /* HAVE_SIGALTSTACK */ /** Handler for SIGILL (illegal instruction). */ void ill_handler(int sig, siginfo_t* info, void*) { @@ -256,16 +260,6 @@ void cvc4_init() throw(Exception) { #endif #ifndef __WIN32__ - stack_t ss; - ss.ss_sp = (char*) malloc(SIGSTKSZ); - if(ss.ss_sp == NULL) { - throw Exception("Can't malloc() space for a signal stack"); - } - ss.ss_size = SIGSTKSZ; - ss.ss_flags = 0; - if(sigaltstack(&ss, NULL) == -1) { - throw Exception(string("sigaltstack() failure: ") + strerror(errno)); - } struct rlimit limit; if(getrlimit(RLIMIT_STACK, &limit)) { throw Exception(string("getrlimit() failure: ") + strerror(errno)); @@ -279,8 +273,6 @@ void cvc4_init() throw(Exception) { throw Exception(string("getrlimit() failure: ") + strerror(errno)); } } - cvc4StackSize = limit.rlim_cur; - cvc4StackBase = ss.ss_sp; struct sigaction act1; act1.sa_sigaction = sigint_handler; @@ -299,20 +291,36 @@ void cvc4_init() throw(Exception) { } struct sigaction act3; - act3.sa_sigaction = segv_handler; - act3.sa_flags = SA_SIGINFO | SA_ONSTACK; + act3.sa_sigaction = ill_handler; + act3.sa_flags = SA_SIGINFO; sigemptyset(&act3.sa_mask); - if(sigaction(SIGSEGV, &act3, NULL)) { - throw Exception(string("sigaction(SIGSEGV) failure: ") + strerror(errno)); + if(sigaction(SIGILL, &act3, NULL)) { + throw Exception(string("sigaction(SIGILL) failure: ") + strerror(errno)); + } + +#ifdef HAVE_SIGALTSTACK + stack_t ss; + ss.ss_sp = (char*) malloc(SIGSTKSZ); + if(ss.ss_sp == NULL) { + throw Exception("Can't malloc() space for a signal stack"); + } + ss.ss_size = SIGSTKSZ; + ss.ss_flags = 0; + if(sigaltstack(&ss, NULL) == -1) { + throw Exception(string("sigaltstack() failure: ") + strerror(errno)); } + cvc4StackSize = limit.rlim_cur; + cvc4StackBase = ss.ss_sp; + struct sigaction act4; act4.sa_sigaction = segv_handler; - act4.sa_flags = SA_SIGINFO; + act4.sa_flags = SA_SIGINFO | SA_ONSTACK; sigemptyset(&act4.sa_mask); - if(sigaction(SIGILL, &act4, NULL)) { - throw Exception(string("sigaction(SIGILL) failure: ") + strerror(errno)); + if(sigaction(SIGSEGV, &act4, NULL)) { + throw Exception(string("sigaction(SIGSEGV) failure: ") + strerror(errno)); } +#endif /* HAVE_SIGALTSTACK */ #endif /* __WIN32__ */ @@ -322,9 +330,11 @@ void cvc4_init() throw(Exception) { void cvc4_shutdown() throw () { #ifndef __WIN32__ +#ifdef HAVE_SIGALTSTACK free(cvc4StackBase); cvc4StackBase = NULL; cvc4StackSize = 0; +#endif /* HAVE_SIGALTSTACK */ #endif /* __WIN32__ */ } |