summaryrefslogtreecommitdiff
path: root/cmake
diff options
context:
space:
mode:
Diffstat (limited to 'cmake')
-rw-r--r--cmake/ConfigureCVC4.cmake14
1 files changed, 14 insertions, 0 deletions
diff --git a/cmake/ConfigureCVC4.cmake b/cmake/ConfigureCVC4.cmake
index 67c1f414d..cdf8e4d9a 100644
--- a/cmake/ConfigureCVC4.cmake
+++ b/cmake/ConfigureCVC4.cmake
@@ -67,6 +67,20 @@ check_symbol_exists(sigaltstack "signal.h" HAVE_SIGALTSTACK)
check_symbol_exists(strerror_r "string.h" HAVE_STRERROR_R)
check_symbol_exists(strtok_r "string.h" HAVE_STRTOK_R)
+# Check whether the verison of CaDiCaL used supports incremental solving
+if(USE_CADICAL)
+ check_cxx_source_compiles(
+ "
+ #include <${CaDiCaL_HOME}/src/cadical.hpp>
+ int main() { return sizeof(&CaDiCaL::Solver::assume); }
+ "
+ CVC4_INCREMENTAL_CADICAL
+ )
+ if(CVC4_INCREMENTAL_CADICAL)
+ add_definitions(-DCVC4_INCREMENTAL_CADICAL)
+ endif()
+endif()
+
# Determine if we have the POSIX (int) or GNU (char *) variant of strerror_r.
check_c_source_compiles(
"
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback