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.

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)