diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
new file mode 100644
index 0000000..25f8fd9
--- /dev/null
+++ b/.github/workflows/ci.yml
@@ -0,0 +1,146 @@
+name: CI
+
+on:
+ pull_request:
+ push:
+
+permissions:
+ contents: read
+
+env:
+ FORCE_JAVASCRIPT_ACTIONS_TO_NODE24: "true"
+ YICES_REF: yices-2.7.0
+
+jobs:
+ unix:
+ name: ${{ matrix.os }}
+ runs-on: ${{ matrix.os }}
+ strategy:
+ fail-fast: false
+ matrix:
+ os:
+ - ubuntu-latest
+ - macos-latest
+
+ steps:
+ - uses: actions/checkout@v5
+
+ - name: Checkout Yices
+ uses: actions/checkout@v5
+ with:
+ repository: SRI-CSL/yices2
+ ref: ${{ env.YICES_REF }}
+ path: y2
+ fetch-depth: 1
+ sparse-checkout: |
+ Makefile
+ Makefile.build
+ configure
+ configure.ac
+ config.guess
+ config.sub
+ gmaketest
+ install-sh
+ make.include.in
+ autoconf
+ configs
+ scripts
+ src
+ utils
+ sparse-checkout-cone-mode: false
+
+ - name: Set up Java
+ uses: actions/setup-java@v5
+ with:
+ distribution: temurin
+ java-version: "17"
+
+ - name: Install Linux dependencies
+ if: runner.os == 'Linux'
+ run: |
+ sudo apt-get update
+ sudo apt-get install -y ant autoconf automake g++ gcc gperf libgmp-dev libtool m4 make pkg-config
+
+ - name: Install macOS dependencies
+ if: runner.os == 'macOS'
+ env:
+ HOMEBREW_NO_AUTO_UPDATE: "1"
+ run: |
+ brew install ant autoconf automake gmp gperf libtool make pkg-config
+
+ - name: Build and test
+ env:
+ YICES_SRC: ${{ github.workspace }}/y2
+ YICES_PREFIX: ${{ runner.temp }}/yices-install
+ run: bash scripts/ci-build-test-unix.sh
+
+ windows:
+ name: windows-latest
+ runs-on: windows-latest
+
+ steps:
+ - run: git config --system core.longpaths true
+
+ - run: git config --global core.autocrlf false && git config --global core.eol lf
+
+ - uses: actions/checkout@v5
+
+ - name: Checkout Yices
+ uses: actions/checkout@v5
+ with:
+ repository: SRI-CSL/yices2
+ ref: ${{ env.YICES_REF }}
+ path: y2
+ fetch-depth: 1
+ sparse-checkout: |
+ Makefile
+ Makefile.build
+ configure
+ configure.ac
+ config.guess
+ config.sub
+ gmaketest
+ install-sh
+ make.include.in
+ autoconf
+ configs
+ scripts
+ src
+ utils
+ sparse-checkout-cone-mode: false
+
+ - name: Set up Java
+ uses: actions/setup-java@v5
+ with:
+ distribution: temurin
+ java-version: "17"
+
+ - name: Install Ant
+ shell: powershell
+ run: choco install ant -y
+
+ - name: Install Cygwin dependencies
+ uses: cygwin/cygwin-install-action@v4
+ with:
+ packages: |
+ autoconf,
+ automake,
+ cmake,
+ coreutils,
+ curl,
+ gperf,
+ libtool,
+ m4,
+ make,
+ mingw64-x86_64-gcc-core,
+ mingw64-x86_64-gcc-g++,
+ moreutils,
+ wget
+
+ - name: Build and test
+ shell: bash
+ env:
+ CYGWIN: winsymlinks:native binmode
+ YICES_SRC: ${{ github.workspace }}/y2
+ YICES_PREFIX: /tmp/yices-install
+ run: bash scripts/ci-build-test-windows.sh
diff --git a/ant.sh b/ant.sh
index 42b359c..5ee5d95 100755
--- a/ant.sh
+++ b/ant.sh
@@ -1,6 +1,8 @@
#!/bin/bash
#uses the build.sh to mimic what 'ant install' does without 'ant'
+set -e
+
REPO_ROOT=${PWD}
YC=${REPO_ROOT}/build/classes
@@ -8,6 +10,6 @@ YI=${REPO_ROOT}/dist/lib
YICES_CLASSPATH=${YC} YICES_JNI=${YI} ./build.sh
-jar -cvfm ${YI}/yices.jar ${REPO_ROOT}/MANIFEST.txt -C ${YC} ${YC}/com/sri/yices/*.class
+jar -cvfm ${YI}/yices.jar ${REPO_ROOT}/MANIFEST.txt -C ${YC} .
java -Djava.library.path=${REPO_ROOT}/dist/lib -jar ${REPO_ROOT}/dist/lib/yices.jar
diff --git a/build.xml b/build.xml
index 8dceaf6..10e30e7 100644
--- a/build.xml
+++ b/build.xml
@@ -223,7 +223,7 @@
Executing "make ${library}" in ${code}
+ failonerror="true">
@@ -233,7 +233,7 @@
+ failonerror="true">
@@ -250,7 +250,7 @@
+ failonerror="true">
@@ -286,12 +286,35 @@
+
+
+ Running CI tests
+ test_classes: ${test_classes}
+ java.library.path: ${java.library.path}
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/scripts/ci-build-test-unix.sh b/scripts/ci-build-test-unix.sh
new file mode 100644
index 0000000..393de65
--- /dev/null
+++ b/scripts/ci-build-test-unix.sh
@@ -0,0 +1,58 @@
+#!/usr/bin/env bash
+
+set -euo pipefail
+
+REPO_ROOT="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)"
+YICES_SRC="${YICES_SRC:?set YICES_SRC}"
+YICES_PREFIX="${YICES_PREFIX:?set YICES_PREFIX}"
+
+configure_brew_env() {
+ if [[ "$(uname)" != "Darwin" ]]; then
+ return
+ fi
+
+ local brew_prefix
+ if [[ -d /opt/homebrew ]]; then
+ brew_prefix=/opt/homebrew
+ else
+ brew_prefix=/usr/local
+ fi
+
+ export CPPFLAGS="-I${brew_prefix}/include ${CPPFLAGS:-}"
+ export LDFLAGS="-L${brew_prefix}/lib ${LDFLAGS:-}"
+ export PKG_CONFIG_PATH="${brew_prefix}/lib/pkgconfig${PKG_CONFIG_PATH:+:${PKG_CONFIG_PATH}}"
+ export DYLD_LIBRARY_PATH="${brew_prefix}/lib${DYLD_LIBRARY_PATH:+:${DYLD_LIBRARY_PATH}}"
+}
+
+build_yices() {
+ rm -rf "${YICES_PREFIX}"
+ mkdir -p "${YICES_PREFIX}"
+ pushd "${YICES_SRC}" >/dev/null
+ autoconf
+ ./configure --prefix="${YICES_PREFIX}" --enable-thread-safety --disable-mcsat
+ make MODE=release
+ make MODE=release install
+ popd >/dev/null
+}
+
+run_java_ci() {
+ export CPPFLAGS="-I${YICES_PREFIX}/include ${CPPFLAGS:-}"
+ export LDFLAGS="-L${YICES_PREFIX}/lib ${LDFLAGS:-}"
+
+ if [[ "$(uname)" == "Darwin" ]]; then
+ export DYLD_LIBRARY_PATH="${YICES_PREFIX}/lib${DYLD_LIBRARY_PATH:+:${DYLD_LIBRARY_PATH}}"
+ else
+ export LD_LIBRARY_PATH="${YICES_PREFIX}/lib${LD_LIBRARY_PATH:+:${LD_LIBRARY_PATH}}"
+ fi
+
+ export YICES_JNI="${REPO_ROOT}/dist/lib"
+ export YICES_CLASSPATH="${REPO_ROOT}/build/classes"
+
+ pushd "${REPO_ROOT}" >/dev/null
+ ant clean ci-test
+ popd >/dev/null
+}
+
+configure_brew_env
+build_yices
+run_java_ci
diff --git a/scripts/ci-build-test-windows.sh b/scripts/ci-build-test-windows.sh
new file mode 100644
index 0000000..122ab20
--- /dev/null
+++ b/scripts/ci-build-test-windows.sh
@@ -0,0 +1,155 @@
+#!/usr/bin/env bash
+
+set -euo pipefail
+
+REPO_ROOT="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)"
+YICES_SRC="$(cygpath -u "${YICES_SRC:?set YICES_SRC}")"
+YICES_PREFIX="${YICES_PREFIX:?set YICES_PREFIX}"
+JAVA_HOME_UNIX="$(cygpath -u "${JAVA_HOME:?set JAVA_HOME}")"
+JAVAC="${JAVA_HOME_UNIX}/bin/javac"
+JAVA="${JAVA_HOME_UNIX}/bin/java"
+JAR="${JAVA_HOME_UNIX}/bin/jar"
+
+win_path() {
+ cygpath -w "$1"
+}
+
+win_path_list() {
+ cygpath -wp "$1"
+}
+
+build_gmp() {
+ mkdir -p /tools/dynamic_gmp /tools/static_gmp
+ pushd /tools >/dev/null
+
+ local archive=gmp-6.3.0.tar.xz
+ if [[ ! -f "${archive}" ]]; then
+ curl -fL --retry 5 --retry-delay 2 --connect-timeout 20 --max-time 600 \
+ https://ftp.gnu.org/gnu/gmp/${archive} -o "${archive}" || \
+ wget --tries=5 --timeout=20 -O "${archive}" https://ftp.gnu.org/gnu/gmp/${archive} || \
+ curl -fL --retry 5 --retry-delay 2 --connect-timeout 20 --max-time 600 \
+ https://mirrors.kernel.org/gnu/gmp/${archive} -o "${archive}" || \
+ wget --tries=5 --timeout=20 -O "${archive}" https://mirrors.kernel.org/gnu/gmp/${archive} || \
+ curl -fL --retry 5 --retry-delay 2 --connect-timeout 20 --max-time 600 \
+ https://gmplib.org/download/gmp/${archive} -o "${archive}" || \
+ wget --tries=5 --timeout=20 -O "${archive}" https://gmplib.org/download/gmp/${archive}
+ fi
+
+ rm -rf gmp-6.3.0
+ tar xf "${archive}"
+ cd gmp-6.3.0
+ ./configure --host=x86_64-w64-mingw32 --build=i686-pc-cygwin --enable-cxx --enable-shared --disable-static --prefix=/tools/dynamic_gmp
+ make
+ make install
+ make clean
+ ./configure --host=x86_64-w64-mingw32 --build=i686-pc-cygwin --enable-cxx --enable-static --disable-shared --prefix=/tools/static_gmp
+ make
+ make install
+
+ popd >/dev/null
+}
+
+build_yices() {
+ pushd "${YICES_SRC}" >/dev/null
+ autoconf
+ ./configure \
+ --host=x86_64-w64-mingw32 \
+ --enable-thread-safety \
+ CPPFLAGS="-I/tools/dynamic_gmp/include" \
+ LDFLAGS="-L/tools/dynamic_gmp/lib" \
+ --with-static-gmp=/tools/static_gmp/lib/libgmp.a \
+ --with-static-gmp-include-dir=/tools/static_gmp/include
+ export LD_LIBRARY_PATH="/usr/local/lib/:${LD_LIBRARY_PATH:-}"
+ make OPTION=mingw64 MODE=release dist
+
+ local dist_dir
+ dist_dir="$(find build -type d -name dist | head -n 1)"
+ if [[ -z "${dist_dir}" ]]; then
+ echo "failed to locate Yices dist directory" >&2
+ exit 1
+ fi
+
+ rm -rf "${YICES_PREFIX}"
+ mkdir -p "${YICES_PREFIX}"
+ cp -R "${dist_dir}/." "${YICES_PREFIX}/"
+ popd >/dev/null
+}
+
+build_java_bindings() {
+ mkdir -p "${REPO_ROOT}/build/classes" "${REPO_ROOT}/build/test_classes" "${REPO_ROOT}/dist/lib"
+
+ pushd "${REPO_ROOT}" >/dev/null
+ find src/main/java/com/sri/yices -name '*.java' | sort > build/main-sources.txt
+ "${JAVAC}" \
+ -d "$(win_path "${REPO_ROOT}/build/classes")" \
+ -h "$(win_path "${REPO_ROOT}/src/main/java/com/sri/yices")" \
+ @"build/main-sources.txt"
+
+ x86_64-w64-mingw32-g++ \
+ -I "${JAVA_HOME_UNIX}/include" \
+ -I "${JAVA_HOME_UNIX}/include/win32" \
+ -I "${YICES_PREFIX}/include" \
+ -I /tools/dynamic_gmp/include \
+ -g -Wall -fpermissive \
+ -c src/main/java/com/sri/yices/yicesJNIforWindows.cpp \
+ -o build/yicesJNIforWindows.o
+
+ x86_64-w64-mingw32-g++ \
+ -shared \
+ -o dist/lib/yices2java.dll \
+ build/yicesJNIforWindows.o \
+ -L "${YICES_PREFIX}/lib" \
+ -L /tools/dynamic_gmp/lib \
+ -lyices -lgmp
+
+ "${JAR}" -cvfm \
+ "$(win_path "${REPO_ROOT}/dist/lib/yices.jar")" \
+ "$(win_path "${REPO_ROOT}/MANIFEST.txt")" \
+ -C "$(win_path "${REPO_ROOT}/build/classes")" .
+ popd >/dev/null
+}
+
+stage_runtime_dlls() {
+ cp "${YICES_PREFIX}/bin/libyices.dll" "${REPO_ROOT}/dist/lib/"
+ cp /tools/dynamic_gmp/bin/libgmp-10.dll "${REPO_ROOT}/dist/lib/"
+ cp /usr/x86_64-w64-mingw32/sys-root/mingw/bin/libstdc++-6.dll "${REPO_ROOT}/dist/lib/"
+ cp /usr/x86_64-w64-mingw32/sys-root/mingw/bin/libgcc_s_seh-1.dll "${REPO_ROOT}/dist/lib/"
+ cp /usr/x86_64-w64-mingw32/sys-root/mingw/bin/libwinpthread-1.dll "${REPO_ROOT}/dist/lib/"
+}
+
+run_tests() {
+ pushd "${REPO_ROOT}" >/dev/null
+ find src/test/java -name '*.java' | sort > build/test-sources.txt
+
+ local compile_cp
+ compile_cp="$(win_path_list "${REPO_ROOT}/dist/lib/yices.jar:${REPO_ROOT}/lib/junit-4.12.jar:${REPO_ROOT}/lib/hamcrest-core-1.3.jar")"
+ "${JAVAC}" \
+ -cp "${compile_cp}" \
+ -d "$(win_path "${REPO_ROOT}/build/test_classes")" \
+ @"build/test-sources.txt"
+
+ local runtime_cp runtime_path
+ runtime_cp="$(win_path_list "${REPO_ROOT}/build/test_classes:${REPO_ROOT}/dist/lib/yices.jar:${REPO_ROOT}/lib/junit-4.12.jar:${REPO_ROOT}/lib/hamcrest-core-1.3.jar")"
+ runtime_path="$(win_path_list "${REPO_ROOT}/dist/lib:/tools/dynamic_gmp/bin:/usr/x86_64-w64-mingw32/sys-root/mingw/bin")"
+
+ env PATH="${runtime_path}" \
+ "${JAVA}" \
+ "-Djava.library.path=$(win_path "${REPO_ROOT}/dist/lib")" \
+ -cp "${runtime_cp}" \
+ org.junit.runner.JUnitCore \
+ com.sri.yices.TestBigRationals \
+ com.sri.yices.TestConstructor \
+ com.sri.yices.TestContext \
+ com.sri.yices.TestStatus \
+ com.sri.yices.TestTypes \
+ com.sri.yices.TestYices \
+ com.sri.yices.TestModels \
+ com.sri.yices.TestTermComponents
+ popd >/dev/null
+}
+
+build_gmp
+build_yices
+build_java_bindings
+stage_runtime_dlls
+run_tests
diff --git a/src/main/java/com/sri/yices/Constructor.java b/src/main/java/com/sri/yices/Constructor.java
index 665436b..0eaa7ff 100644
--- a/src/main/java/com/sri/yices/Constructor.java
+++ b/src/main/java/com/sri/yices/Constructor.java
@@ -11,64 +11,66 @@ public enum Constructor {
// atomic terms
BOOL_CONSTANT(0), // boolean constant
ARITH_CONSTANT(1), // rational constant
- BV_CONSTANT(2), // bitvector constant
- SCALAR_CONSTANT(3), // constant of uninterpreted or scalar type
- VARIABLE(4), // variable in quantifiers
- UNINTERPRETED_TERM(5), // (i.e., global variables, can't be bound)
+ FF_CONSTANT(2), // finite field constant
+ BV_CONSTANT(3), // bitvector constant
+ SCALAR_CONSTANT(4), // constant of uninterpreted or scalar type
+ VARIABLE(5), // variable in quantifiers
+ UNINTERPRETED_TERM(6), // (i.e., global variables, can't be bound)
// composite terms
- ITE_TERM(6), // if-then-else
- APP_TERM(7), // application of an uninterpreted function
- UPDATE_TERM(8), // function update
- TUPLE_TERM(9), // tuple constructor
- EQ_TERM(10), // equality
- DISTINCT_TERM(11), // distinct t_1 ... t_n
- FORALL_TERM(12), // quantifier
- LAMBDA_TERM(13), // lambda
- NOT_TERM(14), // (not t)
- OR_TERM(15), // n-ary OR
- XOR_TERM(16), // n-ary XOR
+ ITE_TERM(7), // if-then-else
+ APP_TERM(8), // application of an uninterpreted function
+ UPDATE_TERM(9), // function update
+ TUPLE_TERM(10), // tuple constructor
+ EQ_TERM(11), // equality
+ DISTINCT_TERM(12), // distinct t_1 ... t_n
+ FORALL_TERM(13), // quantifier
+ LAMBDA_TERM(14), // lambda
+ NOT_TERM(15), // (not t)
+ OR_TERM(16), // n-ary OR
+ XOR_TERM(17), // n-ary XOR
- BV_ARRAY(17), // array of boolean terms
- BV_DIV(18), // unsigned division
- BV_REM(19), // unsigned remainder
- BV_SDIV(20), // signed division
- BV_SREM(21), // remainder in signed division (rounding to 0)
- BV_SMOD(22), // remainder in signed division (rounding to -infinity)
- BV_SHL(23), // shift left (padding with 0)
- BV_LSHR(24), // logical shift right (padding with 0)
- BV_ASHR(25), // arithmetic shift right (padding with sign bit)
- BV_GE_ATOM(26), // unsigned comparison: (t1 >= t2)
- BV_SGE_ATOM(27), // signed comparison (t1 >= t2)
- ARITH_GE_ATOM(28), // atom (t1 >= t2) for arithmetic terms: t2 is always 0
- ARITH_ROOT_ATOM(29), // atom (0 <= k <= root_count(p)) && (x r root(p, k)) for r in <, <=, ==, !=, >, >=
+ BV_ARRAY(18), // array of boolean terms
+ BV_DIV(19), // unsigned division
+ BV_REM(20), // unsigned remainder
+ BV_SDIV(21), // signed division
+ BV_SREM(22), // remainder in signed division (rounding to 0)
+ BV_SMOD(23), // remainder in signed division (rounding to -infinity)
+ BV_SHL(24), // shift left (padding with 0)
+ BV_LSHR(25), // logical shift right (padding with 0)
+ BV_ASHR(26), // arithmetic shift right (padding with sign bit)
+ BV_GE_ATOM(27), // unsigned comparison: (t1 >= t2)
+ BV_SGE_ATOM(28), // signed comparison (t1 >= t2)
+ ARITH_GE_ATOM(29), // atom (t1 >= t2) for arithmetic terms: t2 is always 0
+ ARITH_ROOT_ATOM(30), // atom (0 <= k <= root_count(p)) && (x r root(p, k)) for r in <, <=, ==, !=, >, >=
- ABS(30), // absolute value
- CEIL(31), // ceil
- FLOOR(32), // floor
- RDIV(33), // real division (as in x/y)
- IDIV(34), // integer division
- IMOD(35), // modulo
- IS_INT_ATOM(36), // integrality test: (is-int t)
- DIVIDES_ATOM(37), // divisibility test: (divides t1 t2)
+ ABS(31), // absolute value
+ CEIL(32), // ceil
+ FLOOR(33), // floor
+ RDIV(34), // real division (as in x/y)
+ IDIV(35), // integer division
+ IMOD(36), // modulo
+ IS_INT_ATOM(37), // integrality test: (is-int t)
+ DIVIDES_ATOM(38), // divisibility test: (divides t1 t2)
// projections
- SELECT_TERM(38), // tuple projection
- BIT_TERM(39), // bit-select: extract the i-th bit of a bitvector
+ SELECT_TERM(39), // tuple projection
+ BIT_TERM(40), // bit-select: extract the i-th bit of a bitvector
// sums
- BV_SUM(40), // sum of pairs a * t where a is a bitvector constant (and t is a bitvector term)
- ARITH_SUM(41), // sum of pairs a * t where a is a rational (and t is an arithmetic term)
+ BV_SUM(41), // sum of pairs a * t where a is a bitvector constant (and t is a bitvector term)
+ ARITH_SUM(42), // sum of pairs a * t where a is a rational (and t is an arithmetic term)
+ FF_SUM(43), // sum of pairs a * t where a is a finite-field constant (and t is a finite-field term)
// products
- POWER_PRODUCT(42) // power products: (t1^d1 * ... * t_n^d_n)
+ POWER_PRODUCT(44) // power products: (t1^d1 * ... * t_n^d_n)
;
private int index;
Constructor(int id) { this.index = id; }
public int getIndex() { return index; }
- public static final int NUM_CONSTRUCTORS = 43;
+ public static final int NUM_CONSTRUCTORS = 45;
private static final Constructor[] table;
static {
diff --git a/src/main/java/com/sri/yices/Context.java b/src/main/java/com/sri/yices/Context.java
index 53ac5b6..6803df5 100644
--- a/src/main/java/com/sri/yices/Context.java
+++ b/src/main/java/com/sri/yices/Context.java
@@ -331,7 +331,7 @@ public int getModelInterpolant() {
// Since 2.6.4
public Status checkWithAssumptions(Parameters params, int[] assumptions) {
- int code = Yices.checkContextWithAssumptions(ptr, params.getPtr(), assumptions);
+ int code = Yices.checkContextWithAssumptions(ptr, params == null ? 0 : params.getPtr(), assumptions);
if (code < 0) {
throw new YicesException();
}
@@ -340,7 +340,7 @@ public Status checkWithAssumptions(Parameters params, int[] assumptions) {
// Since 2.6.4
public Status checkWithModel(Parameters params, Model model, int[] assumptions) {
- int code = Yices.checkContextWithModel(ptr, params.getPtr(), model.getPtr(), assumptions);
+ int code = Yices.checkContextWithModel(ptr, params == null ? 0 : params.getPtr(), model.getPtr(), assumptions);
if (code < 0) {
YicesException error = YicesException.checkVersion(2, 6, 4);
if (error == null) {
diff --git a/src/main/java/com/sri/yices/Makefile b/src/main/java/com/sri/yices/Makefile
index 158571b..88eaff0 100644
--- a/src/main/java/com/sri/yices/Makefile
+++ b/src/main/java/com/sri/yices/Makefile
@@ -56,9 +56,15 @@ libyices2java_install_name := $(YICES_JNI)/libyices2java.dylib
# 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 $(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)
CXX ?= g++
@@ -77,16 +83,16 @@ $(YICES_CLASSPATH)/com/sri/yices/%.class: %.java
$(JAVAC) -d $(YICES_CLASSPATH) *.java
com_sri_yices_Yices.h: $(YICES_CLASSPATH)/com/sri/yices/Yices.class
- $(JAVAC) -h . *.java
+ $(JAVAC) -d $(YICES_CLASSPATH) -h . *.java
yicesJNI.o: yicesJNI.cpp com_sri_yices_Yices.h
$(CXX) $(CPPFLAGS) $(CXXFLAGS) -Wall -c yicesJNI.cpp
libyices2java.dylib: yicesJNI.o
- $(CXX) $(CPPFLAGS) $(CXXFLAGS) -dynamiclib -o $@ yicesJNI.o $(LIBS)
+ $(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)
LIBDIR := $(YICES_JNI)
diff --git a/src/main/java/com/sri/yices/YValTag.java b/src/main/java/com/sri/yices/YValTag.java
index eb43561..a960762 100644
--- a/src/main/java/com/sri/yices/YValTag.java
+++ b/src/main/java/com/sri/yices/YValTag.java
@@ -13,6 +13,7 @@ public enum YValTag {
BOOL,
RATIONAL,
ALGEBRAIC,
+ FINITEFIELD,
BV,
SCALAR,
TUPLE,
diff --git a/src/main/java/com/sri/yices/yicesJNI.cpp b/src/main/java/com/sri/yices/yicesJNI.cpp
index 27290e2..abb7c96 100644
--- a/src/main/java/com/sri/yices/yicesJNI.cpp
+++ b/src/main/java/com/sri/yices/yicesJNI.cpp
@@ -2674,7 +2674,7 @@ JNIEXPORT jbooleanArray JNICALL Java_com_sri_yices_Yices_bvConstValue(JNIEnv *en
assert(code >= 0);
result = convertToBoolArray(env, n, tmp);
delete [] tmp;
- } catch (std::bad_alloc) {
+ } catch (std::bad_alloc&) {
out_of_mem_exception(env);
}
}
@@ -3215,10 +3215,10 @@ JNIEXPORT jint JNICALL Java_com_sri_yices_Yices_checkContextWithInterpolation(JN
ctx.model = NULL;
try {
result = yices_check_context_with_interpolation(&ctx, reinterpret_cast(params), build_model);
- if (result == STATUS_UNSAT) {
+ if (result == YICES_STATUS_UNSAT) {
// set the interpolant array
env->SetIntArrayRegion(interpolant, 0, 1, &ctx.interpolant);
- } else if(build_model && result == STATUS_SAT ) {
+ } else if(build_model && result == YICES_STATUS_SAT ) {
model_t *model = ctx.model;
jlong mdl = reinterpret_cast(model);
// set the model array
@@ -3817,7 +3817,7 @@ JNIEXPORT jint JNICALL Java_com_sri_yices_Yices_checkFormula(JNIEnv *env, jclass
}
if (wantModel) {
code = yices_check_formula(formula, ls, &model, ds);
- if (code == STATUS_SAT) {
+ if (code == YICES_STATUS_SAT) {
mdl = reinterpret_cast(model);
env->SetLongArrayRegion(marr, 0, 1, &mdl);
}
@@ -3873,7 +3873,7 @@ JNIEXPORT jint JNICALL Java_com_sri_yices_Yices_checkFormulas(JNIEnv *env, jclas
}
if (wantModel) {
code = yices_check_formulas(tarr, n, ls, &model, ds);
- if (code == STATUS_SAT) {
+ if (code == YICES_STATUS_SAT) {
mdl = reinterpret_cast(model);
env->SetLongArrayRegion(marr, 0, 1, &mdl);
}
diff --git a/src/main/java/com/sri/yices/yicesJNIforWindows.cpp b/src/main/java/com/sri/yices/yicesJNIforWindows.cpp
index 380ff36..0f81cf4 100755
--- a/src/main/java/com/sri/yices/yicesJNIforWindows.cpp
+++ b/src/main/java/com/sri/yices/yicesJNIforWindows.cpp
@@ -21,7 +21,23 @@
#define YICES_AT_LEAST_2_6_2
#endif
+#if __YICES_VERSION > 2 || \
+ (__YICES_VERSION == 2 && (__YICES_VERSION_MAJOR > 6 || \
+ (__YICES_VERSION_MAJOR == 6 && \
+ __YICES_VERSION_PATCHLEVEL > 3)))
+#define YICES_AT_LEAST_2_6_4
+#endif
+
#define YICES_ERROR_REQUIRES_AT_LEAST_2_6_2 -262
+#define YICES_ERROR_REQUIRES_AT_LEAST_2_6_4 -264
+
+/**
+ * Assumes that for each __YICES_VERSION __YICES_VERSION_MAJOR and __YICES_VERSION_PATCHLEVEL
+ * are between 0 and less than 100.
+ */
+JNIEXPORT jlong JNICALL Java_com_sri_yices_Yices_versionOrdinal(JNIEnv *env, jclass){
+ return (10000 * __YICES_VERSION) + (100 * __YICES_VERSION_MAJOR) + __YICES_VERSION_PATCHLEVEL;
+}
/*
@@ -645,6 +661,24 @@ JNIEXPORT void JNICALL Java_com_sri_yices_Yices_resetError(JNIEnv *, jclass) {
yices_clear_error();
}
+JNIEXPORT jobject JNICALL Java_com_sri_yices_Yices_errorReport(JNIEnv *env, jclass) {
+ try {
+ error_report_t* report = yices_error_report();
+ // now construct new ErrorReport(report->code, report->line, report->column, report->term1, report->type1, report->term2, report->type2, report->badval);
+ jclass cls = env->FindClass("com/sri/yices/ErrorReport");
+ if (cls != NULL) {
+ jmethodID constructor = env->GetMethodID(cls, "", "(IIIIIIIJ)V");
+ if (constructor != NULL) {
+ jobject object = env->NewObject(cls, constructor, report->code, report->line, report->column, report->term1, report->type1, report->term2, report->type2, report->badval);
+ return object;
+ }
+ }
+ } catch (std::bad_alloc &ba) {
+ out_of_mem_exception(env);
+ }
+ return 0;
+}
+
// to test the throw exception code
JNIEXPORT void JNICALL Java_com_sri_yices_Yices_testException(JNIEnv *env, jclass) {
@@ -2640,8 +2674,8 @@ JNIEXPORT jbooleanArray JNICALL Java_com_sri_yices_Yices_bvConstValue(JNIEnv *en
assert(code >= 0);
result = convertToBoolArray(env, n, tmp);
delete [] tmp;
- } catch (std::bad_alloc) {
- out_of_mem_exception(env);
+ } catch (std::bad_alloc&) {
+ out_of_mem_exception(env);
}
}
}
@@ -3125,6 +3159,78 @@ JNIEXPORT jint JNICALL Java_com_sri_yices_Yices_checkContext(JNIEnv *env, jclass
return result;
}
+//Since 2.?.? (new in the 2.6.4 bindings)
+JNIEXPORT jint JNICALL Java_com_sri_yices_Yices_checkContextWithAssumptions(JNIEnv *env, jclass, jlong ctx, jlong params, jintArray t) {
+ jsize n = env->GetArrayLength(t);
+ term_t *a = array2terms(env, t, NULL);
+ jint result = -1;
+ if (a == NULL) {
+ out_of_mem_exception(env);
+ } else {
+ try {
+ result = yices_check_context_with_assumptions(reinterpret_cast(ctx), reinterpret_cast(params), n, a);
+ } catch (std::bad_alloc &ba) {
+ out_of_mem_exception(env);
+ }
+ }
+ return result;
+}
+
+// since 2.6.4
+JNIEXPORT jint JNICALL Java_com_sri_yices_Yices_checkContextWithModel(JNIEnv *env, jclass, jlong ctx, jlong params, jlong model, jintArray t){
+#ifdef YICES_AT_LEAST_2_6_4
+ jint result = -1;
+ jsize n = env->GetArrayLength(t);
+ term_t *a = array2terms(env, t, NULL);
+ if (a == NULL) {
+ out_of_mem_exception(env);
+ } else {
+ try {
+ result = yices_check_context_with_model(reinterpret_cast(ctx), reinterpret_cast(params), reinterpret_cast(model), n, a);
+ } catch (std::bad_alloc &ba) {
+ out_of_mem_exception(env);
+ }
+ }
+ return result;
+#else
+ return -1;
+#endif
+}
+
+// since 2.6.4
+JNIEXPORT jint JNICALL Java_com_sri_yices_Yices_checkContextWithInterpolation(JNIEnv *env, jclass, jlong ctxA, jlong ctxB, jlong params, jlongArray marr, jintArray interpolant){
+#ifdef YICES_AT_LEAST_2_6_4
+ jint result = -1;
+ jsize i = (interpolant == 0 ? 0 : env->GetArrayLength(interpolant));
+ if (i < 1) {
+ return result;
+ }
+
+ jsize n = (marr == 0 ? 0 : env->GetArrayLength(marr));
+ int32_t build_model = (n > 0);
+ interpolation_context_t ctx;
+ ctx.ctx_A = reinterpret_cast(ctxA);
+ ctx.ctx_B = reinterpret_cast(ctxB);
+ ctx.interpolant = 0;
+ ctx.model = NULL;
+ try {
+ result = yices_check_context_with_interpolation(&ctx, reinterpret_cast(params), build_model);
+ if (result == YICES_STATUS_UNSAT) {
+ env->SetIntArrayRegion(interpolant, 0, 1, &ctx.interpolant);
+ } else if(build_model && result == YICES_STATUS_SAT ) {
+ model_t *model = ctx.model;
+ jlong mdl = reinterpret_cast(model);
+ env->SetLongArrayRegion(marr, 0, 1, &mdl);
+ }
+ } catch (std::bad_alloc &ba) {
+ out_of_mem_exception(env);
+ }
+ return result;
+#else
+ return -1;
+#endif
+}
+
JNIEXPORT jint JNICALL Java_com_sri_yices_Yices_assertBlockingClause(JNIEnv *env, jclass, jlong ctx) {
jint result = -1;
@@ -3175,6 +3281,39 @@ JNIEXPORT void JNICALL Java_com_sri_yices_Yices_freeParamRecord(JNIEnv *env, jcl
yices_free_param_record(reinterpret_cast(param));
}
+// since 2.?.? (new in the 2.6.4 bindings)
+JNIEXPORT jintArray JNICALL Java_com_sri_yices_Yices_getUnsatCore(JNIEnv *env, jclass, jlong ctx) {
+ jintArray retval = NULL;
+ int32_t code;
+ term_vector_t aux;
+ try {
+ yices_init_term_vector(&aux);
+ code = yices_get_unsat_core(reinterpret_cast(ctx), &aux);
+ if (code >= 0) {
+ retval = convertToIntArray(env, aux.size, aux.data);
+ }
+ yices_delete_term_vector(&aux);
+ } catch (std::bad_alloc &ba) {
+ out_of_mem_exception(env);
+ }
+ return retval;
+}
+
+// since 2.6.4
+JNIEXPORT jint JNICALL Java_com_sri_yices_Yices_getModelInterpolant(JNIEnv *env, jclass, jlong ctx) {
+#ifdef YICES_AT_LEAST_2_6_4
+ jint result = -1;
+ try {
+ result = yices_get_model_interpolant(reinterpret_cast(ctx));
+ } catch (std::bad_alloc &ba) {
+ out_of_mem_exception(env);
+ }
+ return result;
+#else
+ return -1;
+#endif
+}
+
/*
* MODELS
@@ -3190,6 +3329,21 @@ JNIEXPORT jlong JNICALL Java_com_sri_yices_Yices_getModel(JNIEnv *env, jclass, j
return result;
}
+// since 2.6.4
+JNIEXPORT jlong JNICALL Java_com_sri_yices_Yices_newModel(JNIEnv *env, jclass){
+#ifdef YICES_AT_LEAST_2_6_4
+ jlong result = 0; // NULL pointer
+ try {
+ result = reinterpret_cast(yices_new_model());
+ } catch (std::bad_alloc &ba) {
+ out_of_mem_exception(env);
+ }
+ return result;
+#else
+ return NULL;
+#endif
+}
+
JNIEXPORT void JNICALL Java_com_sri_yices_Yices_freeModel(JNIEnv *env, jclass, jlong model) {
yices_free_model(reinterpret_cast(model));
}
@@ -3219,6 +3373,103 @@ JNIEXPORT jlong JNICALL Java_com_sri_yices_Yices_modelFromMap(JNIEnv *env, jclas
return result;
}
+// Since 2.6.4
+JNIEXPORT jint JNICALL Java_com_sri_yices_Yices_modelSetBool(JNIEnv *env, jclass, jlong model, jint var, jint val) {
+#ifdef YICES_AT_LEAST_2_6_4
+ jint result = -1;
+ try {
+ result = yices_model_set_bool(reinterpret_cast(model), reinterpret_cast(var), reinterpret_cast(val));
+ } catch (std::bad_alloc &ba) {
+ out_of_mem_exception(env);
+ }
+ return result;
+#else
+ return -1;
+#endif
+}
+
+// Since 2.6.4
+JNIEXPORT jint JNICALL Java_com_sri_yices_Yices_modelSetInteger(JNIEnv *env, jclass, jlong model, jint var, jlong val){
+#ifdef YICES_AT_LEAST_2_6_4
+ jint result = -1;
+ try {
+ result = yices_model_set_int64(reinterpret_cast(model), reinterpret_cast(var), val);
+ } catch (std::bad_alloc &ba) {
+ out_of_mem_exception(env);
+ }
+ return result;
+#else
+ return -1;
+#endif
+}
+
+// Since 2.6.4
+JNIEXPORT jint JNICALL Java_com_sri_yices_Yices_modelSetRational(JNIEnv *env, jclass, jlong model, jint var, jlong num, jlong den) {
+#ifdef YICES_AT_LEAST_2_6_4
+ jint result = -1;
+ try {
+ result = yices_model_set_rational64(reinterpret_cast(model), reinterpret_cast(var), num, den);
+ } catch (std::bad_alloc &ba) {
+ out_of_mem_exception(env);
+ }
+ return result;
+#else
+ return -1;
+#endif
+}
+
+// Since 2.6.4
+JNIEXPORT jint JNICALL Java_com_sri_yices_Yices_modelSetBVInteger(JNIEnv *env, jclass, jlong model, jint var, jlong val) {
+#ifdef YICES_AT_LEAST_2_6_4
+ jint result = -1;
+ try {
+ result = yices_model_set_bv_uint64(reinterpret_cast(model), reinterpret_cast(var), val);
+ } catch (std::bad_alloc &ba) {
+ out_of_mem_exception(env);
+ }
+ return result;
+#else
+ return -1;
+#endif
+}
+
+// Since 2.6.4
+JNIEXPORT jint JNICALL Java_com_sri_yices_Yices_modelSetBVFromArray(JNIEnv *env, jclass, jlong model, jint var, jintArray arr) {
+#ifdef YICES_AT_LEAST_2_6_4
+ jint result = -1;
+ jsize n = env->GetArrayLength(arr);
+ if (n == 0) {
+ return result;
+ }
+ assert(n > 0);
+ int32_t *vals = array2int32(env, arr, NULL);
+ try {
+ result = yices_model_set_bv_from_array(reinterpret_cast(model), reinterpret_cast(var), n, vals);
+ } catch (std::bad_alloc &ba) {
+ out_of_mem_exception(env);
+ }
+ release_int32_elems(env, arr, vals);
+ return result;
+#else
+ return -1;
+#endif
+}
+
+// since 2.?.? (new in 2.6.4 bindings)
+JNIEXPORT jintArray JNICALL Java_com_sri_yices_Yices_modelCollectDefinedTerms(JNIEnv *env, jclass, jlong model) {
+ term_vector_t aux;
+ jintArray result = NULL;
+ try {
+ yices_init_term_vector(&aux);
+ yices_model_collect_defined_terms(reinterpret_cast(model), &aux);
+ result = convertToIntArray(env, aux.size, aux.data);
+ yices_delete_term_vector(&aux);
+ } catch (std::bad_alloc &ba) {
+ out_of_mem_exception(env);
+ }
+ return result;
+}
+
// returns -1 for error, 0 for false, +1 for true
JNIEXPORT jint JNICALL Java_com_sri_yices_Yices_getBoolValue(JNIEnv *env, jclass, jlong model, jint t) {
int32_t val = -1;
@@ -3557,7 +3808,7 @@ JNIEXPORT jint JNICALL Java_com_sri_yices_Yices_checkFormula(JNIEnv *env, jclass
}
if (wantModel) {
code = yices_check_formula(formula, ls, &model, ds);
- if (code == STATUS_SAT) {
+ if (code == YICES_STATUS_SAT) {
mdl = reinterpret_cast(model);
env->SetLongArrayRegion(marr, 0, 1, &mdl);
}
@@ -3613,7 +3864,7 @@ JNIEXPORT jint JNICALL Java_com_sri_yices_Yices_checkFormulas(JNIEnv *env, jclas
}
if (wantModel) {
code = yices_check_formulas(tarr, n, ls, &model, ds);
- if (code == STATUS_SAT) {
+ if (code == YICES_STATUS_SAT) {
mdl = reinterpret_cast(model);
env->SetLongArrayRegion(marr, 0, 1, &mdl);
}
diff --git a/src/test/java/com/sri/yices/TestTermComponents.java b/src/test/java/com/sri/yices/TestTermComponents.java
new file mode 100644
index 0000000..7329fba
--- /dev/null
+++ b/src/test/java/com/sri/yices/TestTermComponents.java
@@ -0,0 +1,132 @@
+package com.sri.yices;
+
+import org.junit.Assert;
+import org.junit.Test;
+
+import java.lang.reflect.InvocationTargetException;
+import java.lang.reflect.Method;
+import java.math.BigInteger;
+import java.util.HashMap;
+import java.util.Map;
+
+import static org.junit.Assume.assumeTrue;
+
+public class TestTermComponents {
+ @Test
+ public void testProjectedComponentsWhenAvailable() throws Exception {
+ assumeTrue(TestAssumptions.IS_YICES_INSTALLED);
+
+ Method sumComponent = optionalMethod("sumComponent");
+ Method productComponent = optionalMethod("productComponent");
+ if (sumComponent == null || productComponent == null) {
+ return;
+ }
+
+ int x = Terms.newUninterpretedTerm("term_components_x", Types.INT);
+ int y = Terms.newUninterpretedTerm("term_components_y", Types.INT);
+ int bvType = Types.bvType(8);
+ int bx = Terms.newUninterpretedTerm("term_components_bx", bvType);
+ int by = Terms.newUninterpretedTerm("term_components_by", bvType);
+
+ try {
+ int arith = Terms.rationalPoly(new long[] { 3, -5 }, new long[] { 2, 1 }, new int[] { x, y });
+ Assert.assertTrue(Terms.isSum(arith));
+
+ Map arithComponents = collectSumComponents(sumComponent, arith);
+ Assert.assertEquals(2, arithComponents.size());
+ Assert.assertEquals(new BigRational(BigInteger.valueOf(3), BigInteger.valueOf(2)), arithComponents.get(x));
+ Assert.assertEquals(new BigRational(BigInteger.valueOf(-5), BigInteger.ONE), arithComponents.get(y));
+
+ int bsum = Terms.bvAdd(
+ Terms.bvMul(Terms.bvConst(8, 3), bx),
+ Terms.bvMul(Terms.bvConst(8, 5), by));
+ Assert.assertTrue(Terms.isBvSum(bsum));
+
+ Map bvComponents = collectBvSumComponents(sumComponent, bsum);
+ Assert.assertEquals(2, bvComponents.size());
+ Assert.assertArrayEquals(Terms.bvConstValue(Terms.bvConst(8, 3)), bvComponents.get(bx));
+ Assert.assertArrayEquals(Terms.bvConstValue(Terms.bvConst(8, 5)), bvComponents.get(by));
+
+ int product = Terms.mul(Terms.power(x, 3), Terms.power(y, 2));
+ Assert.assertTrue(Terms.isProduct(product));
+
+ Map productComponents = collectProductComponents(productComponent, product);
+ Assert.assertEquals(2, productComponents.size());
+ Assert.assertEquals(Integer.valueOf(3), productComponents.get(x));
+ Assert.assertEquals(Integer.valueOf(2), productComponents.get(y));
+ } finally {
+ Terms.removeName("term_components_x");
+ Terms.removeName("term_components_y");
+ Terms.removeName("term_components_bx");
+ Terms.removeName("term_components_by");
+ }
+ }
+
+ private static Method optionalMethod(String name) {
+ try {
+ return Yices.class.getMethod(name, int.class, int.class);
+ } catch (NoSuchMethodException e) {
+ return null;
+ }
+ }
+
+ private static Map collectSumComponents(Method method, int term) throws Exception {
+ Map result = new HashMap<>();
+ for (int idx = 0; ; idx++) {
+ Object component = invoke(method, term, idx);
+ if (component == null) {
+ break;
+ }
+ int child = (Integer) component.getClass().getMethod("getTerm").invoke(component);
+ Object factor = component.getClass().getMethod("getFactor").invoke(component);
+ Assert.assertTrue(factor instanceof BigRational);
+ result.put(child, (BigRational) factor);
+ }
+ return result;
+ }
+
+ private static Map collectBvSumComponents(Method method, int term) throws Exception {
+ Map result = new HashMap<>();
+ for (int idx = 0; ; idx++) {
+ Object component = invoke(method, term, idx);
+ if (component == null) {
+ break;
+ }
+ int child = (Integer) component.getClass().getMethod("getTerm").invoke(component);
+ Object factor = component.getClass().getMethod("getFactor").invoke(component);
+ if (factor instanceof boolean[]) {
+ result.put(child, (boolean[]) factor);
+ }
+ }
+ return result;
+ }
+
+ private static Map collectProductComponents(Method method, int term) throws Exception {
+ Map result = new HashMap<>();
+ for (int idx = 0; ; idx++) {
+ Object component = invoke(method, term, idx);
+ if (component == null) {
+ break;
+ }
+ int child = (Integer) component.getClass().getMethod("getTerm").invoke(component);
+ int power = (Integer) component.getClass().getMethod("getPower").invoke(component);
+ result.put(child, power);
+ }
+ return result;
+ }
+
+ private static Object invoke(Method method, int term, int idx) throws Exception {
+ try {
+ return method.invoke(null, term, idx);
+ } catch (InvocationTargetException e) {
+ Throwable cause = e.getCause();
+ if (cause instanceof Error) {
+ throw (Error) cause;
+ }
+ if (cause instanceof Exception) {
+ throw (Exception) cause;
+ }
+ throw e;
+ }
+ }
+}
diff --git a/src/test/java/com/sri/yices/TestThreads.java b/src/test/java/com/sri/yices/TestThreads.java
index 217b7f8..26dc871 100644
--- a/src/test/java/com/sri/yices/TestThreads.java
+++ b/src/test/java/com/sri/yices/TestThreads.java
@@ -5,16 +5,18 @@
import static org.junit.Assume.assumeTrue;
+import java.util.concurrent.CountDownLatch;
+import java.util.concurrent.TimeUnit;
+import java.util.concurrent.atomic.AtomicReference;
+
public class TestThreads {
- public static final int THREAD_COUNT = 200;
+ public static final int THREAD_COUNT = Integer.getInteger("com.sri.yices.testThreads.count", 32);
+ public static final long THREAD_TIMEOUT_SECONDS = Long.getLong("com.sri.yices.testThreads.timeoutSeconds", 60L);
public static final String COUNTER_PREFIX = "c@";
public static final String CHOICE_PREFIX = "i@";
- private static final Object lock = new Object();
- private static int waiting = 0;
-
@Test
public void testVersion() {
assumeTrue(TestAssumptions.IS_YICES_INSTALLED);
@@ -43,16 +45,9 @@ private int makeConstraint(int index, int increment, int selector){
return Terms.and(selector, Terms.eq(t1, Terms.add(t2, Terms.intConst(increment))));
}
- private void threadMain(int index, Status[] answers){
-
- synchronized(lock){
- waiting++;
- try {
- lock.wait();
- } catch(InterruptedException e){
- System.err.println(e.getMessage());
- }
- }
+ private void threadMain(int index, Status[] answers, CountDownLatch readyGate, CountDownLatch startGate) throws InterruptedException {
+ readyGate.countDown();
+ Assert.assertTrue("timed out waiting to start worker threads", startGate.await(THREAD_TIMEOUT_SECONDS, TimeUnit.SECONDS));
try (Config cfg = new Config()) {
cfg.set("solver-type", "dpllt");
@@ -82,54 +77,63 @@ private void threadMain(int index, Status[] answers){
}
}
- private Thread makeThread(final int index, final Status[] answers){
+ private Thread makeThread(final int index, final Status[] answers, final CountDownLatch readyGate,
+ final CountDownLatch startGate, final AtomicReference failure){
Runnable runnable = new Runnable(){
public void run(){
- threadMain(index, answers);
+ try {
+ threadMain(index, answers, readyGate, startGate);
+ } catch (Throwable error) {
+ failure.compareAndSet(null, error);
+ }
}
};
- return new Thread(runnable);
+ Thread thread = new Thread(runnable, "yices-test-thread-" + index);
+ thread.setDaemon(true);
+ return thread;
}
- @Test
+ @Test(timeout = 120000)
public void testThreads() {
assumeTrue(TestAssumptions.IS_YICES_INSTALLED);
assumeTrue(Yices.isThreadSafe());
Thread[] threads = new Thread[THREAD_COUNT];
Status[] answers = new Status[THREAD_COUNT];
+ CountDownLatch readyGate = new CountDownLatch(THREAD_COUNT);
+ CountDownLatch startGate = new CountDownLatch(1);
+ AtomicReference failure = new AtomicReference();
for(int i = 0; i < THREAD_COUNT; i++){
- threads[i] = makeThread(i, answers);
+ threads[i] = makeThread(i, answers, readyGate, startGate, failure);
}
for(int i = 0; i < THREAD_COUNT; i++){
threads[i].start();
}
- Thread self = Thread.currentThread();
-
- while(true){
- synchronized(lock){
- if (waiting == THREAD_COUNT){
- lock.notifyAll();
- break;
- }
- }
- }
-
-
try {
+ Assert.assertTrue("timed out waiting for worker threads to become ready",
+ readyGate.await(THREAD_TIMEOUT_SECONDS, TimeUnit.SECONDS));
+ startGate.countDown();
for(int i = 0; i < THREAD_COUNT; i++){
- threads[i].join();
+ threads[i].join(TimeUnit.SECONDS.toMillis(THREAD_TIMEOUT_SECONDS));
+ Assert.assertFalse("worker thread did not finish: " + threads[i].getName(), threads[i].isAlive());
}
} catch (InterruptedException error){
- System.out.println(error.getMessage());
+ Thread.currentThread().interrupt();
+ Assert.fail(error.getMessage());
+ }
+
+ if (failure.get() != null) {
+ AssertionError error = new AssertionError("worker thread failed");
+ error.initCause(failure.get());
+ throw error;
}
for (int i = 0; i < THREAD_COUNT; i++){
- Assert.assertEquals(answers[i], Status.SAT);
+ Assert.assertEquals(Status.SAT, answers[i]);
}