diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2018-09-12 00:08:19 -0700 |
---|---|---|
committer | Mathias Preiner <mathias.preiner@gmail.com> | 2018-09-22 16:30:59 -0700 |
commit | 507748d8bbdd2c9a2d29f83fd7f4ee6ac8d3fe08 (patch) | |
tree | 5bebc96652aa40aa970c51f796e89f8f619192bd /src/parser | |
parent | 52281cf25960740c46275783cf62c881fa8ef703 (diff) |
cmake: Only build libcvc4 and libcvc4parser as libraries.
The sources of all previous libraries are now added to libcvc4 and built as
libcvc4. This removes circular dependencies between libcvc4 and libexpr.
Further, we now only have one parser library and don't build additional
libraries for each language.
Diffstat (limited to 'src/parser')
-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 |
5 files changed, 55 insertions, 123 deletions
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) |