CMake: consistently used target_sources for object libs

src/api/CMakeLists.txt

@@ -17,7 +17,7 @@ $<TARGET_OBJECTS:rewriters>
 $<TARGET_OBJECTS:unsatcores>
 )
 
-add_library(api OBJECT "")
+add_library(api OBJECT)
 
 set(PRIVATE_SOURCES_TO_ADD
     "${CMAKE_CURRENT_SOURCE_DIR}/MainSolver.cc"

src/cnfizers/CMakeLists.txt

@@ -1,4 +1,15 @@
-add_library(cnfizers OBJECT Cnfizer.cc TermMapper.cc Tseitin.cc)
+add_library(cnfizers OBJECT)
+
+target_sources(cnfizers
+PUBLIC
+    "${CMAKE_CURRENT_SOURCE_DIR}/Cnfizer.h"
+    "${CMAKE_CURRENT_SOURCE_DIR}/TermMapper.h"
+    "${CMAKE_CURRENT_SOURCE_DIR}/Tseitin.h"
+PRIVATE
+    "${CMAKE_CURRENT_SOURCE_DIR}/Cnfizer.cc"
+    "${CMAKE_CURRENT_SOURCE_DIR}/TermMapper.cc"
+    "${CMAKE_CURRENT_SOURCE_DIR}/Tseitin.cc"
+)
 
 install(FILES TermMapper.h Tseitin.h Cnfizer.h
 DESTINATION ${INSTALL_HEADERS_DIR}/cnfizers)

src/common/CMakeLists.txt

@@ -1,11 +1,11 @@
-add_library(common OBJECT "")
+add_library(common OBJECT)
 
 target_sources(common
-    PUBLIC
-        "${CMAKE_CURRENT_LIST_DIR}/FastRational.cc"
-        "${CMAKE_CURRENT_LIST_DIR}/FlaPartitionMap.cc"
-        "${CMAKE_CURRENT_LIST_DIR}/Real.h"
-    PRIVATE
+PUBLIC
+    "${CMAKE_CURRENT_LIST_DIR}/FastRational.cc"
+    "${CMAKE_CURRENT_LIST_DIR}/FlaPartitionMap.cc"
+    "${CMAKE_CURRENT_LIST_DIR}/Real.h"
+PRIVATE
     "${CMAKE_CURRENT_LIST_DIR}/SystemQueries.h"
     "${CMAKE_CURRENT_LIST_DIR}/Integer.h"
     "${CMAKE_CURRENT_LIST_DIR}/Number.h"

src/itehandler/CMakeLists.txt

@@ -1,5 +1,10 @@
-
-
-add_library(itehandler OBJECT IteToSwitch.cc IteToSwitchMisc.cc IteHandler.cc)
-
-
+add_library(itehandler OBJECT)
+
+target_sources(itehandler
+PRIVATE
+    "${CMAKE_CURRENT_SOURCE_DIR}/IteToSwitch.h"
+    "${CMAKE_CURRENT_SOURCE_DIR}/IteToSwitch.cc"
+    "${CMAKE_CURRENT_SOURCE_DIR}/IteToSwitchMisc.cc"
+    "${CMAKE_CURRENT_SOURCE_DIR}/IteHandler.h"
+    "${CMAKE_CURRENT_SOURCE_DIR}/IteHandler.cc"
+)

src/logics/CMakeLists.txt

@@ -1,23 +1,27 @@
-add_library(logics OBJECT "")
+add_library(logics OBJECT)
 
 target_sources(logics
-    PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}/LogicFactory.cc"
-	PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}/BVLogic.cc"
-	PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}/BVLogic.h"
-	PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}/Logic.cc"
-	PUBLIC "${CMAKE_CURRENT_SOURCE_DIR}/Logic.h"
-	PUBLIC "${CMAKE_CURRENT_SOURCE_DIR}/LATheory.h"
-	PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}/ArrayTheory.cc"
-	PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}/ArrayHelpers.cc"
-	PUBLIC "${CMAKE_CURRENT_SOURCE_DIR}/ArithLogic.h"
-	PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}/ArithLogic.cc"
-	PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}/Theory.h"
-	PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}/UFLATheory.h"
-	PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}/UFLATheory.cc"
-	PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}/UFTheory.cc"
-	PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}/SubstLoopBreaker.h"
-	PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}/SubstLoopBreaker.cc"
+PUBLIC
+    "${CMAKE_CURRENT_SOURCE_DIR}/Logic.h"
+    "${CMAKE_CURRENT_SOURCE_DIR}/ArithLogic.h"
+    "${CMAKE_CURRENT_SOURCE_DIR}/BVLogic.h"
+    "${CMAKE_CURRENT_SOURCE_DIR}/LogicFactory.h"
+    "${CMAKE_CURRENT_SOURCE_DIR}/Theory.h"
+    "${CMAKE_CURRENT_SOURCE_DIR}/FunctionTools.h"
+PRIVATE
+    "${CMAKE_CURRENT_SOURCE_DIR}/LogicFactory.cc"
+    "${CMAKE_CURRENT_SOURCE_DIR}/BVLogic.cc"
+    "${CMAKE_CURRENT_SOURCE_DIR}/Logic.cc"
+    "${CMAKE_CURRENT_SOURCE_DIR}/ArrayTheory.cc"
+    "${CMAKE_CURRENT_SOURCE_DIR}/ArrayHelpers.cc"
+    "${CMAKE_CURRENT_SOURCE_DIR}/ArithLogic.cc"
+    "${CMAKE_CURRENT_SOURCE_DIR}/LATheory.h"
+    "${CMAKE_CURRENT_SOURCE_DIR}/UFLATheory.h"
+    "${CMAKE_CURRENT_SOURCE_DIR}/UFLATheory.cc"
+    "${CMAKE_CURRENT_SOURCE_DIR}/UFTheory.cc"
+    "${CMAKE_CURRENT_SOURCE_DIR}/SubstLoopBreaker.h"
+    "${CMAKE_CURRENT_SOURCE_DIR}/SubstLoopBreaker.cc"
 )
 
 install(FILES LogicFactory.h Theory.h Logic.h ArithLogic.h BVLogic.h FunctionTools.h
- DESTINATION ${INSTALL_HEADERS_DIR}/logics)
+DESTINATION ${INSTALL_HEADERS_DIR}/logics)

