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.
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
# Add subdirectories
add_subdirectory(base)
+add_subdirectory(context)
add_subdirectory(expr)
add_subdirectory(options)
if (NOT BUILD_LIB_ONLY)
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.
$<BUILD_INTERFACE:${CMAKE_CURRENT_SOURCE_DIR}>
$<INSTALL_INTERFACE:include>
)
+target_link_libraries(cvc4 PRIVATE cvc4support)
include(GenerateExportHeader)
generate_export_header(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)
#-----------------------------------------------------------------------------#
-libcvc4_add_sources(
+set(LIBBASE_SOURCES
check.cpp
check.h
configuration.cpp
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
${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)
--- /dev/null
+###############################################################################
+# 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)
+++ /dev/null
-##
-## 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
+++ /dev/null
-##
-## 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
+++ /dev/null
-##
-## 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
+++ /dev/null
-##
-## 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
projects / cvc5.git / commitdiff