-cmake_minimum_required (VERSION 3.0.1)
+cmake_minimum_required(VERSION 3.1)
#-----------------------------------------------------------------------------#
add_required_cxx_flag(${flag})
endmacro()
-# Collect all libraries that must be linked against libcvc4. These will be
-# actually linked in src/CMakeLists.txt with target_link_libaries(...).
-macro(libcvc4_link_libraries library)
- set(LIBCVC4_LIBRARIES ${LIBCVC4_LIBRARIES} ${library})
-endmacro()
-
-# Collect all include directories that are required for libcvc4. These will be
-# actually included in src/CMakeLists.txt with target_include_directories(...).
-macro(libcvc4_include_directories dirs)
- set(LIBCVC4_INCLUDES ${LIBCVC4_INCLUDES} ${dirs})
-endmacro()
-
# CVC4 Boolean options are three-valued to detect if an option was set by the
# user. The available values are: IGNORE (default), ON, OFF
# Default options do not override options that were set by the user, i.e.,
endif()
endmacro()
+# Prepend 'prepand_value' to each element of the list 'in_list'. The result
+# is stored in 'out_list'.
+function(list_prepend in_list prepand_value out_list)
+ foreach(_elem ${${in_list}})
+ list(APPEND ${out_list} "${prepand_value}${_elem}")
+ endforeach()
+ set(${out_list} ${${out_list}} PARENT_SCOPE)
+endfunction()
+
+#-----------------------------------------------------------------------------#
+# libcvc4 macros
+
+# Collect all libraries that must be linked against libcvc4. These will be
+# actually linked in src/CMakeLists.txt with target_link_libaries(...).
+macro(libcvc4_link_libraries library)
+ set(LIBCVC4_LIBRARIES ${LIBCVC4_LIBRARIES} ${library})
+endmacro()
+
+# Collect all include directories that are required for libcvc4. These will be
+# actually included in src/CMakeLists.txt with target_include_directories(...).
+macro(libcvc4_include_directories dirs)
+ set(LIBCVC4_INCLUDES ${LIBCVC4_INCLUDES} ${dirs})
+endmacro()
+
+# Collect all source files that are required to build libcvc4 in LIBCVC4_SRCS
+# or LIBCVC4_GEN_SRCS. If GENERATED is the first argument the sources are
+# added to LIBCVC4_GEN_SRCS. All sources are prepended with the absolute
+# current path path. CMAKE_CURRENT_BINARY_DIR is prepended
+# to generated source files.
+macro(libcvc4_add_sources)
+ set(_sources ${ARGV})
+
+ # Check if the first argument is GENERATED.
+ list(GET _sources 0 _generated)
+ if(${_generated} STREQUAL "GENERATED")
+ list(REMOVE_AT _sources 0)
+ set(_cur_path ${CMAKE_CURRENT_BINARY_DIR})
+ set(_append_to LIBCVC4_GEN_SRCS)
+ else()
+ set(_cur_path ${CMAKE_CURRENT_SOURCE_DIR})
+ set(_append_to LIBCVC4_SRCS)
+ endif()
+
+ # Prepend source files with current path.
+ foreach(_src ${_sources})
+ list(APPEND ${_append_to} "${_cur_path}/${_src}")
+ endforeach()
+
+ file(RELATIVE_PATH
+ _rel_path "${PROJECT_SOURCE_DIR}/src" "${CMAKE_CURRENT_SOURCE_DIR}")
+
+ # Make changes to list ${_append_to} visible to the parent scope if not
+ # called from src/.
+ # Note: ${_append_to} refers to the variable name whereas ${${_append_to}}
+ # refers to the contents of the variable.
+ if(_rel_path)
+ set(${_append_to} ${${_append_to}} PARENT_SCOPE)
+ endif()
+endmacro()
+
#-----------------------------------------------------------------------------#
# User options
#-----------------------------------------------------------------------------#
+set(GMP_HOME ${GMP_DIR})
+find_package(GMP REQUIRED)
+libcvc4_link_libraries(${GMP_LIBRARIES})
+libcvc4_include_directories(${GMP_INCLUDE_DIR})
+
if(BUILD_BINDINGS_JAVA OR BUILD_BINDINGS_PYTHON)
set(BUILD_BINDINGS TRUE)
endif()
set(RUN_REGRESSION_ARGS ${RUN_REGRESSION_ARGS} --enable-proof)
add_definitions(-DCVC4_PROOF)
set(CVC4_PROOF 1)
- libcvc4_link_libraries(signatures)
endif()
if(ENABLE_REPLAY)
#-----------------------------------------------------------------------------#
+# signatures needs to come before src since it adds source files to libcvc4.
+if(ENABLE_PROOFS)
+ add_subdirectory(proofs/signatures)
+endif()
+
add_subdirectory(doc)
add_subdirectory(src)
if(BUILD_BINDINGS)
add_subdirectory(test/unit)
endif()
-if(ENABLE_PROOFS)
- add_subdirectory(proofs/signatures)
-endif()
-
#-----------------------------------------------------------------------------#
# Print build configuration
if(CVC4_BUILD_PROFILE_PRODUCTION)
${CMAKE_CURRENT_SOURCE_DIR}/signatures.cpp.in
${CMAKE_CURRENT_BINARY_DIR}/signatures.cpp)
-add_library(signatures SHARED ${CMAKE_CURRENT_BINARY_DIR}/signatures.cpp)
+libcvc4_add_sources(GENERATED signatures.cpp)
-set(cvc4_src_files
+libcvc4_add_sources(
api/cvc4cpp.cpp
api/cvc4cpp.h
api/cvc4cppkind.h
decision/decision_strategy.h
decision/justification_heuristic.cpp
decision/justification_heuristic.h
+ lib/clock_gettime.c
+ lib/clock_gettime.h
+ lib/ffs.c
+ lib/ffs.h
+ lib/replacements.h
+ lib/strtok_r.c
+ lib/strtok_r.h
preprocessing/assertion_pipeline.cpp
preprocessing/assertion_pipeline.h
preprocessing/passes/apply_substs.cpp
proof/uf_proof.h
proof/unsat_core.cpp
proof/unsat_core.h
+ prop/bvminisat/bvminisat.cpp
+ prop/bvminisat/bvminisat.h
+ prop/bvminisat/core/Dimacs.h
+ prop/bvminisat/core/Solver.cc
+ prop/bvminisat/core/Solver.h
+ prop/bvminisat/core/SolverTypes.h
+ prop/bvminisat/mtl/Alg.h
+ prop/bvminisat/mtl/Alloc.h
+ prop/bvminisat/mtl/Heap.h
+ prop/bvminisat/mtl/IntTypes.h
+ prop/bvminisat/mtl/Map.h
+ prop/bvminisat/mtl/Queue.h
+ prop/bvminisat/mtl/Sort.h
+ prop/bvminisat/mtl/Vec.h
+ prop/bvminisat/mtl/XAlloc.h
+ prop/bvminisat/simp/SimpSolver.cc
+ prop/bvminisat/simp/SimpSolver.h
+ prop/bvminisat/utils/Options.h
prop/cadical.cpp
prop/cadical.h
prop/cnf_stream.cpp
prop/cnf_stream.h
prop/cryptominisat.cpp
prop/cryptominisat.h
+ prop/minisat/core/Dimacs.h
+ prop/minisat/core/Solver.cc
+ prop/minisat/core/Solver.h
+ prop/minisat/core/SolverTypes.h
+ prop/minisat/minisat.cpp
+ prop/minisat/minisat.h
+ prop/minisat/mtl/Alg.h
+ prop/minisat/mtl/Alloc.h
+ prop/minisat/mtl/Heap.h
+ prop/minisat/mtl/IntTypes.h
+ prop/minisat/mtl/Map.h
+ prop/minisat/mtl/Queue.h
+ prop/minisat/mtl/Sort.h
+ prop/minisat/mtl/Vec.h
+ prop/minisat/mtl/XAlloc.h
+ prop/minisat/simp/SimpSolver.cc
+ prop/minisat/simp/SimpSolver.h
+ prop/minisat/utils/Options.h
prop/prop_engine.cpp
prop/prop_engine.h
prop/registrar.h
smt/term_formula_removal.cpp
smt/term_formula_removal.h
smt/update_ostream.h
+ smt_util/boolean_simplification.cpp
+ smt_util/boolean_simplification.h
+ smt_util/lemma_channels.cpp
+ smt_util/lemma_channels.h
+ smt_util/lemma_input_channel.h
+ smt_util/lemma_output_channel.h
+ smt_util/nary_builder.cpp
+ smt_util/nary_builder.h
+ smt_util/node_visitor.h
theory/arith/approx_simplex.cpp
theory/arith/approx_simplex.h
theory/arith/arith_ite_utils.cpp
theory/valuation.h
)
-# Generated in theory/
-set(cvc4_gen_src_files
- theory/rewriter_tables.h
- theory/theory_traits.h
- theory/type_enumerator.cpp
-)
-# Since these files are generated in a different CMakeLists.txt we have to
-# tell cmake that the files are generated.
-set_source_files_properties(${cvc4_gen_src_files} PROPERTIES GENERATED TRUE)
-
-add_library(cvc4 ${cvc4_src_files} ${cvc4_gen_src_files})
-
-set_target_properties(cvc4
- PROPERTIES
- VERSION ${CVC4_VERSION}
- SOVERSION ${CVC4_SOVERSION}
-)
-
-target_compile_definitions(cvc4
- PRIVATE
- -D__BUILDING_CVC4LIB
- -D__STDC_LIMIT_MACROS
- -D__STDC_FORMAT_MACROS
-)
-add_dependencies(cvc4 gen-theory-files)
-target_link_libraries(cvc4
- base bvminisat expr minisat options smtutil util replacements
- ${LIBCVC4_LIBRARIES}
-)
-target_include_directories(cvc4 PRIVATE ${LIBCVC4_INCLUDES})
-
+# Add required include paths for this and all subdirectories.
include_directories(include)
include_directories(. ${CMAKE_CURRENT_BINARY_DIR})
add_subdirectory(base)
add_subdirectory(expr)
-add_subdirectory(lib)
add_subdirectory(main)
add_subdirectory(options)
add_subdirectory(parser)
-add_subdirectory(prop/bvminisat)
-add_subdirectory(prop/minisat)
-add_subdirectory(smt_util)
add_subdirectory(theory)
add_subdirectory(util)
+# All sources for libcvc4 are now collected via libcvc4_add_sources. We can
+# now build libcvc4.
+set_source_files_properties(${LIBCVC4_GEN_SRCS} PROPERTIES GENERATED TRUE)
+add_library(cvc4 ${LIBCVC4_SRCS} ${LIBCVC4_GEN_SRCS})
+
+set_target_properties(cvc4 PROPERTIES SOVERSION ${CVC4_SOVERSION})
+target_compile_definitions(cvc4
+ PRIVATE
+ -D__BUILDING_CVC4LIB
+ -D__STDC_LIMIT_MACROS
+ -D__STDC_FORMAT_MACROS
+)
+# Add libcvc4 dependencies for generated sources.
+add_dependencies(cvc4 gen-expr gen-options gen-tags gen-theory)
+target_link_libraries(cvc4 ${LIBCVC4_LIBRARIES})
+target_include_directories(cvc4 PUBLIC ${LIBCVC4_INCLUDES})
configure_file(git_versioninfo.cpp.in git_versioninfo.cpp)
-set(base_src_files
+libcvc4_add_sources(
configuration.cpp
configuration.h
configuration_private.h
output.h
)
-add_library(base
- ${base_src_files} ${CMAKE_CURRENT_BINARY_DIR}/git_versioninfo.cpp)
-target_compile_definitions(base PRIVATE -D__BUILDING_CVC4LIB)
-add_dependencies(base tags_headers)
+libcvc4_add_sources(GENERATED git_versioninfo.cpp)
#
# Generate code for debug/trace tags
DEPENDS mktagheaders ${CMAKE_CURRENT_BINARY_DIR}/Trace_tags
)
-add_custom_target(
- tags_headers
+add_custom_target(gen-tags
DEPENDS
${CMAKE_CURRENT_BINARY_DIR}/Debug_tags.h
${CMAKE_CURRENT_BINARY_DIR}/Trace_tags.h
-set(expr_src_files
+libcvc4_add_sources(
array.h
array_store_all.cpp
array_store_all.h
uninterpreted_constant.h
)
-set(expr_gen_src_files
+libcvc4_add_sources(GENERATED
kind.cpp
kind.h
metakind.cpp
type_properties.h
)
-add_library(expr ${expr_src_files} ${expr_gen_src_files})
-target_link_libraries(expr PRIVATE options)
-target_compile_definitions(expr PRIVATE -D__BUILDING_CVC4LIB)
-
#
# Generate code for kinds.
#
> ${CMAKE_CURRENT_BINARY_DIR}/type_checker.cpp
DEPENDS mkexpr type_checker_template.cpp
)
+
+add_custom_target(gen-expr
+ DEPENDS
+ kind.cpp
+ kind.h
+ metakind.cpp
+ metakind.h
+ expr.cpp
+ expr.h
+ expr_manager.cpp
+ expr_manager.h
+ type_checker.cpp
+ type_properties.h
+)
+++ /dev/null
-set(replacements_src_files
- clock_gettime.c
- clock_gettime.h
- ffs.c
- ffs.h
- replacements.h
- strtok_r.c
- strtok_r.h
-)
-
-add_library(replacements ${replacements_src_files})
-target_compile_definitions(replacements PRIVATE -D__BUILDING_CVC4LIB)
util.cpp
)
-add_library(main ${libmain_src_files})
+# Build object library since we will use the object files for cvc4-bin,
+# pcvc4-bin, and main-test library.
+add_library(main OBJECT ${libmain_src_files})
target_compile_definitions(main PRIVATE -D__BUILDING_CVC4DRIVER)
-target_link_libraries(main cvc4 cvc4parser)
-if(USE_READLINE)
- target_link_libraries(main ${Readline_LIBRARIES})
- target_include_directories(main PRIVATE ${Readline_INCLUDE_DIR})
+if(BUILD_SHARED_LIBS)
+ set_target_properties(main PROPERTIES POSITION_INDEPENDENT_CODE 1)
endif()
-add_dependencies(main token-headers)
-add_executable(cvc4-bin main.cpp)
+# We can't use target_link_libraries(...) here since this is only supported for
+# cmake version >= 3.12. Hence, we have to manually add the library
+# dependencies for main. As a consequence, include directories from
+# dependencies are not propagated and we need to manually add the include
+# directories of libcvc4 to main.
+add_dependencies(main cvc4 cvc4parser gen-tokens)
+target_include_directories(main PRIVATE ${LIBCVC4_INCLUDES})
+
+# main-test library is only used for linking against system and unit tests so
+# that we don't have to include all object files of main into each unit/system
+# test. Do not link against main-test in any other case.
+add_library(main-test $<TARGET_OBJECTS:main>)
+target_link_libraries(main-test cvc4 cvc4parser)
+
+add_executable(cvc4-bin main.cpp $<TARGET_OBJECTS:main>)
target_compile_definitions(cvc4-bin PRIVATE -D__BUILDING_CVC4DRIVER)
set_target_properties(cvc4-bin
PROPERTIES
OUTPUT_NAME cvc4
RUNTIME_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/bin)
-target_link_libraries(cvc4-bin main)
+target_link_libraries(cvc4-bin cvc4 cvc4parser)
if(ENABLE_PORTFOLIO)
set(pcvc4_src_files
command_executor_portfolio.h
)
- add_executable(pcvc4-bin ${pcvc4_src_files})
+ add_executable(pcvc4-bin ${pcvc4_src_files} $<TARGET_OBJECTS:main>)
target_compile_definitions(pcvc4-bin PRIVATE -D__BUILDING_CVC4DRIVER)
set_target_properties(pcvc4-bin
PROPERTIES
OUTPUT_NAME pcvc4
RUNTIME_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/bin)
- target_link_libraries(pcvc4-bin main)
- add_dependencies(pcvc4-bin token-headers)
- target_link_libraries(pcvc4-bin ${Boost_LIBRARIES})
+ target_link_libraries(pcvc4-bin cvc4 cvc4parser ${Boost_LIBRARIES})
target_include_directories(pcvc4-bin PRIVATE ${Boost_INCLUDE_DIRS})
endif()
-add_custom_command(
- OUTPUT cvc_tokens.h
- COMMAND
- sh ${CMAKE_CURRENT_LIST_DIR}/gen-token-header.sh
- ${CMAKE_CURRENT_LIST_DIR}/../parser/cvc/Cvc.g
- ${CMAKE_CURRENT_BINARY_DIR}/cvc_tokens.h
- DEPENDS ../parser/cvc/Cvc.g
-)
-
-add_custom_command(
- OUTPUT smt1_tokens.h
- COMMAND
- sh ${CMAKE_CURRENT_LIST_DIR}/gen-token-header.sh
- ${CMAKE_CURRENT_LIST_DIR}/../parser/smt1/Smt1.g
- ${CMAKE_CURRENT_BINARY_DIR}/smt1_tokens.h
- DEPENDS ../parser/smt1/Smt1.g
-)
-
-add_custom_command(
- OUTPUT smt2_tokens.h
- COMMAND
- sh ${CMAKE_CURRENT_LIST_DIR}/gen-token-header.sh
- ${CMAKE_CURRENT_LIST_DIR}/../parser/smt2/Smt2.g
- ${CMAKE_CURRENT_BINARY_DIR}/smt2_tokens.h
- DEPENDS ../parser/smt2/Smt2.g
-)
+if(USE_READLINE)
+ target_link_libraries(cvc4-bin ${Readline_LIBRARIES})
+ target_link_libraries(main-test ${Readline_LIBRARIES})
+ target_include_directories(main PRIVATE ${Readline_INCLUDE_DIR})
+ if(ENABLE_PORTFOLIO)
+ target_link_libraries(pcvc4-bin ${Readline_LIBRARIES})
+ endif()
+endif()
-add_custom_command(
- OUTPUT tptp_tokens.h
- COMMAND
- sh ${CMAKE_CURRENT_LIST_DIR}/gen-token-header.sh
- ${CMAKE_CURRENT_LIST_DIR}/../parser/tptp/Tptp.g
- ${CMAKE_CURRENT_BINARY_DIR}/tptp_tokens.h
- DEPENDS ../parser/tptp/Tptp.g
-)
+foreach(lang Cvc Smt1 Smt2 Tptp)
+ string(TOLOWER ${lang} lang_lc)
+ add_custom_command(
+ OUTPUT ${lang_lc}_tokens.h
+ COMMAND
+ sh ${CMAKE_CURRENT_LIST_DIR}/gen-token-header.sh
+ ${CMAKE_CURRENT_LIST_DIR}/../parser/${lang_lc}/${lang}.g
+ ${CMAKE_CURRENT_BINARY_DIR}/${lang_lc}_tokens.h
+ DEPENDS ../parser/${lang_lc}/${lang}.g
+ )
+endforeach()
-add_custom_target(
- token-headers
- DEPENDS cvc_tokens.h smt1_tokens.h smt2_tokens.h tptp_tokens.h
+add_custom_target(gen-tokens
+ DEPENDS
+ cvc_tokens.h
+ smt1_tokens.h
+ smt2_tokens.h
+ tptp_tokens.h
)
-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()
+libcvc4_add_sources(
+ argument_extender.h
+ argument_extender_implementation.cpp
+ argument_extender_implementation.h
+ arith_heuristic_pivot_rule.cpp
+ arith_heuristic_pivot_rule.h
+ arith_propagation_mode.cpp
+ arith_propagation_mode.h
+ arith_unate_lemma_mode.cpp
+ arith_unate_lemma_mode.h
+ base_handlers.h
+ bv_bitblast_mode.cpp
+ bv_bitblast_mode.h
+ datatypes_modes.h
+ decision_mode.cpp
+ decision_mode.h
+ decision_weight.h
+ didyoumean.cpp
+ didyoumean.h
+ language.cpp
+ language.h
+ open_ostream.cpp
+ open_ostream.h
+ option_exception.h
+ options.h
+ options_handler.cpp
+ options_handler.h
+ options_public_functions.cpp
+ printer_modes.cpp
+ printer_modes.h
+ quantifiers_modes.cpp
+ quantifiers_modes.h
+ set_language.cpp
+ set_language.h
+ simplification_mode.cpp
+ simplification_mode.h
+ sygus_out_mode.h
+ theoryof_mode.cpp
+ theoryof_mode.h
+ ufss_mode.h
+)
set(options_toml_files
arith_options.toml
string(REPLACE "toml" "cpp;" options_gen_cpp_files ${options_toml_files})
string(REPLACE "toml" "h;" options_gen_h_files ${options_toml_files})
-prepend_path(${options_toml_files})
+libcvc4_add_sources(GENERATED options.cpp ${options_gen_cpp_files})
+
+list_prepend(options_toml_files "${CMAKE_CURRENT_LIST_DIR}/" abs_toml_files)
add_custom_command(
- OUTPUT options.cpp options_holder.h ${options_gen_cpp_files} ${options_gen_h_files}
+ OUTPUT
+ options.cpp options_holder.h
+ ${options_gen_cpp_files} ${options_gen_h_files}
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}
+ ${abs_toml_files}
DEPENDS
mkoptions.py
${options_toml_files}
${CMAKE_CURRENT_BINARY_DIR}/../../doc/options.3cvc_template
)
-set(options_src_files
- argument_extender.h
- argument_extender_implementation.cpp
- argument_extender_implementation.h
- arith_heuristic_pivot_rule.cpp
- arith_heuristic_pivot_rule.h
- arith_propagation_mode.cpp
- arith_propagation_mode.h
- arith_unate_lemma_mode.cpp
- arith_unate_lemma_mode.h
- base_handlers.h
- bv_bitblast_mode.cpp
- bv_bitblast_mode.h
- datatypes_modes.h
- decision_mode.cpp
- decision_mode.h
- decision_weight.h
- didyoumean.cpp
- didyoumean.h
- language.cpp
- language.h
- open_ostream.cpp
- open_ostream.h
- option_exception.h
- options.h
- options_handler.cpp
- options_handler.h
- options_public_functions.cpp
- printer_modes.cpp
- printer_modes.h
- quantifiers_modes.cpp
- quantifiers_modes.h
- set_language.cpp
- set_language.h
- simplification_mode.cpp
- simplification_mode.h
- sygus_out_mode.h
- theoryof_mode.cpp
- theoryof_mode.h
- ufss_mode.h
+add_custom_target(gen-options
+ DEPENDS
+ options.cpp
+ options_holder.h
+ ${options_gen_cpp_files}
+ ${options_gen_h_files}
)
-
-add_library(options options.cpp ${options_gen_cpp_files} ${options_src_files})
-target_compile_definitions(options PRIVATE -D__BUILDING_CVC4LIB)
+set(ANTLR_HOME ${ANTLR_DIR})
+find_package(ANTLR REQUIRED)
+
+# Java runtime is required for ANTLR
+find_package(Java COMPONENTS Runtime REQUIRED)
+
set(cvc4parser_src_files
antlr_input.cpp
antlr_input.h
bounded_token_buffer.h
bounded_token_factory.cpp
bounded_token_factory.h
+ cvc/cvc_input.cpp
+ cvc/cvc_input.h
input.cpp
input.h
line_buffer.cpp
parser_builder.cpp
parser_builder.h
parser_exception.h
+ smt1/smt1.cpp
+ smt1/smt1.h
+ smt1/smt1_input.cpp
+ smt1/smt1_input.h
+ smt2/smt2.cpp
+ smt2/smt2.h
+ smt2/smt2_input.cpp
+ smt2/smt2_input.h
+ smt2/sygus_input.cpp
+ smt2/sygus_input.h
+ tptp/TptpLexer.c
+ tptp/TptpParser.c
+ tptp/tptp.cpp
+ tptp/tptp.h
+ tptp/tptp_input.cpp
+ tptp/tptp_input.h
)
-set(ANTLR_HOME ${ANTLR_DIR})
-find_package(ANTLR REQUIRED)
+# Generate parsers for all supported languages
+foreach(lang Cvc Smt1 Smt2 Tptp)
+ string(TOLOWER ${lang} lang_dir)
+ file(MAKE_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR}/${lang_dir})
+ add_custom_command(
+ OUTPUT
+ ${CMAKE_CURRENT_BINARY_DIR}/${lang_dir}/${lang}Lexer.c
+ ${CMAKE_CURRENT_BINARY_DIR}/${lang_dir}/${lang}Lexer.h
+ ${CMAKE_CURRENT_BINARY_DIR}/${lang_dir}/${lang}Parser.c
+ ${CMAKE_CURRENT_BINARY_DIR}/${lang_dir}/${lang}Parser.h
+ ${CMAKE_CURRENT_BINARY_DIR}/${lang_dir}/${lang}.tokens
+ COMMAND
+ ${ANTLR_BINARY}
+ ${CMAKE_CURRENT_SOURCE_DIR}/${lang_dir}/${lang}.g
+ -fo ${CMAKE_CURRENT_BINARY_DIR}/${lang_dir}
+ DEPENDS
+ ${lang_dir}/${lang}.g
+ )
+ set(gen_src_files
+ ${CMAKE_CURRENT_BINARY_DIR}/${lang_dir}/${lang}Lexer.c
+ ${CMAKE_CURRENT_BINARY_DIR}/${lang_dir}/${lang}Parser.c)
-# Java runtime is required for ANTLR
-find_package(Java COMPONENTS Runtime REQUIRED)
+ # Tell cmake that generated source files are actually c++ files
+ set_source_files_properties(${gen_src_files} PROPERTIES LANGUAGE CXX)
+ set_source_files_properties(${gen_src_files} PROPERTIES GENERATED TRUE)
-add_library(cvc4parser ${cvc4parser_src_files})
+ # Add generated source files to the parser source files
+ list(APPEND cvc4parser_src_files ${gen_src_files})
+endforeach()
+add_library(cvc4parser ${cvc4parser_src_files})
set_target_properties(cvc4parser
- PROPERTIES
- VERSION ${CVC4_VERSION}
- SOVERSION ${CVC4_SOVERSION}
-)
-
+ PROPERTIES VERSION ${CVC4_VERSION} SOVERSION ${CVC4_SOVERSION})
target_compile_definitions(cvc4parser PRIVATE -D__BUILDING_CVC4PARSERLIB)
-target_link_libraries(cvc4parser parsercvc parsersmt1 parsersmt2 parsertptp cvc4)
-target_link_libraries(cvc4parser ${ANTLR_LIBRARIES})
-
-# ANTLR includes required for all subdirectories
-include_directories(${ANTLR_INCLUDE_DIR})
-add_subdirectory(cvc)
-add_subdirectory(smt1)
-add_subdirectory(smt2)
-add_subdirectory(tptp)
+target_link_libraries(cvc4parser cvc4 ${ANTLR_LIBRARIES})
+target_include_directories(cvc4parser PRIVATE ${ANTLR_INCLUDE_DIR})
+++ /dev/null
-set(parser_cvc_src_files
- cvc_input.cpp
- cvc_input.h
-)
-
-set(parser_cvc_gen_src_files
- CvcLexer.c
- CvcParser.c
-)
-
-add_custom_command(
- OUTPUT ${parser_cvc_gen_src_files} CvcLexer.h CvcParser.h Cvc.tokens
- COMMAND
- ${ANTLR_BINARY}
- ${CMAKE_CURRENT_SOURCE_DIR}/Cvc.g
- -fo ${CMAKE_CURRENT_BINARY_DIR}
- DEPENDS
- Cvc.g
-)
-
-add_library(parsercvc ${parser_cvc_src_files} ${parser_cvc_gen_src_files})
-target_compile_definitions(parsercvc PRIVATE -D__BUILDING_CVC4PARSERLIB)
-set_source_files_properties(${parser_cvc_gen_src_files} PROPERTIES LANGUAGE CXX)
-target_link_libraries(parsercvc expr)
+++ /dev/null
-set(parser_smt1_src_files
- smt1.cpp
- smt1.h
- smt1_input.cpp
- smt1_input.h
-)
-
-set(parser_smt1_gen_src_files
- Smt1Lexer.c
- Smt1Parser.c
-)
-
-add_custom_command(
- OUTPUT ${parser_smt1_gen_src_files} Smt1Lexer.h Smt1Parser.h Smt1.tokens
- COMMAND
- ${ANTLR_BINARY}
- ${CMAKE_CURRENT_SOURCE_DIR}/Smt1.g
- -fo ${CMAKE_CURRENT_BINARY_DIR}
- DEPENDS
- Smt1.g
-)
-
-add_library(parsersmt1 ${parser_smt1_src_files} ${parser_smt1_gen_src_files})
-target_compile_definitions(parsersmt1 PRIVATE -D__BUILDING_CVC4PARSERLIB)
-set_source_files_properties(${parser_smt1_gen_src_files} PROPERTIES LANGUAGE CXX)
-target_link_libraries(parsersmt1 expr)
+++ /dev/null
-set(parser_smt2_src_files
- smt2.cpp
- smt2.h
- smt2_input.cpp
- smt2_input.h
- sygus_input.cpp
- sygus_input.h
-)
-
-set(parser_smt2_gen_src_files
- Smt2Lexer.c
- Smt2Parser.c
-)
-
-add_custom_command(
- OUTPUT ${parser_smt2_gen_src_files} Smt2Lexer.h Smt2Parser.h Smt2.tokens
- COMMAND
- ${ANTLR_BINARY}
- ${CMAKE_CURRENT_SOURCE_DIR}/Smt2.g
- -fo ${CMAKE_CURRENT_BINARY_DIR}
- DEPENDS
- Smt2.g
-)
-
-add_library(parsersmt2 ${parser_smt2_src_files} ${parser_smt2_gen_src_files})
-target_compile_definitions(parsersmt2 PRIVATE -D__BUILDING_CVC4PARSERLIB)
-set_source_files_properties(${parser_smt2_gen_src_files} PROPERTIES LANGUAGE CXX)
-target_link_libraries(parsersmt2 expr)
+++ /dev/null
-set(parser_tptp_src_files
- tptp.cpp
- tptp.h
- tptp_input.cpp
- tptp_input.h
-)
-
-set(parser_tptp_gen_src_files
- TptpLexer.c
- TptpParser.c
-)
-
-add_custom_command(
- OUTPUT ${parser_tptp_gen_src_files} TptpLexer.h TptpParser.h Tptp.tokens
- COMMAND
- ${ANTLR_BINARY}
- ${CMAKE_CURRENT_SOURCE_DIR}/Tptp.g
- -fo ${CMAKE_CURRENT_BINARY_DIR}
- DEPENDS
- Tptp.g
-)
-
-add_library(parsertptp ${parser_tptp_src_files} ${parser_tptp_gen_src_files})
-target_compile_definitions(parsertptp PRIVATE -D__BUILDING_CVC4PARSERLIB)
-set_source_files_properties(${parser_tptp_gen_src_files} PROPERTIES LANGUAGE CXX)
-target_link_libraries(parsertptp expr)
+++ /dev/null
-set(bvminisat_src_files
- bvminisat.cpp
- bvminisat.h
- core/Dimacs.h
- core/Solver.cc
- core/Solver.h
- core/SolverTypes.h
- mtl/Alg.h
- mtl/Alloc.h
- mtl/Heap.h
- mtl/IntTypes.h
- mtl/Map.h
- mtl/Queue.h
- mtl/Sort.h
- mtl/Vec.h
- mtl/XAlloc.h
- simp/SimpSolver.cc
- simp/SimpSolver.h
- utils/Options.h
-)
-
-add_library(bvminisat ${bvminisat_src_files})
-target_include_directories(bvminisat PRIVATE .)
-target_compile_definitions(bvminisat
- PRIVATE
- -D__BUILDING_CVC4LIB
- -D__STDC_LIMIT_MACROS
- -D__STDC_FORMAT_MACROS
-)
-target_link_libraries(bvminisat expr)
+++ /dev/null
-set(minisat_src_files
- core/Dimacs.h
- core/Solver.cc
- core/Solver.h
- core/SolverTypes.h
- minisat.cpp
- minisat.h
- mtl/Alg.h
- mtl/Alloc.h
- mtl/Heap.h
- mtl/IntTypes.h
- mtl/Map.h
- mtl/Queue.h
- mtl/Sort.h
- mtl/Vec.h
- mtl/XAlloc.h
- simp/SimpSolver.cc
- simp/SimpSolver.h
- utils/Options.h
-)
-
-add_library(minisat ${minisat_src_files})
-target_include_directories(minisat PRIVATE .)
-target_compile_definitions(minisat
- PRIVATE
- -D__BUILDING_CVC4LIB
- -D__STDC_LIMIT_MACROS
- -D__STDC_FORMAT_MACROS
-)
-target_link_libraries(minisat expr)
+++ /dev/null
-set(smtutil_src_files
- boolean_simplification.cpp
- boolean_simplification.h
- lemma_channels.cpp
- lemma_channels.h
- lemma_input_channel.h
- lemma_output_channel.h
- nary_builder.cpp
- nary_builder.h
- node_visitor.h
-)
-
-add_library(smtutil ${smtutil_src_files})
-target_compile_definitions(smtutil PRIVATE -D__BUILDING_CVC4LIB)
-target_link_libraries(smtutil expr)
+libcvc4_add_sources(GENERATED
+ rewriter_tables.h
+ theory_traits.h
+ type_enumerator.cpp
+)
+
file(GLOB kinds_files ${PROJECT_SOURCE_DIR}/src/theory/*/kinds)
set(mktheorytraits_script ${CMAKE_CURRENT_LIST_DIR}/mktheorytraits)
DEPENDS mktheorytraits type_enumerator_template.cpp
)
-add_custom_target(
- gen-theory-files
- DEPENDS type_enumerator.cpp theory_traits.h rewriter_tables.h
+add_custom_target(gen-theory
+ DEPENDS
+ type_enumerator.cpp
+ theory_traits.h
+ rewriter_tables.h
)
configure_file(rational.h.in rational.h)
configure_file(integer.h.in integer.h)
-set(util_src_files
+libcvc4_add_sources(
abstract_value.cpp
abstract_value.h
bin_heap.h
)
if(CVC4_USE_CLN_IMP)
- list(APPEND util_src_files rational_cln_imp.cpp integer_cln_imp.cpp)
+ libcvc4_add_sources(rational_cln_imp.cpp integer_cln_imp.cpp)
endif()
if(CVC4_USE_GMP_IMP)
- list(APPEND util_src_files rational_gmp_imp.cpp integer_gmp_imp.cpp)
+ libcvc4_add_sources(rational_gmp_imp.cpp integer_gmp_imp.cpp)
endif()
-
-set(GMP_HOME ${GMP_DIR})
-find_package(GMP REQUIRED)
-
-add_library(util ${util_src_files})
-target_compile_definitions(util PRIVATE -D__BUILDING_CVC4LIB)
-target_link_libraries(util options ${GMP_LIBRARIES})
-target_include_directories(util PUBLIC ${GMP_INCLUDE_DIR})
-D__BUILDING_CVC4_SYSTEM_TEST -D__STDC_LIMIT_MACROS -D__STDC_FORMAT_MACROS)
macro(cvc4_add_system_test name)
- # add_executable(${name} ${ARGN})
add_executable(${name} ${name}.cpp)
- target_link_libraries(${name} main)
+ target_link_libraries(${name} main-test)
target_compile_definitions(${name} PRIVATE ${CVC4_SYSTEM_TEST_FLAGS})
add_test(system/${name} ${CMAKE_CURRENT_BINARY_DIR}/${name})
set_tests_properties(system/${name} PROPERTIES LABELS "system")
macro(cvc4_add_unit_test is_white name)
cxxtest_add_test(${name} ${name}.cpp ${CMAKE_CURRENT_LIST_DIR}/${name}.h)
set_tests_properties(${name} PROPERTIES LABELS "unit")
- target_link_libraries(${name} main)
+ target_link_libraries(${name} main-test)
target_compile_definitions(${name} PRIVATE ${CVC4_CXXTEST_FLAGS_BLACK})
if(${is_white})
target_compile_options(${name} PRIVATE -fno-access-control)
projects / cvc5.git / commitdiff