src/models/CMakeLists.txt

@@ -1,4 +1,13 @@
-add_library(models OBJECT Model.cc ModelBuilder.cc)
+add_library(models OBJECT)
 
-install(FILES Model.h 
-    DESTINATION ${INSTALL_HEADERS_DIR}/models)
+target_sources(models
+PUBLIC
+    "${CMAKE_CURRENT_SOURCE_DIR}/Model.h"
+PRIVATE
+    "${CMAKE_CURRENT_SOURCE_DIR}/Model.cc"
+    "${CMAKE_CURRENT_SOURCE_DIR}/ModelBuilder.h"
+    "${CMAKE_CURRENT_SOURCE_DIR}/ModelBuilder.cc"
+)
+
+install(FILES Model.h
+DESTINATION ${INSTALL_HEADERS_DIR}/models)

src/options/CMakeLists.txt

@@ -1,3 +1,11 @@
-add_library(options OBJECT SMTConfig.cc)
+add_library(options OBJECT)
 
-install(FILES SMTConfig.h DESTINATION ${INSTALL_HEADERS_DIR}/options)
+target_sources(options
+PUBLIC
+    "${CMAKE_CURRENT_SOURCE_DIR}/SMTConfig.h"
+PRIVATE
+    "${CMAKE_CURRENT_SOURCE_DIR}/SMTConfig.cc"
+)
+
+install(FILES SMTConfig.h
+DESTINATION ${INSTALL_HEADERS_DIR}/options)

