diff options
| -rw-r--r-- | CMakeLists.txt | 149 | ||||
| -rw-r--r-- | cmake/FindANTLR.cmake | 21 | ||||
| -rw-r--r-- | cmake/FindGMP.cmake | 2 | ||||
| -rw-r--r-- | cmake/GetGitRevisionDescription.cmake | 168 | ||||
| -rw-r--r-- | cmake/GetGitRevisionDescription.cmake.in | 41 | ||||
| -rw-r--r-- | proofs/signatures/CMakeLists.txt | 30 | ||||
| -rw-r--r-- | proofs/signatures/signatures.cpp.in | 10 | ||||
| -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 |
13 files changed, 645 insertions, 42 deletions
diff --git a/CMakeLists.txt b/CMakeLists.txt index 9e3580fbb..187f06949 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -1,23 +1,152 @@ -cmake_minimum_required (VERSION 2.8.9) +cmake_minimum_required (VERSION 3.0.1) + +#-----------------------------------------------------------------------------# + +project (cvc4) + +#-----------------------------------------------------------------------------# + +set (CMAKE_MODULE_PATH ${PROJECT_SOURCE_DIR}/cmake) +set(CMAKE_C_STANDARD 99) +set(CMAKE_CXX_STANDARD 11) + +#-----------------------------------------------------------------------------# + +include(CheckCCompilerFlag) +include(CheckCXXCompilerFlag) + +macro(add_c_flag flag) + set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} ${flag}") +endmacro() + +macro(add_check_c_flag flag) + check_c_compiler_flag("${flag}" HAVE_FLAG_${flag}) + if(HAVE_FLAG_${flag}) + add_c_flag(${flag}) + endif() +endmacro() macro(add_cxx_flag flag) - message(STATUS "Configure with flag '${flag}'") set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} ${flag}") endmacro() -project (cvc4) +macro(add_check_cxx_flag flag) + check_cxx_compiler_flag("${flag}" HAVE_FLAG_${flag}) + if(HAVE_FLAG_${flag}) + add_cxx_flag(${flag}) + endif() +endmacro() -set (CMAKE_MODULE_PATH ${PROJECT_SOURCE_DIR}/cmake) +macro(add_c_cxx_flag flag) + add_c_flag(${flag}) + add_cxx_flag(${flag}) + message(STATUS "Configure with flag '${flag}'") +endmacro() + +macro(add_check_c_cxx_flag flag) + add_check_c_flag(${flag}) + add_check_cxx_flag(${flag}) + message(STATUS "Configure with flag '${flag}'") +endmacro() + +#-----------------------------------------------------------------------------# + +set(CMAKE_ARCHIVE_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib) +set(CMAKE_LIBRARY_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib) +set(CMAKE_RUNTIME_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/bin) +message(STATUS "LIB directory is '${CMAKE_BINARY_DIR}/lib'") +message(STATUS "BIN directory is '${CMAKE_BINARY_DIR}/bin'") + +#-----------------------------------------------------------------------------# + +set(build_types Debug Production) +if(NOT CMAKE_BUILD_TYPE) + message(STATUS "No build type set, options are: ${build_types}") + set(CMAKE_BUILD_TYPE Production CACHE STRING "Options are: ${build_types}" FORCE) + # Provide drop down menu options in cmake-gui + set_property(CACHE CMAKE_BUILD_TYPE PROPERTY STRINGS ${build_types}) +endif() +message(STATUS "Building ${CMAKE_BUILD_TYPE} build") + +#-----------------------------------------------------------------------------# + +find_package(PythonInterp REQUIRED) -# TODO: cln find_package(GMP REQUIRED) +message(STATUS "Found GMP headers: ${GMP_INCLUDE_DIR}") set(LIBRARIES ${LIBRARIES} ${GMP_LIBRARIES}) include_directories(${GMP_INCLUDE_DIR}) -add_subdirectory(src) -add_subdirectory(test) -#TODO only if with-lfsc -#add_subdirectory(proofs/signatures) +find_package(ANTLR REQUIRED) +message(STATUS "Found ANTLR headers: ${ANTLR_INCLUDE_DIR}") +set(LIBRARIES ${LIBRARIES} ${ANTLR_LIBRARIES}) +include_directories(${ANTLR_INCLUDE_DIR}) + +#-----------------------------------------------------------------------------# + +add_check_c_flag("-fexceptions") +add_check_c_cxx_flag("-Wno-deprecated") + +#-----------------------------------------------------------------------------# + +set(VERSION "1.6.0-prerelease") +string(TIMESTAMP MAN_DATE "%Y-%m-%d") + +#-----------------------------------------------------------------------------# + +include(GetGitRevisionDescription) +get_git_head_revision(GIT_REFSPEC GIT_SHA1) +git_local_changes(GIT_IS_DIRTY) +if(${GIT_IS_DIRTY} STREQUAL "DIRTY") + set(GIT_IS_DIRTY "true") +else() + set(GIT_IS_DIRTY "false") +endif() + +execute_process( + COMMAND "${GIT_EXECUTABLE}" rev-parse --abbrev-ref HEAD + OUTPUT_VARIABLE GIT_BRANCH + OUTPUT_STRIP_TRAILING_WHITESPACE +) + +#-----------------------------------------------------------------------------# + +configure_file( + ${CMAKE_CURRENT_SOURCE_DIR}/src/git_versioninfo.cpp.in + ${CMAKE_CURRENT_BINARY_DIR}/src/git_versioninfo.cpp) + +configure_file( + ${CMAKE_CURRENT_SOURCE_DIR}/doc/SmtEngine.3cvc_template.in + ${CMAKE_CURRENT_BINARY_DIR}/doc/SmtEngine.3cvc_template) + +configure_file( + ${CMAKE_CURRENT_SOURCE_DIR}/doc/cvc4.1_template.in + ${CMAKE_CURRENT_BINARY_DIR}/doc/cvc4.1_template) + +configure_file( + ${CMAKE_CURRENT_SOURCE_DIR}/doc/cvc4.5.in + ${CMAKE_CURRENT_BINARY_DIR}/doc/cvc4.5) + +configure_file( + ${CMAKE_CURRENT_SOURCE_DIR}/doc/libcvc4.3.in + ${CMAKE_CURRENT_BINARY_DIR}/doc/libcvc4.3) + +configure_file( + ${CMAKE_CURRENT_SOURCE_DIR}/doc/libcvc4compat.3.in + ${CMAKE_CURRENT_BINARY_DIR}/doc/libcvc4compat.3) + +configure_file( + ${CMAKE_CURRENT_SOURCE_DIR}/doc/libcvc4parser.3.in + ${CMAKE_CURRENT_BINARY_DIR}/doc/libcvc4parser.3) + +configure_file( + ${CMAKE_CURRENT_SOURCE_DIR}/doc/options.3cvc_template.in + ${CMAKE_CURRENT_BINARY_DIR}/doc/options.3cvc_template) -#TODO make dist (subdir: examples) +#-----------------------------------------------------------------------------# +add_subdirectory(src/expr) +add_subdirectory(src/options) +add_subdirectory(src/theory) +add_subdirectory(proofs/signatures) +include_directories(src ${CMAKE_CURRENT_BINARY_DIR}/src) diff --git a/cmake/FindANTLR.cmake b/cmake/FindANTLR.cmake new file mode 100644 index 000000000..5d5727186 --- /dev/null +++ b/cmake/FindANTLR.cmake @@ -0,0 +1,21 @@ +# Find ANTLR +# ANTLR_FOUND - system has ANTLR lib +# ANTLR_INCLUDE_DIR - the ANTLR include directory +# ANTLR_LIBRARIES - Libraries needed to use ANTLR + +find_path(ANTLR_INCLUDE_DIR + NAMES antlr3.h + PATHS "${PROJECT_SOURCE_DIR}/antlr-3.4/include" + NO_DEFAULT_PATH + ) + +find_library(ANTLR_LIBRARIES + NAMES antlr3c libantlr3c + PATHS "${PROJECT_SOURCE_DIR}/antlr-3.4/lib" + NO_DEFAULT_PATH + ) + +include(FindPackageHandleStandardArgs) +find_package_handle_standard_args(ANTLR DEFAULT_MSG ANTLR_INCLUDE_DIR ANTLR_LIBRARIES) + +mark_as_advanced(ANTLR_INCLUDE_DIR ANTLR_LIBRARIES) diff --git a/cmake/FindGMP.cmake b/cmake/FindGMP.cmake index 4325f666e..2d7b9b64a 100644 --- a/cmake/FindGMP.cmake +++ b/cmake/FindGMP.cmake @@ -1,4 +1,4 @@ -# Try to find the GMP librairies +# Find GMP # GMP_FOUND - system has GMP lib # GMP_INCLUDE_DIR - the GMP include directory # GMP_LIBRARIES - Libraries needed to use GMP diff --git a/cmake/GetGitRevisionDescription.cmake b/cmake/GetGitRevisionDescription.cmake new file mode 100644 index 000000000..8ab03bc5f --- /dev/null +++ b/cmake/GetGitRevisionDescription.cmake @@ -0,0 +1,168 @@ +# - Returns a version string from Git +# +# These functions force a re-configure on each git commit so that you can +# trust the values of the variables in your build system. +# +# get_git_head_revision(<refspecvar> <hashvar> [<additional arguments to git describe> ...]) +# +# Returns the refspec and sha hash of the current head revision +# +# git_describe(<var> [<additional arguments to git describe> ...]) +# +# Returns the results of git describe on the source tree, and adjusting +# the output so that it tests false if an error occurs. +# +# git_get_exact_tag(<var> [<additional arguments to git describe> ...]) +# +# Returns the results of git describe --exact-match on the source tree, +# and adjusting the output so that it tests false if there was no exact +# matching tag. +# +# git_local_changes(<var>) +# +# Returns either "CLEAN" or "DIRTY" with respect to uncommitted changes. +# Uses the return code of "git diff-index --quiet HEAD --". +# Does not regard untracked files. +# +# Requires CMake 2.6 or newer (uses the 'function' command) +# +# Original Author: +# 2009-2010 Ryan Pavlik <rpavlik@iastate.edu> <abiryan@ryand.net> +# http://academic.cleardefinition.com +# Iowa State University HCI Graduate Program/VRAC +# +# Copyright Iowa State University 2009-2010. +# Distributed under the Boost Software License, Version 1.0. +# (See accompanying file LICENSE_1_0.txt or copy at +# http://www.boost.org/LICENSE_1_0.txt) + +if(__get_git_revision_description) + return() +endif() +set(__get_git_revision_description YES) + +# We must run the following at "include" time, not at function call time, +# to find the path to this module rather than the path to a calling list file +get_filename_component(_gitdescmoddir ${CMAKE_CURRENT_LIST_FILE} PATH) + +function(get_git_head_revision _refspecvar _hashvar) + set(GIT_PARENT_DIR "${CMAKE_CURRENT_SOURCE_DIR}") + set(GIT_DIR "${GIT_PARENT_DIR}/.git") + while(NOT EXISTS "${GIT_DIR}") # .git dir not found, search parent directories + set(GIT_PREVIOUS_PARENT "${GIT_PARENT_DIR}") + get_filename_component(GIT_PARENT_DIR ${GIT_PARENT_DIR} PATH) + if(GIT_PARENT_DIR STREQUAL GIT_PREVIOUS_PARENT) + # We have reached the root directory, we are not in git + set(${_refspecvar} "GITDIR-NOTFOUND" PARENT_SCOPE) + set(${_hashvar} "GITDIR-NOTFOUND" PARENT_SCOPE) + return() + endif() + set(GIT_DIR "${GIT_PARENT_DIR}/.git") + endwhile() + # check if this is a submodule + if(NOT IS_DIRECTORY ${GIT_DIR}) + file(READ ${GIT_DIR} submodule) + string(REGEX REPLACE "gitdir: (.*)\n$" "\\1" GIT_DIR_RELATIVE ${submodule}) + get_filename_component(SUBMODULE_DIR ${GIT_DIR} PATH) + get_filename_component(GIT_DIR ${SUBMODULE_DIR}/${GIT_DIR_RELATIVE} ABSOLUTE) + endif() + set(GIT_DATA "${CMAKE_CURRENT_BINARY_DIR}/CMakeFiles/git-data") + if(NOT EXISTS "${GIT_DATA}") + file(MAKE_DIRECTORY "${GIT_DATA}") + endif() + + if(NOT EXISTS "${GIT_DIR}/HEAD") + return() + endif() + set(HEAD_FILE "${GIT_DATA}/HEAD") + configure_file("${GIT_DIR}/HEAD" "${HEAD_FILE}" COPYONLY) + + configure_file("${_gitdescmoddir}/GetGitRevisionDescription.cmake.in" + "${GIT_DATA}/grabRef.cmake" + @ONLY) + include("${GIT_DATA}/grabRef.cmake") + + set(${_refspecvar} "${HEAD_REF}" PARENT_SCOPE) + set(${_hashvar} "${HEAD_HASH}" PARENT_SCOPE) +endfunction() + +function(git_describe _var) + if(NOT GIT_FOUND) + find_package(Git QUIET) + endif() + get_git_head_revision(refspec hash) + if(NOT GIT_FOUND) + set(${_var} "GIT-NOTFOUND" PARENT_SCOPE) + return() + endif() + if(NOT hash) + set(${_var} "HEAD-HASH-NOTFOUND" PARENT_SCOPE) + return() + endif() + + # TODO sanitize + #if((${ARGN}" MATCHES "&&") OR + # (ARGN MATCHES "||") OR + # (ARGN MATCHES "\\;")) + # message("Please report the following error to the project!") + # message(FATAL_ERROR "Looks like someone's doing something nefarious with git_describe! Passed arguments ${ARGN}") + #endif() + + #message(STATUS "Arguments to execute_process: ${ARGN}") + + execute_process(COMMAND + "${GIT_EXECUTABLE}" + describe + ${hash} + ${ARGN} + WORKING_DIRECTORY + "${CMAKE_CURRENT_SOURCE_DIR}" + RESULT_VARIABLE + res + OUTPUT_VARIABLE + out + ERROR_QUIET + OUTPUT_STRIP_TRAILING_WHITESPACE) + if(NOT res EQUAL 0) + set(out "${out}-${res}-NOTFOUND") + endif() + + set(${_var} "${out}" PARENT_SCOPE) +endfunction() + +function(git_get_exact_tag _var) + git_describe(out --exact-match ${ARGN}) + set(${_var} "${out}" PARENT_SCOPE) +endfunction() + +function(git_local_changes _var) + if(NOT GIT_FOUND) + find_package(Git QUIET) + endif() + get_git_head_revision(refspec hash) + if(NOT GIT_FOUND) + set(${_var} "GIT-NOTFOUND" PARENT_SCOPE) + return() + endif() + if(NOT hash) + set(${_var} "HEAD-HASH-NOTFOUND" PARENT_SCOPE) + return() + endif() + + execute_process(COMMAND + "${GIT_EXECUTABLE}" + diff-index --quiet HEAD -- + WORKING_DIRECTORY + "${CMAKE_CURRENT_SOURCE_DIR}" + RESULT_VARIABLE + res + OUTPUT_VARIABLE + out + ERROR_QUIET + OUTPUT_STRIP_TRAILING_WHITESPACE) + if(res EQUAL 0) + set(${_var} "CLEAN" PARENT_SCOPE) + else() + set(${_var} "DIRTY" PARENT_SCOPE) + endif() +endfunction() diff --git a/cmake/GetGitRevisionDescription.cmake.in b/cmake/GetGitRevisionDescription.cmake.in new file mode 100644 index 000000000..6d8b708ef --- /dev/null +++ b/cmake/GetGitRevisionDescription.cmake.in @@ -0,0 +1,41 @@ +# +# Internal file for GetGitRevisionDescription.cmake +# +# Requires CMake 2.6 or newer (uses the 'function' command) +# +# Original Author: +# 2009-2010 Ryan Pavlik <rpavlik@iastate.edu> <abiryan@ryand.net> +# http://academic.cleardefinition.com +# Iowa State University HCI Graduate Program/VRAC +# +# Copyright Iowa State University 2009-2010. +# Distributed under the Boost Software License, Version 1.0. +# (See accompanying file LICENSE_1_0.txt or copy at +# http://www.boost.org/LICENSE_1_0.txt) + +set(HEAD_HASH) + +file(READ "@HEAD_FILE@" HEAD_CONTENTS LIMIT 1024) + +string(STRIP "${HEAD_CONTENTS}" HEAD_CONTENTS) +if(HEAD_CONTENTS MATCHES "ref") + # named branch + string(REPLACE "ref: " "" HEAD_REF "${HEAD_CONTENTS}") + if(EXISTS "@GIT_DIR@/${HEAD_REF}") + configure_file("@GIT_DIR@/${HEAD_REF}" "@GIT_DATA@/head-ref" COPYONLY) + else() + configure_file("@GIT_DIR@/packed-refs" "@GIT_DATA@/packed-refs" COPYONLY) + file(READ "@GIT_DATA@/packed-refs" PACKED_REFS) + if(${PACKED_REFS} MATCHES "([0-9a-z]*) ${HEAD_REF}") + set(HEAD_HASH "${CMAKE_MATCH_1}") + endif() + endif() +else() + # detached HEAD + configure_file("@GIT_DIR@/HEAD" "@GIT_DATA@/head-ref" COPYONLY) +endif() + +if(NOT HEAD_HASH) + file(READ "@GIT_DATA@/head-ref" HEAD_HASH LIMIT 1024) + string(STRIP "${HEAD_HASH}" HEAD_HASH) +endif() diff --git a/proofs/signatures/CMakeLists.txt b/proofs/signatures/CMakeLists.txt index e69de29bb..139a7c80e 100644 --- a/proofs/signatures/CMakeLists.txt +++ b/proofs/signatures/CMakeLists.txt @@ -0,0 +1,30 @@ +# These CORE_PLFs are combined to give a "master signature" against which +# proofs are checked internally when using --check-proofs. To add support for +# more theories, just list them here in the same order you would to the LFSC +# proof-checker binary. + +set(core_signature_files + sat.plf + smt.plf + th_base.plf + th_arrays.plf + th_bv.plf + th_bv_bitblast.plf + th_bv_rewrites.plf + th_real.plf + th_int.plf +) + +set(CORE_SIGNATURES "") + +foreach(f ${core_signature_files}) + file(READ ${f} tmp) + set(CORE_SIGNATURES "${CORE_SIGNATURES}\n${tmp}") +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) diff --git a/proofs/signatures/signatures.cpp.in b/proofs/signatures/signatures.cpp.in new file mode 100644 index 000000000..0040eb0c6 --- /dev/null +++ b/proofs/signatures/signatures.cpp.in @@ -0,0 +1,10 @@ +namespace CVC4 { +namespace proof { + +extern const char *const plf_signatures; +const char *const plf_signatures = "\ +@CORE_SIGNATURES@ +"; + +} // namespace proof +} // namespace CVC4 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) |