From 94feff6c3b03325115e2c1c91121b83945dba4b0 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Mon, 7 Oct 2019 23:27:44 -0700 Subject: Build system: Add build type for incremental competition builds. (#3365) Previously, competition builds for incremental tracks required to manually pass in -DCVC4_SMTCOMP_APPLICATION_TRACK as compiler flag. This introduces an additional build type for incremental competition builds to simplify configuration for such builds. --- CMakeLists.txt | 38 ++++++++++++++++++++++++-------------- 1 file changed, 24 insertions(+), 14 deletions(-) (limited to 'CMakeLists.txt') 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) -- cgit v1.2.3