src/parallel/CMakeLists.txt

@@ -29,7 +29,7 @@ add_library(PTPLib::PTPLib ALIAS PTPLib)
 message(STATUS "PTPLib include: ${PTPLib_SOURCE_DIR}/include")
 
 #add parallel lib and link against PTPLib*******************************************************************************
-add_library(parallel OBJECT "")
+add_library(parallel OBJECT)
 target_link_libraries(parallel PUBLIC PTPLib::PTPLib)
 list(APPEND PRIVATE_SOURCES_TO_ADD
 		"${CMAKE_CURRENT_SOURCE_DIR}/ScatterSplitter.cc"

src/parsers/smt2new/CMakeLists.txt

@@ -6,7 +6,7 @@
 #PRIVATE "${CMAKE_CURRENT_LIST_DIR}/smt2newparser.cc"
 #)
 
-add_library(parsers OBJECT "")
+add_library(parsers OBJECT)
 
 find_package(BISON 3.0 REQUIRED)
 find_package(FLEX 2.6 REQUIRED)
@@ -16,10 +16,12 @@ FLEX_TARGET(smt2newScanner smt2newlexer.ll ${CMAKE_CURRENT_BINARY_DIR}/smt2newle
 ADD_FLEX_BISON_DEPENDENCY(smt2newScanner smt2newParser)
 
 target_sources(parsers
-    PUBLIC "${CMAKE_CURRENT_SOURCE_DIR}/smt2newcontext.cc"
-    PUBLIC "${CMAKE_CURRENT_SOURCE_DIR}/smt2newcontext.h"
-    PRIVATE ${BISON_smt2newParser_OUTPUTS}
-    PRIVATE ${FLEX_smt2newScanner_OUTPUTS}
+PUBLIC
+    "${CMAKE_CURRENT_SOURCE_DIR}/smt2newcontext.cc"
+    "${CMAKE_CURRENT_SOURCE_DIR}/smt2newcontext.h"
+PRIVATE
+    ${BISON_smt2newParser_OUTPUTS}
+    ${FLEX_smt2newScanner_OUTPUTS}
 )
 
 target_compile_options(parsers PRIVATE -Wno-error)

src/proof/CMakeLists.txt

@@ -1,16 +1,20 @@
-add_library(proof OBJECT "")
+add_library(proof OBJECT)
 
 target_sources(proof
-PUBLIC "${CMAKE_CURRENT_SOURCE_DIR}/PG.h"
-PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}/PGBuild.cc"
-PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}/PGCheck.cc"
-PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}/PGHelp.cc"
-PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}/PGHeuristics.cc"
-PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}/PGMain.cc"
-PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}/PGPrint.cc"
-PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}/PGRules.cc"
-PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}/PGTransformationAlgorithms.cc"
-PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}/InterpolationContext.cc"
+PUBLIC
+    "${CMAKE_CURRENT_SOURCE_DIR}/InterpolationContext.h"
+PRIVATE
+    "${CMAKE_CURRENT_SOURCE_DIR}/PG.h"
+    "${CMAKE_CURRENT_SOURCE_DIR}/PGBuild.cc"
+    "${CMAKE_CURRENT_SOURCE_DIR}/PGCheck.cc"
+    "${CMAKE_CURRENT_SOURCE_DIR}/PGHelp.cc"
+    "${CMAKE_CURRENT_SOURCE_DIR}/PGHeuristics.cc"
+    "${CMAKE_CURRENT_SOURCE_DIR}/PGMain.cc"
+    "${CMAKE_CURRENT_SOURCE_DIR}/PGPrint.cc"
+    "${CMAKE_CURRENT_SOURCE_DIR}/PGRules.cc"
+    "${CMAKE_CURRENT_SOURCE_DIR}/PGTransformationAlgorithms.cc"
+    "${CMAKE_CURRENT_SOURCE_DIR}/InterpolationContext.cc"
 )
 
