From 7c3f54f21acf99681c34ced71c8033bafb853052 Mon Sep 17 00:00:00 2001
From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Mon, 13 Aug 2018 09:06:33 -0700
Subject: [PATCH] cmake: Add libsignatures for proofs.

---
 CMakeLists.txt                      | 9 ++++++++-
 proofs/signatures/CMakeLists.txt    | 3 +++
 proofs/signatures/signatures.cpp.in | 2 +-
 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)
-- 
2.30.2