From 91402f2060d8c88ccbc724881a996fc0a72c659e Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 8 Feb 2013 18:54:44 +0000 Subject: [PATCH 1/3] C API: fixed mk_context/mk_context_rc exception behaviour Adjusted .NET/Java APIs accordingly. Signed-off-by: Christoph M. Wintersteiger --- examples/java/JavaExample.java | 4 ++-- scripts/update_api.py | 35 +++++++++++++++++++++------------- src/api/api_context.cpp | 4 ++++ src/api/api_util.h | 1 + src/api/java/Context.java | 8 ++++---- 5 files changed, 33 insertions(+), 19 deletions(-) diff --git a/examples/java/JavaExample.java b/examples/java/JavaExample.java index a26c21d65..c2743ece8 100644 --- a/examples/java/JavaExample.java +++ b/examples/java/JavaExample.java @@ -2155,7 +2155,7 @@ class JavaExample // But you cannot mix numerals of different sorts // even if the size of their domains are the same: // System.out.println(ctx.mkEq(s1, t1)); - } + } public static void main(String[] args) { @@ -2226,7 +2226,7 @@ class JavaExample Context ctx = new Context(cfg); p.quantifierExample3(ctx); p.quantifierExample4(ctx); - } + } Log.close(); if (Log.isOpen()) diff --git a/scripts/update_api.py b/scripts/update_api.py index 08dd012e3..fa6111482 100644 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -395,8 +395,7 @@ def mk_dotnet(): dotnet.write(' public delegate void Z3_error_handler(Z3_context c, Z3_error_code e);\n\n') dotnet.write(' public unsafe class LIB\n') dotnet.write(' {\n') - dotnet.write(' ' - ' const string Z3_DLL_NAME = \"libz3.dll\";\n' + dotnet.write(' const string Z3_DLL_NAME = \"libz3.dll\";\n' ' \n'); dotnet.write(' [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]\n') dotnet.write(' public extern static void Z3_set_error_handler(Z3_context a0, Z3_error_handler a1);\n\n') @@ -420,7 +419,8 @@ def mk_dotnet(): dotnet.write(' }\n') -DotnetUnwrapped = [ 'Z3_del_context' ] +NULLWrapped = [ 'Z3_mk_context', 'Z3_mk_context_rc' ] +Unwrapped = [ 'Z3_del_context' ] def mk_dotnet_wrappers(): global Type2Str @@ -469,11 +469,15 @@ def mk_dotnet_wrappers(): dotnet.write('a%d' % i) i = i + 1 dotnet.write(');\n'); - if name not in DotnetUnwrapped: - if len(params) > 0 and param_type(params[0]) == CONTEXT: - dotnet.write(" Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);\n") - dotnet.write(" if (err != Z3_error_code.Z3_OK)\n") - dotnet.write(" throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));\n") + if name not in Unwrapped: + if name in NULLWrapped: + dotnet.write(" if (r == IntPtr.Zero)\n") + dotnet.write(" throw new Z3Exception(\"Object allocation failed.\");\n") + else: + if len(params) > 0 and param_type(params[0]) == CONTEXT: + dotnet.write(" Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);\n") + dotnet.write(" if (err != Z3_error_code.Z3_OK)\n") + dotnet.write(" throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));\n") if result == STRING: dotnet.write(" return Marshal.PtrToStringAnsi(r);\n") elif result != VOID: @@ -550,7 +554,7 @@ def mk_java(): java_native.write('%s a%d' % (param2java(param), i)) i = i + 1 java_native.write(')') - if len(params) > 0 and param_type(params[0]) == CONTEXT: + if (len(params) > 0 and param_type(params[0]) == CONTEXT) or name in NULLWrapped: java_native.write(' throws Z3Exception') java_native.write('\n') java_native.write(' {\n') @@ -568,10 +572,15 @@ def mk_java(): java_native.write('a%d' % i) i = i + 1 java_native.write(');\n') - if len(params) > 0 and param_type(params[0]) == CONTEXT: - java_native.write(' Z3_error_code err = Z3_error_code.fromInt(INTERNALgetErrorCode(a0));\n') - java_native.write(' if (err != Z3_error_code.Z3_OK)\n') - java_native.write(' throw new Z3Exception(INTERNALgetErrorMsgEx(a0, err.toInt()));\n') + if name not in Unwrapped: + if name in NULLWrapped: + java_native.write(" if (res == 0)\n") + java_native.write(" throw new Z3Exception(\"Object allocation failed.\");\n") + else: + if len(params) > 0 and param_type(params[0]) == CONTEXT: + java_native.write(' Z3_error_code err = Z3_error_code.fromInt(INTERNALgetErrorCode(a0));\n') + java_native.write(' if (err != Z3_error_code.Z3_OK)\n') + java_native.write(' throw new Z3Exception(INTERNALgetErrorMsgEx(a0, err.toInt()));\n') if result != VOID: java_native.write(' return res;\n') java_native.write(' }\n\n') diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index 6106cb6c7..cf179332a 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -419,17 +419,21 @@ namespace api { extern "C" { Z3_context Z3_API Z3_mk_context(Z3_config c) { + Z3_TRY; LOG_Z3_mk_context(c); memory::initialize(UINT_MAX); Z3_context r = reinterpret_cast(alloc(api::context, reinterpret_cast(c), false)); RETURN_Z3(r); + Z3_CATCH_RETURN_NO_HANDLE(0); } Z3_context Z3_API Z3_mk_context_rc(Z3_config c) { + Z3_TRY; LOG_Z3_mk_context_rc(c); memory::initialize(UINT_MAX); Z3_context r = reinterpret_cast(alloc(api::context, reinterpret_cast(c), true)); RETURN_Z3(r); + Z3_CATCH_RETURN_NO_HANDLE(0); } void Z3_API Z3_del_context(Z3_context c) { diff --git a/src/api/api_util.h b/src/api/api_util.h index c81384f2f..58abf97bf 100644 --- a/src/api/api_util.h +++ b/src/api/api_util.h @@ -26,6 +26,7 @@ Revision History: #define Z3_CATCH_CORE(CODE) } catch (z3_exception & ex) { mk_c(c)->handle_exception(ex); CODE } #define Z3_CATCH Z3_CATCH_CORE(return;) #define Z3_CATCH_RETURN(VAL) Z3_CATCH_CORE(return VAL;) +#define Z3_CATCH_RETURN_NO_HANDLE(VAL) } catch (z3_exception &) { return VAL; } #define CHECK_REF_COUNT(a) (reinterpret_cast(a)->get_ref_count() > 0) #define VALIDATE(a) SASSERT(!a || CHECK_REF_COUNT(a)) diff --git a/src/api/java/Context.java b/src/api/java/Context.java index 7a1a404af..3ad136f12 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -3053,10 +3053,10 @@ public class Context extends IDisposable // OK. } m_ctx = 0; - } else - /* re-queue the finalizer */ - /* BUG: DRQ's need to be taken over too! */ - new Context(m_ctx, m_refCount); + } + /* + else + CMW: re-queue the finalizer? */ } /** From 9e868cdef39bbd7a5b3faa3bf63978331ffa79e4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 8 Feb 2013 16:04:46 -0800 Subject: [PATCH 2/3] fix pretty printer bug found by ken Signed-off-by: Nikolaj Bjorner --- src/ast/ast_smt_pp.cpp | 8 +++++--- src/muz_qe/pdr_generalizers.cpp | 8 ++++---- 2 files changed, 9 insertions(+), 7 deletions(-) diff --git a/src/ast/ast_smt_pp.cpp b/src/ast/ast_smt_pp.cpp index 3dc94d3b3..c6c9c7c0c 100644 --- a/src/ast/ast_smt_pp.cpp +++ b/src/ast/ast_smt_pp.cpp @@ -537,7 +537,7 @@ class smt_printer { } void print_bound(symbol const& name) { - if (name.is_numerical() || '?' != name.bare_str()[0]) { + if (!m_is_smt2 && (name.is_numerical() || '?' != name.bare_str()[0])) { m_out << "?"; } m_out << name; @@ -561,7 +561,7 @@ class smt_printer { m_out << "("; print_bound(m_renaming.get_symbol(q->get_decl_name(i))); m_out << " "; - visit_sort(s, true); + visit_sort(s, !m_is-smt2); m_out << ") "; } if (m_is_smt2) { @@ -642,7 +642,9 @@ class smt_printer { m_out << m_var_names[m_num_var_names - idx - 1]; } else { - m_out << "?" << idx; + if (!m_is_smt2) { + m_out << "?" << idx; + } } } diff --git a/src/muz_qe/pdr_generalizers.cpp b/src/muz_qe/pdr_generalizers.cpp index a02a1cb6e..c9141f23e 100644 --- a/src/muz_qe/pdr_generalizers.cpp +++ b/src/muz_qe/pdr_generalizers.cpp @@ -188,8 +188,8 @@ namespace pdr { } } if (abs(r) >= rational(2) && a.is_int(x)) { - new_core[k] = m.mk_eq(a.mk_mod(x, a.mk_numeral(abs(r), true)), a.mk_numeral(rational(0), true)); - new_core[l] = a.mk_ge(x, a.mk_numeral(r, true)); + new_core[k] = m.mk_eq(a.mk_mod(x, a.mk_numeral(rational(2), true)), a.mk_numeral(rational(0), true)); + new_core[l] = a.mk_le(x, a.mk_numeral(r, true)); } bool inductive = n.pt().check_inductive(n.level(), new_core, uses_level); @@ -258,8 +258,8 @@ namespace pdr { vector & terms1 = it->m_value; vector terms2; if (r >= rational(2) && m_ub.find(r, terms2)) { - bool done = false; - for (unsigned i = 0; !done && i < terms1.size(); ++i) { + for (unsigned i = 0; i < terms1.size(); ++i) { + bool done = false; for (unsigned j = 0; !done && j < terms2.size(); ++j) { expr* t1 = terms1[i].first; expr* t2 = terms2[j].first; From dd90667cc7173d9b449a692f06fbdb5017b509ed Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 8 Feb 2013 16:32:53 -0800 Subject: [PATCH 3/3] fix pretty printer bug found by ken Signed-off-by: Nikolaj Bjorner --- src/ast/ast_smt_pp.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/ast/ast_smt_pp.cpp b/src/ast/ast_smt_pp.cpp index c6c9c7c0c..420961b4e 100644 --- a/src/ast/ast_smt_pp.cpp +++ b/src/ast/ast_smt_pp.cpp @@ -537,7 +537,7 @@ class smt_printer { } void print_bound(symbol const& name) { - if (!m_is_smt2 && (name.is_numerical() || '?' != name.bare_str()[0])) { + if (!is_smt2 && (name.is_numerical() || '?' != name.bare_str()[0])) { m_out << "?"; } m_out << name; @@ -561,7 +561,7 @@ class smt_printer { m_out << "("; print_bound(m_renaming.get_symbol(q->get_decl_name(i))); m_out << " "; - visit_sort(s, !m_is-smt2); + visit_sort(s, true); m_out << ") "; } if (m_is_smt2) {