diff options
| author | Mathias Preiner <mathias.preiner@gmail.com> | 2018-08-13 09:06:33 -0700 |
|---|---|---|
| committer | Mathias Preiner <mathias.preiner@gmail.com> | 2018-09-22 16:30:59 -0700 |
| commit | 7c3f54f21acf99681c34ced71c8033bafb853052 (patch) | |
| tree | 067ab54c96375c87ef6a7a17fc483e88dbd2d49c | |
| parent | 7c2e3700d5f1fe13885cde7f03396c0510d72109 (diff) | |
cmake: Add libsignatures for proofs.
| -rw-r--r-- | CMakeLists.txt | 9 | ||||
| -rw-r--r-- | proofs/signatures/CMakeLists.txt | 3 | ||||
| -rw-r--r-- | proofs/signatures/signatures.cpp.in | 2 | ||||
| -rw-r--r-- | src/CMakeLists.txt | 2 |
4 files changed, 12 insertions, 4 deletions
diff --git a/CMakeLists.txt b/CMakeLists.txt index 02cf58ed1..34281a5f2 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -226,10 +226,17 @@ include_directories(${CMAKE_CURRENT_BINARY_DIR}) set(CVC4_NEED_INT64_T_OVERLOADS 0) set(CVC4_USE_CLN_IMP 0) set(CVC4_USE_GMP_IMP 1) + set(CVC4_USE_SYMFPU 0) +set(CVC4_PROOF 0) + #-----------------------------------------------------------------------------# add_subdirectory(doc) -add_subdirectory(proofs/signatures) add_subdirectory(src) + +if(CVC4_PROOF) + add_subdirectory(proofs/signatures) + set(LIBRARIES ${LIBRARIES} signatures) +endif() diff --git a/proofs/signatures/CMakeLists.txt b/proofs/signatures/CMakeLists.txt index 139a7c80e..fd81e2d42 100644 --- a/proofs/signatures/CMakeLists.txt +++ b/proofs/signatures/CMakeLists.txt @@ -25,6 +25,9 @@ endforeach(f) string(REPLACE "\\" "\\\\" CORE_SIGNATURES "${CORE_SIGNATURES}") string(REPLACE "\"" "\\\"" CORE_SIGNATURES "${CORE_SIGNATURES}") string(REPLACE "\n" "\\n\\\n" CORE_SIGNATURES "${CORE_SIGNATURES}") + configure_file( ${CMAKE_CURRENT_SOURCE_DIR}/signatures.cpp.in ${CMAKE_CURRENT_BINARY_DIR}/signatures.cpp) + +add_library(signatures SHARED ${CMAKE_CURRENT_BINARY_DIR}/signatures.cpp) diff --git a/proofs/signatures/signatures.cpp.in b/proofs/signatures/signatures.cpp.in index 0040eb0c6..37c152b2f 100644 --- a/proofs/signatures/signatures.cpp.in +++ b/proofs/signatures/signatures.cpp.in @@ -3,7 +3,7 @@ namespace proof { extern const char *const plf_signatures; const char *const plf_signatures = "\ -@CORE_SIGNATURES@ +@CORE_SIGNATURES@\ "; } // namespace proof diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index e1e03bd97..92a5ba335 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -580,8 +580,6 @@ target_link_libraries(cvc4 ${LIBRARIES} ) -# TODO: if proofs: libsignatures - include_directories(. ${CMAKE_CURRENT_BINARY_DIR}) include_directories(expr ${CMAKE_CURRENT_BINARY_DIR}/expr) include_directories(include ${CMAKE_CURRENT_BINARY_DIR}/include) |