1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
|
# -*-makefile-*-
#
# This makefile is the _source_ directory's makefile, and is static,
# not generated. Makefile.am is the automake makefile for the build
# top-level (its corresponding Makefile.in is here, too, but the
# corresponding Makefile is under builds/$arch/$buildid.
#
builddir = builds
.PHONY: all install examples install-examples
all install examples install-examples .DEFAULT:
@if test -d $(builddir); then \
echo cd $(builddir); \
cd $(builddir); \
echo $(MAKE) $@; \
$(MAKE) $@ || exit 1; \
$(MAKE) show-config; \
else \
echo; \
echo 'Run configure first, or type "make" in a configured build directory.'; \
echo; \
fi
distclean maintainerclean:
@if test -d $(builddir); then \
echo cd $(builddir); \
cd $(builddir); \
echo $(MAKE) $@; \
$(MAKE) $@ || exit 1; \
fi
test -z "$(builddir)" || rm -fr "$(builddir)"
rm -f config.reconfig
# synonyms for "check"
.PHONY: test
test: check
.PHONY: doc doc-internals
doc: doc-builds
doc-internals: doc-internals-builds
YEAR := $(shell date +%Y)
submission:
@if [ -d builds-smtcomp ]; then \
echo 'ERROR: remove the builds-smtcomp directory' >&2; \
exit 1; \
fi
@if test -d cvc4-smtcomp-$(YEAR) || test -e cvc4-smtcomp-$(YEAR).zip || \
test -d cvc4-smtcomp-main-$(YEAR) || test -e cvc4-smtcomp-main-$(YEAR).zip || \
test -d cvc4-smtcomp-application-$(YEAR) || test -e cvc4-smtcomp-application-$(YEAR).zip || \
test -d cvc4-smtcomp-parallel-$(YEAR) || test -e cvc4-smtcomp-parallel-$(YEAR).zip; then \
echo 'ERROR: remove cvc4-smtcomp*-$(YEAR) and corresponding zipfiles.' >&2; \
exit 1; \
fi
$(MAKE) submission-main
$(MAKE) submission-application
$(MAKE) submission-parallel
mkdir -p cvc4-smtcomp-$(YEAR)/bin
cp -p cvc4-smtcomp-main-$(YEAR)/bin/cvc4 cvc4-smtcomp-$(YEAR)/bin/cvc4-main
cp -p cvc4-smtcomp-main-$(YEAR)/bin/starexec_run_default cvc4-smtcomp-$(YEAR)/bin/starexec_run_default
cp -p cvc4-smtcomp-application-$(YEAR)/bin/cvc4 cvc4-smtcomp-$(YEAR)/bin/cvc4-application
cp -p cvc4-smtcomp-application-$(YEAR)/bin/starexec_run_default cvc4-smtcomp-$(YEAR)/bin/starexec_run_application
cp -p cvc4-smtcomp-parallel-$(YEAR)/bin/cvc4 cvc4-smtcomp-$(YEAR)/bin/pcvc4
cp -p cvc4-smtcomp-parallel-$(YEAR)/bin/starexec_run_default cvc4-smtcomp-$(YEAR)/bin/starexec_run_parallel
cat cvc4-smtcomp-main-$(YEAR)/starexec_description.txt \
cvc4-smtcomp-application-$(YEAR)/starexec_description.txt \
cvc4-smtcomp-parallel-$(YEAR)/starexec_description.txt \
> cvc4-smtcomp-$(YEAR)/starexec_description.txt
cd cvc4-smtcomp-$(YEAR) && zip -r ../cvc4-smtcomp-$(YEAR).zip *
submission-main:
@if [ -d builds-smtcomp/main ]; then \
echo 'ERROR: remove the builds-smtcomp/main directory' >&2; \
exit 1; \
fi
@if [ -n "`ls src/parser/*/generated 2>/dev/null`" ]; then \
echo 'ERROR:' >&2; \
echo 'ERROR: Please make maintainer-clean first.' >&2; \
echo 'ERROR:' >&2; \
exit 1; \
fi
@if test -d cvc4-smtcomp-main-$(YEAR) || test -e cvc4-smtcomp-main-$(YEAR).zip; then \
echo 'ERROR:' >&2; \
echo 'ERROR: Please remove cvc4-smtcomp-main-$(YEAR) and cvc4-smtcomp-main-$(YEAR).zip first.' >&2; \
echo 'ERROR:' >&2; \
exit 1; \
fi
./autogen.sh
mkdir -p builds-smtcomp/main
( cd builds-smtcomp/main; \
../../configure competition --disable-shared --enable-static-binary --with-cln --with-glpk --with-abc --without-readline --enable-gpl; \
$(MAKE) V=1; \
strip src/main/cvc4; \
$(MAKE) check )
# main track
mkdir -p cvc4-smtcomp-main-$(YEAR)/bin
cp -p builds-smtcomp/main/src/main/cvc4 cvc4-smtcomp-main-$(YEAR)/bin/cvc4
cp contrib/run-script-smtcomp2014 cvc4-smtcomp-main-$(YEAR)/bin/starexec_run_default
chmod 755 cvc4-smtcomp-main-$(YEAR)/bin/starexec_run_default
echo "CVC4 for SMT_COMP main track `builds-smtcomp/main/src/main/cvc4 --version | head -1 | sed 's,.*version ,,;s,-,_,g;s,[^a-zA-Z0-9. _],,g'`" > cvc4-smtcomp-main-$(YEAR)/starexec_description.txt
cd cvc4-smtcomp-main-$(YEAR) && zip -r ../cvc4-smtcomp-main-$(YEAR).zip *
submission-application:
# application track is a separate build because it has different preprocessor #defines
@if [ -d builds-smtcomp/application ]; then \
echo 'ERROR: remove the builds-smtcomp/main directory' >&2; \
exit 1; \
fi
@if [ -n "`ls src/parser/*/generated 2>/dev/null`" ]; then \
echo 'ERROR:' >&2; \
echo 'ERROR: Please make maintainer-clean first.' >&2; \
echo 'ERROR:' >&2; \
exit 1; \
fi
@if test -d cvc4-smtcomp-application-$(YEAR) || test -e cvc4-smtcomp-application-$(YEAR).zip; then \
echo 'ERROR:' >&2; \
echo 'ERROR: Please remove cvc4-smtcomp-application-$(YEAR) and cvc4-smtcomp-application-$(YEAR).zip first.' >&2; \
echo 'ERROR:' >&2; \
exit 1; \
fi
./autogen.sh
mkdir -p builds-smtcomp/application
( cd builds-smtcomp/application; \
../../configure competition --disable-shared --enable-static-binary --with-cln --with-glpk --with-abc --without-readline --enable-gpl CXXFLAGS=-DCVC4_SMTCOMP_APPLICATION_TRACK CFLAGS=-DCVC4_SMTCOMP_APPLICATION_TRACK; \
$(MAKE) V=1; \
strip src/main/cvc4; \
$(MAKE) check )
# package the application track zipfile
mkdir -p cvc4-smtcomp-application-$(YEAR)/bin
cp -p builds-smtcomp/application/src/main/cvc4 cvc4-smtcomp-application-$(YEAR)/bin/cvc4
cp contrib/run-script-smtcomp2014-application cvc4-smtcomp-application-$(YEAR)/bin/starexec_run_default
chmod 755 cvc4-smtcomp-application-$(YEAR)/bin/starexec_run_default
echo "CVC4 for SMT_COMP application track `builds-smtcomp/application/src/main/cvc4 --version | head -1 | sed 's,.*version ,,;s,-,_,g;s,[^a-zA-Z0-9. _],,g'`" > cvc4-smtcomp-application-$(YEAR)/starexec_description.txt
cd cvc4-smtcomp-application-$(YEAR) && zip -r ../cvc4-smtcomp-application-$(YEAR).zip *
submission-parallel:
# parallel track can't be built with -cln, so it's a separate build
@if [ -d builds-smtcomp/parallel ]; then \
echo 'ERROR: remove the builds-smtcomp/main directory' >&2; \
exit 1; \
fi
@if [ -n "`ls src/parser/*/generated 2>/dev/null`" ]; then \
echo 'ERROR:' >&2; \
echo 'ERROR: Please make maintainer-clean first.' >&2; \
echo 'ERROR:' >&2; \
exit 1; \
fi
@if test -d cvc4-smtcomp-parallel-$(YEAR) || test -e cvc4-smtcomp-parallel-$(YEAR).zip; then \
echo 'ERROR:' >&2; \
echo 'ERROR: Please remove cvc4-smtcomp-parallel-$(YEAR) and cvc4-smtcomp-parallel-$(YEAR).zip first.' >&2; \
echo 'ERROR:' >&2; \
exit 1; \
fi
./autogen.sh
mkdir -p builds-smtcomp/parallel
( cd builds-smtcomp/parallel; \
../../configure competition --disable-shared --enable-static-binary --with-gmp --with-portfolio --with-glpk --with-abc --without-readline --enable-gpl; \
$(MAKE) V=1; \
strip src/main/pcvc4; \
$(MAKE) check BINARY=pcvc4 CVC4_REGRESSION_ARGS=--fallback-sequential )
# package the parallel track zipfile
mkdir -p cvc4-smtcomp-parallel-$(YEAR)/bin
cp -p builds-smtcomp/parallel/src/main/pcvc4 cvc4-smtcomp-parallel-$(YEAR)/bin/pcvc4
( echo '#!/bin/sh'; \
echo 'exec ./pcvc4 --threads 2 -L smt2 --no-checking --no-interactive "$@"' ) > cvc4-smtcomp-parallel-$(YEAR)/bin/starexec_run_default
chmod 755 cvc4-smtcomp-parallel-$(YEAR)/bin/starexec_run_default
echo "CVC4 for SMT_COMP parallel track `builds-smtcomp/parallel/src/main/pcvc4 --version | head -1 | sed 's,.*version ,,;s,-,_,g;s,[^a-zA-Z0-9. _],,g'`" > cvc4-smtcomp-parallel-$(YEAR)/starexec_description.txt
cd cvc4-smtcomp-parallel-$(YEAR) && zip -r ../cvc4-smtcomp-parallel-$(YEAR).zip *
|
