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.

1 files changed, 70 insertions, 36 deletions

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})