diff options
| -rw-r--r-- | CMakeLists.txt | 38 | ||||
| -rwxr-xr-x | configure.sh | 17 |
2 files changed, 35 insertions, 20 deletions
diff --git a/CMakeLists.txt b/CMakeLists.txt index 706ef51f2..4cef0bc00 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -65,19 +65,21 @@ option(ENABLE_GPL "Enable GPL dependencies") # >> 3-valued: IGNORE ON OFF # > allows to detect if set by user (default: IGNORE) # > only necessary for options set for build types -cvc4_option(ENABLE_ASAN "Enable ASAN build") -cvc4_option(ENABLE_ASSERTIONS "Enable assertions") -cvc4_option(ENABLE_DEBUG_SYMBOLS "Enable debug symbols") -cvc4_option(ENABLE_DUMPING "Enable dumping") -cvc4_option(ENABLE_MUZZLE "Suppress ALL non-result output") -cvc4_option(ENABLE_OPTIMIZED "Enable optimization") -cvc4_option(ENABLE_PROOFS "Enable proof support") -cvc4_option(ENABLE_REPLAY "Enable the replay feature") -cvc4_option(ENABLE_STATISTICS "Enable statistics") -cvc4_option(ENABLE_TRACING "Enable tracing") -cvc4_option(ENABLE_UNIT_TESTING "Enable unit testing") -cvc4_option(ENABLE_VALGRIND "Enable valgrind instrumentation") -cvc4_option(ENABLE_SHARED "Build as shared library") +cvc4_option(ENABLE_ASAN "Enable ASAN build") +cvc4_option(ENABLE_ASSERTIONS "Enable assertions") +cvc4_option(ENABLE_COMP_INC_TRACK + "Enable optimizations for incremental SMT-COMP tracks") +cvc4_option(ENABLE_DEBUG_SYMBOLS "Enable debug symbols") +cvc4_option(ENABLE_DUMPING "Enable dumping") +cvc4_option(ENABLE_MUZZLE "Suppress ALL non-result output") +cvc4_option(ENABLE_OPTIMIZED "Enable optimization") +cvc4_option(ENABLE_PROOFS "Enable proof support") +cvc4_option(ENABLE_REPLAY "Enable the replay feature") +cvc4_option(ENABLE_STATISTICS "Enable statistics") +cvc4_option(ENABLE_TRACING "Enable tracing") +cvc4_option(ENABLE_UNIT_TESTING "Enable unit testing") +cvc4_option(ENABLE_VALGRIND "Enable valgrind instrumentation") +cvc4_option(ENABLE_SHARED "Build as shared library") cvc4_option(ENABLE_STATIC_BINARY "Build static binaries with statically linked system libraries") # >> 2-valued: ON OFF @@ -326,6 +328,10 @@ if(ENABLE_DEBUG_SYMBOLS) add_check_c_cxx_flag("-ggdb3") endif() +if(ENABLE_COMP_INC_TRACK) + add_definitions(-DCVC4_SMTCOMP_APPLICATION_TRACK) +endif() + if(ENABLE_MUZZLE) add_definitions(-DCVC4_MUZZLE) endif() @@ -509,7 +515,11 @@ string(REPLACE ";" " " CVC4_DEFINITIONS "${CVC4_DEFINITIONS}") message("CVC4 ${CVC4_RELEASE_STRING}") message("") -message("Build profile : ${CVC4_BUILD_PROFILE_STRING}") +if(ENABLE_COMP_INC_TRACK) + message("Build profile : ${CVC4_BUILD_PROFILE_STRING} (incremental)") +else() + message("Build profile : ${CVC4_BUILD_PROFILE_STRING}") +endif() message("") print_config("GPL :" ENABLE_GPL) print_config("Best configuration :" ENABLE_BEST) diff --git a/configure.sh b/configure.sh index 2057dd512..244592aee 100755 --- a/configure.sh +++ b/configure.sh @@ -10,6 +10,7 @@ Build types: debug testing competition + competition-inc General options; @@ -110,6 +111,7 @@ assertions=default best=default cadical=default cln=default +comp_inc=default coverage=default cryptominisat=default debug_symbols=default @@ -325,11 +327,12 @@ do -*) die "invalid option '$1' (try -h)";; *) case $1 in - production) buildtype=Production;; - debug) buildtype=Debug;; - testing) buildtype=Testing;; - competition) buildtype=Competition;; - *) die "invalid build type (try -h)";; + production) buildtype=Production;; + debug) buildtype=Debug;; + testing) buildtype=Testing;; + competition) buildtype=Competition;; + competition-inc) buildtype=Competition; comp_inc=ON;; + *) die "invalid build type (try -h)";; esac ;; esac @@ -344,11 +347,13 @@ cmake_opts="" && cmake_opts="$cmake_opts -DCMAKE_BUILD_TYPE=$buildtype" [ $asan != default ] \ - && cmake_opts="$cmake_opts -DENABLE_ASAN=$asan" + && cmake_opts="$cmake_opts -DENABLE_ASAN=$asan" [ $assertions != default ] \ && cmake_opts="$cmake_opts -DENABLE_ASSERTIONS=$assertions" [ $best != default ] \ && cmake_opts="$cmake_opts -DENABLE_BEST=$best" +[ $comp_inc != default ] \ + && cmake_opts="$cmake_opts -DENABLE_COMP_INC_TRACK=$comp_inc" [ $coverage != default ] \ && cmake_opts="$cmake_opts -DENABLE_COVERAGE=$coverage" [ $debug_symbols != default ] \ |