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.

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 706ef51f2f0d369078cd796fde53369e9bb6981b..4cef0bc00e56951fd24a356eecafb053233cdf07 100644 (file)
--- 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 2057dd51290ba1abbbe4835df8f8212e96af97fe..244592aeef138c9ae4ea75a8d529e8f930ef6792 100755 (executable)
--- 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 ] \