diff options
| -rw-r--r-- | CMakeLists.txt | 89 | ||||
| -rw-r--r-- | proofs/signatures/CMakeLists.txt | 2 | ||||
| -rw-r--r-- | src/CMakeLists.txt | 106 | ||||
| -rw-r--r-- | src/base/CMakeLists.txt | 10 | ||||
| -rw-r--r-- | src/expr/CMakeLists.txt | 22 | ||||
| -rw-r--r-- | src/lib/CMakeLists.txt | 12 | ||||
| -rw-r--r-- | src/main/CMakeLists.txt | 97 | ||||
| -rw-r--r-- | src/options/CMakeLists.txt | 108 | ||||
| -rw-r--r-- | src/parser/CMakeLists.txt | 74 | ||||
| -rw-r--r-- | src/parser/cvc/CMakeLists.txt | 24 | ||||
| -rw-r--r-- | src/parser/smt1/CMakeLists.txt | 26 | ||||
| -rw-r--r-- | src/parser/smt2/CMakeLists.txt | 28 | ||||
| -rw-r--r-- | src/parser/tptp/CMakeLists.txt | 26 | ||||
| -rw-r--r-- | src/prop/bvminisat/CMakeLists.txt | 30 | ||||
| -rw-r--r-- | src/prop/minisat/CMakeLists.txt | 30 | ||||
| -rw-r--r-- | src/smt_util/CMakeLists.txt | 15 | ||||
| -rw-r--r-- | src/theory/CMakeLists.txt | 14 | ||||
| -rw-r--r-- | src/util/CMakeLists.txt | 14 | ||||
| -rw-r--r-- | test/system/CMakeLists.txt | 3 | ||||
| -rw-r--r-- | test/unit/CMakeLists.txt | 2 |
20 files changed, 334 insertions, 398 deletions
diff --git a/CMakeLists.txt b/CMakeLists.txt index f1e20e5f3..24b6d0320 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -1,4 +1,4 @@ -cmake_minimum_required (VERSION 3.0.1) +cmake_minimum_required(VERSION 3.1) #-----------------------------------------------------------------------------# @@ -119,18 +119,6 @@ macro(add_required_c_cxx_flag flag) 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., @@ -150,6 +138,66 @@ macro(cvc4_set_option var value) 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 @@ -313,6 +361,11 @@ enable_testing() #-----------------------------------------------------------------------------# +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() @@ -380,7 +433,6 @@ if(ENABLE_PROOFS) 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) @@ -538,6 +590,11 @@ include_directories(${CMAKE_CURRENT_BINARY_DIR}) #-----------------------------------------------------------------------------# +# 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) @@ -552,10 +609,6 @@ if(ENABLE_UNIT_TESTING) add_subdirectory(test/unit) endif() -if(ENABLE_PROOFS) - add_subdirectory(proofs/signatures) -endif() - #-----------------------------------------------------------------------------# # Print build configuration if(CVC4_BUILD_PROFILE_PRODUCTION) diff --git a/proofs/signatures/CMakeLists.txt b/proofs/signatures/CMakeLists.txt index fd81e2d42..7ef94c388 100644 --- a/proofs/signatures/CMakeLists.txt +++ b/proofs/signatures/CMakeLists.txt @@ -30,4 +30,4 @@ configure_file( ${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) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 2e818bad5..a0bb3b0cf 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -1,4 +1,4 @@ -set(cvc4_src_files +libcvc4_add_sources( api/cvc4cpp.cpp api/cvc4cpp.h api/cvc4cppkind.h @@ -26,6 +26,13 @@ set(cvc4_src_files 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 @@ -144,12 +151,48 @@ set(cvc4_src_files 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 @@ -184,6 +227,15 @@ set(cvc4_src_files 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 @@ -594,49 +646,31 @@ set(cvc4_src_files 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}) diff --git a/src/base/CMakeLists.txt b/src/base/CMakeLists.txt index d54564ca6..320049c8c 100644 --- a/src/base/CMakeLists.txt +++ b/src/base/CMakeLists.txt @@ -1,6 +1,6 @@ configure_file(git_versioninfo.cpp.in git_versioninfo.cpp) -set(base_src_files +libcvc4_add_sources( configuration.cpp configuration.h configuration_private.h @@ -17,10 +17,7 @@ set(base_src_files 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 @@ -74,8 +71,7 @@ add_custom_command( 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 diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt index c11333bff..83bd2d585 100644 --- a/src/expr/CMakeLists.txt +++ b/src/expr/CMakeLists.txt @@ -1,4 +1,4 @@ -set(expr_src_files +libcvc4_add_sources( array.h array_store_all.cpp array_store_all.h @@ -49,7 +49,7 @@ set(expr_src_files uninterpreted_constant.h ) -set(expr_gen_src_files +libcvc4_add_sources(GENERATED kind.cpp kind.h metakind.cpp @@ -62,10 +62,6 @@ set(expr_gen_src_files 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. # @@ -174,3 +170,17 @@ add_custom_command( > ${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 +) diff --git a/src/lib/CMakeLists.txt b/src/lib/CMakeLists.txt deleted file mode 100644 index ffebfed82..000000000 --- a/src/lib/CMakeLists.txt +++ /dev/null @@ -1,12 +0,0 @@ -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) diff --git a/src/main/CMakeLists.txt b/src/main/CMakeLists.txt index 23f16ccb7..a95517929 100644 --- a/src/main/CMakeLists.txt +++ b/src/main/CMakeLists.txt @@ -7,22 +7,35 @@ set(libmain_src_files 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 @@ -35,55 +48,41 @@ if(ENABLE_PORTFOLIO) 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 ) diff --git a/src/options/CMakeLists.txt b/src/options/CMakeLists.txt index 10511867f..457fd23cd 100644 --- a/src/options/CMakeLists.txt +++ b/src/options/CMakeLists.txt @@ -1,11 +1,44 @@ -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 @@ -36,17 +69,21 @@ set(options_toml_files 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} @@ -59,47 +96,10 @@ add_custom_command( ${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) diff --git a/src/parser/CMakeLists.txt b/src/parser/CMakeLists.txt index 52fa55f9d..c2b3d76ad 100644 --- a/src/parser/CMakeLists.txt +++ b/src/parser/CMakeLists.txt @@ -1,3 +1,9 @@ +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 @@ -10,6 +16,8 @@ set(cvc4parser_src_files 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 @@ -21,29 +29,57 @@ set(cvc4parser_src_files 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}) diff --git a/src/parser/cvc/CMakeLists.txt b/src/parser/cvc/CMakeLists.txt deleted file mode 100644 index c75df0ab4..000000000 --- a/src/parser/cvc/CMakeLists.txt +++ /dev/null @@ -1,24 +0,0 @@ -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) diff --git a/src/parser/smt1/CMakeLists.txt b/src/parser/smt1/CMakeLists.txt deleted file mode 100644 index cd27bb513..000000000 --- a/src/parser/smt1/CMakeLists.txt +++ /dev/null @@ -1,26 +0,0 @@ -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) diff --git a/src/parser/smt2/CMakeLists.txt b/src/parser/smt2/CMakeLists.txt deleted file mode 100644 index f3258839e..000000000 --- a/src/parser/smt2/CMakeLists.txt +++ /dev/null @@ -1,28 +0,0 @@ -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) diff --git a/src/parser/tptp/CMakeLists.txt b/src/parser/tptp/CMakeLists.txt deleted file mode 100644 index 5712e8175..000000000 --- a/src/parser/tptp/CMakeLists.txt +++ /dev/null @@ -1,26 +0,0 @@ -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) diff --git a/src/prop/bvminisat/CMakeLists.txt b/src/prop/bvminisat/CMakeLists.txt deleted file mode 100644 index 3a5d4dba2..000000000 --- a/src/prop/bvminisat/CMakeLists.txt +++ /dev/null @@ -1,30 +0,0 @@ -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) diff --git a/src/prop/minisat/CMakeLists.txt b/src/prop/minisat/CMakeLists.txt deleted file mode 100644 index fee8233bd..000000000 --- a/src/prop/minisat/CMakeLists.txt +++ /dev/null @@ -1,30 +0,0 @@ -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) diff --git a/src/smt_util/CMakeLists.txt b/src/smt_util/CMakeLists.txt deleted file mode 100644 index f0c61de3b..000000000 --- a/src/smt_util/CMakeLists.txt +++ /dev/null @@ -1,15 +0,0 @@ -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) diff --git a/src/theory/CMakeLists.txt b/src/theory/CMakeLists.txt index ab6dd580f..3259ce6c0 100644 --- a/src/theory/CMakeLists.txt +++ b/src/theory/CMakeLists.txt @@ -1,3 +1,9 @@ +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) @@ -33,7 +39,9 @@ add_custom_command( 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 ) diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt index c18f45a12..a17f7c510 100644 --- a/src/util/CMakeLists.txt +++ b/src/util/CMakeLists.txt @@ -2,7 +2,7 @@ configure_file(floatingpoint.h.in floatingpoint.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 @@ -51,17 +51,9 @@ set(util_src_files ) 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}) diff --git a/test/system/CMakeLists.txt b/test/system/CMakeLists.txt index 291916082..faaf53ae4 100644 --- a/test/system/CMakeLists.txt +++ b/test/system/CMakeLists.txt @@ -9,9 +9,8 @@ set(CVC4_SYSTEM_TEST_FLAGS -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") diff --git a/test/unit/CMakeLists.txt b/test/unit/CMakeLists.txt index f91c5b35e..3d2a08385 100644 --- a/test/unit/CMakeLists.txt +++ b/test/unit/CMakeLists.txt @@ -13,7 +13,7 @@ set(CVC4_CXXTEST_FLAGS_WHITE -fno-access-control ${CVC4_CXXTEST_FLAGS_BLACK}) 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) |