diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/CMakeLists.txt | 34 | ||||
-rw-r--r-- | src/expr/CMakeLists.txt | 115 | ||||
-rw-r--r-- | src/git_versioninfo.cpp.in | 5 | ||||
-rw-r--r-- | src/options/CMakeLists.txt | 54 | ||||
-rw-r--r-- | src/theory/CMakeLists.txt | 51 | ||||
-rw-r--r-- | src/util/CMakeLists.txt | 7 |
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) |