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.

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)