1# Makefile for creating the java wrapper around the cvc library 2# as well as a java command line client 3 4include ../Makefile.local 5 6### Variables 7 8# package name 9PACKAGE = cvc3 10 11# directories 12# source files: java, cpp 13SOURCE_PATH = src 14# header files: h 15HEADER_PATH = include 16# object files: class, o 17OBJ_PATH = obj 18# library files: so, jar 19REL_LIB_PATH = java/lib 20LIB_PATH = $(TOP)/$(REL_LIB_PATH) 21REL_ARCH_LIB_PATH = $(REL_LIB_PATH)/$(PLATFORM_WITH_OPTIONS) 22ARCH_LIB_PATH = $(TOP)/$(REL_ARCH_LIB_PATH) 23 24CPPFLAGS += $(JAVA_INCLUDES) 25 26ifneq ($(CYGWIN),) 27CPPFLAGS += '-D__int64=long long' 28endif 29 30ifeq ($(OPTIMIZED), 1) 31CXXFLAGS += -O2 32else 33CXXFLAGS += -D_CVC3_DEBUG_MODE -g -O0 34endif 35 36 37# Java compiler flags 38# - source 1.4 is needed for Escjava 39# - Xlint may be compiler dependent 40JFLAGS += -Xlint -g -source 1.4 41 42# source files 43# java files of the library wrapper 44LIB_FILES = \ 45 JniUtils \ 46 Cvc3Exception TypecheckException SoundException EvalException \ 47 CLException ParserException SmtlibException DebugException \ 48 Embedded EmbeddedManager \ 49 InputLanguage QueryResult SatResult FormulaValue \ 50 Expr ExprMut ExprManager ExprManagerMut \ 51 Type TypeMut Op OpMut Rational RationalMut \ 52 Theorem TheoremMut Proof ProofMut Context ContextMut \ 53 Flag Flags FlagsMut \ 54 Statistics StatisticsMut ValidityChecker 55# java files of the test program 56TEST_FILES = Test 57# java files of the stand alone program 58PROG_FILES = TimeoutHandler Cvc3 59# all java files, library and stand alone 60JAVA_FILES = $(LIB_FILES) $(TEST_FILES) $(PROG_FILES) 61# jni files of the library wrapper 62JNI_FILES = \ 63 EmbeddedManager \ 64 Expr ExprMut ExprManager \ 65 Type TypeMut Op OpMut Rational RationalMut \ 66 Theorem TheoremMut Proof ProofMut Context ContextMut \ 67 Flag Flags FlagsMut \ 68 Statistics StatisticsMut ValidityChecker 69# stub files 70IMPL_FILES = $(addsuffix _impl.cpp,$(JNI_FILES)) 71# generated files 72JNI_CPP_FILES = $(patsubst %,%.cpp,$(JNI_FILES)) 73# non-generated files 74SRC_CPP_FILES = JniUtils.cpp 75# all cpp files (to compile) 76CPP_FILES = $(SRC_CPP_FILES) $(JNI_CPP_FILES) 77 78HEADER_FILES = JniUtils.h 79PYTHON_FILES = run_all.py run_tests.py create_impl.py 80MANIFEST_FILES = Cvc3_manifest Test_manifest 81 82DIST_FILES = \ 83Makefile \ 84README \ 85$(addprefix $(SOURCE_PATH)/$(PACKAGE)/, \ 86 $(addsuffix .java, $(JAVA_FILES)) \ 87 $(IMPL_FILES) $(SRC_CPP_FILES)) \ 88$(addprefix $(HEADER_PATH)/$(PACKAGE)/, $(HEADER_FILES)) \ 89$(PYTHON_FILES) \ 90$(MANIFEST_FILES) 91 92 93# target files 94# java library files compiled to class files 95LIB_CLASS_FILES = $(patsubst %,%.class,$(LIB_FILES)) 96# test files compiled to class files 97TEST_CLASS_FILES = $(patsubst %,%.class,$(TEST_FILES)) 98# cvc3 standalone files compiled to class files 99PROG_CLASS_FILES = $(patsubst %,%.class,$(PROG_FILES)) 100# all compiled java files, library and stand alone 101CLASS_FILES = $(LIB_CLASS_FILES) $(TEST_CLASS_FILES) $(PROG_CLASS_FILES) 102# jni header files created from the library class files 103H_FILES = $(patsubst %,%.h,$(JNI_FILES)) 104# precompiled header files 105GCH_FILES = $(patsubst %.h,%.h.gch,$(H_FILES)) JniUtils.h.gch 106# cpp files compiled to object files 107JNI_O_FILES = $(patsubst %.cpp,%.o,$(JNI_CPP_FILES)) 108O_FILES = $(patsubst %.cpp,%.o,$(CPP_FILES)) 109 110# library files 111# cpp library 112LIB_PREFIX = lib 113LIB_JNI_NAME = $(LIB_PREFIX)cvc3jni 114ifneq ($(CYGWIN),) 115 LIB_JNI_BASE = $(LIB_JNI_NAME).$(SHARED_LIB_SUFFIX) 116 LIB_JNI = $(LIB_JNI_NAME)-$(subst .,-,$(LIB_VERSION)).$(SHARED_LIB_SUFFIX) 117 LIB_JNI_COMPAT = $(LIB_JNI_NAME)-$(subst .,-,$(LIB_COMPAT_VERSION)).$(SHARED_LIB_SUFFIX) 118 LIB_JNI_MAJOR = $(LIB_JNI_NAME)-$(subst .,-,$(LIB_MAJOR_VERSION)).$(SHARED_LIB_SUFFIX) 119else 120LIB_JNI_BASE = $(LIB_JNI_NAME).$(SHARED_LIB_SUFFIX) 121ifneq ($(MAC_OSX),) 122 LIB_JNI = $(LIB_JNI_NAME).$(LIB_VERSION).$(SHARED_LIB_SUFFIX) 123 LIB_JNI_COMPAT = $(LIB_JNI_NAME).$(LIB_COMPAT_VERSION).$(SHARED_LIB_SUFFIX) 124 LIB_JNI_MAJOR = $(LIB_JNI_NAME).$(LIB_MAJOR_VERSION).$(SHARED_LIB_SUFFIX) 125else 126 LIB_JNI = $(LIB_JNI_BASE).$(LIB_VERSION) 127 LIB_JNI_COMPAT = $(LIB_JNI_BASE).$(LIB_COMPAT_VERSION) 128 LIB_JNI_MAJOR = $(LIB_JNI_BASE).$(LIB_MAJOR_VERSION) 129endif 130endif 131# java library 132LIB_CVC3 = libcvc3-$(LIB_VERSION).jar 133# test alone 134PROG_TEST = cvc3test.jar 135# java stand alone 136PROG_CVC3 = cvc3.jar 137 138 139### virtual file lookup paths 140#VPATH = src/cvc3/ 141vpath %.java $(SOURCE_PATH)/$(PACKAGE) 142vpath %.cpp $(SOURCE_PATH)/$(PACKAGE) 143vpath %.h $(HEADER_PATH)/$(PACKAGE) 144vpath %.h.gch $(HEADER_PATH)/$(PACKAGE) 145vpath %.class $(OBJ_PATH)/$(PACKAGE) 146vpath %.o $(OBJ_PATH)/$(PACKAGE) 147 148 149.PHONY: all classes headers objects libs libjni libcvc3 testlib cvc3 test regress print_src clean distclean %.d 150 151### rules 152 153all: classes headers objects libs 154libs: libjni libcvc3 testlib cvc3 155 156%.d: 157 if [ ! -d $* ]; then mkdir -p $*; fi 158 159$(OBJ_PATH): $(OBJ_PATH).d 160$(LIB_PATH): $(LIB_PATH).d 161$(ARCH_LIB_PATH): $(ARCH_LIB_PATH).d 162 163# compile each java file 164classes: $(OBJ_PATH) $(CLASS_FILES) 165$(CLASS_FILES): %.class: %.java $(OBJ_PATH) 166 $(JAVAC) $(JFLAGS) -sourcepath $(SOURCE_PATH) \ 167 -d $(OBJ_PATH) $(SOURCE_PATH)/$(PACKAGE)/$*.java 168 169# create a jni header file for each library class file 170#headers: $(H_FILES) $(GCH_FILES) 171headers: $(OBJ_PATH) $(H_FILES) 172$(H_FILES): %.h: %.class $(OBJ_PATH) 173 $(JAVAH) -jni -force -classpath $(OBJ_PATH) \ 174 -o $(HEADER_PATH)/$(PACKAGE)/$*.h $(PACKAGE).$* 175 176# precompile headers 177$(GCH_FILES): %.h.gch: %.h 178 $(CXX) $(CPPFLAGS) $(CXXFLAGS) \ 179 -I ../src/include -I $(HEADER_PATH)/$(PACKAGE)/ \ 180 -o $(HEADER_PATH)/$(PACKAGE)/$*.h.gch $(HEADER_PATH)/$(PACKAGE)/$*.h 181 182# compile each cpp file 183$(JNI_CPP_FILES): %.cpp: %_impl.cpp %.h JniUtils.h 184 $(PYTHON) ./create_impl.py \ 185 $(HEADER_PATH)/$(PACKAGE)/$*.h \ 186 $(SOURCE_PATH)/$(PACKAGE)/$*_impl.cpp \ 187 $(SOURCE_PATH)/$(PACKAGE)/$*.cpp 188 189objects: $(OBJ_PATH) $(O_FILES) 190$(O_FILES): %.o: %.cpp %.h $(OBJ_PATH) 191 $(CXX) $(CPPFLAGS) $(CXXFLAGS) -c \ 192 -I ../src/include -I $(HEADER_PATH)/$(PACKAGE)/ \ 193 -o $(OBJ_PATH)/$(PACKAGE)/$*.o $(SOURCE_PATH)/$(PACKAGE)/$*.cpp 194 195# create the cpp jni wrapper library 196 197libjni: $(ARCH_LIB_PATH)/$(LIB_JNI) $(LIB_PATH)/$(LIB_JNI) 198$(ARCH_LIB_PATH)/$(LIB_JNI): $(O_FILES) $(ARCH_LIB_PATH) 199ifneq ($(MAC_OSX),) 200 $(CXX) $(SHARED) $(CXXFLAGS) $(LDFLAGS) \ 201 -install_name $(libdir)/$(LIB_JNI_MAJOR) \ 202 -compatibility_version $(LIB_COMPAT_VERSION) \ 203 -current_version $(LIB_VERSION) \ 204 -L../lib $(OBJ_PATH)/$(PACKAGE)/*.o \ 205 -o '$(ARCH_LIB_PATH)/$(LIB_JNI)' `` -lcvc3 $(LD_LIBS) 206else 207 $(CXX) $(SHARED) $(CXXFLAGS) $(LDFLAGS) \ 208 -Wl,-soname,$(LIB_JNI_COMPAT) \ 209 -L ../lib $(OBJ_PATH)/$(PACKAGE)/*.o \ 210 -o $(ARCH_LIB_PATH)/$(LIB_JNI) -lcvc3 $(LD_LIBS) 211ifeq ($(CYGWIN),) 212 $(LDCONFIG) -nv $(ARCH_LIB_PATH) 213endif 214endif 215 ln -sf $(LIB_JNI) $(ARCH_LIB_PATH)/$(LIB_JNI_COMPAT) 216 ln -sf $(LIB_JNI) $(ARCH_LIB_PATH)/$(LIB_JNI_MAJOR) 217 ln -sf $(LIB_JNI) $(ARCH_LIB_PATH)/$(LIB_JNI_BASE) 218 219# $(CXX) $(CPPFLAGS) $(CXXFLAGS) -shared \ 220 221#$(LIB_PATH)/$(LIB_JNI): $(O_FILES) 222# ar ruvs $(LIB_PATH)/libcvc3jni.a $(OBJ_PATH)/$(PACKAGE)/*.o 223# $(CXX) $(CXXFLAGS) -shared -Wl,-soname,$(LIB_JNI) \ 224# -L ../lib -lc -lcvc3 -lgmp \ 225# $(LIB_PATH)/libcvc3jni.a \ 226# -o $(LIB_PATH)/$(LIB_JNI) 227 228#ar ruvs /media/data/ESCJava/CVC3/cvc3/lib/linux-i686-debug/libvcl.a /media/data/ESCJava/CVC3/cvc3/obj/vcl/linux-i686-debug/vcl.o /media/data/ESCJava/CVC3/cvc3/obj/vcl/linux-i686-debug/vc_cmd.o 229 230$(LIB_PATH)/$(LIB_JNI): $(ARCH_LIB_PATH)/$(LIB_JNI) 231 ln -sf $< $@ 232# [chris] ldconfig seems to just delete the .so's! 233# $(LDCONFIG) -nv '$(call dirx,$@)' 234 ln -sf $(LIB_JNI) '$(call dirx,$@)/$(LIB_JNI_COMPAT)' 235 ln -sf $(LIB_JNI) '$(call dirx,$@)/$(LIB_JNI_MAJOR)' 236 ln -sf $(LIB_JNI) '$(call dirx,$@)/$(LIB_JNI_BASE)' 237 238# create the java wrapper library 239libcvc3: $(LIB_PATH) $(LIB_PATH)/$(LIB_CVC3) 240$(LIB_PATH)/$(LIB_CVC3): $(LIB_CLASS_FILES) 241 cd $(OBJ_PATH) && $(JAR) cf ../../$(REL_LIB_PATH)/$(LIB_CVC3) $(PACKAGE)/*.class 242 243 244install: $(ARCH_LIB_PATH)/$(LIB_JNI) $(LIB_PATH)/$(LIB_CVC3) 245 mkdir -p $(javadir) 246 $(INSTALL) $(INSTALL_FLAGS) -m 644 $(LIB_PATH)/$(LIB_CVC3) $(javadir) 247 mkdir -p $(libdir) 248 $(INSTALL) $(INSTALL_FLAGS) -m 644 $(ARCH_LIB_PATH)/$(LIB_JNI) $(libdir) 249 ln -sf $(LIB_JNI) $(libdir)/$(LIB_JNI_MAJOR) 250 ln -sf $(LIB_JNI) $(libdir)/$(LIB_JNI_COMPAT) 251 ln -sf $(LIB_JNI) $(libdir)/$(LIB_JNI_BASE) 252ifeq ($(MAC_OSX),) 253ifeq ($(CYGWIN),) 254 $(LDCONFIG) -nv $(libdir) 255endif 256endif 257# chmod 644 $(libdir)/$(LIB_JNI) 258 259 260# create the java stand alone program 261cvc3: $(LIB_PATH) $(LIB_PATH)/$(PROG_CVC3) 262$(LIB_PATH)/$(PROG_CVC3): $(PROG_CLASS_FILES) 263 $(JAR) -cmf Cvc3_manifest ../$(REL_LIB_PATH)/$(PROG_CVC3) 264 @for i in $(PROG_CLASS_FILES); do \ 265 echo $(JAR) -uf ../$(REL_LIB_PATH)/$(PROG_CVC3) -C $(OBJ_PATH) $(PACKAGE)/$$i; \ 266 $(JAR) -uf ../$(REL_LIB_PATH)/$(PROG_CVC3) -C $(OBJ_PATH) $(PACKAGE)/$$i; \ 267 done 268 269# create the test stand alone program 270testlib: $(LIB_PATH) $(LIB_PATH)/$(PROG_TEST) 271 272test: testlib 273 $(JAVA) $(JREFLAGS) -Djava.library.path=../$(REL_ARCH_LIB_PATH) -ea -jar ../$(REL_LIB_PATH)/$(PROG_TEST) 274 275$(LIB_PATH)/$(PROG_TEST): $(TEST_CLASS_FILES) 276 echo -e "Main-Class: cvc3/Test\nClass-Path: $(LIB_CVC3)\n" > Test_manifest 277 $(JAR) -cmf Test_manifest ../$(REL_LIB_PATH)/$(PROG_TEST) 278 @for i in $(TEST_CLASS_FILES); do \ 279 echo $(JAR) -uf ../$(REL_LIB_PATH)/$(PROG_TEST) -C $(OBJ_PATH) $(PACKAGE)/$$i; \ 280 $(JAR) -uf ../$(REL_LIB_PATH)/$(PROG_TEST) -C $(OBJ_PATH) $(PACKAGE)/$$i; \ 281 done 282 283regress: cvc3 284 $(PYTHON) ./run_tests.py \ 285 -vc '$(JAVA) $(JREFLAGS) -Djava.library.path=../$(REL_LIB_PATH) -ea -Xss100M -jar ../$(REL_LIB_PATH)/$(PROG_CVC3)' \ 286 -t 15 -m 500 -l 4 ../benchmarks 287 288 289ifndef FILELIST 290FILELIST = /dev/null 291endif 292 293print_src: 294 echo $(addprefix java/, $(DIST_FILES)) >> $(FILELIST) 295# echo $(patsubst %, src/include/%, $(HEADER_NAMES)) >> $(FILELIST) 296 297 298 299# clean up 300 301clean: $(OBJ_PATH) 302 rm -f $(addprefix $(SOURCE_PATH)/$(PACKAGE)/, $(JNI_CPP_FILES)) 303 rm -fr $(OBJ_PATH)/$(PACKAGE)/* 304 rm -fr $(LIB_PATH)/* 305 rm -f $(addprefix $(HEADER_PATH)/$(PACKAGE)/, $(H_FILES) $(GCH_FILES)) 306 307distclean: clean 308