-install(FILES InterpolationContext.h DESTINATION ${INSTALL_HEADERS_DIR}/proof)
+install(FILES InterpolationContext.h
+DESTINATION ${INSTALL_HEADERS_DIR}/proof)

src/pterms/CMakeLists.txt

@@ -1,13 +1,16 @@
-add_library(pterms OBJECT "")
+add_library(pterms OBJECT)
 
 target_sources(pterms
-PUBLIC "${CMAKE_CURRENT_SOURCE_DIR}/PtStructs.h"
-PUBLIC "${CMAKE_CURRENT_SOURCE_DIR}/PtStore.h"
-PUBLIC "${CMAKE_CURRENT_SOURCE_DIR}/Pterm.h"
-PUBLIC "${CMAKE_CURRENT_SOURCE_DIR}/PTRef.h"
-PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}/PtStore.cc"
-PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}/Pterm.cc"
-PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}/PtStructs.cc"
+PUBLIC
+    "${CMAKE_CURRENT_SOURCE_DIR}/PtStructs.h"
+    "${CMAKE_CURRENT_SOURCE_DIR}/PtStore.h"
+    "${CMAKE_CURRENT_SOURCE_DIR}/Pterm.h"
+    "${CMAKE_CURRENT_SOURCE_DIR}/PTRef.h"
+PRIVATE
+    "${CMAKE_CURRENT_SOURCE_DIR}/PtStore.cc"
+    "${CMAKE_CURRENT_SOURCE_DIR}/Pterm.cc"
+    "${CMAKE_CURRENT_SOURCE_DIR}/PtStructs.cc"
 )
 
-install(FILES Pterm.h PtStore.h PTRef.h PtStructs.h DESTINATION ${INSTALL_HEADERS_DIR}/pterms)
+install(FILES Pterm.h PtStore.h PTRef.h PtStructs.h
+DESTINATION ${INSTALL_HEADERS_DIR}/pterms)

src/rewriters/CMakeLists.txt

@@ -1,12 +1,15 @@
-add_library(rewriters OBJECT "")
+add_library(rewriters OBJECT)
 
 target_sources(rewriters
-    PUBLIC "${CMAKE_CURRENT_SOURCE_DIR}/Rewritings.cc"
+PUBLIC
+    "${CMAKE_CURRENT_SOURCE_DIR}/Substitutor.h"
+    "${CMAKE_CURRENT_SOURCE_DIR}/Rewriter.h"
+    "${CMAKE_CURRENT_SOURCE_DIR}/Rewritings.h"
+    "${CMAKE_CURRENT_SOURCE_DIR}/Rewritings.cc"
 )
 
 install(FILES
     Substitutor.h
     Rewriter.h
     Rewritings.h
-    DESTINATION ${INSTALL_HEADERS_DIR}/rewriters
-    )
+DESTINATION ${INSTALL_HEADERS_DIR}/rewriters)

src/simplifiers/CMakeLists.txt

@@ -1,11 +1,13 @@
-add_library(simplifiers OBJECT "")
+add_library(simplifiers OBJECT)
 
 target_sources(simplifiers
-PUBLIC "${CMAKE_CURRENT_SOURCE_DIR}/LA.h"
-PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}/LA.cc"
-        "${CMAKE_CURRENT_SOURCE_DIR}/BoolRewriting.cc"
+PUBLIC
+    "${CMAKE_CURRENT_SOURCE_DIR}/BoolRewriting.h"
+PRIVATE
+    "${CMAKE_CURRENT_SOURCE_DIR}/LA.h"
+    "${CMAKE_CURRENT_SOURCE_DIR}/LA.cc"
+    "${CMAKE_CURRENT_SOURCE_DIR}/BoolRewriting.cc"
 )
 
 install(FILES BoolRewriting.h
-    DESTINATION ${INSTALL_HEADERS_DIR}/simplifiers
-    )
+DESTINATION ${INSTALL_HEADERS_DIR}/simplifiers)

