Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 3 additions & 3 deletions build/build-publish-solvers/solver-yices.xml
Original file line number Diff line number Diff line change
Expand Up @@ -194,16 +194,16 @@ SPDX-License-Identifier: Apache-2.0

<target name="download-jdk21-windows" depends="build-initialize" unless="jdk.downloaded">
<!-- Download a more recent Jdk to avoid compile errors -->
<get src="https://download.oracle.com/java/21/latest/jdk-21_windows-x64_bin.zip" dest="/dependencies" verbose="true"/>
<unzip src="/dependencies/jdk-21_windows-x64_bin.zip" dest="/dependencies"/>
<get src="https://download.oracle.com/java/21/archive/jdk-21.0.10_windows-x64_bin.zip" dest="/dependencies" verbose="true"/>

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@PhilippWendler do we need to add a license of we use Oracle JDKs?

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

One always needs a license for every piece of software that one uses.

Whether the current license of the Oracle JDK allows us to use it for free I don't know, you have to check.

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thank you! We will take a look and add the appropriate license if needed.

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What do you mean with "add"? Why and where would you want to "add" a license? The license is specified by Oracle, not us. We need to be given a license that allows us to use the software.

<unzip src="/dependencies/jdk-21.0.10_windows-x64_bin.zip" dest="/dependencies"/>
<delete file="/dependencies/jdk-21_windows-x64_bin.zip" failonerror="true"/>
<move file="/dependencies/jdk-21.0.10" tofile="/dependencies/jdk21-windows-x64" failonerror="true"/>
</target>

<target name="download-yices2-java" depends="build-initialize" unless="yices-java.downloaded">
<exec executable="git" dir="${yices2.buildDir}" failonerror="true">
<arg value="clone"/>
<arg value="https://github.com/daniel-raffler/yices2_java_bindings.git"/>
<arg value="https://github.com/SRI-CSL/yices2_java_bindings.git"/>
</exec>
</target>
<target name="build-yices2-java" depends="build-yices2, download-jdk21-windows, download-yices2-java" unless="yices-java.installed">
Expand Down
45 changes: 25 additions & 20 deletions lib/native/source/yices2/jni.patch
Original file line number Diff line number Diff line change
Expand Up @@ -40,7 +40,7 @@ diff --git a/build.xml b/build.xml
</target>

<target name="dist" depends="compile"
@@ -220,11 +226,16 @@
@@ -220,11 +237,16 @@
</manifest>
</jar>

Expand Down Expand Up @@ -75,48 +75,53 @@ diff --git a/src/main/java/com/sri/yices/Makefile b/src/main/java/com/sri/yices/
$(error "Unkown OS: $(OS)")
@@ -48,7 +50,11 @@
endif

# name of the library
-libyices2java := libyices2java.$(EXTENSION)
+ifeq ($(OS),win32)
+ libyices2java := yices2java.$(EXTENSION)

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

libyices2java is hardcoded as a name several times below. Do we need to update those as well?

+else
+ libyices2java := libyices2java.$(EXTENSION)
+endif

# install name for darwin
libyices2java_install_name := $(YICES_JNI)/libyices2java.dylib
@@ -56,9 +62,11 @@
@@ -56,15 +62,11 @@
# we ignore versions and soname for now

# default include directories for jni.h and jni_md.h
-CPPFLAGS := -I $(JAVA_HOME)/include -I $(JAVA_HOME)/include/$(OS)
-CXXFLAGS := -g -fPIC
-LIBS := -lyices -lgmp
-GMP_CPPFLAGS ?= $(shell pkg-config --cflags gmp 2>/dev/null)
-GMP_LIBS ?= $(shell pkg-config --libs gmp 2>/dev/null)
+CPPFLAGS := -I $(JNI_PATH) -I $(JNI_PATH)/$(OS) -I $(GMP_PATH)/include -I $(YICES_PATH)/include
+CXXFLAGS := -O3 -fPIC $(CXXFLAGS)
+

-CPPFLAGS += -I $(JAVA_HOME)/include -I $(JAVA_HOME)/include/$(OS) $(GMP_CPPFLAGS)
-CXXFLAGS += -g -fPIC
-ifeq ($(strip $(GMP_LIBS)),)
-GMP_LIBS := -lgmp
-endif
-LIBS += -lyices $(GMP_LIBS)
+LDFLAGS := -L $(YICES_PATH)/lib -L $(CUDD_PATH)/lib -L $(POLY_PATH)/lib -L $(GMP_PATH)/lib
+LIBS := -lyices -lcudd -lpoly -lgmpxx -lgmp
+LIBS = -lyices -lcudd -lpoly -lgmpxx -lgmp

CXX ?= g++
@@ -86,7 +94,10 @@
$(CXX) $(CPPFLAGS) $(CXXFLAGS) -dynamiclib -o $@ yicesJNI.o $(LIBS)

@@ -92,7 +94,10 @@
$(CXX) $(CPPFLAGS) $(CXXFLAGS) $(LDFLAGS) -dynamiclib -o $@ yicesJNI.o $(LIBS)

libyices2java.so: yicesJNI.o
- $(CXX) $(CFLAGS) $(LDFLAGS) -shared -o $@ yicesJNI.o $(LIBS)
- $(CXX) $(CPPFLAGS) $(CXXFLAGS) $(LDFLAGS) -shared -o $@ yicesJNI.o $(LIBS)
+ $(CXX) $(CFLAGS) $(LDFLAGS) -o $@ yicesJNI.o -shared -Wl,-soname,$(libyices2java) -Wl,-Bstatic $(LIBS) -static-libstdc++ -lstdc++ -Wl,-Bdynamic -lc -lm -Wl,--version-script=libyices2java.version
+
+yices2java.dll: yicesJNI.o
+ $(CXX) $(CFLAGS) $(LDFLAGS) -o $@ yicesJNI.o -shared -Wl,-soname,$(libyices2java) -Wl,-Bstatic,--whole-archive -lpthread -Wl,-Bstatic,--no-whole-archive $(LIBS) -static-libgcc -static-libstdc++ -lstdc++ -Wl,-Bdynamic -lm -Wl,--version-script=libyices2java.version

LIBDIR := $(YICES_JNI)
@@ -99,7 +110,10 @@

@@ -105,7 +110,10 @@
install-darwin:
cp $(libyices2java) $(LIBDIR)

+install-win32:
+ cp $(libyices2java) $(LIBDIR)
+
Expand Down
Loading