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