src/smtsolvers/CMakeLists.txt

@@ -1,4 +1,4 @@
-add_library(smtsolvers OBJECT "")
+add_library(smtsolvers OBJECT)
 
 list(APPEND PRIVATE_SOURCES_TO_ADD
 		"${CMAKE_CURRENT_SOURCE_DIR}/SimpSMTSolver.cc"

src/sorts/CMakeLists.txt

@@ -1,3 +1,12 @@
-add_library(sorts OBJECT SStore.cc)
+add_library(sorts OBJECT)
 
-install(FILES SSort.h SStore.h DESTINATION ${INSTALL_HEADERS_DIR}/sorts)
+target_sources(sorts
+PUBLIC
+    "${CMAKE_CURRENT_SOURCE_DIR}/SSort.h"
+    "${CMAKE_CURRENT_SOURCE_DIR}/SStore.h"
+PRIVATE
+    "${CMAKE_CURRENT_SOURCE_DIR}/SStore.cc"
+)
+
+install(FILES SSort.h SStore.h
+DESTINATION ${INSTALL_HEADERS_DIR}/sorts)

src/symbols/CMakeLists.txt

@@ -1,10 +1,13 @@
-add_library(symbols OBJECT "")
+add_library(symbols OBJECT)
 
 target_sources(symbols
-PUBLIC "${CMAKE_CURRENT_SOURCE_DIR}/Symbol.h"
-PUBLIC "${CMAKE_CURRENT_SOURCE_DIR}/SymRef.h"
-PUBLIC "${CMAKE_CURRENT_SOURCE_DIR}/SymStore.h"
-PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}/SymStore.cc"
+PUBLIC
+    "${CMAKE_CURRENT_SOURCE_DIR}/Symbol.h"
+    "${CMAKE_CURRENT_SOURCE_DIR}/SymRef.h"
+    "${CMAKE_CURRENT_SOURCE_DIR}/SymStore.h"
+PRIVATE
+    "${CMAKE_CURRENT_SOURCE_DIR}/SymStore.cc"
 )
 
-install(FILES Symbol.h SymStore.h SymRef.h DESTINATION ${INSTALL_HEADERS_DIR}/symbols)
+install(FILES Symbol.h SymStore.h SymRef.h
+DESTINATION ${INSTALL_HEADERS_DIR}/symbols)

src/tsolvers/CMakeLists.txt

