From fb30e04dc74e76665090fe55dda24c8c8c91f7dc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ren=C3=A9=20Pascal=20Maseli?= Date: Tue, 24 Sep 2024 21:49:50 +0200 Subject: [PATCH 1/2] Add Yices2 for Mac OS --- lib/native/source/yices2j/compile.sh | 106 ++++++++----- lib/native/source/yices2j/includes/defines.h | 13 +- ...java_1smt_solvers_yices2_Yices2NativeApi.c | 144 ++++++++++++------ 3 files changed, 170 insertions(+), 93 deletions(-) diff --git a/lib/native/source/yices2j/compile.sh b/lib/native/source/yices2j/compile.sh index 58f2c52135..fe917205a9 100755 --- a/lib/native/source/yices2j/compile.sh +++ b/lib/native/source/yices2j/compile.sh @@ -34,41 +34,58 @@ cd ${DIR} JNI_HEADERS="$(../get_jni_headers.sh)" +add_include_lib() { + [ -d "$1" ] && CFLAGS="$CFLAGS -I$1" + [ -d "$2" ] && LDFLAGS="$LDFLAGS -L$2" +} RELATIVE_ROOT_DIR="../../../.." -YICES_SRC_DIR=$RELATIVE_ROOT_DIR/"$1"/src/include -YICES_LIB_DIR=$RELATIVE_ROOT_DIR/"$1"/build/x86_64-pc-linux-gnu-release/lib/ -GMP_HEADER_DIR=$RELATIVE_ROOT_DIR/"$2" -GMP_LIB_DIR=$GMP_HEADER_DIR/.libs -GPERF_HEADER_DIR=$RELATIVE_ROOT_DIR/"$3" -GPERF_LIB_DIR=$GPERF_HEADER_DIR/lib +add_include_lib "$RELATIVE_ROOT_DIR/$1/src/include" "$RELATIVE_ROOT_DIR/$1/build/x86_64-pc-linux-gnu-release/lib" +add_include_lib "$RELATIVE_ROOT_DIR/$2" "$RELATIVE_ROOT_DIR/$2/.libs" +add_include_lib "$RELATIVE_ROOT_DIR/$3" "$RELATIVE_ROOT_DIR/$3/lib" +LDFLAGS="-L. $LDFLAGS" + +command_exists() { + command -v "$1" >/dev/null 2>&1 +} +header_exists() { + for F in ${CFLAGS} -I/usr/include -I/include; do + [ "${F}" != "${F#-I}" ] && [ -f "${F#-I}/$1" ] && return 0 + done + echo "Missing path to header \"$1\" in CFLAGS." + return 1 +} +find_library() { + for F in ${LDFLAGS} -L/usr/lib -L/lib; do + [ "${F}" != "${F#-L}" ] && [ -f "${F#-L}/$1" ] && echo "${F#-L}/$1" && return 0 + done + return 1 +} +library_exists() { + find_library "$1" >/dev/null && return 0 + echo "Missing path to library \"$1\" in LDFLAGS." + return 1 +} # check requirements -if [ ! -f "$YICES_LIB_DIR/libyices.a" ]; then - echo "You need to specify the directory with the downloaded and compiled Yices on the command line!" - echo "Can not find $YICES_LIB_DIR/libyices.a" - exit 1 -fi -if [ ! -f "$GMP_LIB_DIR/libgmp.a" ]; then - echo "You need to specify the GMP directory on the command line!" - echo "Can not find $GMP_LIB_DIR/libgmp.a" - exit 1 -fi -if [ ! -f "$GPERF_LIB_DIR/libgp.a" ]; then - echo "You need to specify the GPERF directory on the command line!" - echo "Can not find $GPERF_LIB_DIR/libgp.a" - exit 1 -fi +command_exists cc +header_exists gmp.h +header_exists yices.h +header_exists jni.h +library_exists libyices.a +library_exists libgmp.a +[ $(uname -s) != "Darwin" ] && [ $(uname -m) == "x86_64" ] && library_exists libgp.a -SRC_FILES="org_sosy_1lab_java_1smt_solvers_yices2_Yices2NativeApi.c" -OBJ_FILES="org_sosy_1lab_java_1smt_solvers_yices2_Yices2NativeApi.o" +SRC_FILE="org_sosy_1lab_java_1smt_solvers_yices2_Yices2NativeApi.c" +OBJ_FILE="org_sosy_1lab_java_1smt_solvers_yices2_Yices2NativeApi.o" OUT_FILE="libyices2j.so" +[ $(uname -s) = "Darwin" ] && OUT_FILE="libyices2j.dylib" echo "Compiling the C wrapper code and creating the \"$OUT_FILE\" library..." # This will compile the JNI wrapper part, given the JNI and the Yices header files -gcc -g -std=gnu99 -Wall -Wextra -Wpedantic -Wno-return-type -Wno-unused-parameter \ - $JNI_HEADERS -I$YICES_SRC_DIR -I$GMP_HEADER_DIR -I$GPERF_HEADER_DIR $SRC_FILES -fPIC -c +cc -g -std=gnu99 -Wall -Wextra -Wpedantic -Wno-return-type -Wno-unused-parameter \ + $CFLAGS $JNI_HEADERS $SRC_FILE -fPIC -c -o $OBJ_FILE echo "Compilation Done" echo "Linking libraries together into one file..." @@ -76,37 +93,42 @@ echo "Linking libraries together into one file..." # This will link together the file produced above, the Yices library, the GMP library and the standard libraries. # Everything except the standard libraries is included statically. # The result is a single shared library containing all necessary components. -if [ `uname -m` = "x86_64" ]; then - gcc -Wall -g -o $OUT_FILE -shared -Wl,-soname,libyices2j.so \ - -L. -L$YICES_LIB_DIR -L$GMP_LIB_DIR -L$GPERF_LIB_DIR \ - -I$GMP_HEADER_DIR -I$GPERF_HEADER_DIR $OBJ_FILES -Wl,-Bstatic \ - -lyices -lgmpxx -lgmp -lgp -static-libstdc++ -lstdc++ \ - -Wl,-Bdynamic -lc -lm -Wl,--version-script=libyices2j.version +if [ $(uname -s) = "Darwin" ]; then + LDFLAGS="$LDFLAGS -dynamiclib $(find_library libyices.a) $(find_library libgmp.a)" +elif [ $(uname -m) = "x86_64" ]; then + LDFLAGS="$LDFLAGS -shared -Wl,-soname,libyices2j.so + -Wl,-Bstatic -lyices -lgmpxx -lgmp -lgp -static-libstdc++ -lstdc++ + -Wl,-Bdynamic -lc -lm + -Wl,--version-script=libyices2j.version" else # TODO compiling for/on a 32bit system was not done for quite a long time. We should drop it. - gcc -Wall -g -o ${OUT_FILE} -shared -Wl,-soname,libyices2j.so \ - -L${YICES_LIB_DIR} -L${GMP_LIB_DIR} -L${GPERF_LIB_DIR} \ - -I${GMP_HEADER_DIR} -I${GPERF_HEADER_DIR} ${OBJ_FILES} \ - -Wl,-Bstatic -lyices -lgmpxx -lgmp -Wl,-Bdynamic -lc -lm -lstdc++ + LDFLAGS="$LDFLAGS -shared -Wl,-soname,libyices2j.so + -Wl,-Bstatic -lyices -lgmpxx -lgmp + -Wl,-Bdynamic -lc -lm -lstdc++" fi +cc -Wall -g -o "$OUT_FILE" $LDFLAGS "$OBJ_FILE" if [ $? -ne 0 ]; then - echo "There was a problem during compilation of \"org_sosy_1lab_java_1smt_solvers_yices2_Yices2NativeApi.c\"" + echo "There was a problem during compilation of \"$SRC_FILE\"" exit 1 fi echo "Linking Done" echo "Reducing file size by dropping unused symbols..." -strip ${OUT_FILE} +STRIP_FLAGS="" +[ $(uname -s) = "Darwin" ] && STRIP_FLAGS="-u" +strip $STRIP_FLAGS "$OUT_FILE" echo "Reduction Done" -MISSING_SYMBOLS="$(readelf -Ws ${OUT_FILE} | grep NOTYPE | grep GLOBAL | grep UND)" -if [ ! -z "$MISSING_SYMBOLS" ]; then - echo "Warning: There are the following unresolved dependencies in libyices2j.so:" - readelf -Ws ${OUT_FILE} | grep NOTYPE | grep GLOBAL | grep UND - exit 1 +if command_exists readelf; then + MISSING_SYMBOLS="$(readelf -Ws ${OUT_FILE} | grep NOTYPE | grep GLOBAL | grep UND)" + if [ ! -z "$MISSING_SYMBOLS" ]; then + echo "Warning: There are the following unresolved dependencies in libyices2j.so:" + readelf -Ws ${OUT_FILE} | grep NOTYPE | grep GLOBAL | grep UND + exit 1 + fi fi echo "All Done" diff --git a/lib/native/source/yices2j/includes/defines.h b/lib/native/source/yices2j/includes/defines.h index 7133b275dd..83af55349d 100644 --- a/lib/native/source/yices2j/includes/defines.h +++ b/lib/native/source/yices2j/includes/defines.h @@ -188,6 +188,14 @@ typedef void jvoid; // for symmetry to jint, jlong etc. (*jenv)->ReleaseLongArrayElements(jenv, arg##num, m_arg##num, 0); \ out##num: +#define INT_INIT \ + int retval = -1; + +#define TERM_VECTOR_ARG_INIT INT_INIT + +#define POINTER_INIT(type) \ + type* retval = NULL; + //may cause memory leak through yices_error_string #define INT_RETURN \ if (retval <= 0 && yices_error_code() != 0){ \ @@ -305,7 +313,7 @@ typedef void jvoid; // for symmetry to jint, jlong etc. int yval[2]; \ yval[0] = s_arg##num.node_id; \ yval[1] = s_arg##num.node_tag; \ - jintArray jretval; \ + jintArray jretval = 0; \ if (!(*jenv)->ExceptionCheck(jenv)) { \ jretval = (*jenv)->NewIntArray(jenv, 2); \ if(jretval != NULL){ \ @@ -418,11 +426,13 @@ typedef jlong jjparam; typedef jint jjterm; #define TERM_ARG(num) SIMPLE_ARG(term_t, num) #define TERM_ARG_VOID(num) SIMPLE_ARG(term_t, num) +#define TERM_INIT INT_INIT #define TERM_RETURN INT_RETURN typedef jlong jjmodel; #define MODEL_ARG(num) POINTER_ARG(model_t, num) #define MODEL_ARG_VOID(num) POINTER_ARG(model_t, num) +#define MODEL_INIT POINTER_INIT(model_t) #define MODEL_RETURN POINTER_RETURN //For things like model_t ** #define MODEL_ARG_POINTER(num) POINTER_POINTER_ARG(model_t, num) @@ -434,6 +444,7 @@ typedef jintArray jjtermArray; typedef jint jjtype; #define TYPE_ARG(num) SIMPLE_ARG(type_t, num) +#define TYPE_INIT INT_INIT #define TYPE_RETURN INT_RETURN typedef jintArray jjtypeArray; diff --git a/lib/native/source/yices2j/org_sosy_1lab_java_1smt_solvers_yices2_Yices2NativeApi.c b/lib/native/source/yices2j/org_sosy_1lab_java_1smt_solvers_yices2_Yices2NativeApi.c index 9663fb4e28..6e0c371cd7 100644 --- a/lib/native/source/yices2j/org_sosy_1lab_java_1smt_solvers_yices2_Yices2NativeApi.c +++ b/lib/native/source/yices2j/org_sosy_1lab_java_1smt_solvers_yices2_Yices2NativeApi.c @@ -60,17 +60,19 @@ VOID_CALL1(free_config) DEFINE_FUNC(int, 1set_1config) WITH_THREE_ARGS(jconf, string, string) CONF_ARG(1) +INT_INIT STRING_ARG(2) STRING_ARG(3) -CALL3(int, set_config) +CALL3(, set_config) FREE_STRING_ARG(2) FREE_STRING_ARG(3) INT_RETURN DEFINE_FUNC(int, 1default_1config_1for_1logic) WITH_TWO_ARGS(jconf, string) CONF_ARG(1) +INT_INIT STRING_ARG(2) -CALL2(int, default_config_for_logic) +CALL2(, default_config_for_logic) FREE_STRING_ARG(2) INT_RETURN @@ -95,15 +97,17 @@ VOID_CALL1(free_context) DEFINE_FUNC(int, 1context_1enable_1option) WITH_TWO_ARGS(jctx, string) CTX_ARG(1) +INT_INIT STRING_ARG(2) -CALL2(int, context_enable_option) +CALL2(, context_enable_option) FREE_STRING_ARG(2) INT_RETURN DEFINE_FUNC(int, 1context_1disable_1option) WITH_TWO_ARGS(jctx, string) CTX_ARG(1) +INT_INIT STRING_ARG(2) -CALL2(int, context_disable_option) +CALL2(, context_disable_option) FREE_STRING_ARG(2) INT_RETURN @@ -117,9 +121,10 @@ PARAM_RETURN DEFINE_FUNC(int, 1set_1param) WITH_THREE_ARGS(jparam, string, string) PARAM_ARG(1) +INT_INIT STRING_ARG(2) STRING_ARG(3) -CALL3(int, set_param) +CALL3(, set_param) FREE_STRING_ARG(2) FREE_STRING_ARG(3) INT_RETURN @@ -162,9 +167,10 @@ TYPE_RETURN DEFINE_FUNC(jtype, 1function_1type) WITH_THREE_ARGS(int, jtypeArray, jtype) UINT32_ARG(1) +TYPE_INIT TYPE_ARRAY_ARG(2) TYPE_ARG(3) -CALL3(type_t, function_type) +CALL3(, function_type) FREE_TYPE_ARRAY_ARG(2) TYPE_RETURN @@ -269,16 +275,18 @@ TERM_RETURN DEFINE_FUNC(jterm, 1distinct) WITH_TWO_ARGS(int, jtermArray) UINT32_ARG(1) +TERM_INIT TERM_ARRAY_ARG(2) -CALL2(term_t, distinct) +CALL2(, distinct) FREE_TERM_ARRAY_ARG(2) TERM_RETURN DEFINE_FUNC(jterm, 1application) WITH_THREE_ARGS(jterm, int, jtermArray) TERM_ARG(1) UINT32_ARG(2) +TERM_INIT TERM_ARRAY_ARG(3) -CALL3(term_t, application) +CALL3(, application) FREE_TERM_ARRAY_ARG(3) TERM_RETURN @@ -289,9 +297,10 @@ TERM_RETURN DEFINE_FUNC(jterm, 1update) WITH_FOUR_ARGS(jterm, int, jtermArray, jterm) TERM_ARG(1) UINT32_ARG(2) +TERM_INIT TERM_ARRAY_ARG(3) TERM_ARG(4) -CALL4(term_t, update) +CALL4(, update) FREE_TERM_ARRAY_ARG(3) TERM_RETURN @@ -299,25 +308,28 @@ TERM_RETURN DEFINE_FUNC(jterm, 1forall) WITH_THREE_ARGS(int, jtermArray, jterm) UINT32_ARG(1) +TERM_INIT TERM_ARRAY_ARG(2) TERM_ARG(3) -CALL3(term_t, forall) +CALL3(, forall) FREE_TERM_ARRAY_ARG(2) TERM_RETURN DEFINE_FUNC(jterm, 1exists) WITH_THREE_ARGS(int, jtermArray, jterm) UINT32_ARG(1) +TERM_INIT TERM_ARRAY_ARG(2) TERM_ARG(3) -CALL3(term_t, exists) +CALL3(, exists) FREE_TERM_ARRAY_ARG(2) TERM_RETURN DEFINE_FUNC(jterm, 1lambda) WITH_THREE_ARGS(int, jtermArray, jterm) UINT32_ARG(1) +TERM_INIT TERM_ARRAY_ARG(2) TERM_ARG(3) -CALL3(term_t, lambda) +CALL3(, lambda) FREE_TERM_ARRAY_ARG(2) TERM_RETURN @@ -340,8 +352,9 @@ TERM_RETURN DEFINE_FUNC(jterm, 1and) WITH_TWO_ARGS(int, jtermArray) UINT32_ARG(1) +TERM_INIT TERM_ARRAY_ARG(2) -CALL2(term_t, and) +CALL2(, and) FREE_TERM_ARRAY_ARG(2) TERM_RETURN @@ -360,8 +373,9 @@ TERM_RETURN DEFINE_FUNC(jterm, 1or) WITH_TWO_ARGS(int, jtermArray) UINT32_ARG(1) +TERM_INIT TERM_ARRAY_ARG(2) -CALL2(term_t, or) +CALL2(, or) FREE_TERM_ARRAY_ARG(2) TERM_RETURN @@ -380,8 +394,9 @@ TERM_RETURN DEFINE_FUNC(jterm, 1xor) WITH_TWO_ARGS(int, jtermArray) UINT32_ARG(1) +TERM_INIT TERM_ARRAY_ARG(2) -CALL2(term_t, xor) +CALL2(, xor) FREE_TERM_ARRAY_ARG(2) TERM_RETURN @@ -443,14 +458,16 @@ TERM_RETURN //skipping GMP functions DEFINE_FUNC(jterm, 1parse_1rational) WITH_ONE_ARG(string) +TERM_INIT STRING_ARG(1) -CALL1(term_t, parse_rational) +CALL1(, parse_rational) FREE_STRING_ARG(1) TERM_RETURN DEFINE_FUNC(jterm, 1parse_1float) WITH_ONE_ARG(string) +TERM_INIT STRING_ARG(1) -CALL1(term_t, parse_float) +CALL1(, parse_float) FREE_STRING_ARG(1) TERM_RETURN @@ -496,34 +513,38 @@ TERM_RETURN DEFINE_FUNC(jterm, 1sum) WITH_TWO_ARGS(int, jtermArray) UINT32_ARG(1) +TERM_INIT TERM_ARRAY_ARG(2) -CALL2(term_t, sum) +CALL2(, sum) FREE_TERM_ARRAY_ARG(2) TERM_RETURN DEFINE_FUNC(jterm, 1product) WITH_TWO_ARGS(int, jtermArray) UINT32_ARG(1) +TERM_INIT TERM_ARRAY_ARG(2) -CALL2(term_t, product) +CALL2(, product) FREE_TERM_ARRAY_ARG(2) TERM_RETURN DEFINE_FUNC(jterm, 1poly_1int32) WITH_THREE_ARGS(int, intArray, jtermArray) UINT32_ARG(1) +TERM_INIT INT_ARRAY_ARG(int32_t, 2) TERM_ARRAY_ARG(3) -CALL3(term_t, poly_int32) -FREE_INT_ARRAY_ARG(2) +CALL3(, poly_int32) FREE_TERM_ARRAY_ARG(3) +FREE_INT_ARRAY_ARG(2) TERM_RETURN DEFINE_FUNC(jterm, 1poly_1int64) WITH_THREE_ARGS(int, longArray, jtermArray) UINT32_ARG(1) +TERM_INIT LONG_ARRAY_ARG(int64_t, 2) TERM_ARRAY_ARG(3) -CALL3(term_t, poly_int64) -FREE_LONG_ARRAY_ARG(2) +CALL3(, poly_int64) FREE_TERM_ARRAY_ARG(3) +FREE_LONG_ARRAY_ARG(2) TERM_RETURN //skipping poly_rational32() @@ -637,20 +658,23 @@ TERM_RETURN DEFINE_FUNC(jterm, 1bvconst_1from_1array) WITH_TWO_ARGS(int, intArray) UINT32_ARG(1) +TERM_INIT INT_ARRAY_ARG(int32_t, 2) -CALL2(term_t, bvconst_from_array) +CALL2(, bvconst_from_array) FREE_INT_ARRAY_ARG(2) TERM_RETURN DEFINE_FUNC(jterm, 1parse_1bvbin) WITH_ONE_ARG(string) +TERM_INIT STRING_ARG(1) -CALL1(term_t, parse_bvbin) +CALL1(, parse_bvbin) FREE_STRING_ARG(1) TERM_RETURN DEFINE_FUNC(jterm, 1parse_1bvhex) WITH_ONE_ARG(string) +TERM_INIT STRING_ARG(1) -CALL1(term_t, parse_bvhex) +CALL1(, parse_bvhex) FREE_STRING_ARG(1) TERM_RETURN @@ -690,15 +714,17 @@ TERM_RETURN DEFINE_FUNC(jterm, 1bvsum) WITH_TWO_ARGS(int, jtermArray) UINT32_ARG(1) +TERM_INIT TERM_ARRAY_ARG(2) -CALL2(term_t, bvsum) +CALL2(, bvsum) FREE_TERM_ARRAY_ARG(2) TERM_RETURN DEFINE_FUNC(jterm, 1bvproduct) WITH_TWO_ARGS(int, jtermArray) UINT32_ARG(1) +TERM_INIT TERM_ARRAY_ARG(2) -CALL2(term_t, bvproduct) +CALL2(, bvproduct) FREE_TERM_ARRAY_ARG(2) TERM_RETURN @@ -739,8 +765,9 @@ TERM_RETURN DEFINE_FUNC(jterm, 1bvand) WITH_TWO_ARGS(int, jtermArray) UINT32_ARG(1) +TERM_INIT TERM_ARRAY_ARG(2) -CALL2(term_t, bvand) +CALL2(, bvand) FREE_TERM_ARRAY_ARG(2) TERM_RETURN @@ -759,8 +786,9 @@ TERM_RETURN DEFINE_FUNC(jterm, 1bvor) WITH_TWO_ARGS(int, jtermArray) UINT32_ARG(1) +TERM_INIT TERM_ARRAY_ARG(2) -CALL2(term_t, bvor) +CALL2(, bvor) FREE_TERM_ARRAY_ARG(2) TERM_RETURN @@ -779,8 +807,9 @@ TERM_RETURN DEFINE_FUNC(jterm, 1bvxor) WITH_TWO_ARGS(int, jtermArray) UINT32_ARG(1) +TERM_INIT TERM_ARRAY_ARG(2) -CALL2(term_t, bvxor) +CALL2(, bvxor) FREE_TERM_ARRAY_ARG(2) TERM_RETURN @@ -890,8 +919,9 @@ TERM_RETURN DEFINE_FUNC(jterm, 1bvconcat) WITH_TWO_ARGS(int, jtermArray) UINT32_ARG(1) +TERM_INIT TERM_ARRAY_ARG(2) -CALL2(term_t, bvconcat) +CALL2(, bvconcat) FREE_TERM_ARRAY_ARG(2) TERM_RETURN @@ -937,8 +967,9 @@ TERM_RETURN DEFINE_FUNC(jterm, 1bvarray) WITH_TWO_ARGS(int, jtermArray) UINT32_ARG(1) +TERM_INIT TERM_ARRAY_ARG(2) -CALL2(term_t, bvarray) +CALL2(, bvarray) FREE_TERM_ARRAY_ARG(2) TERM_RETURN @@ -1101,6 +1132,7 @@ MPQ_ARG(3) term_t s_arg4; term_t *m_arg4 = &s_arg4; CALL4(int, sum_component) +jobjectArray jretval = NULL; if (retval == -1) { const char *msg = yices_error_string(); throwException(jenv, "java/lang/IllegalArgumentException", msg); @@ -1112,7 +1144,6 @@ if ((*jenv)->ExceptionCheck(jenv)) { goto out; } jclass stringClass = (*jenv)->FindClass(jenv,"java/lang/String"); -jobjectArray jretval = NULL; jretval = (jobjectArray)(*jenv)->NewObjectArray(jenv, 2,stringClass,(*jenv)->NewStringUTF(jenv, "")); if (jretval != NULL) { (*jenv)->SetObjectArrayElement(jenv, jretval, 0, (*jenv)->NewStringUTF(jenv, mpqString)); @@ -1201,8 +1232,9 @@ INT_RETURN DEFINE_FUNC(int, 1assert_1formulas) WITH_THREE_ARGS(jctx, int, jtermArray) CTX_ARG(1) UINT32_ARG(2) +INT_INIT TERM_ARRAY_ARG(3) -CALL3(int, assert_formulas) +CALL3(, assert_formulas) FREE_TERM_ARRAY_ARG(3) INT_RETURN @@ -1239,15 +1271,17 @@ DEFINE_FUNC(int, 1check_1context_1with_1assumptions) WITH_FOUR_ARGS (jctx, jpara CTX_ARG(1) PARAM_ARG(2) UINT32_ARG(3) +INT_INIT TERM_ARRAY_ARG(4) -CALL4(smt_status_t, check_context_with_assumptions) +CALL4(, check_context_with_assumptions) FREE_TERM_ARRAY_ARG(4) INT_RETURN DEFINE_FUNC(jtermArray, 1get_1unsat_1core) WITH_ONE_ARG(jctx) CTX_ARG(1) +TERM_VECTOR_ARG_INIT TERM_VECTOR_ARG(2) -CALL2(int, get_unsat_core) +CALL2(, get_unsat_core) TERM_VECTOR_ARG_RETURN(2) /* @@ -1262,11 +1296,12 @@ MODEL_RETURN DEFINE_FUNC(jmodel, 1model_1from_1map) WITH_THREE_ARGS(int ,jtermArray, jtermArray) UINT32_ARG(1) +MODEL_INIT TERM_ARRAY_ARG(2) TERM_ARRAY_ARG(3) -CALL3(model_t *, model_from_map) -FREE_TERM_ARRAY_ARG(2) +CALL3(, model_from_map) FREE_TERM_ARRAY_ARG(3) +FREE_TERM_ARRAY_ARG(2) MODEL_RETURN //1model_1collect_1defined_1terms @@ -1275,7 +1310,7 @@ DEFINE_FUNC(jtermArray, 1def_1terms) WITH_ONE_ARG(jmodel) MODEL_ARG(1) TERM_VECTOR_ARG(2) VOID_CALL2_WITH_RETURN(model_collect_defined_terms) -int retval = 0; //declare retval for TERM_VECTOR_ARG_RETURN +TERM_VECTOR_ARG_INIT //declare retval for TERM_VECTOR_ARG_RETURN TERM_VECTOR_ARG_RETURN(2) //yices_exit includes free_model() @@ -1339,8 +1374,9 @@ INT_RETURN DEFINE_FUNC(int, 1formulas_1true_1in_1model) WITH_THREE_ARGS(jmodel, int, jtermArray) MODEL_ARG(1) UINT32_ARG(2) +INT_INIT TERM_ARRAY_ARG(3) -CALL3(int, formulas_true_in_model) +CALL3(, formulas_true_in_model) FREE_TERM_ARRAY_ARG(3) INT_RETURN @@ -1491,8 +1527,9 @@ TERM_RETURN DEFINE_FUNC(int, 1set_1term_1name) WITH_TWO_ARGS(jterm, string) TERM_ARG(1) +INT_INIT STRING_ARG(2) -CALL2(int, set_term_name) +CALL2(, set_term_name) FREE_STRING_ARG(2) INT_RETURN @@ -1502,8 +1539,9 @@ CALL1(const char *, get_term_name) CONST_STRING_RETURN DEFINE_FUNC(jterm, 1get_1term_1by_1name) WITH_ONE_ARG(string) +TERM_INIT STRING_ARG(1) -CALL1(term_t, get_term_by_name) +CALL1(, get_term_by_name) FREE_STRING_ARG(1) TERM_RETURN @@ -1512,19 +1550,21 @@ TERM_RETURN //skipping parse_type DEFINE_FUNC(jterm, 1parse_1term) WITH_ONE_ARG(string) +TERM_INIT STRING_ARG(1) -CALL1(term_t, parse_term) +CALL1(, parse_term) FREE_STRING_ARG(1) TERM_RETURN DEFINE_FUNC(jterm, 1subst_1term) WITH_FOUR_ARGS(int, jtermArray, jtermArray, jterm) UINT32_ARG(1) +TERM_INIT TERM_ARRAY_ARG(2) TERM_ARRAY_ARG(3) TERM_ARG(4) -CALL4(term_t, subst_term) -FREE_TERM_ARRAY_ARG(2) +CALL4(, subst_term) FREE_TERM_ARRAY_ARG(3) +FREE_TERM_ARRAY_ARG(2) TERM_RETURN /* @@ -1604,10 +1644,11 @@ INT_RETURN */ DEFINE_FUNC(int, 1check_1formula) WITH_FOUR_ARGS(jterm, string, jmodel, string) TERM_ARG(1) +INT_INIT STRING_ARG(2) MODEL_ARG_POINTER(3) STRING_ARG(4) -CALL4(smt_status_t, check_formula) +CALL4(, check_formula) FREE_STRING_ARG(2) FREE_STRING_ARG(4) INT_RETURN @@ -1617,12 +1658,13 @@ INT_RETURN * the conjunction of f[0] ... f[n-1] is satisfiable. */ DEFINE_FUNC(int, 1check_1formulas) WITH_FIVE_ARGS(jtermArray, int, string, jmodel, string) +INT_INIT TERM_ARRAY_ARG(1) UINT32_ARG(2) STRING_ARG(3) MODEL_ARG_POINTER(4) STRING_ARG(5) -CALL5(smt_status_t, check_formulas) +CALL5(, check_formulas) FREE_TERM_ARRAY_ARG(1) FREE_STRING_ARG(3) FREE_STRING_ARG(5) @@ -1632,8 +1674,9 @@ INT_RETURN * Checks if the SAT-Solver entered as String is available */ DEFINE_FUNC(int, 1has_1delegate) WITH_ONE_ARG(string) +INT_INIT STRING_ARG(1) -CALL1(int, has_delegate) +CALL1(, has_delegate) FREE_STRING_ARG(1) INT_RETURN @@ -1652,6 +1695,7 @@ TYPE_RETURN DEFINE_FUNC(jtermArray, 1model_1term_1support) WITH_TWO_ARGS(jmodel, jterm) MODEL_ARG(1) TERM_ARG(2) +TERM_VECTOR_ARG_INIT TERM_VECTOR_ARG(3) -CALL3(int, model_term_support) +CALL3(, model_term_support) TERM_VECTOR_ARG_RETURN(3) From 17d4de634da8dbb939a4edd285be90a00b417120 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ren=C3=A9=20Pascal=20Maseli?= Date: Wed, 25 Sep 2024 19:35:43 +0200 Subject: [PATCH 2/2] fixup! Add Yices2 for Mac OS --- lib/native/source/yices2j/compile.sh | 17 ++++++++++++----- 1 file changed, 12 insertions(+), 5 deletions(-) diff --git a/lib/native/source/yices2j/compile.sh b/lib/native/source/yices2j/compile.sh index fe917205a9..979eb95155 100755 --- a/lib/native/source/yices2j/compile.sh +++ b/lib/native/source/yices2j/compile.sh @@ -34,15 +34,22 @@ cd ${DIR} JNI_HEADERS="$(../get_jni_headers.sh)" +RELATIVE_ROOT_DIR="../../../.." +YICES_SRC_DIR=$RELATIVE_ROOT_DIR/"$1"/src/include +YICES_LIB_DIR=$RELATIVE_ROOT_DIR/"$1"/build/x86_64-pc-linux-gnu-release/lib/ +GMP_HEADER_DIR=$RELATIVE_ROOT_DIR/"$2" +GMP_LIB_DIR=$GMP_HEADER_DIR/.libs +GPERF_HEADER_DIR=$RELATIVE_ROOT_DIR/"$3" +GPERF_LIB_DIR=$GPERF_HEADER_DIR/lib + +LDFLAGS="-L. $LDFLAGS" add_include_lib() { [ -d "$1" ] && CFLAGS="$CFLAGS -I$1" [ -d "$2" ] && LDFLAGS="$LDFLAGS -L$2" } -RELATIVE_ROOT_DIR="../../../.." -add_include_lib "$RELATIVE_ROOT_DIR/$1/src/include" "$RELATIVE_ROOT_DIR/$1/build/x86_64-pc-linux-gnu-release/lib" -add_include_lib "$RELATIVE_ROOT_DIR/$2" "$RELATIVE_ROOT_DIR/$2/.libs" -add_include_lib "$RELATIVE_ROOT_DIR/$3" "$RELATIVE_ROOT_DIR/$3/lib" -LDFLAGS="-L. $LDFLAGS" +add_include_lib "$YICES_SRC_DIR" "$YICES_LIB_DIR" +add_include_lib "$GMP_HEADER_DIR" "$GMP_LIB_DIR" +add_include_lib "$GPERF_HEADER_DIR" "$GPERF_LIB_DIR" command_exists() { command -v "$1" >/dev/null 2>&1