diff --git a/.gitignore b/.gitignore index d380fe06f..a26ee7565 100644 --- a/.gitignore +++ b/.gitignore @@ -34,6 +34,8 @@ ncscope.out # Commonly used directories for code bld_dbg/* bld_rel/* +bld_dbg_x64/* +bld_rel_x64/* # Auto generated files. config.log config.status diff --git a/RELEASE_NOTES b/RELEASE_NOTES index 55e873997..e6b63d62d 100644 --- a/RELEASE_NOTES +++ b/RELEASE_NOTES @@ -14,6 +14,8 @@ Version 4.3.2 - Removed 'autoconf' dependency. We do not need to execute 'autoconf' and './configure' anymore to build Z3. +- Fixed incorrect result returned by Z3_solver_get_num_scopes. (Thanks to Herman Venter). This bug was introduced in Z3 4.3.0 + Version 4.3.1 ============= diff --git a/examples/java/JavaExample.java b/examples/java/JavaExample.java index a721c53d2..d0bdcf8d4 100644 --- a/examples/java/JavaExample.java +++ b/examples/java/JavaExample.java @@ -806,7 +806,6 @@ class JavaExample { System.out.println("BasicTests"); - Symbol qi = ctx.MkSymbol(1); Symbol fname = ctx.MkSymbol("f"); Symbol x = ctx.MkSymbol("x"); Symbol y = ctx.MkSymbol("y"); @@ -2207,7 +2206,8 @@ class JavaExample } catch (Z3Exception ex) { System.out.println("Z3 Managed Exception: " + ex.getMessage()); - System.out.println("Stack trace: " + ex.getStackTrace()); + System.out.println("Stack trace: "); + ex.printStackTrace(System.out); } catch (TestFailedException ex) { System.out.println("TEST CASE FAILED: " + ex.getMessage()); diff --git a/scripts/mk_util.py b/scripts/mk_util.py index a0fed0696..2b1eaec93 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -985,7 +985,10 @@ class JavaDLLComponent(Component): else: t = t.replace('PLATFORM', 'win32') out.write(t) - out.write('\t$(SLINK) $(SLINK_OUT_FLAG)libz3java$(SO_EXT) $(SLINK_FLAGS) Native$(OBJ_EXT) libz3$(LIB_EXT)\n') + if IS_WINDOWS: # On Windows, CL creates a .lib file to link against. + out.write('\t$(SLINK) $(SLINK_OUT_FLAG)libz3java$(SO_EXT) $(SLINK_FLAGS) api/java/Native$(OBJ_EXT) libz3$(LIB_EXT)\n') + else: + out.write('\t$(SLINK) $(SLINK_OUT_FLAG)libz3java$(SO_EXT) $(SLINK_FLAGS) api/java/Native$(OBJ_EXT) libz3$(SO_EXT)\n') out.write('%s.jar: libz3java$(SO_EXT) ' % self.package_name) # for java_file in get_java_files(self.src_dir): # out.write('%s ' % java_file) diff --git a/scripts/update_api.py b/scripts/update_api.py index 8d5d5e712..e55a3a356 100644 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -468,18 +468,6 @@ def java_method_name(name): i = i + 1 return result -# Return the Java method name used to retrieve the elements of the given parameter -def java_get_array_elements(p): - if param_type(p) == INT or param_type(p) == UINT: - return 'GetIntArrayElements' - else: - return 'GetLongArrayElements' -# Return the Java method name used to release the elements of the given parameter -def java_release_array_elements(p): - if param_type(p) == INT or param_type(p) == UINT: - return 'ReleaseIntArrayElements' - else: - return 'ReleaseLongArrayElements' # Return the type of the java array elements def java_array_element_type(p): if param_type(p) == INT or param_type(p) == UINT: @@ -536,9 +524,27 @@ def mk_java(): java_wrapper.write('#include"z3.h"\n') java_wrapper.write('#ifdef __cplusplus\n') java_wrapper.write('extern "C" {\n') - java_wrapper.write('#endif\n') + java_wrapper.write('#endif\n\n') + if VS_X64: + java_wrapper.write('#define GETLONGAELEMS(T,OLD,NEW) \\\n') + java_wrapper.write(' T * NEW = (T*) jenv->GetLongArrayElements(OLD, NULL); \n') + java_wrapper.write('#define RELEASELONGAELEMS(OLD,NEW) \\\n') + java_wrapper.write(' jenv->ReleaseLongArrayElements(OLD, (jlong *) NEW, JNI_ABORT); \n\n') + else: + java_wrapper.write('#define GETLONGAELEMS(T,OLD,NEW) \\\n') + java_wrapper.write(' T * NEW = 0; { \\\n') + java_wrapper.write(' jlong * temp = jenv->GetLongArrayElements(OLD, NULL); \\\n') + java_wrapper.write(' unsigned int size = jenv->GetArrayLength(OLD); \\\n') + java_wrapper.write(' NEW = (T*) (new int[size]); \\\n') + java_wrapper.write(' for (unsigned i=0; i < size; i++) \\\n') + java_wrapper.write(' NEW[i] = reinterpret_cast(temp[i]); \\\n') + java_wrapper.write(' jenv->ReleaseLongArrayElements(OLD, temp, JNI_ABORT); \\\n') + java_wrapper.write(' } \n\n') + java_wrapper.write('#define RELEASELONGAELEMS(OLD,NEW) \\\n') + java_wrapper.write(' delete [] NEW; \n\n') + pkg_str = get_component('java').package_name.replace('.', '_') for name, result, params in _dotnet_decls: - java_wrapper.write('JNIEXPORT %s JNICALL Java_Z3Native_%s(JNIEnv * jenv, jclass cls' % (type2javaw(result), java_method_name(name))) + java_wrapper.write('JNIEXPORT %s JNICALL Java_%s_Native_%s(JNIEnv * jenv, jclass cls' % (type2javaw(result), pkg_str, java_method_name(name))) i = 0; for param in params: java_wrapper.write(', ') @@ -552,11 +558,10 @@ def mk_java(): if k == OUT or k == INOUT: java_wrapper.write(' %s _a%s;\n' % (type2str(param_type(param)), i)) elif k == IN_ARRAY or k == INOUT_ARRAY: - java_wrapper.write(' %s * _a%s = (%s *) jenv->%s(a%s, NULL);\n' % (type2str(param_type(param)), - i, - type2str(param_type(param)), - java_get_array_elements(param), - i)) + if param_type(param) == INT or param_type(param) == UINT: + java_wrapper.write(' %s * _a%s = (%s*) jenv->GetIntArrayElements(a%s, NULL);\n' % (type2str(param_type(param)), i, type2str(param_type(param)), i)) + else: + java_wrapper.write(' GETLONGAELEMS(%s, a%s, _a%s);\n' % (type2str(param_type(param)), i, i)) elif k == OUT_ARRAY: java_wrapper.write(' %s * _a%s = (%s *) malloc(((unsigned)a%s) * sizeof(%s));\n' % (type2str(param_type(param)), i, @@ -601,10 +606,11 @@ def mk_java(): i)) java_wrapper.write(' free(_a%s);\n' % i) elif k == IN_ARRAY or k == OUT_ARRAY: - java_wrapper.write(' jenv->%s(a%s, (%s *) _a%s, JNI_ABORT);\n' % (java_release_array_elements(param), - i, - java_array_element_type(param), - i)) + if param_type(param) == INT or param_type(param) == UINT: + java_wrapper.write(' jenv->ReleaseIntArrayElements(a%s, (jint*)_a%s, JNI_ABORT);\n' % (i, i)) + else: + java_wrapper.write(' RELEASELONGAELEMS(a%s, _a%s);\n' % (i, i)) + elif k == OUT or k == INOUT: if param_type(param) == INT or param_type(param) == UINT: java_wrapper.write(' {\n') diff --git a/src/api/java/Context.java b/src/api/java/Context.java index d289d956f..b903f71e0 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -2974,23 +2974,15 @@ public class Context extends IDisposable void CheckContextMatch(Z3Object other) throws Z3Exception { - - if (this == other.Context()) - throw new Z3Exception("Context mismatch"); + if (this != other.Context()) + throw new Z3Exception("Context mismatch"); } void CheckContextMatch(Z3Object[] arr) throws Z3Exception { - - if (arr != null) - { - for (Z3Object a : arr) - { - // It was an assume, now we added the precondition, and we made - // it into an assert - CheckContextMatch(a); - } - } + if (arr != null) + for (Z3Object a : arr) + CheckContextMatch(a); } private ASTDecRefQueue m_AST_DRQ = new ASTDecRefQueue(); @@ -3091,8 +3083,6 @@ public class Context extends IDisposable **/ protected void finalize() { - // Console.WriteLine("Context Finalizer from " + - // System.Threading.Thread.CurrentThread.ManagedThreadId); Dispose(); if (m_refCount == 0) @@ -3102,6 +3092,7 @@ public class Context extends IDisposable m_ctx = 0; } else /* re-queue the finalizer */ + /* BUG: DRQ's need to be taken over too! */ new Context(m_ctx, m_refCount, m_n_err_handler); } @@ -3110,8 +3101,6 @@ public class Context extends IDisposable **/ public void Dispose() { - // Console.WriteLine("Context Dispose from " + - // System.Threading.Thread.CurrentThread.ManagedThreadId); m_AST_DRQ.Clear(this); m_ASTMap_DRQ.Clear(this); m_ASTVector_DRQ.Clear(this); diff --git a/src/api/java/Z3Object.java b/src/api/java/Z3Object.java index e5e4af3c2..877fead79 100644 --- a/src/api/java/Z3Object.java +++ b/src/api/java/Z3Object.java @@ -104,13 +104,12 @@ public class Z3Object extends IDisposable return null; long[] an = new long[a.length]; for (int i = 0; i < a.length; i++) - if (a[i] != null) - an[i] = a[i].NativeObject(); + an[i] = a[i].NativeObject(); return an; } static int ArrayLength(Z3Object[] a) { - return (a == null) ? 0 : (int) a.length; + return (a == null) ? 0 : a.length; } } diff --git a/src/muz_qe/dl_context.cpp b/src/muz_qe/dl_context.cpp index f11c9852d..ec78f8e92 100644 --- a/src/muz_qe/dl_context.cpp +++ b/src/muz_qe/dl_context.cpp @@ -994,7 +994,7 @@ namespace datalog { p.insert(":profile-timeout-milliseconds", CPK_UINT, "instructions and rules that took less than the threshold will not be printed when printed the instruction/rule list"); p.insert(":print-with-fixedpoint-extensions", CPK_BOOL, "(default true) use SMT-LIB2 fixedpoint extensions, instead of pure SMT2, when printing rules"); - p.insert(":print-low-level-smt2", CPK_BOOL, "(default true) use (faster) low-level SMT2 printer (the printer is scalable but the result may not be as readable)"); + p.insert(":print-low-level-smt2", CPK_BOOL, "(default false) use (faster) low-level SMT2 printer (the printer is scalable but the result may not be as readable)"); PRIVATE_PARAMS( p.insert(":dbg-fpr-nonempty-relation-signature", CPK_BOOL, @@ -1651,7 +1651,7 @@ namespace datalog { expr_ref_vector rules(m); svector names; bool use_fixedpoint_extensions = m_params.get_bool(":print-with-fixedpoint-extensions", true); - bool print_low_level = m_params.get_bool(":print-low-level-smt2", true); + bool print_low_level = m_params.get_bool(":print-low-level-smt2", false); #define PP(_e_) if (print_low_level) out << mk_smt_pp(_e_, m); else ast_smt2_pp(out, _e_, env, params); diff --git a/src/solver/strategic_solver.cpp b/src/solver/strategic_solver.cpp index 616ec5342..b6eb98b42 100644 --- a/src/solver/strategic_solver.cpp +++ b/src/solver/strategic_solver.cpp @@ -308,7 +308,7 @@ void strategic_solver::pop(unsigned n) { unsigned strategic_solver::get_scope_level() const { if (m_ctx == 0) return 0; - return m_ctx->m_assertions.size(); + return m_ctx->m_scopes.size(); } struct aux_timeout_eh : public event_handler {