cmake: Add libsignatures for proofs.

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 02cf58ed1788c7e992ea1b46baa3e5878592c863..34281a5f2f116d748da85473e0d37c4991a43d3c 100644 (file)
--- 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 139a7c80e144e93f8fe7854583ac105f8f2ffe57..fd81e2d42dc18564c2f2e0373158b5a94a2290c9 100644 (file)
--- 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 0040eb0c6b3148ad5eefba10192d10f573e30374..37c152b2f32dc6cd5753aa42e101fcc9fbafb78c 100644 (file)
--- 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 e1e03bd9743912411b638957550005ec919af5a6..92a5ba335af486dd374c2ed1aa6a71f0572efd66 100644 (file)
--- 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)