-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)
--- /dev/null
+# 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)
-# 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
--- /dev/null
+# - 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()
--- /dev/null
+#
+# 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()
+# 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)
--- /dev/null
+namespace CVC4 {
+namespace proof {
+
+extern const char *const plf_signatures;
+const char *const plf_signatures = "\
+@CORE_SIGNATURES@
+";
+
+} // namespace proof
+} // namespace CVC4
-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)
+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."
+)
--- /dev/null
+#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@;
+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})
-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."
+)
+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)
projects / cvc5.git / commitdiff