Build support library from base and context. (#6368)

This PR creates a support library from the utilities in base and context, which will be required in the parser as soon as we move the symbol table/manager to the parser.

Note: I decided to always build static libraries from base and context (and optionally enable -fPIC for shared builds) since I'm not sure if we want to have these libraries installed separately. Right now these are considered as cvc5 internal utilities that can be used in all cvc5 libraries, but not outside.

7 files changed, 64 insertions, 253 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index ee59d5d31..e060ae43f 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -19,24 +19,6 @@ libcvc4_add_sources(
   api/cpp/cvc5.h
   api/cpp/cvc5_checks.h
   api/cpp/cvc5_kind.h
-  context/backtrackable.h
-  context/cddense_set.h
-  context/cdhashmap.h
-  context/cdhashmap_forward.h
-  context/cdhashset.h
-  context/cdhashset_forward.h
-  context/cdinsert_hashmap.h
-  context/cdinsert_hashmap_forward.h
-  context/cdlist.h
-  context/cdlist_forward.h
-  context/cdmaybe.h
-  context/cdo.h
-  context/cdqueue.h
-  context/cdtrail_queue.h
-  context/context.cpp
-  context/context.h
-  context/context_mm.cpp
-  context/context_mm.h
   decision/decision_attributes.h
   decision/decision_engine.cpp
   decision/decision_engine.h
@@ -1100,6 +1082,7 @@ set(KINDS_FILES
 # Add subdirectories
 
 add_subdirectory(base)
+add_subdirectory(context)
 add_subdirectory(expr)
 add_subdirectory(options)
 if (NOT BUILD_LIB_ONLY)
@@ -1109,6 +1092,14 @@ add_subdirectory(theory)
 add_subdirectory(util)
 
 #-----------------------------------------------------------------------------#
+# Build support library from base and context that can be used in the main
+# library as well as the parser library.
+
+add_library(cvc4support INTERFACE)
+target_link_libraries(cvc4support INTERFACE cvc4base)
+target_link_libraries(cvc4support INTERFACE cvc4context)
+
+#-----------------------------------------------------------------------------#
 # All sources for libcvc4 are now collected in LIBCVC4_SRCS and (if generated)
 # LIBCVC4_GEN_SRCS (via libcvc4_add_sources). We can now build libcvc4.
 
@@ -1119,6 +1110,7 @@ target_include_directories(cvc4
     $<BUILD_INTERFACE:${CMAKE_CURRENT_SOURCE_DIR}>
     $<INSTALL_INTERFACE:include>
 )
+target_link_libraries(cvc4 PRIVATE cvc4support)
 
 include(GenerateExportHeader)
 generate_export_header(cvc4)
@@ -1129,12 +1121,7 @@ install(TARGETS cvc4
   ARCHIVE DESTINATION ${CMAKE_INSTALL_LIBDIR})
 
 set_target_properties(cvc4 PROPERTIES SOVERSION ${CVC5_SOVERSION})
-target_compile_definitions(cvc4
-  PRIVATE
-    -D__BUILDING_CVC4LIB
-    -D__STDC_LIMIT_MACROS
-    -D__STDC_FORMAT_MACROS
-)
+target_compile_definitions(cvc4 PRIVATE -D__BUILDING_CVC4LIB)
 # Add libcvc4 dependencies for generated sources.
 add_dependencies(cvc4 gen-expr gen-gitinfo gen-options gen-tags gen-theory)
 
diff --git a/src/base/CMakeLists.txt b/src/base/CMakeLists.txt
index 4b3e41ff9..684660f78 100644
--- a/src/base/CMakeLists.txt
+++ b/src/base/CMakeLists.txt
@@ -23,7 +23,7 @@ add_custom_target(gen-gitinfo
 
 #-----------------------------------------------------------------------------#
 
-libcvc4_add_sources(
+set(LIBBASE_SOURCES
   check.cpp
   check.h
   configuration.cpp
@@ -36,9 +36,12 @@ libcvc4_add_sources(
   modal_exception.h
   output.cpp
   output.h
+  ${CMAKE_CURRENT_BINARY_DIR}/git_versioninfo.cpp
+)
+set_source_files_properties(
+  ${CMAKE_CURRENT_BINARY_DIR}/git_versioninfo.cpp
+  PROPERTIES GENERATED TRUE
 )
-
-libcvc4_add_sources(GENERATED git_versioninfo.cpp)
 
 #-----------------------------------------------------------------------------#
 # Generate code for debug/trace tags
@@ -75,3 +78,9 @@ set_source_files_properties(
   ${CMAKE_CURRENT_BINARY_DIR}/Trace_tags.h
   PROPERTIES GENERATED TRUE
 )
+
+add_library(cvc4base STATIC ${LIBBASE_SOURCES})
+if(ENABLE_SHARED)
+  set_target_properties(cvc4base PROPERTIES POSITION_INDEPENDENT_CODE ON)
+endif()
+target_compile_definitions(cvc4base PRIVATE -D__BUILDING_CVC4LIB)
diff --git a/src/context/CMakeLists.txt b/src/context/CMakeLists.txt
new file mode 100644
index 000000000..8800f1a23
--- /dev/null
+++ b/src/context/CMakeLists.txt
@@ -0,0 +1,41 @@
+###############################################################################
+# Top contributors (to current version):
+#   Mathias Preiner, Aina Niemetz, Gereon Kremer
+#
+# This file is part of the cvc5 project.
+#
+# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+# in the top-level source directory and their institutional affiliations.
+# All rights reserved.  See the file COPYING in the top-level source
+# directory for licensing information.
+# #############################################################################
+#
+# The build system configuration.
+##
+
+set(LIBCONTEXT_SOURCES
+  backtrackable.h
+  cddense_set.h
+  cdhashmap.h
+  cdhashmap_forward.h
+  cdhashset.h
+  cdhashset_forward.h
+  cdinsert_hashmap.h
+  cdinsert_hashmap_forward.h
+  cdlist.h
+  cdlist_forward.h
+  cdmaybe.h
+  cdo.h
+  cdqueue.h
+  cdtrail_queue.h
+  context.cpp
+  context.h
+  context_mm.cpp
+  context_mm.h
+)
+
+add_library(cvc4context STATIC ${LIBCONTEXT_SOURCES})
+if(ENABLE_SHARED)
+  set_target_properties(cvc4context PROPERTIES POSITION_INDEPENDENT_CODE ON)
+endif()
+target_compile_definitions(cvc4context PRIVATE -D__BUILDING_CVC4LIB)
diff --git a/src/prop/bvminisat/mtl/config.mk b/src/prop/bvminisat/mtl/config.mk
deleted file mode 100644
index b5c36fc6b..000000000
--- a/src/prop/bvminisat/mtl/config.mk
+++ /dev/null
@@ -1,6 +0,0 @@
-##
-##  This file is for system specific configurations. For instance, on
-##  some systems the path to zlib needs to be added. Example:
-##
-##  CFLAGS += -I/usr/local/include
-##  LFLAGS += -L/usr/local/lib
diff --git a/src/prop/bvminisat/mtl/template.mk b/src/prop/bvminisat/mtl/template.mk
deleted file mode 100644
index 3f443fc38..000000000
--- a/src/prop/bvminisat/mtl/template.mk
+++ /dev/null
@@ -1,107 +0,0 @@
-##
-##  Template makefile for Standard, Profile, Debug, Release, and Release-static versions
-##
-##    eg: "make rs" for a statically linked release version.
-##        "make d"  for a debug version (no optimizations).
-##        "make"    for the standard version (optimized, but with debug information and assertions active)
-
-PWD        = $(shell pwd)
-EXEC      ?= $(notdir $(PWD))
-
-CSRCS      = $(wildcard $(PWD)/*.cc) 
-DSRCS      = $(foreach dir, $(DEPDIR), $(filter-out $(MROOT)/$(dir)/Main.cc, $(wildcard $(MROOT)/$(dir)/*.cc)))
-CHDRS      = $(wildcard $(PWD)/*.h)
-COBJS      = $(CSRCS:.cc=.o) $(DSRCS:.cc=.o)
-
-PCOBJS     = $(addsuffix p,  $(COBJS))
-DCOBJS     = $(addsuffix d,  $(COBJS))
-RCOBJS     = $(addsuffix r,  $(COBJS))
-
-
-CXX       ?= g++
-CFLAGS    ?= -Wall -Wno-parentheses
-LFLAGS    ?= -Wall
-
-COPTIMIZE ?= -O3
-
-CFLAGS    += -I$(MROOT) -D __STDC_LIMIT_MACROS -D __STDC_FORMAT_MACROS
-LFLAGS    += -lz
-
-.PHONY : s p d r rs clean 
-
-s:	$(EXEC)
-p:	$(EXEC)_profile
-d:	$(EXEC)_debug
-r:	$(EXEC)_release
-rs:	$(EXEC)_static
-
-libs:	lib$(LIB)_standard.a
-libp:	lib$(LIB)_profile.a
-libd:	lib$(LIB)_debug.a
-libr:	lib$(LIB)_release.a
-
-## Compile options
-%.o:			CFLAGS +=$(COPTIMIZE) -g -D DEBUG
-%.op:			CFLAGS +=$(COPTIMIZE) -pg -g -D NDEBUG
-%.od:			CFLAGS +=-O0 -g -D DEBUG
-%.or:			CFLAGS +=$(COPTIMIZE) -g -D NDEBUG
-
-## Link options
-$(EXEC):		LFLAGS += -g
-$(EXEC)_profile:	LFLAGS += -g -pg
-$(EXEC)_debug:		LFLAGS += -g
-#$(EXEC)_release:	LFLAGS += ...
-$(EXEC)_static:		LFLAGS += --static
-
-## Dependencies
-$(EXEC):		$(COBJS)
-$(EXEC)_profile:	$(PCOBJS)
-$(EXEC)_debug:		$(DCOBJS)
-$(EXEC)_release:	$(RCOBJS)
-$(EXEC)_static:		$(RCOBJS)
-
-lib$(LIB)_standard.a:	$(filter-out */Main.o,  $(COBJS))
-lib$(LIB)_profile.a:	$(filter-out */Main.op, $(PCOBJS))
-lib$(LIB)_debug.a:	$(filter-out */Main.od, $(DCOBJS))
-lib$(LIB)_release.a:	$(filter-out */Main.or, $(RCOBJS))
-
-
-## Build rule
-%.o %.op %.od %.or:	%.cc
-	@echo Compiling: $(subst $(MROOT)/,,$@)
-	@$(CXX) $(CFLAGS) -c -o $@ $<
-
-## Linking rules (standard/profile/debug/release)
-$(EXEC) $(EXEC)_profile $(EXEC)_debug $(EXEC)_release $(EXEC)_static:
-	@echo Linking: "$@ ( $(foreach f,$^,$(subst $(MROOT)/,,$f)) )"
-	@$(CXX) $^ $(LFLAGS) -o $@
-
-## Library rules (standard/profile/debug/release)
-lib$(LIB)_standard.a lib$(LIB)_profile.a lib$(LIB)_release.a lib$(LIB)_debug.a:
-	@echo Making library: "$@ ( $(foreach f,$^,$(subst $(MROOT)/,,$f)) )"
-	@$(AR) -rcsv $@ $^
-
-## Library Soft Link rule:
-libs libp libd libr:
-	@echo "Making Soft Link: $^ -> lib$(LIB).a"
-	@ln -sf $^ lib$(LIB).a
-
-## Clean rule
-clean:
-	@rm -f $(EXEC) $(EXEC)_profile $(EXEC)_debug $(EXEC)_release $(EXEC)_static \
-	  $(COBJS) $(PCOBJS) $(DCOBJS) $(RCOBJS) *.core depend.mk 
-
-## Make dependencies
-depend.mk: $(CSRCS) $(CHDRS)
-	@echo Making dependencies
-	@$(CXX) $(CFLAGS) -I$(MROOT) \
-	   $(CSRCS) -MM | sed 's|\(.*\):|$(PWD)/\1 $(PWD)/\1r $(PWD)/\1d $(PWD)/\1p:|' > depend.mk
-	@for dir in $(DEPDIR); do \
-	      if [ -r $(MROOT)/$${dir}/depend.mk ]; then \
-		  echo Depends on: $${dir}; \
-		  cat $(MROOT)/$${dir}/depend.mk >> depend.mk; \
-	      fi; \
-	  done
-
--include $(MROOT)/mtl/config.mk
--include depend.mk
diff --git a/src/prop/minisat/mtl/config.mk b/src/prop/minisat/mtl/config.mk
deleted file mode 100644
index b5c36fc6b..000000000
--- a/src/prop/minisat/mtl/config.mk
+++ /dev/null
@@ -1,6 +0,0 @@
-##
-##  This file is for system specific configurations. For instance, on
-##  some systems the path to zlib needs to be added. Example:
-##
-##  CFLAGS += -I/usr/local/include
-##  LFLAGS += -L/usr/local/lib
diff --git a/src/prop/minisat/mtl/template.mk b/src/prop/minisat/mtl/template.mk
deleted file mode 100644
index 3f443fc38..000000000
--- a/src/prop/minisat/mtl/template.mk
+++ /dev/null
@@ -1,107 +0,0 @@
-##
-##  Template makefile for Standard, Profile, Debug, Release, and Release-static versions
-##
-##    eg: "make rs" for a statically linked release version.
-##        "make d"  for a debug version (no optimizations).
-##        "make"    for the standard version (optimized, but with debug information and assertions active)
-
-PWD        = $(shell pwd)
-EXEC      ?= $(notdir $(PWD))
-
-CSRCS      = $(wildcard $(PWD)/*.cc) 
-DSRCS      = $(foreach dir, $(DEPDIR), $(filter-out $(MROOT)/$(dir)/Main.cc, $(wildcard $(MROOT)/$(dir)/*.cc)))
-CHDRS      = $(wildcard $(PWD)/*.h)
-COBJS      = $(CSRCS:.cc=.o) $(DSRCS:.cc=.o)
-
-PCOBJS     = $(addsuffix p,  $(COBJS))
-DCOBJS     = $(addsuffix d,  $(COBJS))
-RCOBJS     = $(addsuffix r,  $(COBJS))
-
-
-CXX       ?= g++
-CFLAGS    ?= -Wall -Wno-parentheses
-LFLAGS    ?= -Wall
-
-COPTIMIZE ?= -O3
-
-CFLAGS    += -I$(MROOT) -D __STDC_LIMIT_MACROS -D __STDC_FORMAT_MACROS
-LFLAGS    += -lz
-
-.PHONY : s p d r rs clean 
-
-s:	$(EXEC)
-p:	$(EXEC)_profile
-d:	$(EXEC)_debug
-r:	$(EXEC)_release
-rs:	$(EXEC)_static
-
-libs:	lib$(LIB)_standard.a
-libp:	lib$(LIB)_profile.a
-libd:	lib$(LIB)_debug.a
-libr:	lib$(LIB)_release.a
-
-## Compile options
-%.o:			CFLAGS +=$(COPTIMIZE) -g -D DEBUG
-%.op:			CFLAGS +=$(COPTIMIZE) -pg -g -D NDEBUG
-%.od:			CFLAGS +=-O0 -g -D DEBUG
-%.or:			CFLAGS +=$(COPTIMIZE) -g -D NDEBUG
-
-## Link options
-$(EXEC):		LFLAGS += -g
-$(EXEC)_profile:	LFLAGS += -g -pg
-$(EXEC)_debug:		LFLAGS += -g
-#$(EXEC)_release:	LFLAGS += ...
-$(EXEC)_static:		LFLAGS += --static
-
-## Dependencies
-$(EXEC):		$(COBJS)
-$(EXEC)_profile:	$(PCOBJS)
-$(EXEC)_debug:		$(DCOBJS)
-$(EXEC)_release:	$(RCOBJS)
-$(EXEC)_static:		$(RCOBJS)
-
-lib$(LIB)_standard.a:	$(filter-out */Main.o,  $(COBJS))
-lib$(LIB)_profile.a:	$(filter-out */Main.op, $(PCOBJS))
-lib$(LIB)_debug.a:	$(filter-out */Main.od, $(DCOBJS))
-lib$(LIB)_release.a:	$(filter-out */Main.or, $(RCOBJS))
-
-
-## Build rule
-%.o %.op %.od %.or:	%.cc
-	@echo Compiling: $(subst $(MROOT)/,,$@)
-	@$(CXX) $(CFLAGS) -c -o $@ $<
-
-## Linking rules (standard/profile/debug/release)
-$(EXEC) $(EXEC)_profile $(EXEC)_debug $(EXEC)_release $(EXEC)_static:
-	@echo Linking: "$@ ( $(foreach f,$^,$(subst $(MROOT)/,,$f)) )"
-	@$(CXX) $^ $(LFLAGS) -o $@
-
-## Library rules (standard/profile/debug/release)
-lib$(LIB)_standard.a lib$(LIB)_profile.a lib$(LIB)_release.a lib$(LIB)_debug.a:
-	@echo Making library: "$@ ( $(foreach f,$^,$(subst $(MROOT)/,,$f)) )"
-	@$(AR) -rcsv $@ $^
-
-## Library Soft Link rule:
-libs libp libd libr:
-	@echo "Making Soft Link: $^ -> lib$(LIB).a"
-	@ln -sf $^ lib$(LIB).a
-
-## Clean rule
-clean:
-	@rm -f $(EXEC) $(EXEC)_profile $(EXEC)_debug $(EXEC)_release $(EXEC)_static \
-	  $(COBJS) $(PCOBJS) $(DCOBJS) $(RCOBJS) *.core depend.mk 
-
-## Make dependencies
-depend.mk: $(CSRCS) $(CHDRS)
-	@echo Making dependencies
-	@$(CXX) $(CFLAGS) -I$(MROOT) \
-	   $(CSRCS) -MM | sed 's|\(.*\):|$(PWD)/\1 $(PWD)/\1r $(PWD)/\1d $(PWD)/\1p:|' > depend.mk
-	@for dir in $(DEPDIR); do \
-	      if [ -r $(MROOT)/$${dir}/depend.mk ]; then \
-		  echo Depends on: $${dir}; \
-		  cat $(MROOT)/$${dir}/depend.mk >> depend.mk; \
-	      fi; \
-	  done
-
--include $(MROOT)/mtl/config.mk
--include depend.mk