Skip to content

Commit fb0cc0c

Browse files
daniel-rafflerdaniel-raffler
committed
OpenSMT: Add SWIG generated files to the repository and combine opensmtjava.so and opensmt.so into a single library
1 parent 14669d6 commit fb0cc0c

34 files changed

+13220
-43
lines changed

‎build/build-publish-solvers/solver-opensmt.xml

+18-10
Original file line numberDiff line numberDiff line change
@@ -90,8 +90,7 @@ SPDX-License-Identifier: Apache-2.0
9090
<arg value="swig/opensmt.i"/>
9191
</exec>
9292

93-
<!-- Copy (only!) the required java files to the source tree. This should make sure that compilation fails
94-
if the OpenSMT interface changed, but the swig header wasn't updated -->
93+
<!-- Copy the generated Java classes and the c++ wrapper to the source tree -->
9594
<copy todir="${path.source}/src/org/sosy_lab/java_smt/solvers/opensmt/api">
9695
<fileset dir="${path.install}/java/opensmt">
9796
<include name="ArithLogic.java"/>
@@ -121,6 +120,13 @@ SPDX-License-Identifier: Apache-2.0
121120
<include name="VectorVectorInt.java"/>
122121
</fileset>
123122
</copy>
123+
<copy file="${path.install}/opensmt-wrap.cpp" toFile="${path.source}/opensmt-wrap.cpp"/>
124+
125+
<!-- Apply the patch to add the license headers -->
126+
<exec executable="git" failonerror="true">
127+
<arg value="apply"/>
128+
<arg value="${path.source}/swigWrapper.patch"/>
129+
</exec>
124130

125131
<!-- Package swig generated source code -->
126132
<jar destfile="opensmt-${opensmt.version}-sources.jar" basedir="${path.source}/src"/>
@@ -131,14 +137,10 @@ SPDX-License-Identifier: Apache-2.0
131137
<jar destfile="opensmt-${opensmt.version}-javadoc.jar" basedir="${path.source}/doc"/>
132138
<delete dir="${path.source}/doc"/>
133139

134-
<!-- Copy the lib to the root directory for later packaging-->
135-
<copy file="${path.install}/lib/libopensmt.so" toFile="libopensmt-${opensmt.version}.so"/>
136-
137140
<!-- Dump ${opensmt.version} to a file so that we can use it for the swig wrapper -->
138141
<echo file="${path.source}/version.h">#define VERSION "${opensmt.version}"</echo>
139142

140-
<!-- Copy the swig wrapper to the source tree and compile it-->
141-
<copy file="${path.install}/opensmt-wrap.cpp" toFile="${path.source}/opensmt-wrap.cpp"/>
143+
<!-- Compile the swig wrapper to create the library -->
142144
<exec executable="gcc" dir="${path.source}" failonerror="true">
143145
<arg value="-fPIC"/>
144146
<arg value="-std=c++20"/>
@@ -150,16 +152,22 @@ SPDX-License-Identifier: Apache-2.0
150152
<arg value="-I${java.home}/include/"/>
151153
<arg value="-I${java.home}/include/linux"/>
152154
</exec>
155+
<delete file="${path.source}/version.h"/>
153156

154157
<!-- Link the wrapper and create a new lib -->
155-
<symlink link="libopensmt.so" resource="libopensmt-${opensmt.version}.so"/>
156158
<exec executable="gcc" dir="${path.source}" failonerror="true">
157159
<arg value="-shared"/>
158160
<arg value="-o"/>
159161
<arg value="${user.dir}/libopensmtjava-${opensmt.version}.so"/>
160162
<arg value="opensmt-wrap.o"/>
161-
<arg value="-L${path.install}/lib"/>
162-
<arg value="-l:libopensmt.a"/>
163+
<arg value="-lstdc++"/>
164+
<arg value="-Wl,--whole-archive"/>
165+
<arg value="/dependencies/gmp-6.2.1/.libs/libgmp.a"/>
166+
<arg value="/dependencies/gmp-6.2.1/.libs/libgmpxx.a"/>
167+
<arg value="${path.install}/lib/libopensmt.a"/>
168+
<arg value="-Wl,--no-whole-archive"/>
169+
<arg value="-lm"/>
170+
<arg value="-Wl,-z,defs"/>
163171
</exec>
164172
<delete file="${path.source}/opensmt-wrap.o"/>
165173

