cmake: .cpp generation done, .h generation not yet complete

6 files changed, 235 insertions, 31 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 26e93f8b5..500900bb1 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -1,17 +1,17 @@
-add_subdirectory(base)
-add_subdirectory(bindings)
-add_subdirectory(compat)
-add_subdirectory(context)
-add_subdirectory(decision)
-add_subdirectory(expr)
-add_subdirectory(lib)
-add_subdirectory(main)
-add_subdirectory(options)
-add_subdirectory(parser)
-add_subdirectory(printer)
-add_subdirectory(proof)
-add_subdirectory(prop)
-add_subdirectory(smt)
-add_subdirectory(smt_util)
-add_subdirectory(theory)
-add_subdirectory(util)
+#add_subdirectory(base)
+#add_subdirectory(bindings)
+#add_subdirectory(compat)
+#add_subdirectory(context)
+#add_subdirectory(decision)
+#add_subdirectory(expr)
+#add_subdirectory(lib)
+#add_subdirectory(main)
+#add_subdirectory(options)
+#add_subdirectory(parser)
+#add_subdirectory(printer)
+#add_subdirectory(proof)
+#add_subdirectory(prop)
+#add_subdirectory(smt)
+#add_subdirectory(smt_util)
+#add_subdirectory(theory)
+#add_subdirectory(util)
diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt
index e69de29bb..c0f75d918 100644
--- a/src/expr/CMakeLists.txt
+++ b/src/expr/CMakeLists.txt
@@ -0,0 +1,115 @@
+file(GLOB kinds_files ${PROJECT_SOURCE_DIR}/src/theory/*/kinds)
+
+set(mkkind_script ${CMAKE_CURRENT_LIST_DIR}/mkkind)
+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."
+)
+
+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."
+)
+
+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."
+)
+
+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."
+)
+
+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."
+)
+
+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."
+)
+
+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."
+)
+
+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."
+)
+
+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."
+)
+
+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."
+)
diff --git a/src/git_versioninfo.cpp.in b/src/git_versioninfo.cpp.in
new file mode 100644
index 000000000..e601a851a
--- /dev/null
+++ b/src/git_versioninfo.cpp.in
@@ -0,0 +1,5 @@
+#include "base/configuration.h"
+const bool ::CVC4::Configuration::IS_GIT_BUILD = true;
+const char* const ::CVC4::Configuration::GIT_BRANCH_NAME = "@GIT_BRANCH@";
+const char* const ::CVC4::Configuration::GIT_COMMIT = "@GIT_SHA1@";
+const bool ::CVC4::Configuration::GIT_HAS_MODIFICATIONS = @GIT_IS_DIRTY@;
diff --git a/src/options/CMakeLists.txt b/src/options/CMakeLists.txt
index e69de29bb..89f6ff16e 100644
--- a/src/options/CMakeLists.txt
+++ b/src/options/CMakeLists.txt
@@ -0,0 +1,54 @@
+macro(prepend_path)
+  foreach(SOURCE_FILE ${ARGN})
+    set(PREPEND_PATH_SOURCES
+      ${PREPEND_PATH_SOURCES}
+      ${CMAKE_CURRENT_LIST_DIR}/${SOURCE_FILE})
+  endforeach()
+  set(PREPEND_PATH_SOURCES ${PREPEND_PATH_SOURCES} PARENT_SCOPE)
+endmacro()
+
+set(options_toml_files
+  arith_options.toml
+  arrays_options.toml
+  base_options.toml
+  booleans_options.toml
+  builtin_options.toml
+  bv_options.toml
+  datatypes_options.toml
+  decision_options.toml
+  expr_options.toml
+  fp_options.toml
+  idl_options.toml
+  main_options.toml
+  parser_options.toml
+  printer_options.toml
+  proof_options.toml
+  prop_options.toml
+  quantifiers_options.toml
+  sep_options.toml
+  sets_options.toml
+  smt_options.toml
+  strings_options.toml
+  theory_options.toml
+  uf_options.toml
+)
+
+string(REPLACE "toml" "cpp;" options_cpp_files ${options_toml_files})
+string(REPLACE "toml" "h;"   options_h_files ${options_toml_files})
+
+prepend_path(${options_toml_files})
+
+add_custom_command(
+    COMMAND
+      ${PYTHON_EXECUTABLE}
+      ${CMAKE_CURRENT_LIST_DIR}/mkoptions.py
+      ${CMAKE_CURRENT_LIST_DIR}
+      ${CMAKE_CURRENT_BINARY_DIR}/../../doc
+      ${CMAKE_CURRENT_BINARY_DIR}
+      ${PREPEND_PATH_SOURCES}
+    DEPENDS mkoptions.py ${options_toml_files}
+    OUTPUT ${options_cpp_files} ${options_h_files}
+    COMMENT "Generating code for options."
+)
+
+#add_library(options STATIC ${options_cpp_files})
diff --git a/src/theory/CMakeLists.txt b/src/theory/CMakeLists.txt
index 01a98aff8..43592c48b 100644
--- a/src/theory/CMakeLists.txt
+++ b/src/theory/CMakeLists.txt
@@ -1,14 +1,37 @@
-add_subdirectory(arith)
-add_subdirectory(arrays)
-add_subdirectory(booleans)
-add_subdirectory(builtin)
-add_subdirectory(bv)
-add_subdirectory(datatypes)
-add_subdirectory(example)
-add_subdirectory(fp)
-add_subdirectory(idl)
-add_subdirectory(quantifiers)
-add_subdirectory(sep)
-add_subdirectory(sets)
-add_subdirectory(strings)
-add_subdirectory(uf)
+file(GLOB kinds_files ${PROJECT_SOURCE_DIR}/src/theory/*/kinds)
+
+set(mktheorytraits_script ${CMAKE_CURRENT_LIST_DIR}/mktheorytraits)
+set(mkrewriter_script ${CMAKE_CURRENT_LIST_DIR}/mkrewriter)
+
+add_custom_command(
+    COMMAND
+      ${mkrewriter_script}
+      ${CMAKE_CURRENT_LIST_DIR}/rewriter_tables_template.h
+      ${kinds_files}
+      > ${CMAKE_CURRENT_BINARY_DIR}/rewriter_tables.h
+    DEPENDS mkrewriter rewriter_tables_template.h
+    OUTPUT rewriter_tables.h
+      COMMENT "Generating rewriter_tables.h."
+)
+
+add_custom_command(
+    COMMAND
+      ${mktheorytraits_script}
+      ${CMAKE_CURRENT_LIST_DIR}/theory_traits_template.h
+      ${kinds_files}
+      > ${CMAKE_CURRENT_BINARY_DIR}/theory_traits.h
+    DEPENDS mktheorytraits theory_traits_template.h
+    OUTPUT theory_traits.h
+    COMMENT "Generating theory_traits.h."
+)
+
+add_custom_command(
+    COMMAND
+      ${mktheorytraits_script}
+      ${CMAKE_CURRENT_LIST_DIR}/type_enumerator_template.cpp
+      ${kinds_files}
+      > ${CMAKE_CURRENT_BINARY_DIR}/type_enumerator.cpp
+    DEPENDS mktheorytraits type_enumerator_template.cpp
+    OUTPUT type_enumerator.cpp
+    COMMENT "Generating type_enumerator.cpp."
+)
diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt
index e69de29bb..5ea76962c 100644
--- a/src/util/CMakeLists.txt
+++ b/src/util/CMakeLists.txt
@@ -0,0 +1,7 @@
+configure_file(
+  ${CMAKE_CURRENT_SOURCE_DIR}/src/util/rational.h.in
+  ${CMAKE_CURRENT_BINARY_DIR}/src/util/rational.h)
+
+configure_file(
+  ${CMAKE_CURRENT_SOURCE_DIR}/src/util/integer.h.in
+  ${CMAKE_CURRENT_BINARY_DIR}/src/util/integer.h)