@@ -1,20 +1,28 @@
-add_library(tsolvers OBJECT "")
+add_library(tsolvers OBJECT)
 
 target_sources(tsolvers
-PUBLIC "${CMAKE_CURRENT_SOURCE_DIR}/Deductions.h"
-PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}/Deductions.cc"
-PUBLIC "${CMAKE_CURRENT_SOURCE_DIR}/TSolverHandler.h"
-PUBLIC "${CMAKE_CURRENT_SOURCE_DIR}/TSolver.h"
-PUBLIC "${CMAKE_CURRENT_SOURCE_DIR}/TResult.h"
-PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}/IDLTHandler.cc"
-PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}/RDLTHandler.cc"
-PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}/LATHandler.cc"
-PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}/THandler.cc"
-PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}/TSolverHandler.cc"
-PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}/UFLATHandler.cc"
-PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}/UFTHandler.cc"
-PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}/TSolver.cc"
-PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}/ArrayTHandler.cc"
+PUBLIC
+    "${CMAKE_CURRENT_SOURCE_DIR}/Deductions.h"
+    "${CMAKE_CURRENT_SOURCE_DIR}/TSolverHandler.h"
+    "${CMAKE_CURRENT_SOURCE_DIR}/TResult.h"
+    "${CMAKE_CURRENT_SOURCE_DIR}/LATHandler.h"
+    "${CMAKE_CURRENT_SOURCE_DIR}/UFTHandler.h"
+    "${CMAKE_CURRENT_SOURCE_DIR}/IDLTHandler.h"
+    "${CMAKE_CURRENT_SOURCE_DIR}/RDLTHandler.h"
+    "${CMAKE_CURRENT_SOURCE_DIR}/TSolver.h"
+    "${CMAKE_CURRENT_SOURCE_DIR}/THandler.h"
+PRIVATE
+    "${CMAKE_CURRENT_SOURCE_DIR}/Deductions.cc"
+    "${CMAKE_CURRENT_SOURCE_DIR}/IDLTHandler.cc"
+    "${CMAKE_CURRENT_SOURCE_DIR}/RDLTHandler.cc"
+    "${CMAKE_CURRENT_SOURCE_DIR}/LATHandler.cc"
+    "${CMAKE_CURRENT_SOURCE_DIR}/THandler.cc"
+    "${CMAKE_CURRENT_SOURCE_DIR}/TSolverHandler.cc"
+    "${CMAKE_CURRENT_SOURCE_DIR}/UFLATHandler.cc"
+    "${CMAKE_CURRENT_SOURCE_DIR}/UFTHandler.cc"
+    "${CMAKE_CURRENT_SOURCE_DIR}/TSolver.cc"
+    "${CMAKE_CURRENT_SOURCE_DIR}/ArrayTHandler.h"
+    "${CMAKE_CURRENT_SOURCE_DIR}/ArrayTHandler.cc"
 )
 
 include(egraph/CMakeLists.txt)

src/tsolvers/arraysolver/CMakeLists.txt

@@ -1,4 +1,5 @@
 target_sources(tsolvers
-        PUBLIC "${CMAKE_CURRENT_LIST_DIR}/ArraySolver.h"
-        PRIVATE "${CMAKE_CURRENT_LIST_DIR}/ArraySolver.cc"
-        )
+PRIVATE
+    "${CMAKE_CURRENT_LIST_DIR}/ArraySolver.h"
+    "${CMAKE_CURRENT_LIST_DIR}/ArraySolver.cc"
+)

src/tsolvers/bvsolver/CMakeLists.txt

@@ -1,12 +1,14 @@
 target_sources(tsolvers
-PRIVATE "${CMAKE_CURRENT_LIST_DIR}/BVSolver.cc"
-PRIVATE "${CMAKE_CURRENT_LIST_DIR}/BVStore.cc"
-PRIVATE "${CMAKE_CURRENT_LIST_DIR}/BitBlaster.cc"
-PRIVATE "${CMAKE_CURRENT_LIST_DIR}/BVSolver.cc"
-PUBLIC "${CMAKE_CURRENT_LIST_DIR}/BVSolver.h"
-PUBLIC "${CMAKE_CURRENT_LIST_DIR}/BVStore.h"
-PUBLIC "${CMAKE_CURRENT_LIST_DIR}/BitBlaster.h"
-PUBLIC "${CMAKE_CURRENT_LIST_DIR}/Bvector.h"
+PUBLIC
+    "${CMAKE_CURRENT_LIST_DIR}/BVStore.h"
+    "${CMAKE_CURRENT_LIST_DIR}/BitBlaster.h"
+    "${CMAKE_CURRENT_LIST_DIR}/Bvector.h"
+PRIVATE
+    "${CMAKE_CURRENT_LIST_DIR}/BVSolver.h"
+    "${CMAKE_CURRENT_LIST_DIR}/BVSolver.cc"
+    "${CMAKE_CURRENT_LIST_DIR}/BVStore.cc"
+    "${CMAKE_CURRENT_LIST_DIR}/BitBlaster.cc"
+    "${CMAKE_CURRENT_LIST_DIR}/BVSolver.cc"
 )
 
 install(FILES