‎doc/Example-Maven-Project/pom.xml

+1-15
Original file line numberDiff line numberDiff line change
@@ -248,21 +248,14 @@ SPDX-License-Identifier: Apache-2.0
248248
<classifier>libyices2j</classifier>
249249
</dependency>
250250

251-
<!-- OpenSMT has three dependencies (on Linux) -->
251+
<!-- OpenSMT has two dependencies (on Linux) -->
252252
<dependency>
253253
<groupId>org.sosy-lab</groupId>
254254
<artifactId>javasmt-solver-opensmt</artifactId>
255255
<version>${opensmt.version}</version>
256256
<type>jar</type>
257257
<classifier>opensmt</classifier>
258258
</dependency>
259-
<dependency>
260-
<groupId>org.sosy-lab</groupId>
261-
<artifactId>javasmt-solver-opensmt</artifactId>
262-
<version>${opensmt.version}</version>
263-
<type>so</type>
264-
<classifier>libopensmt</classifier>
265-
</dependency>
266259
<dependency>
267260
<groupId>org.sosy-lab</groupId>
268261
<artifactId>javasmt-solver-opensmt</artifactId>
@@ -498,13 +491,6 @@ SPDX-License-Identifier: Apache-2.0
498491
<classifier>libopensmtjava</classifier>
499492
<destFileName>libopensmtjava.so</destFileName>
500493
</artifactItem>
501-
<artifactItem>
502-
<groupId>org.sosy-lab</groupId>
503-
<artifactId>javasmt-solver-opensmt</artifactId>
504-
<type>so</type>
505-
<classifier>libopensmt</classifier>
506-
<destFileName>libopensmt.so</destFileName>
507-
</artifactItem>
508494
</artifactItems>
509495
</configuration>
510496
</plugin>

‎doc/Example-Maven-Web-Project/pom.xml

+1-16
Original file line numberDiff line numberDiff line change
@@ -249,21 +249,14 @@ SPDX-License-Identifier: Apache-2.0
249249
<classifier>libyices2j</classifier>
250250
</dependency>
251251

252-
<!-- OpenSMT has three dependencies (on Linux) -->
252+
<!-- OpenSMT has two dependencies (on Linux) -->
253253
<dependency>
254254
<groupId>org.sosy-lab</groupId>
255255
<artifactId>javasmt-solver-opensmt</artifactId>
256256
<version>${opensmt.version}</version>
257257
<type>jar</type>
258258
<classifier>opensmt</classifier>
259259
</dependency>
260-
<dependency>
261-
<groupId>org.sosy-lab</groupId>
262-
<artifactId>javasmt-solver-opensmt</artifactId>
263-
<version>${opensmt.version}</version>
264-
<type>so</type>
265-
<classifier>libopensmt</classifier>
266-
</dependency>
267260
<dependency>
268261
<groupId>org.sosy-lab</groupId>
269262
<artifactId>javasmt-solver-opensmt</artifactId>
@@ -334,7 +327,6 @@ SPDX-License-Identifier: Apache-2.0
334327
<include>libpoly.so</include>
335328
<include>libpolyxx.so</include>
336329
<include>libyices2j.so</include>
337-
<include>libopensmt.so</include>
338330
<include>libopensmtjava.so</include>
339331
</includes>
340332
<targetPath>WEB-INF/lib</targetPath>
@@ -545,13 +537,6 @@ SPDX-License-Identifier: Apache-2.0
545537
<classifier>libopensmtjava</classifier>
546538
<destFileName>libopensmtjava.so</destFileName>
547539
</artifactItem>
548-
<artifactItem>
549-
<groupId>org.sosy-lab</groupId>
550-
<artifactId>javasmt-solver-opensmt</artifactId>
551-
<type>so</type>
552-
<classifier>libopensmt</classifier>
553-
<destFileName>libopensmt.so</destFileName>
554-
</artifactItem>
555540
</artifactItems>
556541
</configuration>
557542
</plugin>

0 commit comments

Comments
 (0)