cmake: Working build infrastructure.

TODO: cvc4autoconfig.h

1 files changed, 138 insertions, 80 deletions

diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt
index c0f75d918..a2e55f874 100644
--- a/src/expr/CMakeLists.txt
+++ b/src/expr/CMakeLists.txt
@@ -1,3 +1,71 @@
+set(expr_src_files
+  array.h
+  array_store_all.cpp
+  array_store_all.h
+  ascription_type.h
+  attribute.h
+  attribute.cpp
+  attribute_internals.h
+  attribute_unique_id.h
+  chain.h
+  emptyset.cpp
+  emptyset.h
+  expr_iomanip.cpp
+  expr_iomanip.h
+  expr_manager_scope.h
+  expr_stream.h
+  kind_map.h
+  matcher.h
+  node.cpp
+  node.h
+  node_builder.h
+  node_manager.cpp
+  node_manager.h
+  node_manager_attributes.h
+  node_manager_listeners.cpp
+  node_manager_listeners.h
+  node_self_iterator.h
+  node_value.cpp
+  node_value.h
+  pickle_data.cpp
+  pickle_data.h
+  pickler.cpp
+  pickler.h
+  symbol_table.cpp
+  symbol_table.h
+  type.cpp
+  type.h
+  type_checker.h
+  type_node.cpp
+  type_node.h
+  variable_type_map.h
+  datatype.h
+  datatype.cpp
+  record.cpp
+  record.h
+  uninterpreted_constant.cpp
+  uninterpreted_constant.h
+)
+
+set(expr_gen_src_files
+  kind.cpp
+  kind.h
+  metakind.cpp
+  metakind.h
+  expr.cpp
+  expr.h
+  expr_manager.cpp
+  expr_manager.h
+  type_checker.cpp
+  type_properties.h
+)
+
+add_library(expr SHARED ${expr_src_files} ${expr_gen_src_files})
+set_target_properties(expr PROPERTIES COMPILE_DEFINITIONS __BUILDING_CVC4LIB)
+
+#
+# Generate code for kinds.
+#
 file(GLOB kinds_files ${PROJECT_SOURCE_DIR}/src/theory/*/kinds)
 
 set(mkkind_script ${CMAKE_CURRENT_LIST_DIR}/mkkind)
@@ -5,111 +73,101 @@ set(mkmetakind_script ${CMAKE_CURRENT_LIST_DIR}/mkmetakind)
 set(mkexpr_script ${CMAKE_CURRENT_LIST_DIR}/mkexpr)
 
 add_custom_command(
-    COMMAND
-      ${mkkind_script}
-      ${CMAKE_CURRENT_LIST_DIR}/kind_template.h
-      ${kinds_files}
-      > ${CMAKE_CURRENT_BINARY_DIR}/kind.h
-    DEPENDS mkkind kind_template.h
-    OUTPUT kind.h
-    COMMENT "Generating kind.h."
+  OUTPUT kind.h
+  COMMAND
+    ${mkkind_script}
+    ${CMAKE_CURRENT_LIST_DIR}/kind_template.h
+    ${kinds_files}
+    > ${CMAKE_CURRENT_BINARY_DIR}/kind.h
+  DEPENDS mkkind kind_template.h
 )
 
 add_custom_command(
-    COMMAND
-      ${mkkind_script}
-      ${CMAKE_CURRENT_LIST_DIR}/kind_template.cpp
-      ${kinds_files}
-      > ${CMAKE_CURRENT_BINARY_DIR}/kind.cpp
-    DEPENDS mkkind kind_template.cpp kind.h
-    OUTPUT kind.cpp
-    COMMENT "Generating kind.cpp."
+  OUTPUT kind.cpp
+  COMMAND
+    ${mkkind_script}
+    ${CMAKE_CURRENT_LIST_DIR}/kind_template.cpp
+    ${kinds_files}
+    > ${CMAKE_CURRENT_BINARY_DIR}/kind.cpp
+  DEPENDS mkkind kind_template.cpp kind.h
 )
 
 add_custom_command(
-    COMMAND
-      ${mkkind_script}
-      ${CMAKE_CURRENT_LIST_DIR}/type_properties_template.h
-      ${kinds_files}
-      > ${CMAKE_CURRENT_BINARY_DIR}/type_properties.h
-    DEPENDS mkkind type_properties_template.h
-    OUTPUT type_properties.h
-    COMMENT "Generating type_properties.h."
+  OUTPUT type_properties.h
+  COMMAND
+    ${mkkind_script}
+    ${CMAKE_CURRENT_LIST_DIR}/type_properties_template.h
+    ${kinds_files}
+    > ${CMAKE_CURRENT_BINARY_DIR}/type_properties.h
+  DEPENDS mkkind type_properties_template.h
 )
 
 add_custom_command(
-    COMMAND
-      ${mkmetakind_script}
-      ${CMAKE_CURRENT_LIST_DIR}/metakind_template.h
-      ${kinds_files}
-      > ${CMAKE_CURRENT_BINARY_DIR}/metakind.h
-    DEPENDS mkmetakind metakind_template.h
-    OUTPUT metakind.h
-    COMMENT "Generating metakind.h."
+  OUTPUT metakind.h
+  COMMAND
+    ${mkmetakind_script}
+    ${CMAKE_CURRENT_LIST_DIR}/metakind_template.h
+    ${kinds_files}
+    > ${CMAKE_CURRENT_BINARY_DIR}/metakind.h
+  DEPENDS mkmetakind metakind_template.h
 )
 
 add_custom_command(
-    COMMAND
-      ${mkmetakind_script}
-      ${CMAKE_CURRENT_LIST_DIR}/metakind_template.cpp
-      ${kinds_files}
-      > ${CMAKE_CURRENT_BINARY_DIR}/metakind.cpp
-    DEPENDS mkmetakind metakind_template.cpp metakind.h
-    OUTPUT metakind.cpp
-    COMMENT "Generating metakind.cpp."
+  OUTPUT metakind.cpp
+  COMMAND
+    ${mkmetakind_script}
+    ${CMAKE_CURRENT_LIST_DIR}/metakind_template.cpp
+    ${kinds_files}
+    > ${CMAKE_CURRENT_BINARY_DIR}/metakind.cpp
+  DEPENDS mkmetakind metakind_template.cpp metakind.h
 )
 
 add_custom_command(
-    COMMAND
-      ${mkexpr_script}
-      ${CMAKE_CURRENT_LIST_DIR}/expr_template.h
-      ${kinds_files}
-      > ${CMAKE_CURRENT_BINARY_DIR}/expr.h
-    DEPENDS mkexpr expr_template.h kind.h
-    OUTPUT expr.h
-    COMMENT "Generating expr.h."
+  OUTPUT expr.h
+  COMMAND
+    ${mkexpr_script}
+    ${CMAKE_CURRENT_LIST_DIR}/expr_template.h
+    ${kinds_files}
+    > ${CMAKE_CURRENT_BINARY_DIR}/expr.h
+  DEPENDS mkexpr expr_template.h kind.h
 )
 
 add_custom_command(
-    COMMAND
-      ${mkexpr_script}
-      ${CMAKE_CURRENT_LIST_DIR}/expr_template.cpp
-      ${kinds_files}
-      > ${CMAKE_CURRENT_BINARY_DIR}/expr.cpp
-    DEPENDS mkexpr expr_template.cpp expr.h
-    OUTPUT expr.cpp
-    COMMENT "Generating expr.cpp."
+  OUTPUT expr.cpp
+  COMMAND
+    ${mkexpr_script}
+    ${CMAKE_CURRENT_LIST_DIR}/expr_template.cpp
+    ${kinds_files}
+    > ${CMAKE_CURRENT_BINARY_DIR}/expr.cpp
+  DEPENDS mkexpr expr_template.cpp expr.h
 )
 
 add_custom_command(
-    COMMAND
-      ${mkexpr_script}
-      ${CMAKE_CURRENT_LIST_DIR}/expr_manager_template.h
-      ${kinds_files}
-      > ${CMAKE_CURRENT_BINARY_DIR}/expr_manager.h
-    DEPENDS mkexpr expr_manager_template.h expr.h
-    OUTPUT expr_manager.h
-    COMMENT "Generating expr_manager.h."
+  OUTPUT expr_manager.h
+  COMMAND
+    ${mkexpr_script}
+    ${CMAKE_CURRENT_LIST_DIR}/expr_manager_template.h
+    ${kinds_files}
+    > ${CMAKE_CURRENT_BINARY_DIR}/expr_manager.h
+  DEPENDS mkexpr expr_manager_template.h expr.h
 )
 
 add_custom_command(
-    COMMAND
-      ${mkexpr_script}
-      ${CMAKE_CURRENT_LIST_DIR}/expr_manager_template.cpp
-      ${kinds_files}
-      > ${CMAKE_CURRENT_BINARY_DIR}/expr_manager.cpp
-    DEPENDS mkexpr expr_manager_template.cpp expr_manager.h
-    OUTPUT expr_manager.cpp
-    COMMENT "Generating expr_manager.cpp."
+  OUTPUT expr_manager.cpp
+  COMMAND
+    ${mkexpr_script}
+    ${CMAKE_CURRENT_LIST_DIR}/expr_manager_template.cpp
+    ${kinds_files}
+    > ${CMAKE_CURRENT_BINARY_DIR}/expr_manager.cpp
+  DEPENDS mkexpr expr_manager_template.cpp expr_manager.h
 )
 
 add_custom_command(
-    COMMAND
-      ${mkexpr_script}
-      ${CMAKE_CURRENT_LIST_DIR}/type_checker_template.cpp
-      ${kinds_files}
-      > ${CMAKE_CURRENT_BINARY_DIR}/type_checker.cpp
-    DEPENDS mkexpr type_checker_template.cpp
-    OUTPUT type_checker.cpp
-    COMMENT "Generating type_checker.cpp."
+  OUTPUT type_checker.cpp
+  COMMAND
+    ${mkexpr_script}
+    ${CMAKE_CURRENT_LIST_DIR}/type_checker_template.cpp
+    ${kinds_files}
+    > ${CMAKE_CURRENT_BINARY_DIR}/type_checker.cpp
+  DEPENDS mkexpr type_checker_template.cpp
 )