diff options
| -rw-r--r-- | src/CMakeLists.txt | 35 | ||||
| -rw-r--r-- | src/base/CMakeLists.txt | 15 | ||||
| -rw-r--r-- | src/context/CMakeLists.txt | 41 | ||||
| -rw-r--r-- | src/prop/bvminisat/mtl/config.mk | 6 | ||||
| -rw-r--r-- | src/prop/bvminisat/mtl/template.mk | 107 | ||||
| -rw-r--r-- | src/prop/minisat/mtl/config.mk | 6 | ||||
| -rw-r--r-- | src/prop/minisat/mtl/template.mk | 107 |
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 |