From 22097efd4a494b50447d1886aae30d6f73464638 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martin=20R=2E=20Neuh=C3=A4u=C3=9Fer?= Date: Tue, 7 Jun 2016 12:15:51 +0200 Subject: [PATCH 01/17] Extend build scripts to support MinGW64 cross-compilation on Windows. --- README.md | 10 ++++++++++ scripts/mk_util.py | 34 +++++++++++++++++++++++++++------- 2 files changed, 37 insertions(+), 7 deletions(-) diff --git a/README.md b/README.md index 3985fad27..502b32147 100644 --- a/README.md +++ b/README.md @@ -56,6 +56,16 @@ CXX=clang++ CC=clang python scripts/mk_make.py Note that Clang < 3.7 does not support OpenMP. +You can also build Z3 for Windows using Cygwin and the Mingw-w64 cross-compiler. +To configure that case correctly, make sure to use Cygwin's own python and not +some Windows installation of Python. + +For a 64 bit build (from Cygwin64), configure Z3's sources with +```bash +CXX=x86_64-w64-mingw32-g++ CC=x86_64-w64-mingw32-gcc AR=x86_64-w64-mingw32-ar python scripts/mk_make.py +``` +A 32 bit build should work similarly (but is untested); the same is true for 32/64 bit builds from within Cygwin32. + By default, it will install z3 executable at ``PREFIX/bin``, libraries at ``PREFIX/lib``, and include files at ``PREFIX/include``, where ``PREFIX`` installation prefix if inferred by the ``mk_make.py`` script. It is usually diff --git a/scripts/mk_util.py b/scripts/mk_util.py index a73a0e59c..53f3e15c6 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -70,6 +70,7 @@ IS_OSX=False IS_FREEBSD=False IS_OPENBSD=False IS_CYGWIN=False +IS_CYGWIN_MINGW=False VERBOSE=True DEBUG_MODE=False SHOW_CPPS = True @@ -143,6 +144,9 @@ def is_osx(): def is_cygwin(): return IS_CYGWIN +def is_cygwin_mingw(): + return IS_CYGWIN_MINGW + def norm_path(p): # We use '/' on mk_project for convenience return os.path.join(*(p.split('/'))) @@ -219,7 +223,10 @@ def rmf(fname): def exec_compiler_cmd(cmd): r = exec_cmd(cmd) - rmf('a.out') + if is_windows() or is_cygwin_mingw(): + rmf('a.exe') + else: + rmf('a.out') return r def test_cxx_compiler(cc): @@ -597,6 +604,8 @@ elif os.name == 'posix': IS_OPENBSD=True elif os.uname()[0][:6] == 'CYGWIN': IS_CYGWIN=True + if ("mingw" in CC): + IS_CYGWIN_MINGW=True def display_help(exit_code): print("mk_make.py: Z3 Makefile generator\n") @@ -1821,7 +1830,7 @@ class MLComponent(Component): CP_CMD='copy' OCAML_FLAGS = '' - if DEBUG_MODE: + if DEBUG_MODE: OCAML_FLAGS += '-g' OCAMLCF = OCAMLC + ' ' + OCAML_FLAGS OCAMLOPTF = OCAMLOPT + ' ' + OCAML_FLAGS @@ -1875,12 +1884,15 @@ class MLComponent(Component): OCAMLMKLIB = 'ocamlmklib' - LIBZ3 = '-L. -lz3' - if is_cygwin(): - # Some ocamlmklib's don't like -g; observed on cygwin, but may be others as well. + + LIBZ3 = '-L. -lz3' + if is_cygwin() and not(is_cygwin_mingw()): LIBZ3 = 'libz3.dll' - elif DEBUG_MODE: + + if DEBUG_MODE and not(is_cygwin()): + # Some ocamlmklib's don't like -g; observed on cygwin, but may be others as well. OCAMLMKLIB += ' -g' + z3mls = os.path.join(self.sub_dir, 'z3ml') out.write('%s.cma: %s %s %s\n' % (z3mls, cmos, stubso, z3dllso)) out.write('\t%s -o %s -I %s %s %s %s\n' % (OCAMLMKLIB, z3mls, self.sub_dir, stubso, cmos, LIBZ3)) @@ -1943,7 +1955,7 @@ class MLComponent(Component): out.write(' %s' % ((os.path.join(self.sub_dir, 'z3ml.cmxa')))) out.write(' %s' % ((os.path.join(self.sub_dir, 'z3ml.cmxs')))) out.write(' %s' % ((os.path.join(self.sub_dir, 'dllz3ml')))) - if IS_WINDOWS: + if is_windows() or is_cygwin_mingw(): out.write('.dll') else: out.write('.so') # .so also on OSX! @@ -2382,6 +2394,12 @@ def mk_config(): CPPFLAGS = '%s -DNDEBUG -D_EXTERNAL_RELEASE' % CPPFLAGS if TRACE or DEBUG_MODE: CPPFLAGS = '%s -D_TRACE' % CPPFLAGS + if is_cygwin_mingw(): + # when cross-compiling with MinGW, we need to statically link its standard libraries + # and to make it create an import library. + SLIBEXTRAFLAGS = '%s -static-libgcc -static-libstdc++ -Wl,--out-implib,libz3.dll.a' % SLIBEXTRAFLAGS + LDFLAGS = '%s -static-libgcc -static-libstdc++' % LDFLAGS + config.write('PREFIX=%s\n' % PREFIX) config.write('CC=%s\n' % CC) config.write('CXX=%s\n' % CXX) @@ -2411,6 +2429,8 @@ def mk_config(): print('Host platform: %s' % sysname) print('C++ Compiler: %s' % CXX) print('C Compiler : %s' % CC) + if is_cygwin_mingw(): + print('MinGW32 cross: %s' % (is_cygwin_mingw())) print('Archive Tool: %s' % AR) print('Arithmetic: %s' % ARITH) print('OpenMP: %s' % HAS_OMP) From f069b1c0e980094048826183d88276c0db73961b Mon Sep 17 00:00:00 2001 From: martin-neuhaeusser Date: Wed, 25 May 2016 09:59:36 +0200 Subject: [PATCH 02/17] Make C-layer of OCaml bindings C89 compatible. This patch ensures that the C code generated for the OCaml stubs complies with C89. It is needed to compile Z3 with OCaml support with Visual Studio versions older than VS2013. --- scripts/update_api.py | 86 +++++++++++++++++++++++++-------- src/api/ml/z3native_stubs.c.pre | 7 +-- 2 files changed, 69 insertions(+), 24 deletions(-) diff --git a/scripts/update_api.py b/scripts/update_api.py index a06f1fbb1..733d5b1fa 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -1324,36 +1324,80 @@ def mk_z3native_stubs_c(ml_dir): # C interface if len(ap) > 0: ml_wrapper.write(' unsigned _i;\n') - # declare locals, preprocess arrays, strings, in/out arguments - have_context = False + # determine if the function has a context as parameter. + have_context = (len(params) > 0) and (param_type(params[0]) == CONTEXT) + + if have_context and name not in Unwrapped: + ml_wrapper.write(' Z3_error_code ec;\n') + + if result != VOID: + ts = type2str(result) + if ml_has_plus_type(ts): + pts = ml_plus_type(ts) + ml_wrapper.write(' %s z3rv_m;\n' % ts) + ml_wrapper.write(' %s z3rv;\n' % pts) + else: + ml_wrapper.write(' %s z3rv;\n' % ts) + + # declare all required local variables + # To comply with C89, we need to first declare the variables and initialize them + # only afterwards. i = 0 for param in params: if param_type(param) == CONTEXT and i == 0: - ml_wrapper.write(' Z3_context_plus ctx_p = *(Z3_context_plus*) Data_custom_val(a' + str(i) + ');\n') - ml_wrapper.write(' Z3_context _a0 = ctx_p->ctx;\n') - have_context = True + ml_wrapper.write(' Z3_context_plus ctx_p;\n') + ml_wrapper.write(' Z3_context _a0;\n') else: k = param_kind(param) if k == OUT_ARRAY: - ml_wrapper.write(' %s * _a%s = (%s*) malloc(sizeof(%s) * (_a%s));\n' % ( - type2str(param_type(param)), + ml_wrapper.write(' %s * _a%s;\n' % (type2str(param_type(param)), i)) + elif k == OUT_MANAGED_ARRAY: + ml_wrapper.write(' %s * _a%s;\n' % (type2str(param_type(param)), i)) + elif k == IN_ARRAY or k == INOUT_ARRAY: + t = param_type(param) + ts = type2str(t) + ml_wrapper.write(' %s * _a%s;\n' % (ts, i)) + elif k == IN: + t = param_type(param) + ml_wrapper.write(' %s _a%s;\n' % (type2str(t), i)) + elif k == OUT or k == INOUT: + t = param_type(param) + ml_wrapper.write(' %s _a%s;\n' % (type2str(t), i)) + ts = type2str(t) + if ml_has_plus_type(ts): + pts = ml_plus_type(ts) + ml_wrapper.write(' %s _a%dp;\n' % (pts, i)) + i = i + 1 + + + # End of variable declarations in outermost block: + # To comply with C89, no variable declarations may occur in the outermost block + # from that point onwards (breaks builds with at least VC 2012 and prior) + ml_wrapper.write('\n') + + # Declare locals, preprocess arrays, strings, in/out arguments + i = 0 + for param in params: + if param_type(param) == CONTEXT and i == 0: + ml_wrapper.write(' ctx_p = *(Z3_context_plus*) Data_custom_val(a' + str(i) + ');\n') + ml_wrapper.write(' _a0 = ctx_p->ctx;\n') + else: + k = param_kind(param) + if k == OUT_ARRAY: + ml_wrapper.write(' _a%s = (%s*) malloc(sizeof(%s) * (_a%s));\n' % ( i, type2str(param_type(param)), type2str(param_type(param)), param_array_capacity_pos(param))) elif k == OUT_MANAGED_ARRAY: - ml_wrapper.write(' %s * _a%s = 0;\n' % (type2str(param_type(param)), i)) + ml_wrapper.write(' _a%s = 0;\n' % i) elif k == IN_ARRAY or k == INOUT_ARRAY: t = param_type(param) ts = type2str(t) - ml_wrapper.write(' %s * _a%s = (%s*) malloc(sizeof(%s) * _a%s);\n' % (ts, i, ts, ts, param_array_capacity_pos(param))) + ml_wrapper.write(' _a%s = (%s*) malloc(sizeof(%s) * _a%s);\n' % (i, ts, ts, param_array_capacity_pos(param))) elif k == IN: t = param_type(param) - ml_wrapper.write(' %s _a%s = %s;\n' % (type2str(t), i, ml_unwrap(t, type2str(t), 'a' + str(i)))) - elif k == OUT: - ml_wrapper.write(' %s _a%s;\n' % (type2str(param_type(param)), i)) - elif k == INOUT: - ml_wrapper.write(' %s _a%s = a%s;\n' % (type2str(param_type(param)), i, i)) + ml_wrapper.write(' _a%s = %s;\n' % (i, ml_unwrap(t, type2str(t), 'a' + str(i)))) i = i + 1 i = 0 @@ -1375,9 +1419,9 @@ def mk_z3native_stubs_c(ml_dir): # C interface if result != VOID: ts = type2str(result) if ml_has_plus_type(ts): - ml_wrapper.write('%s z3rv_m = ' % ts) + ml_wrapper.write('z3rv_m = ') else: - ml_wrapper.write('%s z3rv = ' % ts) + ml_wrapper.write('z3rv = ') # invoke procedure ml_wrapper.write('%s(' % name) @@ -1397,8 +1441,8 @@ def mk_z3native_stubs_c(ml_dir): # C interface ml_wrapper.write(');\n') if have_context and name not in Unwrapped: - ml_wrapper.write(' int ec = Z3_get_error_code(ctx_p->ctx);\n') - ml_wrapper.write(' if (ec != 0) {\n') + ml_wrapper.write(' ec = Z3_get_error_code(ctx_p->ctx);\n') + ml_wrapper.write(' if (ec != Z3_OK) {\n') ml_wrapper.write(' const char * msg = Z3_get_error_msg(ctx_p->ctx, ec);\n') ml_wrapper.write(' caml_raise_with_string(*caml_named_value("Z3EXCEPTION"), msg);\n') ml_wrapper.write(' }\n') @@ -1408,9 +1452,9 @@ def mk_z3native_stubs_c(ml_dir): # C interface if ml_has_plus_type(ts): pts = ml_plus_type(ts) if name in NULLWrapped: - ml_wrapper.write(' %s z3rv = %s_mk(z3rv_m);\n' % (pts, pts)) + ml_wrapper.write(' z3rv = %s_mk(z3rv_m);\n' % pts) else: - ml_wrapper.write(' %s z3rv = %s_mk(ctx_p, (%s) z3rv_m);\n' % (pts, pts, ml_minus_type(ts))) + ml_wrapper.write(' z3rv = %s_mk(ctx_p, (%s) z3rv_m);\n' % (pts, ml_minus_type(ts))) # convert output params if len(op) > 0: @@ -1450,7 +1494,7 @@ def mk_z3native_stubs_c(ml_dir): # C interface elif is_out_param(p): if ml_has_plus_type(ts): pts = ml_plus_type(ts) - ml_wrapper.write(' %s _a%dp = %s_mk(ctx_p, (%s) _a%d);\n' % (pts, i, pts, ml_minus_type(ts), i)) + ml_wrapper.write(' _a%dp = %s_mk(ctx_p, (%s) _a%d);\n' % (i, pts, ml_minus_type(ts), i)) ml_wrapper.write(' %s\n' % ml_alloc_and_store(pt, '_a%d_val' % i, '_a%dp' % i)) else: ml_wrapper.write(' %s\n' % ml_alloc_and_store(pt, '_a%d_val' % i, '_a%d' % i)) diff --git a/src/api/ml/z3native_stubs.c.pre b/src/api/ml/z3native_stubs.c.pre index d6b2cdab4..5960d5095 100644 --- a/src/api/ml/z3native_stubs.c.pre +++ b/src/api/ml/z3native_stubs.c.pre @@ -227,6 +227,7 @@ void Z3_ast_finalize(value v) { int Z3_ast_compare(value v1, value v2) { Z3_ast_plus * a1 = (Z3_ast_plus*)Data_custom_val(v1); Z3_ast_plus * a2 = (Z3_ast_plus*)Data_custom_val(v2); + unsigned id1, id2; /* if the two ASTs belong to different contexts, we take their contexts' addresses to order them (arbitrarily, but fixed) */ @@ -242,8 +243,8 @@ int Z3_ast_compare(value v1, value v2) { return +1; /* Comparison according to AST ids. */ - unsigned id1 = Z3_get_ast_id(a1->cp->ctx, a1->p); - unsigned id2 = Z3_get_ast_id(a2->cp->ctx, a2->p); + id1 = Z3_get_ast_id(a1->cp->ctx, a1->p); + id2 = Z3_get_ast_id(a2->cp->ctx, a2->p); if (id1 == id2) return 0; else if (id1 < id2) @@ -255,7 +256,7 @@ int Z3_ast_compare(value v1, value v2) { int Z3_ast_compare_ext(value v1, value v2) { Z3_ast_plus * a1 = (Z3_ast_plus*)Data_custom_val(v1); unsigned id1; - int id2 = Val_int(v2); + unsigned id2 = (unsigned)Val_int(v2); if (a1->p == NULL && id2 == 0) return 0; if (a1->p == NULL) From dfc80d3b697125a2d4b3694786ef9507245c52a6 Mon Sep 17 00:00:00 2001 From: George Karpenkov Date: Sun, 12 Jun 2016 14:14:11 +0200 Subject: [PATCH 03/17] Do not needlessly catch exceptions in Java bindings A lot of existing code in Java bindings catches exceptions just to silence them later. This is: a) Unnecessary: it is OK for a function to throw a RuntimeException without declaring it. b) Highly unidiomatic and not recommended by Java experts (see Effective Java and others) c) Confusing as has the potential to hide the existing bugs and have them resurface at the most inconvenient/unexpected moment. --- src/api/java/AST.java | 11 ++--------- src/api/java/ASTMap.java | 8 +------- src/api/java/ASTVector.java | 11 ++--------- src/api/java/ApplyResult.java | 11 ++--------- src/api/java/BitVecNum.java | 8 +------- src/api/java/FPNum.java | 8 +------- src/api/java/FiniteDomainNum.java | 8 +------- src/api/java/Fixedpoint.java | 8 +------- src/api/java/FuncDecl.java | 8 +------- src/api/java/Goal.java | 11 ++--------- src/api/java/IntNum.java | 11 ++--------- src/api/java/Model.java | 11 ++--------- src/api/java/ParamDescrs.java | 11 ++--------- src/api/java/Params.java | 8 +------- src/api/java/Pattern.java | 8 +------- src/api/java/RatNum.java | 11 ++--------- src/api/java/Solver.java | 10 ++-------- src/api/java/Sort.java | 12 +++--------- src/api/java/Statistics.java | 21 +++++---------------- 19 files changed, 34 insertions(+), 161 deletions(-) diff --git a/src/api/java/AST.java b/src/api/java/AST.java index e84dc8c81..f43aa85d2 100644 --- a/src/api/java/AST.java +++ b/src/api/java/AST.java @@ -175,15 +175,8 @@ public class AST extends Z3Object implements Comparable * A string representation of the AST. **/ @Override - public String toString() - { - try - { - return Native.astToString(getContext().nCtx(), getNativeObject()); - } catch (Z3Exception e) - { - return "Z3Exception: " + e.getMessage(); - } + public String toString() { + return Native.astToString(getContext().nCtx(), getNativeObject()); } /** diff --git a/src/api/java/ASTMap.java b/src/api/java/ASTMap.java index 7bc485bf5..a6201d8a0 100644 --- a/src/api/java/ASTMap.java +++ b/src/api/java/ASTMap.java @@ -104,13 +104,7 @@ class ASTMap extends Z3Object @Override public String toString() { - try - { - return Native.astMapToString(getContext().nCtx(), getNativeObject()); - } catch (Z3Exception e) - { - return "Z3Exception: " + e.getMessage(); - } + return Native.astMapToString(getContext().nCtx(), getNativeObject()); } ASTMap(Context ctx, long obj) diff --git a/src/api/java/ASTVector.java b/src/api/java/ASTVector.java index ab99e2aee..da1ab0f12 100644 --- a/src/api/java/ASTVector.java +++ b/src/api/java/ASTVector.java @@ -88,15 +88,8 @@ public class ASTVector extends Z3Object * Retrieves a string representation of the vector. **/ @Override - public String toString() - { - try - { - return Native.astVectorToString(getContext().nCtx(), getNativeObject()); - } catch (Z3Exception e) - { - return "Z3Exception: " + e.getMessage(); - } + public String toString() { + return Native.astVectorToString(getContext().nCtx(), getNativeObject()); } ASTVector(Context ctx, long obj) diff --git a/src/api/java/ApplyResult.java b/src/api/java/ApplyResult.java index 84c63e966..f598c9504 100644 --- a/src/api/java/ApplyResult.java +++ b/src/api/java/ApplyResult.java @@ -64,15 +64,8 @@ public class ApplyResult extends Z3Object * A string representation of the ApplyResult. **/ @Override - public String toString() - { - try - { - return Native.applyResultToString(getContext().nCtx(), getNativeObject()); - } catch (Z3Exception e) - { - return "Z3Exception: " + e.getMessage(); - } + public String toString() { + return Native.applyResultToString(getContext().nCtx(), getNativeObject()); } ApplyResult(Context ctx, long obj) diff --git a/src/api/java/BitVecNum.java b/src/api/java/BitVecNum.java index 5a62f8087..d6c176855 100644 --- a/src/api/java/BitVecNum.java +++ b/src/api/java/BitVecNum.java @@ -66,13 +66,7 @@ public class BitVecNum extends BitVecExpr @Override public String toString() { - try - { - return Native.getNumeralString(getContext().nCtx(), getNativeObject()); - } catch (Z3Exception e) - { - return "Z3Exception: " + e.getMessage(); - } + return Native.getNumeralString(getContext().nCtx(), getNativeObject()); } BitVecNum(Context ctx, long obj) diff --git a/src/api/java/FPNum.java b/src/api/java/FPNum.java index 69a44c559..9aeb41759 100644 --- a/src/api/java/FPNum.java +++ b/src/api/java/FPNum.java @@ -87,13 +87,7 @@ public class FPNum extends FPExpr */ public String toString() { - try - { - return Native.getNumeralString(getContext().nCtx(), getNativeObject()); - } catch (Z3Exception e) - { - return "Z3Exception: " + e.getMessage(); - } + return Native.getNumeralString(getContext().nCtx(), getNativeObject()); } } diff --git a/src/api/java/FiniteDomainNum.java b/src/api/java/FiniteDomainNum.java index e53ed22b2..68467e408 100644 --- a/src/api/java/FiniteDomainNum.java +++ b/src/api/java/FiniteDomainNum.java @@ -68,12 +68,6 @@ public class FiniteDomainNum extends FiniteDomainExpr @Override public String toString() { - try - { - return Native.getNumeralString(getContext().nCtx(), getNativeObject()); - } catch (Z3Exception e) - { - return "Z3Exception: " + e.getMessage(); - } + return Native.getNumeralString(getContext().nCtx(), getNativeObject()); } } diff --git a/src/api/java/Fixedpoint.java b/src/api/java/Fixedpoint.java index 14fb3a44a..2ff10a1f3 100644 --- a/src/api/java/Fixedpoint.java +++ b/src/api/java/Fixedpoint.java @@ -255,14 +255,8 @@ public class Fixedpoint extends Z3Object @Override public String toString() { - try - { - return Native.fixedpointToString(getContext().nCtx(), getNativeObject(), + return Native.fixedpointToString(getContext().nCtx(), getNativeObject(), 0, null); - } catch (Z3Exception e) - { - return "Z3Exception: " + e.getMessage(); - } } /** diff --git a/src/api/java/FuncDecl.java b/src/api/java/FuncDecl.java index 301978c44..273e853c0 100644 --- a/src/api/java/FuncDecl.java +++ b/src/api/java/FuncDecl.java @@ -47,13 +47,7 @@ public class FuncDecl extends AST @Override public String toString() { - try - { - return Native.funcDeclToString(getContext().nCtx(), getNativeObject()); - } catch (Z3Exception e) - { - return "Z3Exception: " + e.getMessage(); - } + return Native.funcDeclToString(getContext().nCtx(), getNativeObject()); } /** diff --git a/src/api/java/Goal.java b/src/api/java/Goal.java index 46b04f6bf..e60971179 100644 --- a/src/api/java/Goal.java +++ b/src/api/java/Goal.java @@ -211,15 +211,8 @@ public class Goal extends Z3Object * * @return A string representation of the Goal. **/ - public String toString() - { - try - { - return Native.goalToString(getContext().nCtx(), getNativeObject()); - } catch (Z3Exception e) - { - return "Z3Exception: " + e.getMessage(); - } + public String toString() { + return Native.goalToString(getContext().nCtx(), getNativeObject()); } /** diff --git a/src/api/java/IntNum.java b/src/api/java/IntNum.java index 71d878311..d3a5b456f 100644 --- a/src/api/java/IntNum.java +++ b/src/api/java/IntNum.java @@ -63,14 +63,7 @@ public class IntNum extends IntExpr /** * Returns a string representation of the numeral. **/ - public String toString() - { - try - { - return Native.getNumeralString(getContext().nCtx(), getNativeObject()); - } catch (Z3Exception e) - { - return "Z3Exception: " + e.getMessage(); - } + public String toString() { + return Native.getNumeralString(getContext().nCtx(), getNativeObject()); } } diff --git a/src/api/java/Model.java b/src/api/java/Model.java index 0695d7cf1..1bf77d246 100644 --- a/src/api/java/Model.java +++ b/src/api/java/Model.java @@ -283,15 +283,8 @@ public class Model extends Z3Object * @return A string representation of the model. **/ @Override - public String toString() - { - try - { - return Native.modelToString(getContext().nCtx(), getNativeObject()); - } catch (Z3Exception e) - { - return "Z3Exception: " + e.getMessage(); - } + public String toString() { + return Native.modelToString(getContext().nCtx(), getNativeObject()); } Model(Context ctx, long obj) diff --git a/src/api/java/ParamDescrs.java b/src/api/java/ParamDescrs.java index 8f8c6df0b..f265fb19e 100644 --- a/src/api/java/ParamDescrs.java +++ b/src/api/java/ParamDescrs.java @@ -82,15 +82,8 @@ public class ParamDescrs extends Z3Object * Retrieves a string representation of the ParamDescrs. **/ @Override - public String toString() - { - try - { - return Native.paramDescrsToString(getContext().nCtx(), getNativeObject()); - } catch (Z3Exception e) - { - return "Z3Exception: " + e.getMessage(); - } + public String toString() { + return Native.paramDescrsToString(getContext().nCtx(), getNativeObject()); } ParamDescrs(Context ctx, long obj) diff --git a/src/api/java/Params.java b/src/api/java/Params.java index 25d009b12..4be36c23d 100644 --- a/src/api/java/Params.java +++ b/src/api/java/Params.java @@ -115,13 +115,7 @@ public class Params extends Z3Object @Override public String toString() { - try - { - return Native.paramsToString(getContext().nCtx(), getNativeObject()); - } catch (Z3Exception e) - { - return "Z3Exception: " + e.getMessage(); - } + return Native.paramsToString(getContext().nCtx(), getNativeObject()); } Params(Context ctx) diff --git a/src/api/java/Pattern.java b/src/api/java/Pattern.java index eb12b6448..852ffcd0f 100644 --- a/src/api/java/Pattern.java +++ b/src/api/java/Pattern.java @@ -53,13 +53,7 @@ public class Pattern extends AST @Override public String toString() { - try - { - return Native.patternToString(getContext().nCtx(), getNativeObject()); - } catch (Z3Exception e) - { - return "Z3Exception: " + e.getMessage(); - } + return Native.patternToString(getContext().nCtx(), getNativeObject()); } Pattern(Context ctx, long obj) diff --git a/src/api/java/RatNum.java b/src/api/java/RatNum.java index f44823a2b..2bf1b28dd 100644 --- a/src/api/java/RatNum.java +++ b/src/api/java/RatNum.java @@ -75,15 +75,8 @@ public class RatNum extends RealExpr * Returns a string representation of the numeral. **/ @Override - public String toString() - { - try - { - return Native.getNumeralString(getContext().nCtx(), getNativeObject()); - } catch (Z3Exception e) - { - return "Z3Exception: " + e.getMessage(); - } + public String toString() { + return Native.getNumeralString(getContext().nCtx(), getNativeObject()); } RatNum(Context ctx, long obj) diff --git a/src/api/java/Solver.java b/src/api/java/Solver.java index ea76637c8..431811b8d 100644 --- a/src/api/java/Solver.java +++ b/src/api/java/Solver.java @@ -323,14 +323,8 @@ public class Solver extends Z3Object @Override public String toString() { - try - { - return Native - .solverToString(getContext().nCtx(), getNativeObject()); - } catch (Z3Exception e) - { - return "Z3Exception: " + e.getMessage(); - } + return Native + .solverToString(getContext().nCtx(), getNativeObject()); } Solver(Context ctx, long obj) diff --git a/src/api/java/Sort.java b/src/api/java/Sort.java index e30e0b8b3..30a43e7dd 100644 --- a/src/api/java/Sort.java +++ b/src/api/java/Sort.java @@ -82,15 +82,9 @@ public class Sort extends AST /** * A string representation of the sort. **/ - public String toString() - { - try - { - return Native.sortToString(getContext().nCtx(), getNativeObject()); - } catch (Z3Exception e) - { - return "Z3Exception: " + e.getMessage(); - } + @Override + public String toString() { + return Native.sortToString(getContext().nCtx(), getNativeObject()); } /** diff --git a/src/api/java/Statistics.java b/src/api/java/Statistics.java index 5af0cf863..1e842a892 100644 --- a/src/api/java/Statistics.java +++ b/src/api/java/Statistics.java @@ -84,15 +84,9 @@ public class Statistics extends Z3Object /** * The string representation of the Entry. **/ - public String toString() - { - try - { - return Key + ": " + getValueString(); - } catch (Z3Exception e) - { - return "Z3Exception: " + e.getMessage(); - } + @Override + public String toString() { + return Key + ": " + getValueString(); } private boolean m_is_int = false; @@ -118,15 +112,10 @@ public class Statistics extends Z3Object /** * A string representation of the statistical data. **/ + @Override public String toString() { - try - { - return Native.statsToString(getContext().nCtx(), getNativeObject()); - } catch (Z3Exception e) - { - return "Z3Exception: " + e.getMessage(); - } + return Native.statsToString(getContext().nCtx(), getNativeObject()); } /** From 495ef0f055f300089ec57f7aa71c2cc48d0fd402 Mon Sep 17 00:00:00 2001 From: George Karpenkov Date: Sun, 12 Jun 2016 14:18:13 +0200 Subject: [PATCH 04/17] Java bindings with no finalizers Replacing finalizers with PhantomReferences, required quite a lot of changes to the codebase. --- src/api/java/AST.java | 25 +-- src/api/java/ASTDecRefQueue.java | 25 +-- src/api/java/ASTMap.java | 11 +- src/api/java/ASTVector.java | 11 +- src/api/java/ApplyResult.java | 14 +- src/api/java/ApplyResultDecRefQueue.java | 25 +-- src/api/java/AstMapDecRefQueue.java | 25 +-- src/api/java/AstVectorDecRefQueue.java | 25 +-- src/api/java/BoolExpr.java | 10 +- src/api/java/Constructor.java | 44 ++--- src/api/java/ConstructorList.java | 25 +-- src/api/java/Context.java | 176 +++++++++---------- src/api/java/EnumSort.java | 12 +- src/api/java/Expr.java | 25 +-- src/api/java/FPNum.java | 6 +- src/api/java/Fixedpoint.java | 13 +- src/api/java/FixedpointDecRefQueue.java | 21 +-- src/api/java/FuncInterp.java | 86 +++------ src/api/java/FuncInterpDecRefQueue.java | 25 +-- src/api/java/FuncInterpEntryDecRefQueue.java | 25 +-- src/api/java/Goal.java | 25 +-- src/api/java/GoalDecRefQueue.java | 23 +-- src/api/java/IDecRefQueue.java | 59 ++++--- src/api/java/IDisposable.java | 25 --- src/api/java/InterpolationContext.java | 21 ++- src/api/java/ListSort.java | 15 +- src/api/java/Model.java | 14 +- src/api/java/ModelDecRefQueue.java | 25 +-- src/api/java/Optimize.java | 15 +- src/api/java/OptimizeDecRefQueue.java | 26 +-- src/api/java/ParamDescrs.java | 14 +- src/api/java/ParamDescrsDecRefQueue.java | 25 +-- src/api/java/Params.java | 14 +- src/api/java/ParamsDecRefQueue.java | 25 +-- src/api/java/Probe.java | 11 +- src/api/java/ProbeDecRefQueue.java | 22 +-- src/api/java/Quantifier.java | 73 ++++---- src/api/java/Solver.java | 20 +-- src/api/java/SolverDecRefQueue.java | 25 +-- src/api/java/Sort.java | 1 + src/api/java/Statistics.java | 14 +- src/api/java/StatisticsDecRefQueue.java | 25 +-- src/api/java/StringSymbol.java | 4 +- src/api/java/Symbol.java | 25 ++- src/api/java/Tactic.java | 11 +- src/api/java/TacticDecRefQueue.java | 25 +-- src/api/java/TupleSort.java | 8 +- src/api/java/Z3Object.java | 88 ++-------- 48 files changed, 368 insertions(+), 939 deletions(-) delete mode 100644 src/api/java/IDisposable.java diff --git a/src/api/java/AST.java b/src/api/java/AST.java index f43aa85d2..4b5b37d46 100644 --- a/src/api/java/AST.java +++ b/src/api/java/AST.java @@ -187,34 +187,15 @@ public class AST extends Z3Object implements Comparable return Native.astToString(getContext().nCtx(), getNativeObject()); } - AST(Context ctx) - { - super(ctx); - } - - AST(Context ctx, long obj) - { + AST(Context ctx, long obj) { super(ctx, obj); } @Override void incRef(long o) { - // Console.WriteLine("AST IncRef()"); - if (getContext() == null || o == 0) - return; - getContext().getASTDRQ().incAndClear(getContext(), o); - super.incRef(o); - } - - @Override - void decRef(long o) - { - // Console.WriteLine("AST DecRef()"); - if (getContext() == null || o == 0) - return; - getContext().getASTDRQ().add(o); - super.decRef(o); + Native.incRef(getContext().nCtx(), o); + getContext().getASTDRQ().storeReference(getContext(), this); } static AST create(Context ctx, long obj) diff --git a/src/api/java/ASTDecRefQueue.java b/src/api/java/ASTDecRefQueue.java index 32f6a5d0e..d462e16d5 100644 --- a/src/api/java/ASTDecRefQueue.java +++ b/src/api/java/ASTDecRefQueue.java @@ -17,7 +17,7 @@ Notes: package com.microsoft.z3; -class ASTDecRefQueue extends IDecRefQueue +class ASTDecRefQueue extends IDecRefQueue { public ASTDecRefQueue() { @@ -30,26 +30,7 @@ class ASTDecRefQueue extends IDecRefQueue } @Override - protected void incRef(Context ctx, long obj) - { - try - { - Native.incRef(ctx.nCtx(), obj); - } catch (Z3Exception e) - { - // OK. - } - } - - @Override - protected void decRef(Context ctx, long obj) - { - try - { - Native.decRef(ctx.nCtx(), obj); - } catch (Z3Exception e) - { - // OK. - } + protected void decRef(Context ctx, long obj) { + Native.decRef(ctx.nCtx(), obj); } }; diff --git a/src/api/java/ASTMap.java b/src/api/java/ASTMap.java index a6201d8a0..b4ae7102a 100644 --- a/src/api/java/ASTMap.java +++ b/src/api/java/ASTMap.java @@ -120,14 +120,7 @@ class ASTMap extends Z3Object @Override void incRef(long o) { - getContext().getASTMapDRQ().incAndClear(getContext(), o); - super.incRef(o); - } - - @Override - void decRef(long o) - { - getContext().getASTMapDRQ().add(o); - super.decRef(o); + Native.astMapIncRef(getContext().nCtx(), o); + getContext().getASTMapDRQ().storeReference(getContext(), this); } } diff --git a/src/api/java/ASTVector.java b/src/api/java/ASTVector.java index da1ab0f12..7c5ca1067 100644 --- a/src/api/java/ASTVector.java +++ b/src/api/java/ASTVector.java @@ -105,17 +105,10 @@ public class ASTVector extends Z3Object @Override void incRef(long o) { - getContext().getASTVectorDRQ().incAndClear(getContext(), o); - super.incRef(o); + Native.astVectorIncRef(getContext().nCtx(), o); + getContext().getASTVectorDRQ().storeReference(getContext(), this); } - @Override - void decRef(long o) - { - getContext().getASTVectorDRQ().add(o); - super.decRef(o); - } - /** * Translates the AST vector into an AST[] * */ diff --git a/src/api/java/ApplyResult.java b/src/api/java/ApplyResult.java index f598c9504..8b3c1daf6 100644 --- a/src/api/java/ApplyResult.java +++ b/src/api/java/ApplyResult.java @@ -74,16 +74,8 @@ public class ApplyResult extends Z3Object } @Override - void incRef(long o) - { - getContext().getApplyResultDRQ().incAndClear(getContext(), o); - super.incRef(o); - } - - @Override - void decRef(long o) - { - getContext().getApplyResultDRQ().add(o); - super.decRef(o); + void incRef(long o) { + Native.applyResultIncRef(getContext().nCtx(), o); + getContext().getApplyResultDRQ().storeReference(getContext(), this); } } diff --git a/src/api/java/ApplyResultDecRefQueue.java b/src/api/java/ApplyResultDecRefQueue.java index 63f315ecd..d28ff755e 100644 --- a/src/api/java/ApplyResultDecRefQueue.java +++ b/src/api/java/ApplyResultDecRefQueue.java @@ -17,7 +17,7 @@ Notes: package com.microsoft.z3; -class ApplyResultDecRefQueue extends IDecRefQueue +class ApplyResultDecRefQueue extends IDecRefQueue { public ApplyResultDecRefQueue() { @@ -30,26 +30,7 @@ class ApplyResultDecRefQueue extends IDecRefQueue } @Override - protected void incRef(Context ctx, long obj) - { - try - { - Native.applyResultIncRef(ctx.nCtx(), obj); - } catch (Z3Exception e) - { - // OK. - } - } - - @Override - protected void decRef(Context ctx, long obj) - { - try - { - Native.applyResultDecRef(ctx.nCtx(), obj); - } catch (Z3Exception e) - { - // OK. - } + protected void decRef(Context ctx, long obj) { + Native.applyResultDecRef(ctx.nCtx(), obj); } }; diff --git a/src/api/java/AstMapDecRefQueue.java b/src/api/java/AstMapDecRefQueue.java index 1598f75e7..234b7eec4 100644 --- a/src/api/java/AstMapDecRefQueue.java +++ b/src/api/java/AstMapDecRefQueue.java @@ -17,7 +17,7 @@ Notes: package com.microsoft.z3; -class ASTMapDecRefQueue extends IDecRefQueue +class ASTMapDecRefQueue extends IDecRefQueue { public ASTMapDecRefQueue() { @@ -30,26 +30,7 @@ class ASTMapDecRefQueue extends IDecRefQueue } @Override - protected void incRef(Context ctx, long obj) - { - try - { - Native.astMapIncRef(ctx.nCtx(), obj); - } catch (Z3Exception e) - { - // OK. - } - } - - @Override - protected void decRef(Context ctx, long obj) - { - try - { - Native.astMapDecRef(ctx.nCtx(), obj); - } catch (Z3Exception e) - { - // OK. - } + protected void decRef(Context ctx, long obj) { + Native.astMapDecRef(ctx.nCtx(), obj); } }; diff --git a/src/api/java/AstVectorDecRefQueue.java b/src/api/java/AstVectorDecRefQueue.java index a63d808d3..3a486ee06 100644 --- a/src/api/java/AstVectorDecRefQueue.java +++ b/src/api/java/AstVectorDecRefQueue.java @@ -17,7 +17,7 @@ Notes: package com.microsoft.z3; -class ASTVectorDecRefQueue extends IDecRefQueue +class ASTVectorDecRefQueue extends IDecRefQueue { public ASTVectorDecRefQueue() { @@ -30,26 +30,7 @@ class ASTVectorDecRefQueue extends IDecRefQueue } @Override - protected void incRef(Context ctx, long obj) - { - try - { - Native.astVectorIncRef(ctx.nCtx(), obj); - } catch (Z3Exception e) - { - // OK. - } - } - - @Override - protected void decRef(Context ctx, long obj) - { - try - { - Native.astVectorDecRef(ctx.nCtx(), obj); - } catch (Z3Exception e) - { - // OK. - } + protected void decRef(Context ctx, long obj) { + Native.astVectorDecRef(ctx.nCtx(), obj); } }; diff --git a/src/api/java/BoolExpr.java b/src/api/java/BoolExpr.java index 02eabd2b5..dc75b2e7c 100644 --- a/src/api/java/BoolExpr.java +++ b/src/api/java/BoolExpr.java @@ -20,15 +20,7 @@ package com.microsoft.z3; /** * Boolean expressions **/ -public class BoolExpr extends Expr -{ - /** - * Constructor for BoolExpr - **/ - protected BoolExpr(Context ctx) - { - super(ctx); - } +public class BoolExpr extends Expr { /** * Constructor for BoolExpr diff --git a/src/api/java/Constructor.java b/src/api/java/Constructor.java index a6c2856d4..28558b15a 100644 --- a/src/api/java/Constructor.java +++ b/src/api/java/Constructor.java @@ -20,8 +20,14 @@ package com.microsoft.z3; /** * Constructors are used for datatype sorts. **/ -public class Constructor extends Z3Object -{ +public class Constructor extends Z3Object { + private final int n; + + Constructor(Context ctx, int n, long nativeObj) { + super(ctx, nativeObj); + this.n = n; + } + /** * The number of fields of the constructor. * @throws Z3Exception @@ -78,29 +84,16 @@ public class Constructor extends Z3Object return t; } - /** - * Destructor. - * @throws Throwable - * @throws Z3Exception on error - **/ - protected void finalize() throws Throwable - { - try { - Native.delConstructor(getContext().nCtx(), getNativeObject()); - } finally { - super.finalize(); - } + @Override + void incRef(long o) { + + // Datatype constructors are not reference counted. + getContext().getConstructorDRQ().storeReference(getContext(), this); } - private int n = 0; - - Constructor(Context ctx, Symbol name, Symbol recognizer, - Symbol[] fieldNames, Sort[] sorts, int[] sortRefs) - - { - super(ctx); - - n = AST.arrayLength(fieldNames); + static Constructor of(Context ctx, Symbol name, Symbol recognizer, + Symbol[] fieldNames, Sort[] sorts, int[] sortRefs) { + int n = AST.arrayLength(fieldNames); if (n != AST.arrayLength(sorts)) throw new Z3Exception( @@ -112,9 +105,10 @@ public class Constructor extends Z3Object if (sortRefs == null) sortRefs = new int[n]; - setNativeObject(Native.mkConstructor(ctx.nCtx(), name.getNativeObject(), + long nativeObj = Native.mkConstructor(ctx.nCtx(), name.getNativeObject(), recognizer.getNativeObject(), n, Symbol.arrayToNative(fieldNames), - Sort.arrayToNative(sorts), sortRefs)); + Sort.arrayToNative(sorts), sortRefs); + return new Constructor(ctx, n, nativeObj); } } diff --git a/src/api/java/ConstructorList.java b/src/api/java/ConstructorList.java index fe3fae1ac..3f1835082 100644 --- a/src/api/java/ConstructorList.java +++ b/src/api/java/ConstructorList.java @@ -20,32 +20,21 @@ package com.microsoft.z3; /** * Lists of constructors **/ -public class ConstructorList extends Z3Object -{ - /** - * Destructor. - * @throws Throwable - * @throws Z3Exception on error - **/ - protected void finalize() throws Throwable - { - try { - Native.delConstructorList(getContext().nCtx(), getNativeObject()); - } finally { - super.finalize(); - } - } +public class ConstructorList extends Z3Object { ConstructorList(Context ctx, long obj) { super(ctx, obj); } + @Override + void incRef(long o) { + getContext().getConstructorListDRQ().storeReference(getContext(), this); + } + ConstructorList(Context ctx, Constructor[] constructors) { - super(ctx); - - setNativeObject(Native.mkConstructorList(getContext().nCtx(), + super(ctx, Native.mkConstructorList(ctx.nCtx(), constructors.length, Constructor.arrayToNative(constructors))); } diff --git a/src/api/java/Context.java b/src/api/java/Context.java index 9fa17fcd4..41fb027fe 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -17,34 +17,35 @@ Notes: package com.microsoft.z3; -import java.util.Map; -import java.util.concurrent.atomic.AtomicInteger; +import static com.microsoft.z3.Constructor.of; import com.microsoft.z3.enumerations.Z3_ast_print_mode; +import java.util.Map; + /** * The main interaction with Z3 happens via the Context. **/ -public class Context extends IDisposable -{ - /** - * Constructor. - **/ - public Context() - { - super(); - synchronized (creation_lock) { +public class Context implements AutoCloseable { + private final long m_ctx; + static final Object creation_lock = new Object(); + + public static Context mkContext() { + long m_ctx; + synchronized (creation_lock) { m_ctx = Native.mkContextRc(0); - initContext(); + // TODO: then adding settings will not be under the lock. } + return new Context(m_ctx); } + /** * Constructor. * Remarks: - * The following parameters can be set: + * The following parameters can be set: * - proof (Boolean) Enable proof generation - * - debug_ref_count (Boolean) Enable debug support for Z3_ast reference counting + * - debug_ref_count (Boolean) Enable debug support for Z3_ast reference counting * - trace (Boolean) Tracing support for VCC * - trace_file_name (String) Trace out file for VCC traces * - timeout (unsigned) default timeout (in milliseconds) used for solvers @@ -53,20 +54,32 @@ public class Context extends IDisposable * - model model generation for solvers, this parameter can be overwritten when creating a solver * - model_validate validate models produced by solvers * - unsat_core unsat-core generation for solvers, this parameter can be overwritten when creating a solver - * Note that in previous versions of Z3, this constructor was also used to set global and + * Note that in previous versions of Z3, this constructor was also used to set global and * module parameters. For this purpose we should now use {@code Global.setParameter} **/ - public Context(Map settings) + public static Context mkContext(Map settings) { - super(); - synchronized (creation_lock) { + long m_ctx; + synchronized (creation_lock) { long cfg = Native.mkConfig(); for (Map.Entry kv : settings.entrySet()) Native.setParamValue(cfg, kv.getKey(), kv.getValue()); m_ctx = Native.mkContextRc(cfg); Native.delConfig(cfg); - initContext(); } + return new Context(m_ctx); + } + + /** + * Constructor. + **/ + protected Context(long m_ctx) + { + this.m_ctx = m_ctx; + + // Code which used to be in "initContext". + setPrintMode(Z3_ast_print_mode.Z3_PRINT_SMTLIB2_COMPLIANT); + Native.setInternalErrorHandler(m_ctx); } /** @@ -242,7 +255,7 @@ public class Context extends IDisposable checkContextMatch(name); checkContextMatch(fieldNames); checkContextMatch(fieldSorts); - return new TupleSort(this, name, (int) fieldNames.length, fieldNames, + return new TupleSort(this, name, fieldNames.length, fieldNames, fieldSorts); } @@ -319,8 +332,7 @@ public class Context extends IDisposable Symbol[] fieldNames, Sort[] sorts, int[] sortRefs) { - - return new Constructor(this, name, recognizer, fieldNames, sorts, + return of(this, name, recognizer, fieldNames, sorts, sortRefs); } @@ -329,10 +341,8 @@ public class Context extends IDisposable **/ public Constructor mkConstructor(String name, String recognizer, String[] fieldNames, Sort[] sorts, int[] sortRefs) - { - - return new Constructor(this, mkSymbol(name), mkSymbol(recognizer), + return of(this, mkSymbol(name), mkSymbol(recognizer), mkSymbols(fieldNames), sorts, sortRefs); } @@ -525,7 +535,7 @@ public class Context extends IDisposable throw new Z3Exception("Cannot create a pattern from zero terms"); long[] termsNative = AST.arrayToNative(terms); - return new Pattern(this, Native.mkPattern(nCtx(), (int) terms.length, + return new Pattern(this, Native.mkPattern(nCtx(), terms.length, termsNative)); } @@ -688,7 +698,7 @@ public class Context extends IDisposable public BoolExpr mkDistinct(Expr... args) { checkContextMatch(args); - return new BoolExpr(this, Native.mkDistinct(nCtx(), (int) args.length, + return new BoolExpr(this, Native.mkDistinct(nCtx(), args.length, AST.arrayToNative(args))); } @@ -756,7 +766,7 @@ public class Context extends IDisposable public BoolExpr mkAnd(BoolExpr... t) { checkContextMatch(t); - return new BoolExpr(this, Native.mkAnd(nCtx(), (int) t.length, + return new BoolExpr(this, Native.mkAnd(nCtx(), t.length, AST.arrayToNative(t))); } @@ -766,7 +776,7 @@ public class Context extends IDisposable public BoolExpr mkOr(BoolExpr... t) { checkContextMatch(t); - return new BoolExpr(this, Native.mkOr(nCtx(), (int) t.length, + return new BoolExpr(this, Native.mkOr(nCtx(), t.length, AST.arrayToNative(t))); } @@ -777,7 +787,7 @@ public class Context extends IDisposable { checkContextMatch(t); return (ArithExpr) Expr.create(this, - Native.mkAdd(nCtx(), (int) t.length, AST.arrayToNative(t))); + Native.mkAdd(nCtx(), t.length, AST.arrayToNative(t))); } /** @@ -787,7 +797,7 @@ public class Context extends IDisposable { checkContextMatch(t); return (ArithExpr) Expr.create(this, - Native.mkMul(nCtx(), (int) t.length, AST.arrayToNative(t))); + Native.mkMul(nCtx(), t.length, AST.arrayToNative(t))); } /** @@ -797,7 +807,7 @@ public class Context extends IDisposable { checkContextMatch(t); return (ArithExpr) Expr.create(this, - Native.mkSub(nCtx(), (int) t.length, AST.arrayToNative(t))); + Native.mkSub(nCtx(), t.length, AST.arrayToNative(t))); } /** @@ -1814,7 +1824,7 @@ public class Context extends IDisposable { checkContextMatch(args); return (ArrayExpr)Expr.create(this, - Native.mkSetUnion(nCtx(), (int) args.length, + Native.mkSetUnion(nCtx(), args.length, AST.arrayToNative(args))); } @@ -1825,7 +1835,7 @@ public class Context extends IDisposable { checkContextMatch(args); return (ArrayExpr)Expr.create(this, - Native.mkSetIntersect(nCtx(), (int) args.length, + Native.mkSetIntersect(nCtx(), args.length, AST.arrayToNative(args))); } @@ -1912,7 +1922,7 @@ public class Context extends IDisposable public SeqExpr MkConcat(SeqExpr... t) { checkContextMatch(t); - return new SeqExpr(this, Native.mkSeqConcat(nCtx(), (int)t.length, AST.arrayToNative(t))); + return new SeqExpr(this, Native.mkSeqConcat(nCtx(), t.length, AST.arrayToNative(t))); } @@ -2040,7 +2050,7 @@ public class Context extends IDisposable public ReExpr MkConcat(ReExpr... t) { checkContextMatch(t); - return new ReExpr(this, Native.mkReConcat(nCtx(), (int)t.length, AST.arrayToNative(t))); + return new ReExpr(this, Native.mkReConcat(nCtx(), t.length, AST.arrayToNative(t))); } /** @@ -2049,7 +2059,7 @@ public class Context extends IDisposable public ReExpr MkUnion(ReExpr... t) { checkContextMatch(t); - return new ReExpr(this, Native.mkReUnion(nCtx(), (int)t.length, AST.arrayToNative(t))); + return new ReExpr(this, Native.mkReUnion(nCtx(), t.length, AST.arrayToNative(t))); } @@ -2258,7 +2268,7 @@ public class Context extends IDisposable Symbol quantifierID, Symbol skolemID) { - return new Quantifier(this, true, sorts, names, body, weight, patterns, + return Quantifier.of(this, true, sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID); } @@ -2271,7 +2281,7 @@ public class Context extends IDisposable Symbol skolemID) { - return new Quantifier(this, true, boundConstants, body, weight, + return Quantifier.of(this, true, boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID); } @@ -2284,7 +2294,7 @@ public class Context extends IDisposable Symbol quantifierID, Symbol skolemID) { - return new Quantifier(this, false, sorts, names, body, weight, + return Quantifier.of(this, false, sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID); } @@ -2297,7 +2307,7 @@ public class Context extends IDisposable Symbol skolemID) { - return new Quantifier(this, false, boundConstants, body, weight, + return Quantifier.of(this, false, boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID); } @@ -3814,7 +3824,7 @@ public class Context extends IDisposable * must be a native object obtained from Z3 (e.g., through * {@code UnwrapAST}) and that it must have a correct reference count. * @see Native#incRef - * @see unwrapAST + * @see #unwrapAST * @param nativeObject The native pointer to wrap. **/ public AST wrapAST(long nativeObject) @@ -3869,19 +3879,12 @@ public class Context extends IDisposable Native.updateParamValue(nCtx(), id, value); } - protected long m_ctx = 0; - protected static final Object creation_lock = new Object(); long nCtx() { return m_ctx; } - void initContext() - { - setPrintMode(Z3_ast_print_mode.Z3_PRINT_SMTLIB2_COMPLIANT); - Native.setInternalErrorHandler(nCtx()); - } void checkContextMatch(Z3Object other) { @@ -3925,110 +3928,103 @@ public class Context extends IDisposable private TacticDecRefQueue m_Tactic_DRQ = new TacticDecRefQueue(10); private FixedpointDecRefQueue m_Fixedpoint_DRQ = new FixedpointDecRefQueue(10); private OptimizeDecRefQueue m_Optimize_DRQ = new OptimizeDecRefQueue(10); + private ConstructorDecRefQueue m_Constructor_DRQ = new ConstructorDecRefQueue(10); + private ConstructorListDecRefQueue m_ConstructorList_DRQ = + new ConstructorListDecRefQueue(10); - public IDecRefQueue getASTDRQ() + public IDecRefQueue getConstructorDRQ() { + return m_Constructor_DRQ; + } + + public IDecRefQueue getConstructorListDRQ() { + return m_ConstructorList_DRQ; + } + + public IDecRefQueue getASTDRQ() { return m_AST_DRQ; } - public IDecRefQueue getASTMapDRQ() + public IDecRefQueue getASTMapDRQ() { return m_ASTMap_DRQ; } - public IDecRefQueue getASTVectorDRQ() + public IDecRefQueue getASTVectorDRQ() { return m_ASTVector_DRQ; } - public IDecRefQueue getApplyResultDRQ() + public IDecRefQueue getApplyResultDRQ() { return m_ApplyResult_DRQ; } - public IDecRefQueue getFuncEntryDRQ() + public IDecRefQueue getFuncEntryDRQ() { return m_FuncEntry_DRQ; } - public IDecRefQueue getFuncInterpDRQ() + public IDecRefQueue getFuncInterpDRQ() { return m_FuncInterp_DRQ; } - public IDecRefQueue getGoalDRQ() + public IDecRefQueue getGoalDRQ() { return m_Goal_DRQ; } - public IDecRefQueue getModelDRQ() + public IDecRefQueue getModelDRQ() { return m_Model_DRQ; } - public IDecRefQueue getParamsDRQ() + public IDecRefQueue getParamsDRQ() { return m_Params_DRQ; } - public IDecRefQueue getParamDescrsDRQ() + public IDecRefQueue getParamDescrsDRQ() { return m_ParamDescrs_DRQ; } - public IDecRefQueue getProbeDRQ() + public IDecRefQueue getProbeDRQ() { return m_Probe_DRQ; } - public IDecRefQueue getSolverDRQ() + public IDecRefQueue getSolverDRQ() { return m_Solver_DRQ; } - public IDecRefQueue getStatisticsDRQ() + public IDecRefQueue getStatisticsDRQ() { return m_Statistics_DRQ; } - public IDecRefQueue getTacticDRQ() + public IDecRefQueue getTacticDRQ() { return m_Tactic_DRQ; } - public IDecRefQueue getFixedpointDRQ() + public IDecRefQueue getFixedpointDRQ() { return m_Fixedpoint_DRQ; } - public IDecRefQueue getOptimizeDRQ() + public IDecRefQueue getOptimizeDRQ() { return m_Optimize_DRQ; } - protected AtomicInteger m_refCount = new AtomicInteger(0); - - /** - * Finalizer. - * @throws Throwable - **/ - protected void finalize() throws Throwable - { - try { - dispose(); - } - catch (Throwable t) { - throw t; - } - finally { - super.finalize(); - } - } - /** * Disposes of the context. **/ - public void dispose() + @Override + public void close() { m_AST_DRQ.clear(this); m_ASTMap_DRQ.clear(this); @@ -4052,15 +4048,7 @@ public class Context extends IDisposable m_stringSort = null; synchronized (creation_lock) { - if (m_refCount.get() == 0 && m_ctx != 0) { - try { - Native.delContext(m_ctx); - } catch (Z3Exception e) { - // OK? - System.out.println("Context deletion failed; memory leak possible."); - } - m_ctx = 0; - } + Native.delContext(m_ctx); } } } diff --git a/src/api/java/EnumSort.java b/src/api/java/EnumSort.java index bb60eef56..ce2f8d578 100644 --- a/src/api/java/EnumSort.java +++ b/src/api/java/EnumSort.java @@ -92,13 +92,9 @@ public class EnumSort extends Sort EnumSort(Context ctx, Symbol name, Symbol[] enumNames) { - super(ctx, 0); - - int n = enumNames.length; - long[] n_constdecls = new long[n]; - long[] n_testers = new long[n]; - setNativeObject(Native.mkEnumerationSort(ctx.nCtx(), - name.getNativeObject(), n, Symbol.arrayToNative(enumNames), - n_constdecls, n_testers)); + super(ctx, Native.mkEnumerationSort(ctx.nCtx(), + name.getNativeObject(), enumNames.length, + Symbol.arrayToNative(enumNames), + new long[enumNames.length], new long[enumNames.length])); } }; diff --git a/src/api/java/Expr.java b/src/api/java/Expr.java index b24d3ac62..ea3fd2147 100644 --- a/src/api/java/Expr.java +++ b/src/api/java/Expr.java @@ -120,13 +120,13 @@ public class Expr extends AST * @param args arguments * @throws Z3Exception on error **/ - public void update(Expr[] args) + public Expr update(Expr[] args) { getContext().checkContextMatch(args); if (isApp() && args.length != getNumArgs()) { throw new Z3Exception("Number of arguments does not match"); } - setNativeObject(Native.updateTerm(getContext().nCtx(), getNativeObject(), + return new Expr(getContext(), Native.updateTerm(getContext().nCtx(), getNativeObject(), args.length, Expr.arrayToNative(args))); } @@ -2091,36 +2091,23 @@ public class Expr extends AST **/ public int getIndex() { - if (!isVar()) + if (!isVar()) { throw new Z3Exception("Term is not a bound variable."); + } return Native.getIndexValue(getContext().nCtx(), getNativeObject()); } - /** - * Constructor for Expr - **/ - protected Expr(Context ctx) - { - super(ctx); - { - } - } - /** * Constructor for Expr * @throws Z3Exception on error **/ - protected Expr(Context ctx, long obj) - { + protected Expr(Context ctx, long obj) { super(ctx, obj); - { - } } @Override - void checkNativeObject(long obj) - { + void checkNativeObject(long obj) { if (!Native.isApp(getContext().nCtx(), obj) && Native.getAstKind(getContext().nCtx(), obj) != Z3_ast_kind.Z3_VAR_AST.toInt() && Native.getAstKind(getContext().nCtx(), obj) != Z3_ast_kind.Z3_QUANTIFIER_AST.toInt()) { diff --git a/src/api/java/FPNum.java b/src/api/java/FPNum.java index 9aeb41759..402d25ebe 100644 --- a/src/api/java/FPNum.java +++ b/src/api/java/FPNum.java @@ -28,7 +28,7 @@ public class FPNum extends FPExpr */ public boolean getSign() { Native.IntPtr res = new Native.IntPtr(); - if (Native.fpaGetNumeralSign(getContext().nCtx(), getNativeObject(), res) ^ true) + if (!Native.fpaGetNumeralSign(getContext().nCtx(), getNativeObject(), res)) throw new Z3Exception("Sign is not a Boolean value"); return res.value != 0; } @@ -53,7 +53,7 @@ public class FPNum extends FPExpr public long getSignificandUInt64() { Native.LongPtr res = new Native.LongPtr(); - if (Native.fpaGetNumeralSignificandUint64(getContext().nCtx(), getNativeObject(), res) ^ true) + if (!Native.fpaGetNumeralSignificandUint64(getContext().nCtx(), getNativeObject(), res)) throw new Z3Exception("Significand is not a 64 bit unsigned integer"); return res.value; } @@ -72,7 +72,7 @@ public class FPNum extends FPExpr */ public long getExponentInt64() { Native.LongPtr res = new Native.LongPtr(); - if (Native.fpaGetNumeralExponentInt64(getContext().nCtx(), getNativeObject(), res) ^ true) + if (!Native.fpaGetNumeralExponentInt64(getContext().nCtx(), getNativeObject(), res)) throw new Z3Exception("Exponent is not a 64 bit integer"); return res.value; } diff --git a/src/api/java/Fixedpoint.java b/src/api/java/Fixedpoint.java index 2ff10a1f3..5a7958364 100644 --- a/src/api/java/Fixedpoint.java +++ b/src/api/java/Fixedpoint.java @@ -349,16 +349,11 @@ public class Fixedpoint extends Z3Object } @Override - void incRef(long o) - { - getContext().getFixedpointDRQ().incAndClear(getContext(), o); - super.incRef(o); + void incRef(long o) { + Native.fixedpointIncRef(getContext().nCtx(), o); + getContext().getFixedpointDRQ().storeReference(getContext(), this); } @Override - void decRef(long o) - { - getContext().getFixedpointDRQ().add(o); - super.decRef(o); - } + void checkNativeObject(long obj) { } } diff --git a/src/api/java/FixedpointDecRefQueue.java b/src/api/java/FixedpointDecRefQueue.java index e65538a30..d5ae79a2b 100644 --- a/src/api/java/FixedpointDecRefQueue.java +++ b/src/api/java/FixedpointDecRefQueue.java @@ -17,7 +17,7 @@ Notes: package com.microsoft.z3; -class FixedpointDecRefQueue extends IDecRefQueue +class FixedpointDecRefQueue extends IDecRefQueue { public FixedpointDecRefQueue() { @@ -29,27 +29,10 @@ class FixedpointDecRefQueue extends IDecRefQueue super(move_limit); } - @Override - protected void incRef(Context ctx, long obj) - { - try - { - Native.fixedpointIncRef(ctx.nCtx(), obj); - } catch (Z3Exception e) - { - // OK. - } - } @Override protected void decRef(Context ctx, long obj) { - try - { - Native.fixedpointDecRef(ctx.nCtx(), obj); - } catch (Z3Exception e) - { - // OK. - } + Native.fixedpointDecRef(ctx.nCtx(), obj); } }; diff --git a/src/api/java/FuncInterp.java b/src/api/java/FuncInterp.java index 72f6bb25d..c84979aa1 100644 --- a/src/api/java/FuncInterp.java +++ b/src/api/java/FuncInterp.java @@ -73,18 +73,12 @@ public class FuncInterp extends Z3Object @Override public String toString() { - try - { - int n = getNumArgs(); - String res = "["; - Expr[] args = getArgs(); - for (int i = 0; i < n; i++) - res += args[i] + ", "; - return res + getValue() + "]"; - } catch (Z3Exception e) - { - return "Z3Exception: " + e.getMessage(); - } + int n = getNumArgs(); + String res = "["; + Expr[] args = getArgs(); + for (int i = 0; i < n; i++) + res += args[i] + ", "; + return res + getValue() + "]"; } Entry(Context ctx, long obj) @@ -93,17 +87,9 @@ public class FuncInterp extends Z3Object } @Override - void incRef(long o) - { - getContext().getFuncEntryDRQ().incAndClear(getContext(), o); - super.incRef(o); - } - - @Override - void decRef(long o) - { - getContext().getFuncEntryDRQ().add(o); - super.decRef(o); + void incRef(long o) { + Native.funcEntryIncRef(getContext().nCtx(), o);; + getContext().getFuncEntryDRQ().storeReference(getContext(), this); } } @@ -161,33 +147,27 @@ public class FuncInterp extends Z3Object **/ public String toString() { - try + String res = ""; + res += "["; + for (Entry e : getEntries()) { - String res = ""; - res += "["; - for (Entry e : getEntries()) + int n = e.getNumArgs(); + if (n > 1) + res += "["; + Expr[] args = e.getArgs(); + for (int i = 0; i < n; i++) { - int n = e.getNumArgs(); - if (n > 1) - res += "["; - Expr[] args = e.getArgs(); - for (int i = 0; i < n; i++) - { - if (i != 0) - res += ", "; - res += args[i]; - } - if (n > 1) - res += "]"; - res += " -> " + e.getValue() + ", "; + if (i != 0) + res += ", "; + res += args[i]; } - res += "else -> " + getElse(); - res += "]"; - return res; - } catch (Z3Exception e) - { - return "Z3Exception: " + e.getMessage(); + if (n > 1) + res += "]"; + res += " -> " + e.getValue() + ", "; } + res += "else -> " + getElse(); + res += "]"; + return res; } FuncInterp(Context ctx, long obj) @@ -196,16 +176,8 @@ public class FuncInterp extends Z3Object } @Override - void incRef(long o) - { - getContext().getFuncInterpDRQ().incAndClear(getContext(), o); - super.incRef(o); - } - - @Override - void decRef(long o) - { - getContext().getFuncInterpDRQ().add(o); - super.decRef(o); + void incRef(long o) { + Native.funcInterpIncRef(getContext().nCtx(), o); + getContext().getFuncInterpDRQ().storeReference(getContext(), this); } } diff --git a/src/api/java/FuncInterpDecRefQueue.java b/src/api/java/FuncInterpDecRefQueue.java index c888e9e3d..136c07b6a 100644 --- a/src/api/java/FuncInterpDecRefQueue.java +++ b/src/api/java/FuncInterpDecRefQueue.java @@ -17,7 +17,7 @@ Notes: package com.microsoft.z3; -class FuncInterpDecRefQueue extends IDecRefQueue +class FuncInterpDecRefQueue extends IDecRefQueue { public FuncInterpDecRefQueue() { @@ -30,26 +30,7 @@ class FuncInterpDecRefQueue extends IDecRefQueue } @Override - protected void incRef(Context ctx, long obj) - { - try - { - Native.funcInterpIncRef(ctx.nCtx(), obj); - } catch (Z3Exception e) - { - // OK. - } - } - - @Override - protected void decRef(Context ctx, long obj) - { - try - { - Native.funcInterpDecRef(ctx.nCtx(), obj); - } catch (Z3Exception e) - { - // OK. - } + protected void decRef(Context ctx, long obj) { + Native.funcInterpDecRef(ctx.nCtx(), obj); } }; diff --git a/src/api/java/FuncInterpEntryDecRefQueue.java b/src/api/java/FuncInterpEntryDecRefQueue.java index 7dfdaa27d..8f6741ba0 100644 --- a/src/api/java/FuncInterpEntryDecRefQueue.java +++ b/src/api/java/FuncInterpEntryDecRefQueue.java @@ -17,7 +17,7 @@ Notes: package com.microsoft.z3; -class FuncInterpEntryDecRefQueue extends IDecRefQueue +class FuncInterpEntryDecRefQueue extends IDecRefQueue { public FuncInterpEntryDecRefQueue() { @@ -30,26 +30,7 @@ class FuncInterpEntryDecRefQueue extends IDecRefQueue } @Override - protected void incRef(Context ctx, long obj) - { - try - { - Native.funcEntryIncRef(ctx.nCtx(), obj); - } catch (Z3Exception e) - { - // OK. - } - } - - @Override - protected void decRef(Context ctx, long obj) - { - try - { - Native.funcEntryDecRef(ctx.nCtx(), obj); - } catch (Z3Exception e) - { - // OK. - } + protected void decRef(Context ctx, long obj) { + Native.funcEntryDecRef(ctx.nCtx(), obj); } }; diff --git a/src/api/java/Goal.java b/src/api/java/Goal.java index e60971179..a6d41ccd2 100644 --- a/src/api/java/Goal.java +++ b/src/api/java/Goal.java @@ -222,11 +222,11 @@ public class Goal extends Z3Object **/ public BoolExpr AsBoolExpr() { int n = size(); - if (n == 0) + if (n == 0) { return getContext().mkTrue(); - else if (n == 1) + } else if (n == 1) { return getFormulas()[0]; - else { + } else { return getContext().mkAnd(getFormulas()); } } @@ -236,23 +236,14 @@ public class Goal extends Z3Object super(ctx, obj); } - Goal(Context ctx, boolean models, boolean unsatCores, boolean proofs) - - { + Goal(Context ctx, boolean models, boolean unsatCores, boolean proofs) { super(ctx, Native.mkGoal(ctx.nCtx(), (models), (unsatCores), (proofs))); } - void incRef(long o) - { - getContext().getGoalDRQ().incAndClear(getContext(), o); - super.incRef(o); + @Override + void incRef(long o) { + Native.goalIncRef(getContext().nCtx(), o); + getContext().getGoalDRQ().storeReference(getContext(), this); } - - void decRef(long o) - { - getContext().getGoalDRQ().add(o); - super.decRef(o); - } - } diff --git a/src/api/java/GoalDecRefQueue.java b/src/api/java/GoalDecRefQueue.java index be921241b..724ec003f 100644 --- a/src/api/java/GoalDecRefQueue.java +++ b/src/api/java/GoalDecRefQueue.java @@ -17,7 +17,7 @@ Notes: package com.microsoft.z3; -class GoalDecRefQueue extends IDecRefQueue +class GoalDecRefQueue extends IDecRefQueue { public GoalDecRefQueue() { @@ -30,26 +30,7 @@ class GoalDecRefQueue extends IDecRefQueue } @Override - protected void incRef(Context ctx, long obj) - { - try - { - Native.goalIncRef(ctx.nCtx(), obj); - } catch (Z3Exception e) - { - // OK. - } - } - - @Override - protected void decRef(Context ctx, long obj) - { - try - { + protected void decRef(Context ctx, long obj) { Native.goalDecRef(ctx.nCtx(), obj); - } catch (Z3Exception e) - { - // OK. - } } }; diff --git a/src/api/java/IDecRefQueue.java b/src/api/java/IDecRefQueue.java index 1a99a3d92..b0a93b552 100644 --- a/src/api/java/IDecRefQueue.java +++ b/src/api/java/IDecRefQueue.java @@ -17,13 +17,21 @@ Notes: package com.microsoft.z3; -import java.util.LinkedList; +import java.lang.ref.PhantomReference; +import java.lang.ref.Reference; +import java.lang.ref.ReferenceQueue; +import java.util.IdentityHashMap; +import java.util.Map; -public abstract class IDecRefQueue +public abstract class IDecRefQueue { - protected final Object m_lock = new Object(); - protected LinkedList m_queue = new LinkedList(); - protected int m_move_limit; + private final int m_move_limit; + + // TODO: problem: ReferenceQueue has no API to return length. + private final ReferenceQueue referenceQueue = new ReferenceQueue<>(); + private int queueSize = 0; + private final Map, Long> referenceMap = + new IdentityHashMap<>(); protected IDecRefQueue() { @@ -34,38 +42,31 @@ public abstract class IDecRefQueue { m_move_limit = move_limit; } - - public void setLimit(int l) { m_move_limit = l; } - - protected abstract void incRef(Context ctx, long obj); + /** + * An implementation of this method should decrement the reference on a + * given native object. + * This function should be always called on the {@code ctx} thread. + * + * @param ctx Z3 context. + * @param obj Pointer to a Z3 object. + */ protected abstract void decRef(Context ctx, long obj); - protected void incAndClear(Context ctx, long o) - { - incRef(ctx, o); - if (m_queue.size() >= m_move_limit) - clear(ctx); - } + public void storeReference(Context ctx, T obj) { + PhantomReference ref = new PhantomReference<>(obj, referenceQueue); + referenceMap.put(ref, obj.getNativeObject()); - protected void add(long o) - { - if (o == 0) - return; - - synchronized (m_lock) - { - m_queue.add(o); - } + // TODO: use move_limit, somehow get the size of referenceQueue. + clear(ctx); } protected void clear(Context ctx) { - synchronized (m_lock) - { - for (Long o : m_queue) - decRef(ctx, o); - m_queue.clear(); + Reference ref; + while ((ref = referenceQueue.poll()) != null) { + long z3ast = referenceMap.remove(ref); + decRef(ctx, z3ast); } } } diff --git a/src/api/java/IDisposable.java b/src/api/java/IDisposable.java deleted file mode 100644 index dae8a7262..000000000 --- a/src/api/java/IDisposable.java +++ /dev/null @@ -1,25 +0,0 @@ -/*++ -Copyright (c) 2012 Microsoft Corporation - -Module Name: - - IDisposable.java - -Abstract: - - Compatability interface (C# -> Java) - -Author: - - Christoph Wintersteiger (cwinter) 2012-03-16 - -Notes: - ---*/ - -package com.microsoft.z3; - -public abstract class IDisposable -{ - public abstract void dispose(); -} diff --git a/src/api/java/InterpolationContext.java b/src/api/java/InterpolationContext.java index 47a128643..99a63821f 100644 --- a/src/api/java/InterpolationContext.java +++ b/src/api/java/InterpolationContext.java @@ -17,11 +17,10 @@ Notes: package com.microsoft.z3; -import java.util.Map; -import java.lang.String; - import com.microsoft.z3.enumerations.Z3_lbool; +import java.util.Map; + /** * The InterpolationContext is suitable for generation of interpolants. * @@ -33,13 +32,13 @@ public class InterpolationContext extends Context /** * Constructor. **/ - public InterpolationContext() + public static InterpolationContext mkContext() { - super(); + long m_ctx; synchronized(creation_lock) { m_ctx = Native.mkInterpolationContext(0); - initContext(); } + return new InterpolationContext(m_ctx); } /** @@ -49,17 +48,21 @@ public class InterpolationContext extends Context * Remarks: * @see Context#Context **/ - public InterpolationContext(Map settings) + public static InterpolationContext mkContext(Map settings) { - super(); + long m_ctx; synchronized(creation_lock) { long cfg = Native.mkConfig(); for (Map.Entry kv : settings.entrySet()) Native.setParamValue(cfg, kv.getKey(), kv.getValue()); m_ctx = Native.mkInterpolationContext(cfg); Native.delConfig(cfg); - initContext(); } + return new InterpolationContext(m_ctx); + } + + private InterpolationContext(long m_ctx) { + super(m_ctx); } /** diff --git a/src/api/java/ListSort.java b/src/api/java/ListSort.java index 705e93579..0ff2c36cf 100644 --- a/src/api/java/ListSort.java +++ b/src/api/java/ListSort.java @@ -17,6 +17,8 @@ Notes: package com.microsoft.z3; +import com.microsoft.z3.Native.LongPtr; + /** * List sorts. **/ @@ -88,14 +90,9 @@ public class ListSort extends Sort ListSort(Context ctx, Symbol name, Sort elemSort) { - super(ctx, 0); - - Native.LongPtr inil = new Native.LongPtr(), iisnil = new Native.LongPtr(); - Native.LongPtr icons = new Native.LongPtr(), iiscons = new Native.LongPtr(); - Native.LongPtr ihead = new Native.LongPtr(), itail = new Native.LongPtr(); - - setNativeObject(Native.mkListSort(ctx.nCtx(), name.getNativeObject(), - elemSort.getNativeObject(), inil, iisnil, icons, iiscons, ihead, - itail)); + super(ctx, Native.mkListSort(ctx.nCtx(), name.getNativeObject(), + elemSort.getNativeObject(), + new LongPtr(), new Native.LongPtr(), new LongPtr(), + new LongPtr(), new LongPtr(), new LongPtr())); } }; diff --git a/src/api/java/Model.java b/src/api/java/Model.java index 1bf77d246..fc6c6046b 100644 --- a/src/api/java/Model.java +++ b/src/api/java/Model.java @@ -293,16 +293,8 @@ public class Model extends Z3Object } @Override - void incRef(long o) - { - getContext().getModelDRQ().incAndClear(getContext(), o); - super.incRef(o); - } - - @Override - void decRef(long o) - { - getContext().getModelDRQ().add(o); - super.decRef(o); + void incRef(long o) { + Native.modelIncRef(getContext().nCtx(), o); + getContext().getModelDRQ().storeReference(getContext(), this); } } diff --git a/src/api/java/ModelDecRefQueue.java b/src/api/java/ModelDecRefQueue.java index b97add310..6b141078e 100644 --- a/src/api/java/ModelDecRefQueue.java +++ b/src/api/java/ModelDecRefQueue.java @@ -17,7 +17,7 @@ Notes: package com.microsoft.z3; -class ModelDecRefQueue extends IDecRefQueue +class ModelDecRefQueue extends IDecRefQueue { public ModelDecRefQueue() { @@ -30,26 +30,7 @@ class ModelDecRefQueue extends IDecRefQueue } @Override - protected void incRef(Context ctx, long obj) - { - try - { - Native.modelIncRef(ctx.nCtx(), obj); - } catch (Z3Exception e) - { - // OK. - } - } - - @Override - protected void decRef(Context ctx, long obj) - { - try - { - Native.modelDecRef(ctx.nCtx(), obj); - } catch (Z3Exception e) - { - // OK. - } + protected void decRef(Context ctx, long obj) { + Native.modelDecRef(ctx.nCtx(), obj); } }; diff --git a/src/api/java/Optimize.java b/src/api/java/Optimize.java index 5dfe8fcf4..a5705a388 100644 --- a/src/api/java/Optimize.java +++ b/src/api/java/Optimize.java @@ -266,17 +266,8 @@ public class Optimize extends Z3Object } @Override - void incRef(long o) - { - getContext().getOptimizeDRQ().incAndClear(getContext(), o); - super.incRef(o); + void incRef(long o) { + Native.optimizeIncRef(getContext().nCtx(), o); + getContext().getOptimizeDRQ().storeReference(getContext(), this); } - - @Override - void decRef(long o) - { - getContext().getOptimizeDRQ().add(o); - super.decRef(o); - } - } diff --git a/src/api/java/OptimizeDecRefQueue.java b/src/api/java/OptimizeDecRefQueue.java index 795a8a399..a06165f3e 100644 --- a/src/api/java/OptimizeDecRefQueue.java +++ b/src/api/java/OptimizeDecRefQueue.java @@ -17,8 +17,7 @@ Notes: package com.microsoft.z3; -class OptimizeDecRefQueue extends IDecRefQueue -{ +class OptimizeDecRefQueue extends IDecRefQueue { public OptimizeDecRefQueue() { super(); @@ -30,26 +29,7 @@ class OptimizeDecRefQueue extends IDecRefQueue } @Override - protected void incRef(Context ctx, long obj) - { - try - { - Native.fixedpointIncRef(ctx.nCtx(), obj); - } catch (Z3Exception e) - { - // OK. - } - } - - @Override - protected void decRef(Context ctx, long obj) - { - try - { - Native.fixedpointDecRef(ctx.nCtx(), obj); - } catch (Z3Exception e) - { - // OK. - } + protected void decRef(Context ctx, long obj) { + Native.optimizeDecRef(ctx.nCtx(), obj); } }; diff --git a/src/api/java/ParamDescrs.java b/src/api/java/ParamDescrs.java index f265fb19e..f90e4dd99 100644 --- a/src/api/java/ParamDescrs.java +++ b/src/api/java/ParamDescrs.java @@ -92,16 +92,8 @@ public class ParamDescrs extends Z3Object } @Override - void incRef(long o) - { - getContext().getParamDescrsDRQ().incAndClear(getContext(), o); - super.incRef(o); - } - - @Override - void decRef(long o) - { - getContext().getParamDescrsDRQ().add(o); - super.decRef(o); + void incRef(long o) { + Native.paramDescrsIncRef(getContext().nCtx(), o); + getContext().getParamDescrsDRQ().storeReference(getContext(), this); } } diff --git a/src/api/java/ParamDescrsDecRefQueue.java b/src/api/java/ParamDescrsDecRefQueue.java index e3515bff6..ab7f4ddd6 100644 --- a/src/api/java/ParamDescrsDecRefQueue.java +++ b/src/api/java/ParamDescrsDecRefQueue.java @@ -17,39 +17,20 @@ Notes: package com.microsoft.z3; -class ParamDescrsDecRefQueue extends IDecRefQueue +class ParamDescrsDecRefQueue extends IDecRefQueue { public ParamDescrsDecRefQueue() { super(); } - public ParamDescrsDecRefQueue(int move_limit) - { + public ParamDescrsDecRefQueue(int move_limit) { super(move_limit); } - @Override - protected void incRef(Context ctx, long obj) - { - try - { - Native.paramDescrsIncRef(ctx.nCtx(), obj); - } catch (Z3Exception e) - { - // OK. - } - } - @Override protected void decRef(Context ctx, long obj) { - try - { - Native.paramDescrsDecRef(ctx.nCtx(), obj); - } catch (Z3Exception e) - { - // OK. - } + Native.paramDescrsDecRef(ctx.nCtx(), obj); } }; diff --git a/src/api/java/Params.java b/src/api/java/Params.java index 4be36c23d..e3b143371 100644 --- a/src/api/java/Params.java +++ b/src/api/java/Params.java @@ -124,16 +124,8 @@ public class Params extends Z3Object } @Override - void incRef(long o) - { - getContext().getParamsDRQ().incAndClear(getContext(), o); - super.incRef(o); - } - - @Override - void decRef(long o) - { - getContext().getParamsDRQ().add(o); - super.decRef(o); + void incRef(long o) { + Native.paramsIncRef(getContext().nCtx(), o); + getContext().getParamsDRQ().storeReference(getContext(), this); } } diff --git a/src/api/java/ParamsDecRefQueue.java b/src/api/java/ParamsDecRefQueue.java index f989f8015..b5281ecbc 100644 --- a/src/api/java/ParamsDecRefQueue.java +++ b/src/api/java/ParamsDecRefQueue.java @@ -17,7 +17,7 @@ Notes: package com.microsoft.z3; -class ParamsDecRefQueue extends IDecRefQueue +class ParamsDecRefQueue extends IDecRefQueue { public ParamsDecRefQueue() { @@ -30,26 +30,7 @@ class ParamsDecRefQueue extends IDecRefQueue } @Override - protected void incRef(Context ctx, long obj) - { - try - { - Native.paramsIncRef(ctx.nCtx(), obj); - } catch (Z3Exception e) - { - // OK. - } - } - - @Override - protected void decRef(Context ctx, long obj) - { - try - { - Native.paramsDecRef(ctx.nCtx(), obj); - } catch (Z3Exception e) - { - // OK. - } + protected void decRef(Context ctx, long obj) { + Native.paramsDecRef(ctx.nCtx(), obj); } }; diff --git a/src/api/java/Probe.java b/src/api/java/Probe.java index bcaa76ce6..6983613c1 100644 --- a/src/api/java/Probe.java +++ b/src/api/java/Probe.java @@ -54,14 +54,7 @@ public class Probe extends Z3Object @Override void incRef(long o) { - getContext().getProbeDRQ().incAndClear(getContext(), o); - super.incRef(o); - } - - @Override - void decRef(long o) - { - getContext().getProbeDRQ().add(o); - super.decRef(o); + Native.probeIncRef(getContext().nCtx(), o); + getContext().getProbeDRQ().storeReference(getContext(), this); } } diff --git a/src/api/java/ProbeDecRefQueue.java b/src/api/java/ProbeDecRefQueue.java index 368bd5bba..3f78c6288 100644 --- a/src/api/java/ProbeDecRefQueue.java +++ b/src/api/java/ProbeDecRefQueue.java @@ -17,7 +17,7 @@ Notes: package com.microsoft.z3; -class ProbeDecRefQueue extends IDecRefQueue +class ProbeDecRefQueue extends IDecRefQueue { public ProbeDecRefQueue() { @@ -29,27 +29,9 @@ class ProbeDecRefQueue extends IDecRefQueue super(move_limit); } - @Override - protected void incRef(Context ctx, long obj) - { - try - { - Native.probeIncRef(ctx.nCtx(), obj); - } catch (Z3Exception e) - { - // OK. - } - } - @Override protected void decRef(Context ctx, long obj) { - try - { - Native.probeDecRef(ctx.nCtx(), obj); - } catch (Z3Exception e) - { - // OK. - } + Native.probeDecRef(ctx.nCtx(), obj); } }; diff --git a/src/api/java/Quantifier.java b/src/api/java/Quantifier.java index 1b425d3e4..a78277839 100644 --- a/src/api/java/Quantifier.java +++ b/src/api/java/Quantifier.java @@ -145,68 +145,67 @@ public class Quantifier extends BoolExpr .nCtx(), getNativeObject())); } - Quantifier(Context ctx, boolean isForall, Sort[] sorts, Symbol[] names, + public static Quantifier of( + Context ctx, boolean isForall, Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, - Symbol quantifierID, Symbol skolemID) - { - super(ctx, 0); - - getContext().checkContextMatch(patterns); - getContext().checkContextMatch(noPatterns); - getContext().checkContextMatch(sorts); - getContext().checkContextMatch(names); - getContext().checkContextMatch(body); + Symbol quantifierID, Symbol skolemID + ) { + ctx.checkContextMatch(patterns); + ctx.checkContextMatch(noPatterns); + ctx.checkContextMatch(sorts); + ctx.checkContextMatch(names); + ctx.checkContextMatch(body); if (sorts.length != names.length) throw new Z3Exception( "Number of sorts does not match number of names"); - if (noPatterns == null && quantifierID == null && skolemID == null) - { - setNativeObject(Native.mkQuantifier(ctx.nCtx(), (isForall), weight, AST.arrayLength(patterns), AST + long nativeObj; + if (noPatterns == null && quantifierID == null && skolemID == null) { + nativeObj = Native.mkQuantifier(ctx.nCtx(), (isForall), weight, AST.arrayLength(patterns), AST .arrayToNative(patterns), AST.arrayLength(sorts), AST .arrayToNative(sorts), Symbol.arrayToNative(names), body - .getNativeObject())); - } else - { - setNativeObject(Native.mkQuantifierEx(ctx.nCtx(), - (isForall), weight, AST.getNativeObject(quantifierID), - AST.getNativeObject(skolemID), - AST.arrayLength(patterns), AST.arrayToNative(patterns), - AST.arrayLength(noPatterns), AST.arrayToNative(noPatterns), - AST.arrayLength(sorts), AST.arrayToNative(sorts), - Symbol.arrayToNative(names), - body.getNativeObject())); + .getNativeObject()); + } else { + nativeObj = Native.mkQuantifierEx(ctx.nCtx(), + (isForall), weight, AST.getNativeObject(quantifierID), + AST.getNativeObject(skolemID), + AST.arrayLength(patterns), AST.arrayToNative(patterns), + AST.arrayLength(noPatterns), AST.arrayToNative(noPatterns), + AST.arrayLength(sorts), AST.arrayToNative(sorts), + Symbol.arrayToNative(names), + body.getNativeObject()); } + return new Quantifier(ctx, nativeObj); } - Quantifier(Context ctx, boolean isForall, Expr[] bound, Expr body, + + public static Quantifier of(Context ctx, boolean isForall, Expr[] bound, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) { - super(ctx, 0); - - getContext().checkContextMatch(noPatterns); - getContext().checkContextMatch(patterns); - // Context().CheckContextMatch(bound); - getContext().checkContextMatch(body); + ctx.checkContextMatch(noPatterns); + ctx.checkContextMatch(patterns); + // ctx.CheckContextMatch(bound); + ctx.checkContextMatch(body); + long nativeObj; if (noPatterns == null && quantifierID == null && skolemID == null) { - setNativeObject(Native.mkQuantifierConst(ctx.nCtx(), + nativeObj = Native.mkQuantifierConst(ctx.nCtx(), isForall, weight, AST.arrayLength(bound), AST.arrayToNative(bound), AST.arrayLength(patterns), - AST.arrayToNative(patterns), body.getNativeObject())); - } else - { - setNativeObject(Native.mkQuantifierConstEx(ctx.nCtx(), + AST.arrayToNative(patterns), body.getNativeObject()); + } else { + nativeObj = Native.mkQuantifierConstEx(ctx.nCtx(), isForall, weight, AST.getNativeObject(quantifierID), AST.getNativeObject(skolemID), AST.arrayLength(bound), AST.arrayToNative(bound), AST.arrayLength(patterns), AST.arrayToNative(patterns), AST.arrayLength(noPatterns), - AST.arrayToNative(noPatterns), body.getNativeObject())); + AST.arrayToNative(noPatterns), body.getNativeObject()); } + return new Quantifier(ctx, nativeObj); } Quantifier(Context ctx, long obj) diff --git a/src/api/java/Solver.java b/src/api/java/Solver.java index 431811b8d..5d538b2f3 100644 --- a/src/api/java/Solver.java +++ b/src/api/java/Solver.java @@ -127,13 +127,13 @@ public class Solver extends Z3Object * using the Boolean constants in ps. * * Remarks: - * This API is an alternative to {@link check} with assumptions for + * This API is an alternative to {@link #check()} with assumptions for * extracting unsat cores. * Both APIs can be used in the same solver. The unsat core will contain a * combination - * of the Boolean variables provided using {@link assertAndTrack} + * of the Boolean variables provided using {@code #assertAndTrack} * and the Boolean literals - * provided using {@link check} with assumptions. + * provided using {@link #check()} with assumptions. **/ public void assertAndTrack(BoolExpr[] constraints, BoolExpr[] ps) { @@ -333,16 +333,8 @@ public class Solver extends Z3Object } @Override - void incRef(long o) - { - getContext().getSolverDRQ().incAndClear(getContext(), o); - super.incRef(o); - } - - @Override - void decRef(long o) - { - getContext().getSolverDRQ().add(o); - super.decRef(o); + void incRef(long o) { + Native.solverIncRef(getContext().nCtx(), o); + getContext().getSolverDRQ().storeReference(getContext(), this); } } diff --git a/src/api/java/SolverDecRefQueue.java b/src/api/java/SolverDecRefQueue.java index f4d5fb139..106892fec 100644 --- a/src/api/java/SolverDecRefQueue.java +++ b/src/api/java/SolverDecRefQueue.java @@ -17,7 +17,7 @@ Notes: package com.microsoft.z3; -class SolverDecRefQueue extends IDecRefQueue +class SolverDecRefQueue extends IDecRefQueue { public SolverDecRefQueue() { super(); } @@ -27,26 +27,7 @@ class SolverDecRefQueue extends IDecRefQueue } @Override - protected void incRef(Context ctx, long obj) - { - try - { - Native.solverIncRef(ctx.nCtx(), obj); - } catch (Z3Exception e) - { - // OK. - } - } - - @Override - protected void decRef(Context ctx, long obj) - { - try - { - Native.solverDecRef(ctx.nCtx(), obj); - } catch (Z3Exception e) - { - // OK. - } + protected void decRef(Context ctx, long obj) { + Native.solverDecRef(ctx.nCtx(), obj); } }; diff --git a/src/api/java/Sort.java b/src/api/java/Sort.java index 30a43e7dd..0763a69a3 100644 --- a/src/api/java/Sort.java +++ b/src/api/java/Sort.java @@ -95,6 +95,7 @@ public class Sort extends AST super(ctx, obj); } + @Override void checkNativeObject(long obj) { if (Native.getAstKind(getContext().nCtx(), obj) != Z3_ast_kind.Z3_SORT_AST diff --git a/src/api/java/Statistics.java b/src/api/java/Statistics.java index 1e842a892..d2ba2bbd3 100644 --- a/src/api/java/Statistics.java +++ b/src/api/java/Statistics.java @@ -190,15 +190,9 @@ public class Statistics extends Z3Object super(ctx, obj); } - void incRef(long o) - { - getContext().getStatisticsDRQ().incAndClear(getContext(), o); - super.incRef(o); - } - - void decRef(long o) - { - getContext().getStatisticsDRQ().add(o); - super.decRef(o); + @Override + void incRef(long o) { + Native.statsIncRef(getContext().nCtx(), o); + getContext().getStatisticsDRQ().storeReference(getContext(), this); } } diff --git a/src/api/java/StatisticsDecRefQueue.java b/src/api/java/StatisticsDecRefQueue.java index 89c66a746..fecf52267 100644 --- a/src/api/java/StatisticsDecRefQueue.java +++ b/src/api/java/StatisticsDecRefQueue.java @@ -17,7 +17,7 @@ Notes: package com.microsoft.z3; -class StatisticsDecRefQueue extends IDecRefQueue +class StatisticsDecRefQueue extends IDecRefQueue { public StatisticsDecRefQueue() { @@ -29,25 +29,8 @@ class StatisticsDecRefQueue extends IDecRefQueue super(move_limit); } - protected void incRef(Context ctx, long obj) - { - try - { - Native.statsIncRef(ctx.nCtx(), obj); - } catch (Z3Exception e) - { - // OK. - } - } - - protected void decRef(Context ctx, long obj) - { - try - { - Native.statsDecRef(ctx.nCtx(), obj); - } catch (Z3Exception e) - { - // OK. - } + @Override + protected void decRef(Context ctx, long obj) { + Native.statsDecRef(ctx.nCtx(), obj); } }; diff --git a/src/api/java/StringSymbol.java b/src/api/java/StringSymbol.java index 8470e1cd4..576737ea7 100644 --- a/src/api/java/StringSymbol.java +++ b/src/api/java/StringSymbol.java @@ -48,9 +48,9 @@ public class StringSymbol extends Symbol void checkNativeObject(long obj) { if (Native.getSymbolKind(getContext().nCtx(), obj) != Z3_symbol_kind.Z3_STRING_SYMBOL - .toInt()) + .toInt()) { throw new Z3Exception("Symbol is not of String kind"); - + } super.checkNativeObject(obj); } } diff --git a/src/api/java/Symbol.java b/src/api/java/Symbol.java index beeaebb69..21925b099 100644 --- a/src/api/java/Symbol.java +++ b/src/api/java/Symbol.java @@ -62,19 +62,13 @@ public class Symbol extends Z3Object * A string representation of the symbol. **/ @Override - public String toString() - { - try - { - if (isIntSymbol()) - return Integer.toString(((IntSymbol) this).getInt()); - else if (isStringSymbol()) - return ((StringSymbol) this).getString(); - else - return "Z3Exception: Unknown symbol kind encountered."; - } catch (Z3Exception ex) - { - return "Z3Exception: " + ex.getMessage(); + public String toString() { + if (isIntSymbol()) { + return Integer.toString(((IntSymbol) this).getInt()); + } else if (isStringSymbol()) { + return ((StringSymbol) this).getString(); + } else { + return "Z3Exception: Unknown symbol kind encountered."; } } @@ -86,6 +80,11 @@ public class Symbol extends Z3Object super(ctx, obj); } + @Override + void incRef(long o) { + // Symbol does not require tracking. + } + static Symbol create(Context ctx, long obj) { switch (Z3_symbol_kind.fromInt(Native.getSymbolKind(ctx.nCtx(), obj))) diff --git a/src/api/java/Tactic.java b/src/api/java/Tactic.java index 786f8a6ec..f7e030f04 100644 --- a/src/api/java/Tactic.java +++ b/src/api/java/Tactic.java @@ -92,15 +92,10 @@ public class Tactic extends Z3Object super(ctx, Native.mkTactic(ctx.nCtx(), name)); } + @Override void incRef(long o) { - getContext().getTacticDRQ().incAndClear(getContext(), o); - super.incRef(o); - } - - void decRef(long o) - { - getContext().getTacticDRQ().add(o); - super.decRef(o); + Native.tacticIncRef(getContext().nCtx(), o); + getContext().getTacticDRQ().storeReference(getContext(), this); } } diff --git a/src/api/java/TacticDecRefQueue.java b/src/api/java/TacticDecRefQueue.java index 026760e46..079904175 100644 --- a/src/api/java/TacticDecRefQueue.java +++ b/src/api/java/TacticDecRefQueue.java @@ -17,8 +17,7 @@ Notes: package com.microsoft.z3; -class TacticDecRefQueue extends IDecRefQueue -{ +class TacticDecRefQueue extends IDecRefQueue { public TacticDecRefQueue() { super(); @@ -29,25 +28,9 @@ class TacticDecRefQueue extends IDecRefQueue super(move_limit); } - protected void incRef(Context ctx, long obj) - { - try - { - Native.tacticIncRef(ctx.nCtx(), obj); - } catch (Z3Exception e) - { - // OK. - } - } - + @Override protected void decRef(Context ctx, long obj) { - try - { - Native.tacticDecRef(ctx.nCtx(), obj); - } catch (Z3Exception e) - { - // OK. - } + Native.tacticDecRef(ctx.nCtx(), obj); } -}; +} diff --git a/src/api/java/TupleSort.java b/src/api/java/TupleSort.java index 1594b874d..ede20d260 100644 --- a/src/api/java/TupleSort.java +++ b/src/api/java/TupleSort.java @@ -59,11 +59,9 @@ public class TupleSort extends Sort TupleSort(Context ctx, Symbol name, int numFields, Symbol[] fieldNames, Sort[] fieldSorts) { - super(ctx, 0); - - Native.LongPtr t = new Native.LongPtr(); - setNativeObject(Native.mkTupleSort(ctx.nCtx(), name.getNativeObject(), + super(ctx, Native.mkTupleSort(ctx.nCtx(), name.getNativeObject(), numFields, Symbol.arrayToNative(fieldNames), - AST.arrayToNative(fieldSorts), t, new long[numFields])); + AST.arrayToNative(fieldSorts), new Native.LongPtr(), + new long[numFields])); } }; diff --git a/src/api/java/Z3Object.java b/src/api/java/Z3Object.java index dc1feecbf..6fd12bfba 100644 --- a/src/api/java/Z3Object.java +++ b/src/api/java/Z3Object.java @@ -21,88 +21,38 @@ package com.microsoft.z3; * Internal base class for interfacing with native Z3 objects. Should not be * used externally. **/ -public class Z3Object extends IDisposable -{ - /** - * Finalizer. - * @throws Throwable - **/ - protected void finalize() throws Throwable - { - try { - dispose(); - } finally { - super.finalize(); - } - } +public abstract class Z3Object { - /** - * Disposes of the underlying native Z3 object. - **/ - public void dispose() - { - if (m_n_obj != 0) - { - decRef(m_n_obj); - m_n_obj = 0; - } + private final Context m_ctx; + private final long m_n_obj; - if (m_ctx != null) - { - if (m_ctx.m_refCount.decrementAndGet() == 0) - m_ctx.dispose(); - m_ctx = null; - } - } - - private Context m_ctx = null; - private long m_n_obj = 0; - - Z3Object(Context ctx) - { - ctx.m_refCount.incrementAndGet(); - m_ctx = ctx; - } - - Z3Object(Context ctx, long obj) - { - ctx.m_refCount.incrementAndGet(); + Z3Object(Context ctx, long obj) { m_ctx = ctx; + checkNativeObject(obj); incRef(obj); m_n_obj = obj; } - void incRef(long o) - { - } + /** + * Increment reference count on {@code o}. + * + * @param o Z3 object. + */ + abstract void incRef(long o); - void decRef(long o) - { - } - - void checkNativeObject(long obj) - { - } + /** + * This function is provided for overriding, and a child class + * can insert consistency checks on {@code obj}. + * + * @param obj Z3 native object. + */ + void checkNativeObject(long obj) {} long getNativeObject() { return m_n_obj; } - void setNativeObject(long value) - { - if (value != 0) - { - checkNativeObject(value); - incRef(value); - } - if (m_n_obj != 0) - { - decRef(m_n_obj); - } - m_n_obj = value; - } - static long getNativeObject(Z3Object s) { if (s == null) @@ -121,7 +71,7 @@ public class Z3Object extends IDisposable return null; long[] an = new long[a.length]; for (int i = 0; i < a.length; i++) - an[i] = (a[i] == null) ? 0 : a[i].getNativeObject(); + an[i] = (a[i] == null) ? 0 : a[i].getNativeObject(); return an; } From 5657399d554f0c67715855840d2cee09e20c5ed1 Mon Sep 17 00:00:00 2001 From: George Karpenkov Date: Sun, 12 Jun 2016 20:39:54 +0200 Subject: [PATCH 05/17] Bugfix for incorrect order of operations. --- src/api/java/Z3Object.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/java/Z3Object.java b/src/api/java/Z3Object.java index 6fd12bfba..f982bba1c 100644 --- a/src/api/java/Z3Object.java +++ b/src/api/java/Z3Object.java @@ -29,8 +29,8 @@ public abstract class Z3Object { Z3Object(Context ctx, long obj) { m_ctx = ctx; checkNativeObject(obj); - incRef(obj); m_n_obj = obj; + incRef(obj); } /** From 2a347f04bf79a6e223899cfba6690123d388b9f3 Mon Sep 17 00:00:00 2001 From: George Karpenkov Date: Sun, 12 Jun 2016 21:00:51 +0200 Subject: [PATCH 06/17] Java API: FuncInterp.Entry should be an inner static class ...as it does not use any fields of the outer FuncInterp object. --- src/api/java/FuncInterp.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/api/java/FuncInterp.java b/src/api/java/FuncInterp.java index c84979aa1..52f09c5a4 100644 --- a/src/api/java/FuncInterp.java +++ b/src/api/java/FuncInterp.java @@ -28,8 +28,8 @@ public class FuncInterp extends Z3Object * An Entry object represents an element in the finite map used to encode a * function interpretation. **/ - public class Entry extends Z3Object - { + public static class Entry extends Z3Object { + /** * Return the (symbolic) value of this entry. * From 22ffd65d1e2a02583128a9a19a547d8b340e2547 Mon Sep 17 00:00:00 2001 From: George Karpenkov Date: Sun, 12 Jun 2016 21:01:58 +0200 Subject: [PATCH 07/17] Java API: split incRef into incRef and addToReferenceQueue One method should do one thing only, it's easy to mix things up otherwise. --- src/api/java/AST.java | 9 ++++--- src/api/java/ASTMap.java | 12 +++++---- src/api/java/ASTVector.java | 12 +++++---- src/api/java/ApplyResult.java | 11 ++++++--- src/api/java/Constructor.java | 7 ++++-- src/api/java/ConstructorList.java | 7 +++++- src/api/java/Fixedpoint.java | 8 ++++-- src/api/java/FixedpointDecRefQueue.java | 4 +-- src/api/java/FuncInterp.java | 33 +++++++++++++++---------- src/api/java/Goal.java | 11 ++++++--- src/api/java/Model.java | 11 ++++++--- src/api/java/Optimize.java | 8 ++++-- src/api/java/ParamDescrs.java | 11 ++++++--- src/api/java/Params.java | 12 ++++++--- src/api/java/Probe.java | 15 +++++------ src/api/java/Solver.java | 17 +++++++------ src/api/java/Statistics.java | 11 ++++++--- src/api/java/Symbol.java | 11 ++++++--- src/api/java/Tactic.java | 12 +++++---- src/api/java/Z3Object.java | 15 +++++++---- 20 files changed, 150 insertions(+), 87 deletions(-) diff --git a/src/api/java/AST.java b/src/api/java/AST.java index 4b5b37d46..e1cde837f 100644 --- a/src/api/java/AST.java +++ b/src/api/java/AST.java @@ -192,9 +192,12 @@ public class AST extends Z3Object implements Comparable } @Override - void incRef(long o) - { - Native.incRef(getContext().nCtx(), o); + void incRef() { + Native.incRef(getContext().nCtx(), getNativeObject()); + } + + @Override + void addToReferenceQueue() { getContext().getASTDRQ().storeReference(getContext(), this); } diff --git a/src/api/java/ASTMap.java b/src/api/java/ASTMap.java index b4ae7102a..916811cec 100644 --- a/src/api/java/ASTMap.java +++ b/src/api/java/ASTMap.java @@ -20,8 +20,7 @@ package com.microsoft.z3; /** * Map from AST to AST **/ -class ASTMap extends Z3Object -{ +class ASTMap extends Z3Object { /** * Checks whether the map contains the key {@code k}. * @param k An AST @@ -118,9 +117,12 @@ class ASTMap extends Z3Object } @Override - void incRef(long o) - { - Native.astMapIncRef(getContext().nCtx(), o); + void incRef() { + Native.astMapIncRef(getContext().nCtx(), getNativeObject()); + } + + @Override + void addToReferenceQueue() { getContext().getASTMapDRQ().storeReference(getContext(), this); } } diff --git a/src/api/java/ASTVector.java b/src/api/java/ASTVector.java index 7c5ca1067..4d9ab291a 100644 --- a/src/api/java/ASTVector.java +++ b/src/api/java/ASTVector.java @@ -20,8 +20,7 @@ package com.microsoft.z3; /** * Vectors of ASTs. **/ -public class ASTVector extends Z3Object -{ +public class ASTVector extends Z3Object { /** * The size of the vector **/ @@ -103,9 +102,12 @@ public class ASTVector extends Z3Object } @Override - void incRef(long o) - { - Native.astVectorIncRef(getContext().nCtx(), o); + void incRef() { + Native.astVectorIncRef(getContext().nCtx(), getNativeObject()); + } + + @Override + void addToReferenceQueue() { getContext().getASTVectorDRQ().storeReference(getContext(), this); } diff --git a/src/api/java/ApplyResult.java b/src/api/java/ApplyResult.java index 8b3c1daf6..6fafbd888 100644 --- a/src/api/java/ApplyResult.java +++ b/src/api/java/ApplyResult.java @@ -21,8 +21,7 @@ package com.microsoft.z3; * ApplyResult objects represent the result of an application of a tactic to a * goal. It contains the subgoals that were produced. **/ -public class ApplyResult extends Z3Object -{ +public class ApplyResult extends Z3Object { /** * The number of Subgoals. **/ @@ -74,8 +73,12 @@ public class ApplyResult extends Z3Object } @Override - void incRef(long o) { - Native.applyResultIncRef(getContext().nCtx(), o); + void incRef() { + Native.applyResultIncRef(getContext().nCtx(), getNativeObject()); + } + + @Override + void addToReferenceQueue() { getContext().getApplyResultDRQ().storeReference(getContext(), this); } } diff --git a/src/api/java/Constructor.java b/src/api/java/Constructor.java index 28558b15a..87ab86c3f 100644 --- a/src/api/java/Constructor.java +++ b/src/api/java/Constructor.java @@ -85,9 +85,12 @@ public class Constructor extends Z3Object { } @Override - void incRef(long o) { - + void incRef() { // Datatype constructors are not reference counted. + } + + @Override + void addToReferenceQueue() { getContext().getConstructorDRQ().storeReference(getContext(), this); } diff --git a/src/api/java/ConstructorList.java b/src/api/java/ConstructorList.java index 3f1835082..c79e08d9e 100644 --- a/src/api/java/ConstructorList.java +++ b/src/api/java/ConstructorList.java @@ -28,7 +28,12 @@ public class ConstructorList extends Z3Object { } @Override - void incRef(long o) { + void incRef() { + // Constructor lists are not reference counted. + } + + @Override + void addToReferenceQueue() { getContext().getConstructorListDRQ().storeReference(getContext(), this); } diff --git a/src/api/java/Fixedpoint.java b/src/api/java/Fixedpoint.java index 5a7958364..876345f1e 100644 --- a/src/api/java/Fixedpoint.java +++ b/src/api/java/Fixedpoint.java @@ -349,8 +349,12 @@ public class Fixedpoint extends Z3Object } @Override - void incRef(long o) { - Native.fixedpointIncRef(getContext().nCtx(), o); + void incRef() { + Native.fixedpointIncRef(getContext().nCtx(), getNativeObject()); + } + + @Override + void addToReferenceQueue() { getContext().getFixedpointDRQ().storeReference(getContext(), this); } diff --git a/src/api/java/FixedpointDecRefQueue.java b/src/api/java/FixedpointDecRefQueue.java index d5ae79a2b..3cba67ced 100644 --- a/src/api/java/FixedpointDecRefQueue.java +++ b/src/api/java/FixedpointDecRefQueue.java @@ -17,8 +17,7 @@ Notes: package com.microsoft.z3; -class FixedpointDecRefQueue extends IDecRefQueue -{ +class FixedpointDecRefQueue extends IDecRefQueue { public FixedpointDecRefQueue() { super(); @@ -29,7 +28,6 @@ class FixedpointDecRefQueue extends IDecRefQueue super(move_limit); } - @Override protected void decRef(Context ctx, long obj) { diff --git a/src/api/java/FuncInterp.java b/src/api/java/FuncInterp.java index 52f09c5a4..b5873d98e 100644 --- a/src/api/java/FuncInterp.java +++ b/src/api/java/FuncInterp.java @@ -22,8 +22,8 @@ package com.microsoft.z3; * Each entry in the finite map represents the value of a function given a set * of arguments. **/ -public class FuncInterp extends Z3Object -{ +public class FuncInterp extends Z3Object { + /** * An Entry object represents an element in the finite map used to encode a * function interpretation. @@ -32,10 +32,10 @@ public class FuncInterp extends Z3Object /** * Return the (symbolic) value of this entry. - * + * * @throws Z3Exception * @throws Z3Exception on error - **/ + **/ public Expr getValue() { return Expr.create(getContext(), @@ -45,7 +45,7 @@ public class FuncInterp extends Z3Object /** * The number of arguments of the entry. * @throws Z3Exception on error - **/ + **/ public int getNumArgs() { return Native.funcEntryGetNumArgs(getContext().nCtx(), getNativeObject()); @@ -53,10 +53,10 @@ public class FuncInterp extends Z3Object /** * The arguments of the function entry. - * + * * @throws Z3Exception * @throws Z3Exception on error - **/ + **/ public Expr[] getArgs() { int n = getNumArgs(); @@ -81,14 +81,17 @@ public class FuncInterp extends Z3Object return res + getValue() + "]"; } - Entry(Context ctx, long obj) - { + Entry(Context ctx, long obj) { super(ctx, obj); } @Override - void incRef(long o) { - Native.funcEntryIncRef(getContext().nCtx(), o);; + void incRef() { + Native.funcEntryIncRef(getContext().nCtx(), getNativeObject()); + } + + @Override + void addToReferenceQueue() { getContext().getFuncEntryDRQ().storeReference(getContext(), this); } } @@ -176,8 +179,12 @@ public class FuncInterp extends Z3Object } @Override - void incRef(long o) { - Native.funcInterpIncRef(getContext().nCtx(), o); + void incRef() { + Native.funcInterpIncRef(getContext().nCtx(), getNativeObject()); + } + + @Override + void addToReferenceQueue() { getContext().getFuncInterpDRQ().storeReference(getContext(), this); } } diff --git a/src/api/java/Goal.java b/src/api/java/Goal.java index a6d41ccd2..25b1fe511 100644 --- a/src/api/java/Goal.java +++ b/src/api/java/Goal.java @@ -23,8 +23,7 @@ import com.microsoft.z3.enumerations.Z3_goal_prec; * A goal (aka problem). A goal is essentially a set of formulas, that can be * solved and/or transformed using tactics and solvers. **/ -public class Goal extends Z3Object -{ +public class Goal extends Z3Object { /** * The precision of the goal. * Remarks: Goals can be transformed using over @@ -242,8 +241,12 @@ public class Goal extends Z3Object } @Override - void incRef(long o) { - Native.goalIncRef(getContext().nCtx(), o); + void incRef() { + Native.goalIncRef(getContext().nCtx(), getNativeObject()); + } + + @Override + void addToReferenceQueue() { getContext().getGoalDRQ().storeReference(getContext(), this); } } diff --git a/src/api/java/Model.java b/src/api/java/Model.java index fc6c6046b..60abb001d 100644 --- a/src/api/java/Model.java +++ b/src/api/java/Model.java @@ -22,8 +22,7 @@ import com.microsoft.z3.enumerations.Z3_sort_kind; /** * A Model contains interpretations (assignments) of constants and functions. **/ -public class Model extends Z3Object -{ +public class Model extends Z3Object { /** * Retrieves the interpretation (the assignment) of {@code a} in * the model. @@ -293,8 +292,12 @@ public class Model extends Z3Object } @Override - void incRef(long o) { - Native.modelIncRef(getContext().nCtx(), o); + void incRef() { + Native.modelIncRef(getContext().nCtx(), getNativeObject()); + } + + @Override + void addToReferenceQueue() { getContext().getModelDRQ().storeReference(getContext(), this); } } diff --git a/src/api/java/Optimize.java b/src/api/java/Optimize.java index a5705a388..ea100d1ca 100644 --- a/src/api/java/Optimize.java +++ b/src/api/java/Optimize.java @@ -266,8 +266,12 @@ public class Optimize extends Z3Object } @Override - void incRef(long o) { - Native.optimizeIncRef(getContext().nCtx(), o); + void incRef() { + Native.optimizeIncRef(getContext().nCtx(), getNativeObject()); + } + + @Override + void addToReferenceQueue() { getContext().getOptimizeDRQ().storeReference(getContext(), this); } } diff --git a/src/api/java/ParamDescrs.java b/src/api/java/ParamDescrs.java index f90e4dd99..0008515e3 100644 --- a/src/api/java/ParamDescrs.java +++ b/src/api/java/ParamDescrs.java @@ -22,8 +22,7 @@ import com.microsoft.z3.enumerations.Z3_param_kind; /** * A ParamDescrs describes a set of parameters. **/ -public class ParamDescrs extends Z3Object -{ +public class ParamDescrs extends Z3Object { /** * validate a set of parameters. **/ @@ -92,8 +91,12 @@ public class ParamDescrs extends Z3Object } @Override - void incRef(long o) { - Native.paramDescrsIncRef(getContext().nCtx(), o); + void incRef() { + Native.paramDescrsIncRef(getContext().nCtx(), getNativeObject()); + } + + @Override + void addToReferenceQueue() { getContext().getParamDescrsDRQ().storeReference(getContext(), this); } } diff --git a/src/api/java/Params.java b/src/api/java/Params.java index e3b143371..a76dd3cab 100644 --- a/src/api/java/Params.java +++ b/src/api/java/Params.java @@ -21,8 +21,7 @@ package com.microsoft.z3; /** * A ParameterSet represents a configuration in the form of Symbol/value pairs. **/ -public class Params extends Z3Object -{ +public class Params extends Z3Object { /** * Adds a parameter setting. **/ @@ -123,9 +122,14 @@ public class Params extends Z3Object super(ctx, Native.mkParams(ctx.nCtx())); } + @Override - void incRef(long o) { - Native.paramsIncRef(getContext().nCtx(), o); + void incRef() { + Native.paramsIncRef(getContext().nCtx(), getNativeObject()); + } + + @Override + void addToReferenceQueue() { getContext().getParamsDRQ().storeReference(getContext(), this); } } diff --git a/src/api/java/Probe.java b/src/api/java/Probe.java index 6983613c1..a36f3b64b 100644 --- a/src/api/java/Probe.java +++ b/src/api/java/Probe.java @@ -25,8 +25,7 @@ package com.microsoft.z3; * also be obtained using the command {@code (help-tactic)} in the SMT 2.0 * front-end. **/ -public class Probe extends Z3Object -{ +public class Probe extends Z3Object { /** * Execute the probe over the goal. * @@ -46,15 +45,17 @@ public class Probe extends Z3Object super(ctx, obj); } - Probe(Context ctx, String name) - { + Probe(Context ctx, String name) { super(ctx, Native.mkProbe(ctx.nCtx(), name)); } @Override - void incRef(long o) - { - Native.probeIncRef(getContext().nCtx(), o); + void incRef() { + Native.probeIncRef(getContext().nCtx(), getNativeObject()); + } + + @Override + void addToReferenceQueue() { getContext().getProbeDRQ().storeReference(getContext(), this); } } diff --git a/src/api/java/Solver.java b/src/api/java/Solver.java index 5d538b2f3..a98fcbf94 100644 --- a/src/api/java/Solver.java +++ b/src/api/java/Solver.java @@ -22,8 +22,7 @@ import com.microsoft.z3.enumerations.Z3_lbool; /** * Solvers. **/ -public class Solver extends Z3Object -{ +public class Solver extends Z3Object { /** * A string that describes all available solver parameters. **/ @@ -154,13 +153,13 @@ public class Solver extends Z3Object * using the Boolean constant p. * * Remarks: - * This API is an alternative to {@link check} with assumptions for + * This API is an alternative to {@link #check} with assumptions for * extracting unsat cores. * Both APIs can be used in the same solver. The unsat core will contain a * combination - * of the Boolean variables provided using {@link assertAndTrack} + * of the Boolean variables provided using {@link #assertAndTrack} * and the Boolean literals - * provided using {@link check} with assumptions. + * provided using {@link #check} with assumptions. */ public void assertAndTrack(BoolExpr constraint, BoolExpr p) { @@ -333,8 +332,12 @@ public class Solver extends Z3Object } @Override - void incRef(long o) { - Native.solverIncRef(getContext().nCtx(), o); + void incRef() { + Native.solverIncRef(getContext().nCtx(), getNativeObject()); + } + + @Override + void addToReferenceQueue() { getContext().getSolverDRQ().storeReference(getContext(), this); } } diff --git a/src/api/java/Statistics.java b/src/api/java/Statistics.java index d2ba2bbd3..356cbeadb 100644 --- a/src/api/java/Statistics.java +++ b/src/api/java/Statistics.java @@ -20,8 +20,7 @@ package com.microsoft.z3; /** * Objects of this class track statistical information about solvers. **/ -public class Statistics extends Z3Object -{ +public class Statistics extends Z3Object { /** * Statistical data is organized into pairs of [Key, Entry], where every * Entry is either a {@code DoubleEntry} or a {@code UIntEntry} @@ -191,8 +190,12 @@ public class Statistics extends Z3Object } @Override - void incRef(long o) { - Native.statsIncRef(getContext().nCtx(), o); + void incRef() { getContext().getStatisticsDRQ().storeReference(getContext(), this); } + + @Override + void addToReferenceQueue() { + Native.statsIncRef(getContext().nCtx(), getNativeObject()); + } } diff --git a/src/api/java/Symbol.java b/src/api/java/Symbol.java index 21925b099..139894be1 100644 --- a/src/api/java/Symbol.java +++ b/src/api/java/Symbol.java @@ -22,8 +22,7 @@ import com.microsoft.z3.enumerations.Z3_symbol_kind; /** * Symbols are used to name several term and type constructors. **/ -public class Symbol extends Z3Object -{ +public class Symbol extends Z3Object { /** * The kind of the symbol (int or string) **/ @@ -81,7 +80,13 @@ public class Symbol extends Z3Object } @Override - void incRef(long o) { + void incRef() { + // Symbol does not require tracking. + } + + @Override + void addToReferenceQueue() { + // Symbol does not require tracking. } diff --git a/src/api/java/Tactic.java b/src/api/java/Tactic.java index f7e030f04..11d02ca73 100644 --- a/src/api/java/Tactic.java +++ b/src/api/java/Tactic.java @@ -24,8 +24,7 @@ package com.microsoft.z3; * also be obtained using the command {@code (help-tactic)} in the SMT 2.0 * front-end. **/ -public class Tactic extends Z3Object -{ +public class Tactic extends Z3Object { /** * A string containing a description of parameters accepted by the tactic. **/ @@ -93,9 +92,12 @@ public class Tactic extends Z3Object } @Override - void incRef(long o) - { - Native.tacticIncRef(getContext().nCtx(), o); + void incRef() { + Native.tacticIncRef(getContext().nCtx(), getNativeObject()); + } + + @Override + void addToReferenceQueue() { getContext().getTacticDRQ().storeReference(getContext(), this); } } diff --git a/src/api/java/Z3Object.java b/src/api/java/Z3Object.java index f982bba1c..7c5f606d9 100644 --- a/src/api/java/Z3Object.java +++ b/src/api/java/Z3Object.java @@ -30,15 +30,20 @@ public abstract class Z3Object { m_ctx = ctx; checkNativeObject(obj); m_n_obj = obj; - incRef(obj); + incRef(); + addToReferenceQueue(); } /** - * Increment reference count on {@code o}. - * - * @param o Z3 object. + * Add to ReferenceQueue for tracking reachability on the object and + * decreasing the reference count when the object is no longer reachable. */ - abstract void incRef(long o); + abstract void addToReferenceQueue(); + + /** + * Increment reference count on {@code this}. + */ + abstract void incRef(); /** * This function is provided for overriding, and a child class From 27aa37946e56a4d9722de416791a2e40dc5d2054 Mon Sep 17 00:00:00 2001 From: George Karpenkov Date: Mon, 13 Jun 2016 12:09:34 +0200 Subject: [PATCH 08/17] Do not lock on context creation and deletion. --- src/api/java/Context.java | 24 +++++++----------------- 1 file changed, 7 insertions(+), 17 deletions(-) diff --git a/src/api/java/Context.java b/src/api/java/Context.java index 41fb027fe..e66920441 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -31,12 +31,7 @@ public class Context implements AutoCloseable { static final Object creation_lock = new Object(); public static Context mkContext() { - long m_ctx; - synchronized (creation_lock) { - m_ctx = Native.mkContextRc(0); - // TODO: then adding settings will not be under the lock. - } - return new Context(m_ctx); + return new Context(Native.mkContextRc(0)); } @@ -59,14 +54,11 @@ public class Context implements AutoCloseable { **/ public static Context mkContext(Map settings) { - long m_ctx; - synchronized (creation_lock) { - long cfg = Native.mkConfig(); - for (Map.Entry kv : settings.entrySet()) - Native.setParamValue(cfg, kv.getKey(), kv.getValue()); - m_ctx = Native.mkContextRc(cfg); - Native.delConfig(cfg); - } + long cfg = Native.mkConfig(); + for (Map.Entry kv : settings.entrySet()) + Native.setParamValue(cfg, kv.getKey(), kv.getValue()); + long m_ctx = Native.mkContextRc(cfg); + Native.delConfig(cfg); return new Context(m_ctx); } @@ -4047,8 +4039,6 @@ public class Context implements AutoCloseable { m_realSort = null; m_stringSort = null; - synchronized (creation_lock) { - Native.delContext(m_ctx); - } + Native.delContext(m_ctx); } } From 26d6c99aac2ecf1304f695c75540f47715e0ce6d Mon Sep 17 00:00:00 2001 From: George Karpenkov Date: Mon, 13 Jun 2016 12:11:03 +0200 Subject: [PATCH 09/17] Typo in Javadoc. --- src/api/java/IDecRefQueue.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/java/IDecRefQueue.java b/src/api/java/IDecRefQueue.java index b0a93b552..f3cea7249 100644 --- a/src/api/java/IDecRefQueue.java +++ b/src/api/java/IDecRefQueue.java @@ -46,7 +46,7 @@ public abstract class IDecRefQueue /** * An implementation of this method should decrement the reference on a * given native object. - * This function should be always called on the {@code ctx} thread. + * This function should always be called on the {@code ctx} thread. * * @param ctx Z3 context. * @param obj Pointer to a Z3 object. From a914822346179531cf36c79809e5f01842267c84 Mon Sep 17 00:00:00 2001 From: George Karpenkov Date: Mon, 13 Jun 2016 12:18:31 +0200 Subject: [PATCH 10/17] JavaAPI: DecRefQueue -- do not use move_limit for now. --- src/api/java/ASTDecRefQueue.java | 5 --- src/api/java/ApplyResultDecRefQueue.java | 5 --- src/api/java/AstMapDecRefQueue.java | 10 ++---- src/api/java/AstVectorDecRefQueue.java | 10 ++---- src/api/java/ConstructorDecRefQueue.java | 12 +++++++ src/api/java/ConstructorListDecRefQueue.java | 12 +++++++ src/api/java/Context.java | 34 ++++++++++---------- src/api/java/FixedpointDecRefQueue.java | 5 --- src/api/java/FuncInterpDecRefQueue.java | 5 --- src/api/java/FuncInterpEntryDecRefQueue.java | 10 ++---- src/api/java/GoalDecRefQueue.java | 10 ++---- src/api/java/IDecRefQueue.java | 23 ++++--------- src/api/java/ModelDecRefQueue.java | 10 ++---- src/api/java/OptimizeDecRefQueue.java | 5 --- src/api/java/ParamDescrsDecRefQueue.java | 9 ++---- src/api/java/ParamsDecRefQueue.java | 10 ++---- src/api/java/ProbeDecRefQueue.java | 5 --- src/api/java/SolverDecRefQueue.java | 10 ++---- src/api/java/StatisticsDecRefQueue.java | 10 ++---- src/api/java/TacticDecRefQueue.java | 5 --- 20 files changed, 65 insertions(+), 140 deletions(-) create mode 100644 src/api/java/ConstructorDecRefQueue.java create mode 100644 src/api/java/ConstructorListDecRefQueue.java diff --git a/src/api/java/ASTDecRefQueue.java b/src/api/java/ASTDecRefQueue.java index d462e16d5..b0a6fa217 100644 --- a/src/api/java/ASTDecRefQueue.java +++ b/src/api/java/ASTDecRefQueue.java @@ -24,11 +24,6 @@ class ASTDecRefQueue extends IDecRefQueue super(); } - public ASTDecRefQueue(int move_limit) - { - super(move_limit); - } - @Override protected void decRef(Context ctx, long obj) { Native.decRef(ctx.nCtx(), obj); diff --git a/src/api/java/ApplyResultDecRefQueue.java b/src/api/java/ApplyResultDecRefQueue.java index d28ff755e..e1a660781 100644 --- a/src/api/java/ApplyResultDecRefQueue.java +++ b/src/api/java/ApplyResultDecRefQueue.java @@ -24,11 +24,6 @@ class ApplyResultDecRefQueue extends IDecRefQueue super(); } - public ApplyResultDecRefQueue(int move_limit) - { - super(move_limit); - } - @Override protected void decRef(Context ctx, long obj) { Native.applyResultDecRef(ctx.nCtx(), obj); diff --git a/src/api/java/AstMapDecRefQueue.java b/src/api/java/AstMapDecRefQueue.java index 234b7eec4..6c96970b7 100644 --- a/src/api/java/AstMapDecRefQueue.java +++ b/src/api/java/AstMapDecRefQueue.java @@ -17,20 +17,14 @@ Notes: package com.microsoft.z3; -class ASTMapDecRefQueue extends IDecRefQueue -{ +class ASTMapDecRefQueue extends IDecRefQueue { public ASTMapDecRefQueue() { super(); } - public ASTMapDecRefQueue(int move_limit) - { - super(move_limit); - } - @Override protected void decRef(Context ctx, long obj) { Native.astMapDecRef(ctx.nCtx(), obj); } -}; +} diff --git a/src/api/java/AstVectorDecRefQueue.java b/src/api/java/AstVectorDecRefQueue.java index 3a486ee06..e7ce3e33e 100644 --- a/src/api/java/AstVectorDecRefQueue.java +++ b/src/api/java/AstVectorDecRefQueue.java @@ -17,20 +17,14 @@ Notes: package com.microsoft.z3; -class ASTVectorDecRefQueue extends IDecRefQueue -{ +class ASTVectorDecRefQueue extends IDecRefQueue { public ASTVectorDecRefQueue() { super(); } - public ASTVectorDecRefQueue(int move_limit) - { - super(move_limit); - } - @Override protected void decRef(Context ctx, long obj) { Native.astVectorDecRef(ctx.nCtx(), obj); } -}; +} diff --git a/src/api/java/ConstructorDecRefQueue.java b/src/api/java/ConstructorDecRefQueue.java new file mode 100644 index 000000000..5003dde5f --- /dev/null +++ b/src/api/java/ConstructorDecRefQueue.java @@ -0,0 +1,12 @@ +package com.microsoft.z3; + +public class ConstructorDecRefQueue extends IDecRefQueue { + public ConstructorDecRefQueue() { + super(); + } + + @Override + protected void decRef(Context ctx, long obj) { + Native.delConstructor(ctx.nCtx(), obj); + } +} diff --git a/src/api/java/ConstructorListDecRefQueue.java b/src/api/java/ConstructorListDecRefQueue.java new file mode 100644 index 000000000..1a2460731 --- /dev/null +++ b/src/api/java/ConstructorListDecRefQueue.java @@ -0,0 +1,12 @@ +package com.microsoft.z3; + +public class ConstructorListDecRefQueue extends IDecRefQueue { + public ConstructorListDecRefQueue() { + super(); + } + + @Override + protected void decRef(Context ctx, long obj) { + Native.delConstructorList(ctx.nCtx(), obj); + } +} diff --git a/src/api/java/Context.java b/src/api/java/Context.java index e66920441..1e2b5d4fa 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -3905,24 +3905,24 @@ public class Context implements AutoCloseable { } private ASTDecRefQueue m_AST_DRQ = new ASTDecRefQueue(); - private ASTMapDecRefQueue m_ASTMap_DRQ = new ASTMapDecRefQueue(10); - private ASTVectorDecRefQueue m_ASTVector_DRQ = new ASTVectorDecRefQueue(10); - private ApplyResultDecRefQueue m_ApplyResult_DRQ = new ApplyResultDecRefQueue(10); - private FuncInterpEntryDecRefQueue m_FuncEntry_DRQ = new FuncInterpEntryDecRefQueue(10); - private FuncInterpDecRefQueue m_FuncInterp_DRQ = new FuncInterpDecRefQueue(10); - private GoalDecRefQueue m_Goal_DRQ = new GoalDecRefQueue(10); - private ModelDecRefQueue m_Model_DRQ = new ModelDecRefQueue(10); - private ParamsDecRefQueue m_Params_DRQ = new ParamsDecRefQueue(10); - private ParamDescrsDecRefQueue m_ParamDescrs_DRQ = new ParamDescrsDecRefQueue(10); - private ProbeDecRefQueue m_Probe_DRQ = new ProbeDecRefQueue(10); - private SolverDecRefQueue m_Solver_DRQ = new SolverDecRefQueue(10); - private StatisticsDecRefQueue m_Statistics_DRQ = new StatisticsDecRefQueue(10); - private TacticDecRefQueue m_Tactic_DRQ = new TacticDecRefQueue(10); - private FixedpointDecRefQueue m_Fixedpoint_DRQ = new FixedpointDecRefQueue(10); - private OptimizeDecRefQueue m_Optimize_DRQ = new OptimizeDecRefQueue(10); - private ConstructorDecRefQueue m_Constructor_DRQ = new ConstructorDecRefQueue(10); + private ASTMapDecRefQueue m_ASTMap_DRQ = new ASTMapDecRefQueue(); + private ASTVectorDecRefQueue m_ASTVector_DRQ = new ASTVectorDecRefQueue(); + private ApplyResultDecRefQueue m_ApplyResult_DRQ = new ApplyResultDecRefQueue(); + private FuncInterpEntryDecRefQueue m_FuncEntry_DRQ = new FuncInterpEntryDecRefQueue(); + private FuncInterpDecRefQueue m_FuncInterp_DRQ = new FuncInterpDecRefQueue(); + private GoalDecRefQueue m_Goal_DRQ = new GoalDecRefQueue(); + private ModelDecRefQueue m_Model_DRQ = new ModelDecRefQueue(); + private ParamsDecRefQueue m_Params_DRQ = new ParamsDecRefQueue(); + private ParamDescrsDecRefQueue m_ParamDescrs_DRQ = new ParamDescrsDecRefQueue(); + private ProbeDecRefQueue m_Probe_DRQ = new ProbeDecRefQueue(); + private SolverDecRefQueue m_Solver_DRQ = new SolverDecRefQueue(); + private StatisticsDecRefQueue m_Statistics_DRQ = new StatisticsDecRefQueue(); + private TacticDecRefQueue m_Tactic_DRQ = new TacticDecRefQueue(); + private FixedpointDecRefQueue m_Fixedpoint_DRQ = new FixedpointDecRefQueue(); + private OptimizeDecRefQueue m_Optimize_DRQ = new OptimizeDecRefQueue(); + private ConstructorDecRefQueue m_Constructor_DRQ = new ConstructorDecRefQueue(); private ConstructorListDecRefQueue m_ConstructorList_DRQ = - new ConstructorListDecRefQueue(10); + new ConstructorListDecRefQueue(); public IDecRefQueue getConstructorDRQ() { return m_Constructor_DRQ; diff --git a/src/api/java/FixedpointDecRefQueue.java b/src/api/java/FixedpointDecRefQueue.java index 3cba67ced..69ed82092 100644 --- a/src/api/java/FixedpointDecRefQueue.java +++ b/src/api/java/FixedpointDecRefQueue.java @@ -23,11 +23,6 @@ class FixedpointDecRefQueue extends IDecRefQueue { super(); } - public FixedpointDecRefQueue(int move_limit) - { - super(move_limit); - } - @Override protected void decRef(Context ctx, long obj) { diff --git a/src/api/java/FuncInterpDecRefQueue.java b/src/api/java/FuncInterpDecRefQueue.java index 136c07b6a..d8715bd0e 100644 --- a/src/api/java/FuncInterpDecRefQueue.java +++ b/src/api/java/FuncInterpDecRefQueue.java @@ -24,11 +24,6 @@ class FuncInterpDecRefQueue extends IDecRefQueue super(); } - public FuncInterpDecRefQueue(int move_limit) - { - super(move_limit); - } - @Override protected void decRef(Context ctx, long obj) { Native.funcInterpDecRef(ctx.nCtx(), obj); diff --git a/src/api/java/FuncInterpEntryDecRefQueue.java b/src/api/java/FuncInterpEntryDecRefQueue.java index 8f6741ba0..a4d8a0690 100644 --- a/src/api/java/FuncInterpEntryDecRefQueue.java +++ b/src/api/java/FuncInterpEntryDecRefQueue.java @@ -17,20 +17,14 @@ Notes: package com.microsoft.z3; -class FuncInterpEntryDecRefQueue extends IDecRefQueue -{ +class FuncInterpEntryDecRefQueue extends IDecRefQueue { public FuncInterpEntryDecRefQueue() { super(); } - public FuncInterpEntryDecRefQueue(int move_limit) - { - super(move_limit); - } - @Override protected void decRef(Context ctx, long obj) { Native.funcEntryDecRef(ctx.nCtx(), obj); } -}; +} diff --git a/src/api/java/GoalDecRefQueue.java b/src/api/java/GoalDecRefQueue.java index 724ec003f..90bad1fb1 100644 --- a/src/api/java/GoalDecRefQueue.java +++ b/src/api/java/GoalDecRefQueue.java @@ -17,20 +17,14 @@ Notes: package com.microsoft.z3; -class GoalDecRefQueue extends IDecRefQueue -{ +class GoalDecRefQueue extends IDecRefQueue { public GoalDecRefQueue() { super(); } - public GoalDecRefQueue(int move_limit) - { - super(move_limit); - } - @Override protected void decRef(Context ctx, long obj) { Native.goalDecRef(ctx.nCtx(), obj); } -}; +} diff --git a/src/api/java/IDecRefQueue.java b/src/api/java/IDecRefQueue.java index f3cea7249..5a80adf5f 100644 --- a/src/api/java/IDecRefQueue.java +++ b/src/api/java/IDecRefQueue.java @@ -23,25 +23,16 @@ import java.lang.ref.ReferenceQueue; import java.util.IdentityHashMap; import java.util.Map; -public abstract class IDecRefQueue -{ - private final int m_move_limit; - - // TODO: problem: ReferenceQueue has no API to return length. +/** + * + * @param + */ +public abstract class IDecRefQueue { private final ReferenceQueue referenceQueue = new ReferenceQueue<>(); - private int queueSize = 0; private final Map, Long> referenceMap = new IdentityHashMap<>(); - protected IDecRefQueue() - { - m_move_limit = 1024; - } - - protected IDecRefQueue(int move_limit) - { - m_move_limit = move_limit; - } + protected IDecRefQueue() {} /** * An implementation of this method should decrement the reference on a @@ -56,8 +47,6 @@ public abstract class IDecRefQueue public void storeReference(Context ctx, T obj) { PhantomReference ref = new PhantomReference<>(obj, referenceQueue); referenceMap.put(ref, obj.getNativeObject()); - - // TODO: use move_limit, somehow get the size of referenceQueue. clear(ctx); } diff --git a/src/api/java/ModelDecRefQueue.java b/src/api/java/ModelDecRefQueue.java index 6b141078e..f1b7c3fdd 100644 --- a/src/api/java/ModelDecRefQueue.java +++ b/src/api/java/ModelDecRefQueue.java @@ -17,20 +17,14 @@ Notes: package com.microsoft.z3; -class ModelDecRefQueue extends IDecRefQueue -{ +class ModelDecRefQueue extends IDecRefQueue { public ModelDecRefQueue() { super(); } - public ModelDecRefQueue(int move_limit) - { - super(move_limit); - } - @Override protected void decRef(Context ctx, long obj) { Native.modelDecRef(ctx.nCtx(), obj); } -}; +} diff --git a/src/api/java/OptimizeDecRefQueue.java b/src/api/java/OptimizeDecRefQueue.java index a06165f3e..0acf20068 100644 --- a/src/api/java/OptimizeDecRefQueue.java +++ b/src/api/java/OptimizeDecRefQueue.java @@ -23,11 +23,6 @@ class OptimizeDecRefQueue extends IDecRefQueue { super(); } - public OptimizeDecRefQueue(int move_limit) - { - super(move_limit); - } - @Override protected void decRef(Context ctx, long obj) { Native.optimizeDecRef(ctx.nCtx(), obj); diff --git a/src/api/java/ParamDescrsDecRefQueue.java b/src/api/java/ParamDescrsDecRefQueue.java index ab7f4ddd6..ee3257db9 100644 --- a/src/api/java/ParamDescrsDecRefQueue.java +++ b/src/api/java/ParamDescrsDecRefQueue.java @@ -17,20 +17,15 @@ Notes: package com.microsoft.z3; -class ParamDescrsDecRefQueue extends IDecRefQueue -{ +class ParamDescrsDecRefQueue extends IDecRefQueue { public ParamDescrsDecRefQueue() { super(); } - public ParamDescrsDecRefQueue(int move_limit) { - super(move_limit); - } - @Override protected void decRef(Context ctx, long obj) { Native.paramDescrsDecRef(ctx.nCtx(), obj); } -}; +} diff --git a/src/api/java/ParamsDecRefQueue.java b/src/api/java/ParamsDecRefQueue.java index b5281ecbc..349713f67 100644 --- a/src/api/java/ParamsDecRefQueue.java +++ b/src/api/java/ParamsDecRefQueue.java @@ -17,20 +17,14 @@ Notes: package com.microsoft.z3; -class ParamsDecRefQueue extends IDecRefQueue -{ +class ParamsDecRefQueue extends IDecRefQueue { public ParamsDecRefQueue() { super(); } - public ParamsDecRefQueue(int move_limit) - { - super(move_limit); - } - @Override protected void decRef(Context ctx, long obj) { Native.paramsDecRef(ctx.nCtx(), obj); } -}; +} diff --git a/src/api/java/ProbeDecRefQueue.java b/src/api/java/ProbeDecRefQueue.java index 3f78c6288..b25446c0c 100644 --- a/src/api/java/ProbeDecRefQueue.java +++ b/src/api/java/ProbeDecRefQueue.java @@ -24,11 +24,6 @@ class ProbeDecRefQueue extends IDecRefQueue super(); } - public ProbeDecRefQueue(int move_limit) - { - super(move_limit); - } - @Override protected void decRef(Context ctx, long obj) { diff --git a/src/api/java/SolverDecRefQueue.java b/src/api/java/SolverDecRefQueue.java index 106892fec..efa15d939 100644 --- a/src/api/java/SolverDecRefQueue.java +++ b/src/api/java/SolverDecRefQueue.java @@ -17,17 +17,11 @@ Notes: package com.microsoft.z3; -class SolverDecRefQueue extends IDecRefQueue -{ +class SolverDecRefQueue extends IDecRefQueue { public SolverDecRefQueue() { super(); } - public SolverDecRefQueue(int move_limit) - { - super(move_limit); - } - @Override protected void decRef(Context ctx, long obj) { Native.solverDecRef(ctx.nCtx(), obj); } -}; +} diff --git a/src/api/java/StatisticsDecRefQueue.java b/src/api/java/StatisticsDecRefQueue.java index fecf52267..ed698e4ca 100644 --- a/src/api/java/StatisticsDecRefQueue.java +++ b/src/api/java/StatisticsDecRefQueue.java @@ -17,20 +17,14 @@ Notes: package com.microsoft.z3; -class StatisticsDecRefQueue extends IDecRefQueue -{ +class StatisticsDecRefQueue extends IDecRefQueue { public StatisticsDecRefQueue() { super(); } - public StatisticsDecRefQueue(int move_limit) - { - super(move_limit); - } - @Override protected void decRef(Context ctx, long obj) { Native.statsDecRef(ctx.nCtx(), obj); } -}; +} diff --git a/src/api/java/TacticDecRefQueue.java b/src/api/java/TacticDecRefQueue.java index 079904175..8f151f25c 100644 --- a/src/api/java/TacticDecRefQueue.java +++ b/src/api/java/TacticDecRefQueue.java @@ -23,11 +23,6 @@ class TacticDecRefQueue extends IDecRefQueue { super(); } - public TacticDecRefQueue(int move_limit) - { - super(move_limit); - } - @Override protected void decRef(Context ctx, long obj) { From b65d83aacfea8adacebe7d2919c55bdedb475a8c Mon Sep 17 00:00:00 2001 From: George Karpenkov Date: Mon, 13 Jun 2016 12:22:32 +0200 Subject: [PATCH 11/17] Java API: explain the phantom references mechanics in Javadoc. --- src/api/java/IDecRefQueue.java | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/src/api/java/IDecRefQueue.java b/src/api/java/IDecRefQueue.java index 5a80adf5f..2deb9c0f9 100644 --- a/src/api/java/IDecRefQueue.java +++ b/src/api/java/IDecRefQueue.java @@ -24,8 +24,17 @@ import java.util.IdentityHashMap; import java.util.Map; /** + * A queue to handle management of native memory. * - * @param + *

Mechanics: once an object is created, a metadata is stored for it in + * {@code referenceMap}, and a {@link PhantomReference} is created with a + * reference to {@code referenceQueue}. + * Once the object becomes strongly unreachable, the phantom reference gets + * added by JVM to the {@code referenceQueue}. + * After each object creation, we iterate through the available objects in + * {@code referenceQueue} and decrement references for them. + * + * @param Type of object stored in queue. */ public abstract class IDecRefQueue { private final ReferenceQueue referenceQueue = new ReferenceQueue<>(); From b086aac45ff1069159f35bd5243ca6d479963ebc Mon Sep 17 00:00:00 2001 From: George Karpenkov Date: Thu, 16 Jun 2016 18:21:55 +0200 Subject: [PATCH 12/17] Use constructors instead of static methods for Context.java. --- src/api/java/Context.java | 24 +++++++++--------------- 1 file changed, 9 insertions(+), 15 deletions(-) diff --git a/src/api/java/Context.java b/src/api/java/Context.java index 1e2b5d4fa..39d35d9d3 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -30,8 +30,9 @@ public class Context implements AutoCloseable { private final long m_ctx; static final Object creation_lock = new Object(); - public static Context mkContext() { - return new Context(Native.mkContextRc(0)); + public Context () { + m_ctx = Native.mkContextRc(0); + init(); } @@ -52,24 +53,17 @@ public class Context implements AutoCloseable { * Note that in previous versions of Z3, this constructor was also used to set global and * module parameters. For this purpose we should now use {@code Global.setParameter} **/ - public static Context mkContext(Map settings) - { + public Context(Map settings) { long cfg = Native.mkConfig(); - for (Map.Entry kv : settings.entrySet()) + for (Map.Entry kv : settings.entrySet()) { Native.setParamValue(cfg, kv.getKey(), kv.getValue()); - long m_ctx = Native.mkContextRc(cfg); + } + m_ctx = Native.mkContextRc(cfg); Native.delConfig(cfg); - return new Context(m_ctx); + init(); } - /** - * Constructor. - **/ - protected Context(long m_ctx) - { - this.m_ctx = m_ctx; - - // Code which used to be in "initContext". + private void init() { setPrintMode(Z3_ast_print_mode.Z3_PRINT_SMTLIB2_COMPLIANT); Native.setInternalErrorHandler(m_ctx); } From 8bde7b8a4cdabe15f4d72c07d172460d598ebd99 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 23 Jun 2016 19:31:00 +0100 Subject: [PATCH 13/17] Added facilities for dumping smt_params for debugging purposes --- src/ast/pattern/pattern_inference_params.cpp | 15 +++ src/ast/pattern/pattern_inference_params.h | 2 + .../rewriter/bit_blaster/bit_blaster_params.h | 7 +- .../simplifier/arith_simplifier_params.cpp | 7 ++ src/ast/simplifier/arith_simplifier_params.h | 2 + src/ast/simplifier/bv_simplifier_params.cpp | 7 ++ src/ast/simplifier/bv_simplifier_params.h | 2 + src/smt/params/dyn_ack_params.cpp | 11 +++ src/smt/params/dyn_ack_params.h | 2 + src/smt/params/preprocessor_params.cpp | 30 ++++++ src/smt/params/preprocessor_params.h | 2 + src/smt/params/qi_params.cpp | 27 ++++++ src/smt/params/qi_params.h | 4 +- src/smt/params/smt_params.cpp | 93 +++++++++++++++++++ src/smt/params/smt_params.h | 2 + src/smt/params/theory_arith_params.cpp | 48 ++++++++++ src/smt/params/theory_arith_params.h | 2 + src/smt/params/theory_array_params.cpp | 12 +++ src/smt/params/theory_array_params.h | 1 + src/smt/params/theory_bv_params.cpp | 11 +++ src/smt/params/theory_bv_params.h | 2 + src/smt/params/theory_datatype_params.h | 2 + src/smt/params/theory_pb_params.cpp | 9 ++ src/smt/params/theory_pb_params.h | 2 + 24 files changed, 300 insertions(+), 2 deletions(-) diff --git a/src/ast/pattern/pattern_inference_params.cpp b/src/ast/pattern/pattern_inference_params.cpp index 8adbdb9f1..b36d372f5 100644 --- a/src/ast/pattern/pattern_inference_params.cpp +++ b/src/ast/pattern/pattern_inference_params.cpp @@ -30,3 +30,18 @@ void pattern_inference_params::updt_params(params_ref const & _p) { m_pi_pull_quantifiers = p.pull_quantifiers(); m_pi_warnings = p.warnings(); } + +#define DISPLAY_PARAM(X) out << #X"=" << X << std::endl; + +void pattern_inference_params::display(std::ostream & out) const { + DISPLAY_PARAM(m_pi_max_multi_patterns); + DISPLAY_PARAM(m_pi_block_loop_patterns); + DISPLAY_PARAM(m_pi_arith); + DISPLAY_PARAM(m_pi_use_database); + DISPLAY_PARAM(m_pi_arith_weight); + DISPLAY_PARAM(m_pi_non_nested_arith_weight); + DISPLAY_PARAM(m_pi_pull_quantifiers); + DISPLAY_PARAM(m_pi_nopat_weight); + DISPLAY_PARAM(m_pi_avoid_skolems); + DISPLAY_PARAM(m_pi_warnings); +} \ No newline at end of file diff --git a/src/ast/pattern/pattern_inference_params.h b/src/ast/pattern/pattern_inference_params.h index a941b7dd6..0dc413399 100644 --- a/src/ast/pattern/pattern_inference_params.h +++ b/src/ast/pattern/pattern_inference_params.h @@ -46,6 +46,8 @@ struct pattern_inference_params { } void updt_params(params_ref const & _p); + + void display(std::ostream & out) const; }; #endif /* PATTERN_INFERENCE_PARAMS_H_ */ diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_params.h b/src/ast/rewriter/bit_blaster/bit_blaster_params.h index ee32d005a..15ece0043 100644 --- a/src/ast/rewriter/bit_blaster/bit_blaster_params.h +++ b/src/ast/rewriter/bit_blaster/bit_blaster_params.h @@ -22,7 +22,7 @@ Revision History: struct bit_blaster_params { bool m_bb_ext_gates; bool m_bb_quantifiers; - bit_blaster_params(): + bit_blaster_params() : m_bb_ext_gates(false), m_bb_quantifiers(false) { } @@ -32,6 +32,11 @@ struct bit_blaster_params { p.register_bool_param("bb_quantifiers", m_bb_quantifiers, "convert bit-vectors to Booleans in quantifiers"); } #endif + + void display(std::ostream & out) const { + out << "m_bb_ext_gates=" << m_bb_ext_gates << std::endl; + out << "m_bb_quantifiers=" << m_bb_quantifiers << std::endl; + } }; #endif /* BIT_BLASTER_PARAMS_H_ */ diff --git a/src/ast/simplifier/arith_simplifier_params.cpp b/src/ast/simplifier/arith_simplifier_params.cpp index a3fabe02f..8584cdae0 100644 --- a/src/ast/simplifier/arith_simplifier_params.cpp +++ b/src/ast/simplifier/arith_simplifier_params.cpp @@ -24,3 +24,10 @@ void arith_simplifier_params::updt_params(params_ref const & _p) { m_arith_expand_eqs = p.arith_expand_eqs(); m_arith_process_all_eqs = p.arith_process_all_eqs(); } + +#define DISPLAY_PARAM(X) out << #X"=" << X << std::endl; + +void arith_simplifier_params::display(std::ostream & out) const { + DISPLAY_PARAM(m_arith_expand_eqs); + DISPLAY_PARAM(m_arith_process_all_eqs); +} \ No newline at end of file diff --git a/src/ast/simplifier/arith_simplifier_params.h b/src/ast/simplifier/arith_simplifier_params.h index 2ff8fe2c0..6186ee4a2 100644 --- a/src/ast/simplifier/arith_simplifier_params.h +++ b/src/ast/simplifier/arith_simplifier_params.h @@ -30,6 +30,8 @@ struct arith_simplifier_params { } void updt_params(params_ref const & _p); + + void display(std::ostream & out) const; }; #endif /* ARITH_SIMPLIFIER_PARAMS_H_ */ diff --git a/src/ast/simplifier/bv_simplifier_params.cpp b/src/ast/simplifier/bv_simplifier_params.cpp index 5d6cd363f..1ed263aa6 100644 --- a/src/ast/simplifier/bv_simplifier_params.cpp +++ b/src/ast/simplifier/bv_simplifier_params.cpp @@ -27,3 +27,10 @@ void bv_simplifier_params::updt_params(params_ref const & _p) { m_bv2int_distribute = p.bv_bv2int_distribute(); } + +#define DISPLAY_PARAM(X) out << #X"=" << X << std::endl; + +void bv_simplifier_params::display(std::ostream & out) const { + DISPLAY_PARAM(m_hi_div0); + DISPLAY_PARAM(m_bv2int_distribute); +} \ No newline at end of file diff --git a/src/ast/simplifier/bv_simplifier_params.h b/src/ast/simplifier/bv_simplifier_params.h index 50015b7ca..dafa99065 100644 --- a/src/ast/simplifier/bv_simplifier_params.h +++ b/src/ast/simplifier/bv_simplifier_params.h @@ -30,6 +30,8 @@ struct bv_simplifier_params { } void updt_params(params_ref const & _p); + + void display(std::ostream & out) const; }; #endif /* BV_SIMPLIFIER_PARAMS_H_ */ diff --git a/src/smt/params/dyn_ack_params.cpp b/src/smt/params/dyn_ack_params.cpp index 15f48bad1..b62530fbf 100644 --- a/src/smt/params/dyn_ack_params.cpp +++ b/src/smt/params/dyn_ack_params.cpp @@ -28,3 +28,14 @@ void dyn_ack_params::updt_params(params_ref const & _p) { m_dack_gc = p.dack_gc(); m_dack_gc_inv_decay = p.dack_gc_inv_decay(); } + +#define DISPLAY_PARAM(X) out << #X"=" << X << std::endl; + +void dyn_ack_params::display(std::ostream & out) const { + DISPLAY_PARAM(m_dack); + DISPLAY_PARAM(m_dack_eq); + DISPLAY_PARAM(m_dack_factor); + DISPLAY_PARAM(m_dack_threshold); + DISPLAY_PARAM(m_dack_gc); + DISPLAY_PARAM(m_dack_gc_inv_decay); +} \ No newline at end of file diff --git a/src/smt/params/dyn_ack_params.h b/src/smt/params/dyn_ack_params.h index f87e3b6df..017b7fe94 100644 --- a/src/smt/params/dyn_ack_params.h +++ b/src/smt/params/dyn_ack_params.h @@ -47,6 +47,8 @@ public: } void updt_params(params_ref const & _p); + + void display(std::ostream & out) const; }; diff --git a/src/smt/params/preprocessor_params.cpp b/src/smt/params/preprocessor_params.cpp index 9ad787c2a..7a0e96248 100644 --- a/src/smt/params/preprocessor_params.cpp +++ b/src/smt/params/preprocessor_params.cpp @@ -32,3 +32,33 @@ void preprocessor_params::updt_params(params_ref const & p) { arith_simplifier_params::updt_params(p); updt_local_params(p); } + +#define DISPLAY_PARAM(X) out << #X"=" << X << std::endl; + +void preprocessor_params::display(std::ostream & out) const { + pattern_inference_params::display(out); + bit_blaster_params::display(out); + bv_simplifier_params::display(out); + arith_simplifier_params::display(out); + + DISPLAY_PARAM(m_lift_ite); + DISPLAY_PARAM(m_ng_lift_ite); + DISPLAY_PARAM(m_pull_cheap_ite_trees); + DISPLAY_PARAM(m_pull_nested_quantifiers); + DISPLAY_PARAM(m_eliminate_term_ite); + DISPLAY_PARAM(m_eliminate_and); + DISPLAY_PARAM(m_macro_finder); + DISPLAY_PARAM(m_propagate_values); + DISPLAY_PARAM(m_propagate_booleans); + DISPLAY_PARAM(m_refine_inj_axiom); + DISPLAY_PARAM(m_eliminate_bounds); + DISPLAY_PARAM(m_simplify_bit2int); + DISPLAY_PARAM(m_nnf_cnf); + DISPLAY_PARAM(m_distribute_forall); + DISPLAY_PARAM(m_reduce_args); + DISPLAY_PARAM(m_quasi_macros); + DISPLAY_PARAM(m_restricted_quasi_macros); + DISPLAY_PARAM(m_max_bv_sharing); + DISPLAY_PARAM(m_pre_simplifier); + DISPLAY_PARAM(m_nlquant_elim); +} diff --git a/src/smt/params/preprocessor_params.h b/src/smt/params/preprocessor_params.h index 3806b26cf..4ffad48a2 100644 --- a/src/smt/params/preprocessor_params.h +++ b/src/smt/params/preprocessor_params.h @@ -83,6 +83,8 @@ public: void updt_local_params(params_ref const & p); void updt_params(params_ref const & p); + + void display(std::ostream & out) const; }; #endif /* PREPROCESSOR_PARAMS_H_ */ diff --git a/src/smt/params/qi_params.cpp b/src/smt/params/qi_params.cpp index 60fcd6fc4..a341040ce 100644 --- a/src/smt/params/qi_params.cpp +++ b/src/smt/params/qi_params.cpp @@ -36,3 +36,30 @@ void qi_params::updt_params(params_ref const & _p) { m_qi_cost = p.qi_cost(); m_qi_max_eager_multipatterns = p.qi_max_multi_patterns(); } + +#define DISPLAY_PARAM(X) out << #X"=" << X << std::endl; + +void qi_params::display(std::ostream & out) const { + DISPLAY_PARAM(m_qi_ematching); + DISPLAY_PARAM(m_qi_cost); + DISPLAY_PARAM(m_qi_new_gen); + DISPLAY_PARAM(m_qi_eager_threshold); + DISPLAY_PARAM(m_qi_lazy_threshold); + DISPLAY_PARAM(m_qi_max_eager_multipatterns); + DISPLAY_PARAM(m_qi_max_lazy_multipattern_matching); + DISPLAY_PARAM(m_qi_profile); + DISPLAY_PARAM(m_qi_profile_freq); + DISPLAY_PARAM(m_qi_quick_checker); + DISPLAY_PARAM(m_qi_lazy_quick_checker); + DISPLAY_PARAM(m_qi_promote_unsat); + DISPLAY_PARAM(m_qi_max_instances); + DISPLAY_PARAM(m_qi_lazy_instantiation); + DISPLAY_PARAM(m_qi_conservative_final_check); + DISPLAY_PARAM(m_mbqi); + DISPLAY_PARAM(m_mbqi_max_cexs); + DISPLAY_PARAM(m_mbqi_max_cexs_incr); + DISPLAY_PARAM(m_mbqi_max_iterations); + DISPLAY_PARAM(m_mbqi_trace); + DISPLAY_PARAM(m_mbqi_force_template); + DISPLAY_PARAM(m_mbqi_id); +} \ No newline at end of file diff --git a/src/smt/params/qi_params.h b/src/smt/params/qi_params.h index 00baea170..c9736909a 100644 --- a/src/smt/params/qi_params.h +++ b/src/smt/params/qi_params.h @@ -98,13 +98,15 @@ struct qi_params { m_mbqi_max_cexs_incr(1), m_mbqi_max_iterations(1000), m_mbqi_trace(false), - m_mbqi_force_template(10), + m_mbqi_force_template(10), m_mbqi_id(0) { updt_params(p); } void updt_params(params_ref const & p); + + void display(std::ostream & out) const; }; #endif /* QI_PARAMS_H_ */ diff --git a/src/smt/params/smt_params.cpp b/src/smt/params/smt_params.cpp index 8222c3d60..8a9188e2b 100644 --- a/src/smt/params/smt_params.cpp +++ b/src/smt/params/smt_params.cpp @@ -63,3 +63,96 @@ void smt_params::updt_params(context_params const & p) { m_auto_config = p.m_auto_config; m_model = p.m_model; } + +#define DISPLAY_PARAM(X) out << #X"=" << X << std::endl; + +void smt_params::display(std::ostream & out) const { + preprocessor_params::display(out); + dyn_ack_params::display(out); + qi_params::display(out); + theory_arith_params::display(out); + theory_array_params::display(out); + theory_bv_params::display(out); + theory_pb_params::display(out); + theory_datatype_params::display(out); + + DISPLAY_PARAM(m_display_proof); + DISPLAY_PARAM(m_display_dot_proof); + DISPLAY_PARAM(m_display_unsat_core); + DISPLAY_PARAM(m_check_proof); + DISPLAY_PARAM(m_eq_propagation); + DISPLAY_PARAM(m_binary_clause_opt); + DISPLAY_PARAM(m_relevancy_lvl); + DISPLAY_PARAM(m_relevancy_lemma); + DISPLAY_PARAM(m_random_seed); + DISPLAY_PARAM(m_random_var_freq); + DISPLAY_PARAM(m_inv_decay); + DISPLAY_PARAM(m_clause_decay); + DISPLAY_PARAM(m_random_initial_activity); + DISPLAY_PARAM(m_phase_selection); + DISPLAY_PARAM(m_phase_caching_on); + DISPLAY_PARAM(m_phase_caching_off); + DISPLAY_PARAM(m_minimize_lemmas); + DISPLAY_PARAM(m_max_conflicts); + DISPLAY_PARAM(m_simplify_clauses); + DISPLAY_PARAM(m_tick); + DISPLAY_PARAM(m_display_features); + DISPLAY_PARAM(m_new_core2th_eq); + DISPLAY_PARAM(m_ematching); + + DISPLAY_PARAM(m_case_split_strategy); + DISPLAY_PARAM(m_rel_case_split_order); + DISPLAY_PARAM(m_lookahead_diseq); + + DISPLAY_PARAM(m_delay_units); + DISPLAY_PARAM(m_delay_units_threshold); + + DISPLAY_PARAM(m_theory_resolve); + + DISPLAY_PARAM(m_restart_strategy); + DISPLAY_PARAM(m_restart_initial); + DISPLAY_PARAM(m_restart_factor); + DISPLAY_PARAM(m_restart_adaptive); + DISPLAY_PARAM(m_agility_factor); + DISPLAY_PARAM(m_restart_agility_threshold); + + DISPLAY_PARAM(m_lemma_gc_strategy); + DISPLAY_PARAM(m_lemma_gc_half); + DISPLAY_PARAM(m_recent_lemmas_size); + DISPLAY_PARAM(m_lemma_gc_initial); + DISPLAY_PARAM(m_lemma_gc_factor); + DISPLAY_PARAM(m_new_old_ratio); + DISPLAY_PARAM(m_new_clause_activity); + DISPLAY_PARAM(m_old_clause_activity); + DISPLAY_PARAM(m_new_clause_relevancy); + DISPLAY_PARAM(m_old_clause_relevancy); + DISPLAY_PARAM(m_inv_clause_decay); + + DISPLAY_PARAM(m_smtlib_dump_lemmas); + DISPLAY_PARAM(m_logic); + + DISPLAY_PARAM(m_profile_res_sub); + DISPLAY_PARAM(m_display_bool_var2expr); + DISPLAY_PARAM(m_display_ll_bool_var2expr); + DISPLAY_PARAM(m_abort_after_preproc); + + DISPLAY_PARAM(m_model); + DISPLAY_PARAM(m_model_compact); + DISPLAY_PARAM(m_model_on_timeout); + DISPLAY_PARAM(m_model_on_final_check); + + DISPLAY_PARAM(m_progress_sampling_freq); + + DISPLAY_PARAM(m_display_installed_theories); + DISPLAY_PARAM(m_core_validate); + + DISPLAY_PARAM(m_preprocess); + DISPLAY_PARAM(m_user_theory_preprocess_axioms); + DISPLAY_PARAM(m_user_theory_persist_axioms); + DISPLAY_PARAM(m_timeout); + DISPLAY_PARAM(m_rlimit); + DISPLAY_PARAM(m_at_labels_cex); + DISPLAY_PARAM(m_check_at_labels); + DISPLAY_PARAM(m_dump_goal_as_smt); + DISPLAY_PARAM(m_auto_config); +} \ No newline at end of file diff --git a/src/smt/params/smt_params.h b/src/smt/params/smt_params.h index 9c1eec649..366570365 100644 --- a/src/smt/params/smt_params.h +++ b/src/smt/params/smt_params.h @@ -289,6 +289,8 @@ struct smt_params : public preprocessor_params, void updt_params(params_ref const & p); void updt_params(context_params const & p); + + void display(std::ostream & out) const; }; #endif /* SMT_PARAMS_H_ */ diff --git a/src/smt/params/theory_arith_params.cpp b/src/smt/params/theory_arith_params.cpp index fef7ca2a0..1e3f29142 100644 --- a/src/smt/params/theory_arith_params.cpp +++ b/src/smt/params/theory_arith_params.cpp @@ -38,3 +38,51 @@ void theory_arith_params::updt_params(params_ref const & _p) { } +#define DISPLAY_PARAM(X) out << #X"=" << X << std::endl; + +void theory_arith_params::display(std::ostream & out) const { + DISPLAY_PARAM(m_arith_mode); + DISPLAY_PARAM(m_arith_auto_config_simplex); //!< force simplex solver in auto_config + DISPLAY_PARAM(m_arith_blands_rule_threshold); + DISPLAY_PARAM(m_arith_propagate_eqs); + DISPLAY_PARAM(m_arith_bound_prop); + DISPLAY_PARAM(m_arith_stronger_lemmas); + DISPLAY_PARAM(m_arith_skip_rows_with_big_coeffs); + DISPLAY_PARAM(m_arith_max_lemma_size); + DISPLAY_PARAM(m_arith_small_lemma_size); + DISPLAY_PARAM(m_arith_reflect); + DISPLAY_PARAM(m_arith_ignore_int); + DISPLAY_PARAM(m_arith_lazy_pivoting_lvl); + DISPLAY_PARAM(m_arith_random_seed); + DISPLAY_PARAM(m_arith_random_initial_value); + DISPLAY_PARAM(m_arith_random_lower); + DISPLAY_PARAM(m_arith_random_upper); + DISPLAY_PARAM(m_arith_adaptive); + DISPLAY_PARAM(m_arith_adaptive_assertion_threshold); + DISPLAY_PARAM(m_arith_adaptive_propagation_threshold); + DISPLAY_PARAM(m_arith_dump_lemmas); + DISPLAY_PARAM(m_arith_eager_eq_axioms); + DISPLAY_PARAM(m_arith_branch_cut_ratio); + DISPLAY_PARAM(m_arith_int_eq_branching); + DISPLAY_PARAM(m_arith_enum_const_mod); + DISPLAY_PARAM(m_arith_gcd_test); + DISPLAY_PARAM(m_arith_eager_gcd); + DISPLAY_PARAM(m_arith_adaptive_gcd); + DISPLAY_PARAM(m_arith_propagation_threshold); + DISPLAY_PARAM(m_arith_pivot_strategy); + DISPLAY_PARAM(m_arith_add_binary_bounds); + DISPLAY_PARAM(m_arith_propagation_strategy); + DISPLAY_PARAM(m_arith_eq_bounds); + DISPLAY_PARAM(m_arith_lazy_adapter); + DISPLAY_PARAM(m_arith_fixnum); + DISPLAY_PARAM(m_arith_int_only); + DISPLAY_PARAM(m_nl_arith); + DISPLAY_PARAM(m_nl_arith_gb); + DISPLAY_PARAM(m_nl_arith_gb_threshold); + DISPLAY_PARAM(m_nl_arith_gb_eqs); + DISPLAY_PARAM(m_nl_arith_gb_perturbate); + DISPLAY_PARAM(m_nl_arith_max_degree); + DISPLAY_PARAM(m_nl_arith_branching); + DISPLAY_PARAM(m_nl_arith_rounds); + DISPLAY_PARAM(m_arith_euclidean_solver); +} \ No newline at end of file diff --git a/src/smt/params/theory_arith_params.h b/src/smt/params/theory_arith_params.h index 18418d1ef..943bd711e 100644 --- a/src/smt/params/theory_arith_params.h +++ b/src/smt/params/theory_arith_params.h @@ -156,6 +156,8 @@ struct theory_arith_params { } void updt_params(params_ref const & p); + + void display(std::ostream & out) const; }; #endif /* THEORY_ARITH_PARAMS_H_ */ diff --git a/src/smt/params/theory_array_params.cpp b/src/smt/params/theory_array_params.cpp index e3c8b2448..c0015bf2c 100644 --- a/src/smt/params/theory_array_params.cpp +++ b/src/smt/params/theory_array_params.cpp @@ -25,4 +25,16 @@ void theory_array_params::updt_params(params_ref const & _p) { m_array_extensional = p.array_extensional(); } +#define DISPLAY_PARAM(X) out << #X"=" << X << std::endl; +void theory_array_params::display(std::ostream & out) const { + DISPLAY_PARAM(m_array_mode); + DISPLAY_PARAM(m_array_weak); + DISPLAY_PARAM(m_array_extensional); + DISPLAY_PARAM(m_array_laziness); + DISPLAY_PARAM(m_array_delay_exp_axiom); + DISPLAY_PARAM(m_array_cg); + DISPLAY_PARAM(m_array_always_prop_upward); + DISPLAY_PARAM(m_array_lazy_ieq); + DISPLAY_PARAM(m_array_lazy_ieq_delay); +} \ No newline at end of file diff --git a/src/smt/params/theory_array_params.h b/src/smt/params/theory_array_params.h index 85996078f..af51427c4 100644 --- a/src/smt/params/theory_array_params.h +++ b/src/smt/params/theory_array_params.h @@ -71,6 +71,7 @@ struct theory_array_params : public array_simplifier_params { } #endif + void display(std::ostream & out) const; }; diff --git a/src/smt/params/theory_bv_params.cpp b/src/smt/params/theory_bv_params.cpp index d3f386ab4..631c5765b 100644 --- a/src/smt/params/theory_bv_params.cpp +++ b/src/smt/params/theory_bv_params.cpp @@ -24,3 +24,14 @@ void theory_bv_params::updt_params(params_ref const & _p) { m_bv_reflect = p.bv_reflect(); m_bv_enable_int2bv2int = p.bv_enable_int2bv(); } + +#define DISPLAY_PARAM(X) out << #X"=" << X << std::endl; + +void theory_bv_params::display(std::ostream & out) const { + DISPLAY_PARAM(m_bv_mode); + DISPLAY_PARAM(m_bv_reflect); + DISPLAY_PARAM(m_bv_lazy_le); + DISPLAY_PARAM(m_bv_cc); + DISPLAY_PARAM(m_bv_blast_max_size); + DISPLAY_PARAM(m_bv_enable_int2bv2int); +} \ No newline at end of file diff --git a/src/smt/params/theory_bv_params.h b/src/smt/params/theory_bv_params.h index 00565969e..5830e5176 100644 --- a/src/smt/params/theory_bv_params.h +++ b/src/smt/params/theory_bv_params.h @@ -44,6 +44,8 @@ struct theory_bv_params { } void updt_params(params_ref const & p); + + void display(std::ostream & out) const; }; #endif /* THEORY_BV_PARAMS_H_ */ diff --git a/src/smt/params/theory_datatype_params.h b/src/smt/params/theory_datatype_params.h index 4dd09a596..9f801e46c 100644 --- a/src/smt/params/theory_datatype_params.h +++ b/src/smt/params/theory_datatype_params.h @@ -31,6 +31,8 @@ struct theory_datatype_params { p.register_unsigned_param("dt_lazy_splits", m_dt_lazy_splits, "How lazy datatype splits are performed: 0- eager, 1- lazy for infinite types, 2- lazy"); } #endif + + void display(std::ostream & out) const { out << "m_dt_lazy_splits=" << m_dt_lazy_splits << std::endl; } }; diff --git a/src/smt/params/theory_pb_params.cpp b/src/smt/params/theory_pb_params.cpp index 6d980fe5d..a1e13a6e7 100644 --- a/src/smt/params/theory_pb_params.cpp +++ b/src/smt/params/theory_pb_params.cpp @@ -26,3 +26,12 @@ void theory_pb_params::updt_params(params_ref const & _p) { m_pb_enable_compilation = p.pb_enable_compilation(); m_pb_enable_simplex = p.pb_enable_simplex(); } + +#define DISPLAY_PARAM(X) out << #X"=" << X << std::endl; + +void theory_pb_params::display(std::ostream & out) const { + DISPLAY_PARAM(m_pb_conflict_frequency); + DISPLAY_PARAM(m_pb_learn_complements); + DISPLAY_PARAM(m_pb_enable_compilation); + DISPLAY_PARAM(m_pb_enable_simplex); +} \ No newline at end of file diff --git a/src/smt/params/theory_pb_params.h b/src/smt/params/theory_pb_params.h index 2af4f04b7..6a129e601 100644 --- a/src/smt/params/theory_pb_params.h +++ b/src/smt/params/theory_pb_params.h @@ -35,6 +35,8 @@ struct theory_pb_params { {} void updt_params(params_ref const & p); + + void display(std::ostream & out) const; }; #endif /* THEORY_PB_PARAMS_H_ */ From c72ed3e6b4c7fdde58bb564e90dd925097c79a97 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 23 Jun 2016 21:39:28 -0700 Subject: [PATCH 14/17] update core minimization code Signed-off-by: Nikolaj Bjorner --- src/opt/maxres.cpp | 11 +- src/qe/qsat.cpp | 8 +- src/smt/params/smt_params_helper.pyg | 3 +- src/smt/smt_solver.cpp | 42 +++- src/solver/mus.cpp | 286 +++++++++++++++++++-------- src/solver/mus.h | 8 +- src/solver/solver_na2as.h | 1 + src/util/hashtable.h | 36 +++- src/util/obj_hashtable.h | 1 + 9 files changed, 287 insertions(+), 109 deletions(-) diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp index b52c7d9b9..b6950f674 100644 --- a/src/opt/maxres.cpp +++ b/src/opt/maxres.cpp @@ -544,18 +544,11 @@ public: return l_true; } m_mus.reset(); - for (unsigned i = 0; i < core.size(); ++i) { - VERIFY(i == m_mus.add_soft(core[i])); - } - unsigned_vector mus_idx; - lbool is_sat = m_mus.get_mus(mus_idx); + m_mus.add_soft(core.size(), core.c_ptr()); + lbool is_sat = m_mus.get_mus(m_new_core); if (is_sat != l_true) { return is_sat; } - m_new_core.reset(); - for (unsigned i = 0; i < mus_idx.size(); ++i) { - m_new_core.push_back(core[mus_idx[i]]); - } core.reset(); core.append(m_new_core); return l_true; diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp index 74b6769ae..02c6d26cd 100644 --- a/src/qe/qsat.cpp +++ b/src/qe/qsat.cpp @@ -811,14 +811,10 @@ namespace qe { } TRACE("qe", tout << core1.size() << " " << core2.size() << "\n";); if (core1.size() > 8) { - unsigned_vector core_idxs; - if (l_true != mus.get_mus(core_idxs)) { + if (l_true != mus.get_mus(core2)) { return false; } - TRACE("qe", tout << core1.size() << " -> " << core_idxs.size() << "\n";); - for (unsigned i = 0; i < core_idxs.size(); ++i) { - core2.push_back(core1[core_idxs[i]].get()); - } + TRACE("qe", tout << core1.size() << " -> " << core2.size() << "\n";); core.reset(); core.append(core2); } diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index a9f6ccc18..153d948f5 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -61,5 +61,6 @@ def_module_params(module_name='smt', ('dack.gc', UINT, 2000, 'Dynamic ackermannization garbage collection frequency (per conflict)'), ('dack.gc_inv_decay', DOUBLE, 0.8, 'Dynamic ackermannization garbage collection decay'), ('dack.threshold', UINT, 10, ' number of times the congruence rule must be used before Leibniz\'s axiom is expanded'), - ('core.validate', BOOL, False, 'validate unsat core produced by SMT context') + ('core.validate', BOOL, False, 'validate unsat core produced by SMT context'), + ('core.minimize', BOOL, False, 'minimize unsat core produced by SMT context') )) diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index 59c08006b..6ae7f107c 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -20,19 +20,25 @@ Notes: #include"smt_kernel.h" #include"reg_decl_plugins.h" #include"smt_params.h" +#include"smt_params_helper.hpp" +#include"mus.h" namespace smt { class solver : public solver_na2as { - smt_params m_params; + smt_params m_smt_params; + params_ref m_params; smt::kernel m_context; progress_callback * m_callback; symbol m_logic; + bool m_minimizing_core; public: solver(ast_manager & m, params_ref const & p, symbol const & l): solver_na2as(m), + m_smt_params(p), m_params(p), - m_context(m, m_params) { + m_context(m, m_smt_params), + m_minimizing_core(false) { m_logic = l; if (m_logic != symbol::null) m_context.set_logic(m_logic); @@ -48,7 +54,8 @@ namespace smt { } virtual void updt_params(params_ref const & p) { - m_params.updt_params(p); + m_smt_params.updt_params(p); + m_params.copy(p); m_context.updt_params(p); } @@ -77,10 +84,37 @@ namespace smt { return m_context.check(num_assumptions, assumptions); } + struct scoped_minimize_core { + solver& s; + expr_ref_vector m_assumptions; + scoped_minimize_core(solver& s): s(s), m_assumptions(s.m_assumptions) { + s.m_minimizing_core = true; + s.m_assumptions.reset(); + } + + ~scoped_minimize_core() { + s.m_minimizing_core = false; + s.m_assumptions.append(m_assumptions); + } + }; + virtual void get_unsat_core(ptr_vector & r) { unsigned sz = m_context.get_unsat_core_size(); - for (unsigned i = 0; i < sz; i++) + for (unsigned i = 0; i < sz; i++) { r.push_back(m_context.get_unsat_core_expr(i)); + } + + if (m_minimizing_core || smt_params_helper(m_params).core_minimize() == false) { + return; + } + scoped_minimize_core scm(*this); + mus mus(*this); + mus.add_soft(r.size(), r.c_ptr()); + ptr_vector r2; + if (l_true == mus.get_mus(r2)) { + r.reset(); + r.append(r2); + } } virtual void get_model(model_ref & m) { diff --git a/src/solver/mus.cpp b/src/solver/mus.cpp index 4960a3d2a..adfe42192 100644 --- a/src/solver/mus.cpp +++ b/src/solver/mus.cpp @@ -22,10 +22,13 @@ Notes: #include "mus.h" #include "ast_pp.h" #include "ast_util.h" -#include "uint_set.h" +#include "model_evaluator.h" struct mus::imp { + + typedef obj_hashtable expr_set; + solver& m_solver; ast_manager& m; expr_ref_vector m_lit2expr; @@ -56,7 +59,7 @@ struct mus::imp { unsigned idx = m_lit2expr.size(); m_expr2lit.insert(lit, idx); m_lit2expr.push_back(lit); - TRACE("opt", tout << idx << ": " << mk_pp(lit, m) << "\n" << m_lit2expr << "\n";); + TRACE("mus", tout << idx << ": " << mk_pp(lit, m) << "\n" << m_lit2expr << "\n";); return idx; } @@ -64,66 +67,61 @@ struct mus::imp { SASSERT(is_literal(lit)); m_assumptions.push_back(lit); } - - lbool get_mus(unsigned_vector& mus) { - // SASSERT: mus does not have duplicates. + + lbool get_mus(expr_ref_vector& mus) { m_model.reset(); - unsigned_vector core; - for (unsigned i = 0; i < m_lit2expr.size(); ++i) { - core.push_back(i); - } - if (core.size() == 1) { - mus.push_back(core.back()); + mus.reset(); + if (m_lit2expr.size() == 1) { + mus.push_back(m_lit2expr.back()); return l_true; } + return get_mus1(mus); + } + lbool get_mus(ptr_vector& mus) { mus.reset(); - if (false && core.size() > 64) { - return qx(mus); - } + expr_ref_vector result(m); + lbool r = get_mus(result); + mus.append(result.size(), result.c_ptr()); + return r; + } - expr_ref_vector assumptions(m); + lbool get_mus1(expr_ref_vector& mus) { + ptr_vector unknown(m_lit2expr.size(), m_lit2expr.c_ptr()); ptr_vector core_exprs; - while (!core.empty()) { - IF_VERBOSE(12, verbose_stream() << "(opt.mus reducing core: " << core.size() << " new core: " << mus.size() << ")\n";); - unsigned lit_id = core.back(); - TRACE("opt", - display_vec(tout << "core: ", core); - display_vec(tout << "mus: ", mus); - ); - core.pop_back(); - expr* lit = m_lit2expr[lit_id].get(); - expr_ref not_lit(m); - not_lit = mk_not(m, lit); + while (!unknown.empty()) { + IF_VERBOSE(12, verbose_stream() << "(mus reducing core: " << unknown.size() << " new core: " << mus.size() << ")\n";); + TRACE("mus", display_vec(tout << "core: ", unknown); display_vec(tout << "mus: ", mus);); + expr* lit = unknown.back(); + unknown.pop_back(); + expr_ref not_lit(mk_not(m, lit), m); lbool is_sat = l_undef; { - scoped_append _sa1(*this, assumptions, core); - scoped_append _sa2(*this, assumptions, m_assumptions); - assumptions.push_back(not_lit); - is_sat = m_solver.check_sat(assumptions); + scoped_append _sa1(*this, mus, unknown); + scoped_append _sa2(*this, mus, m_assumptions); + mus.push_back(not_lit); + is_sat = m_solver.check_sat(mus); } switch (is_sat) { case l_undef: return is_sat; case l_true: - assumptions.push_back(lit); - mus.push_back(lit_id); + mus.push_back(lit); update_model(); break; default: core_exprs.reset(); m_solver.get_unsat_core(core_exprs); if (!core_exprs.contains(not_lit)) { - // core := core_exprs \ mus - core.reset(); + // unknown := core_exprs \ mus + unknown.reset(); for (unsigned i = 0; i < core_exprs.size(); ++i) { - lit = core_exprs[i]; - if (m_expr2lit.find(lit, lit_id) && !mus.contains(lit_id)) { - core.push_back(lit_id); + if (!mus.contains(core_exprs[i])) { + unknown.push_back(core_exprs[i]); } } - TRACE("opt", display_vec(tout << "core exprs:", core_exprs); - display_vec(tout << "core:", core); + TRACE("mus", display_vec(tout << "core exprs:", core_exprs); + display_vec(tout << "core:", unknown); display_vec(tout << "mus:", mus); ); @@ -131,36 +129,146 @@ struct mus::imp { break; } } -#if 0 - DEBUG_CODE( - assumptions.reset(); - for (unsigned i = 0; i < mus.size(); ++i) { - assumptions.push_back(m_lit2expr[mus[i]].get()); - } - lbool is_sat = m_solver.check_sat(assumptions.size(), assumptions.c_ptr()); - SASSERT(is_sat == l_false); - ); -#endif + // SASSERT(is_core(mus)); return l_true; } + // use correction sets + lbool get_mus2(expr_ref_vector& mus) { + expr* lit = 0; + lbool is_sat; + ptr_vector unknown(m_lit2expr.size(), m_lit2expr.c_ptr()); + while (!unknown.empty()) { + IF_VERBOSE(12, verbose_stream() << "(mus reducing core: " << unknown.size() << " new core: " << mus.size() << ")\n";); + { + scoped_append _sa1(*this, mus, m_assumptions); + is_sat = get_next_mcs(mus, unknown, lit); + } + if (l_false == is_sat) { + mus.push_back(lit); + } + else { + return is_sat; + } + } + + //SASSERT(is_core(mus)); + return l_true; + } + + // find the next literal to be a member of a core. + lbool get_next_mcs(expr_ref_vector& mus, ptr_vector& unknown, expr*& core_literal) { + ptr_vector mss; + expr_ref_vector nmcs(m); + expr_set core, min_core, nmcs_set; + bool min_core_valid = false; + expr* min_lit = 0; + while (!unknown.empty()) { + expr* lit = unknown.back(); + unknown.pop_back(); + model_ref mdl; + scoped_append assume_mss(*this, mus, mss); // current satisfied literals + scoped_append assume_nmcs(*this, mus, nmcs); // current non-satisfied literals + scoped_append assume_lit(*this, mus, lit); // current unknown literal + switch (m_solver.check_sat(mus)) { + case l_true: { + TRACE("mus", tout << "literal can be satisfied: " << mk_pp(lit, m) << "\n";); + mss.push_back(lit); + m_solver.get_model(mdl); + model_evaluator eval(*mdl.get()); + for (unsigned i = 0; i < unknown.size(); ) { + expr_ref tmp(m); + eval(unknown[i], tmp); + if (m.is_true(tmp)) { + mss.push_back(unknown[i]); + unknown[i] = unknown.back(); + unknown.pop_back(); + } + else { + ++i; + } + } + break; + } + case l_false: + TRACE("mus", tout << "literal is in a core: " << mk_pp(lit, m) << "\n";); + nmcs.push_back(mk_not(m, lit)); + nmcs_set.insert(nmcs.back()); + get_core(core); + if (!core.contains(lit)) { + // The current mus is already a core. + unknown.reset(); + return l_true; + } + if (have_intersection(nmcs_set, core)) { + // can't use this core directly. Hypothetically, we + // could try to combine min_core with core and + // see if the combination produces a better minimal core. + SASSERT(min_core_valid); + break; + } + if (!min_core_valid || core.size() < min_core.size()) { + // The current core is smallest so far, so we get fewer unknowns from it. + min_core = core; + min_core_valid = true; + min_lit = lit; + } + break; + case l_undef: + return l_undef; + } + } + SASSERT(min_core_valid); + if (!min_core_valid) { + // all unknown soft constraints were satisfiable + return l_true; + } + + expr_set mss_set; + for (unsigned i = 0; i < mss.size(); ++i) { + mss_set.insert(mss[i]); + } + expr_set::iterator it = min_core.begin(), end = min_core.end(); + for (; it != end; ++it) { + if (mss_set.contains(*it) && min_lit != *it) { + unknown.push_back(*it); + } + } + core_literal = min_lit; + + return l_false; + } + + bool have_intersection(expr_set const& A, expr_set const& B) { + if (A.size() < B.size()) { + expr_set::iterator it = A.begin(), end = A.end(); + for (; it != end; ++it) { + if (B.contains(*it)) return true; + } + } + else { + expr_set::iterator it = B.begin(), end = B.end(); + for (; it != end; ++it) { + if (A.contains(*it)) return true; + } + } + return false; + } + + bool is_core(expr_ref_vector const& mus) { + return l_false == m_solver.check_sat(mus); + } + class scoped_append { expr_ref_vector& m_fmls; unsigned m_size; public: - scoped_append(imp& imp, expr_ref_vector& fmls1, unsigned_vector const& fmls2): + scoped_append(imp& imp, expr_ref_vector& fmls1, expr_set const& fmls2): m_fmls(fmls1), m_size(fmls1.size()) { - for (unsigned i = 0; i < fmls2.size(); ++i) { - fmls1.push_back(imp.m_lit2expr[fmls2[i]].get()); - } - } - scoped_append(imp& imp, expr_ref_vector& fmls1, uint_set const& fmls2): - m_fmls(fmls1), - m_size(fmls1.size()) { - uint_set::iterator it = fmls2.begin(), end = fmls2.end(); + expr_set::iterator it = fmls2.begin(), end = fmls2.end(); for (; it != end; ++it) { - fmls1.push_back(imp.m_lit2expr[*it].get()); + fmls1.push_back(*it); } } scoped_append(imp& imp, expr_ref_vector& fmls1, expr_ref_vector const& fmls2): @@ -168,17 +276,21 @@ struct mus::imp { m_size(fmls1.size()) { fmls1.append(fmls2); } + scoped_append(imp& imp, expr_ref_vector& fmls1, ptr_vector const& fmls2): + m_fmls(fmls1), + m_size(fmls1.size()) { + fmls1.append(fmls2.size(), fmls2.c_ptr()); + } + scoped_append(imp& imp, expr_ref_vector& fmls1, expr* fml): + m_fmls(fmls1), + m_size(fmls1.size()) { + fmls1.push_back(fml); + } ~scoped_append() { m_fmls.shrink(m_size); } }; - void add_core(unsigned_vector const& core, expr_ref_vector& assumptions) { - for (unsigned i = 0; i < core.size(); ++i) { - assumptions.push_back(m_lit2expr[core[i]].get()); - } - } - template void display_vec(std::ostream& out, T const& v) const { for (unsigned i = 0; i < v.size(); ++i) { @@ -234,14 +346,14 @@ struct mus::imp { } - lbool qx(unsigned_vector& mus) { - uint_set core, support; + lbool qx(expr_ref_vector& mus) { + expr_set core, support; for (unsigned i = 0; i < m_lit2expr.size(); ++i) { - core.insert(i); + core.insert(m_lit2expr[i].get()); } lbool is_sat = qx(core, support, false); if (is_sat == l_true) { - uint_set::iterator it = core.begin(), end = core.end(); + expr_set::iterator it = core.begin(), end = core.end(); mus.reset(); for (; it != end; ++it) { mus.push_back(*it); @@ -250,7 +362,7 @@ struct mus::imp { return is_sat; } - lbool qx(uint_set& assignment, uint_set& support, bool has_support) { + lbool qx(expr_set& assignment, expr_set& support, bool has_support) { lbool is_sat = l_true; #if 0 if (s.m_config.m_minimize_core_partial && s.m_stats.m_restart - m_restart > m_max_restarts) { @@ -265,7 +377,7 @@ struct mus::imp { is_sat = m_solver.check_sat(asms); switch (is_sat) { case l_false: { - uint_set core; + expr_set core; get_core(core); support &= core; assignment.reset(); @@ -280,10 +392,10 @@ struct mus::imp { break; } } - if (assignment.num_elems() == 1) { + if (assignment.size() == 1) { return l_true; } - uint_set assign2; + expr_set assign2; split(assignment, assign2); support |= assignment; is_sat = qx(assign2, support, !assignment.empty()); @@ -296,20 +408,20 @@ struct mus::imp { return is_sat; } - void get_core(uint_set& core) { + void get_core(expr_set& core) { + core.reset(); ptr_vector core_exprs; - unsigned lit_id; m_solver.get_unsat_core(core_exprs); for (unsigned i = 0; i < core_exprs.size(); ++i) { - if (m_expr2lit.find(core_exprs[i], lit_id)) { - core.insert(lit_id); + if (m_expr2lit.contains(core_exprs[i])) { + core.insert(core_exprs[i]); } } } - void unsplit(uint_set& A, uint_set& B) { - uint_set A1, B1; - uint_set::iterator it = A.begin(), end = A.end(); + void unsplit(expr_set& A, expr_set& B) { + expr_set A1, B1; + expr_set::iterator it = A.begin(), end = A.end(); for (; it != end; ++it) { if (B.contains(*it)) { B1.insert(*it); @@ -322,10 +434,10 @@ struct mus::imp { B = B1; } - void split(uint_set& lits1, uint_set& lits2) { - unsigned half = lits1.num_elems()/2; - uint_set lits3; - uint_set::iterator it = lits1.begin(), end = lits1.end(); + void split(expr_set& lits1, expr_set& lits2) { + unsigned half = lits1.size()/2; + expr_set lits3; + expr_set::iterator it = lits1.begin(), end = lits1.end(); for (unsigned i = 0; it != end; ++it, ++i) { if (i < half) { lits3.insert(*it); @@ -355,7 +467,11 @@ void mus::add_assumption(expr* lit) { return m_imp->add_assumption(lit); } -lbool mus::get_mus(unsigned_vector& mus) { +lbool mus::get_mus(ptr_vector& mus) { + return m_imp->get_mus(mus); +} + +lbool mus::get_mus(expr_ref_vector& mus) { return m_imp->get_mus(mus); } diff --git a/src/solver/mus.h b/src/solver/mus.h index d2411b6ec..f2e543f04 100644 --- a/src/solver/mus.h +++ b/src/solver/mus.h @@ -33,6 +33,10 @@ class mus { Assume also that cls is a literal. */ unsigned add_soft(expr* cls); + + void add_soft(unsigned sz, expr* const* clss) { + for (unsigned i = 0; i < sz; ++i) add_soft(clss[i]); + } /** Additional assumption for solver to be used along with solver context, @@ -43,7 +47,9 @@ class mus { */ void add_assumption(expr* lit); - lbool get_mus(unsigned_vector& mus); + lbool get_mus(ptr_vector& mus); + + lbool get_mus(expr_ref_vector& mus); void reset(); diff --git a/src/solver/solver_na2as.h b/src/solver/solver_na2as.h index 019468fd7..9aeb56fb1 100644 --- a/src/solver/solver_na2as.h +++ b/src/solver/solver_na2as.h @@ -25,6 +25,7 @@ Notes: #include"solver.h" class solver_na2as : public solver { + protected: ast_manager & m; expr_ref_vector m_assumptions; unsigned_vector m_scopes; diff --git a/src/util/hashtable.h b/src/util/hashtable.h index 488157c00..fe51963e0 100644 --- a/src/util/hashtable.h +++ b/src/util/hashtable.h @@ -556,6 +556,38 @@ public: out << "]"; } + core_hashtable& operator|=(core_hashtable const& other) { + if (this == &other) return *this; + iterator i = begin(), e = end(); + for (; i != e; ++i) { + insert(*i); + } + return *this; + } + + + core_hashtable& operator&=(core_hashtable const& other) { + if (this == &other) return *this; + core_hashtable copy(*this); + iterator i = copy.begin(), e = copy.end(); + for (; i != e; ++i) { + if (!other.contains(*i)) { + remove(*i); + } + } + return *this; + } + + core_hashtable& operator=(core_hashtable const& other) { + if (this == &other) return *this; + reset(); + core_hashtable::iterator i = other.begin(), e = other.end(); + for (; i != e; ++i) { + insert(*i); + } + return *this; + } + #ifdef Z3DEBUG bool check_invariant() { entry * curr = m_table; @@ -582,9 +614,6 @@ public: unsigned long long get_num_collision() const { return 0; } #endif - private: - - core_hashtable& operator=(core_hashtable const&); }; @@ -640,4 +669,5 @@ public: core_hashtable, HashProc, EqProc>(initial_capacity, h, e) {} }; + #endif /* HASHTABLE_H_ */ diff --git a/src/util/obj_hashtable.h b/src/util/obj_hashtable.h index 4e948d96d..383ecaeb3 100644 --- a/src/util/obj_hashtable.h +++ b/src/util/obj_hashtable.h @@ -51,6 +51,7 @@ class obj_hashtable : public core_hashtable, obj_ptr_hash, public: obj_hashtable(unsigned initial_capacity = DEFAULT_HASHTABLE_INITIAL_CAPACITY): core_hashtable, obj_ptr_hash, ptr_eq >(initial_capacity) {} + }; template From 5845e633962845424ff38571ab80f04857667b51 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martin=20R=2E=20Neuh=C3=A4u=C3=9Fer?= Date: Tue, 14 Jun 2016 14:13:44 +0200 Subject: [PATCH 15/17] Make cmake not emit -fPIC to mingw64 for Windows builds. This patch detects a mingw64 build of the shared library and does not emit -fPIC to the compiler. This is necessary to avoid a warning message, as Windows native code DLLs are generally relocatable and not position independent. --- CMakeLists.txt | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index ee0810295..c9a01daed 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -304,7 +304,10 @@ endif() # library. If not building a shared library ``-fPIC`` isn't needed and would add # unnecessary overhead. if (BUILD_LIBZ3_SHARED) - if (NOT MSVC) + # Avoid adding -fPIC compiler switch if we compile with MSVC (which does not + # support the flag) or if we target Windows, which generally does not use + # position independent code for native code shared libraries (DLLs). + if (NOT (MSVC OR MINGW OR WIN32)) z3_add_cxx_flag("-fPIC" REQUIRED) endif() endif() @@ -387,4 +390,3 @@ option(ENABLE_EXAMPLE_TARGETS "Build Z3 api examples" ON) if (ENABLE_EXAMPLE_TARGETS) add_subdirectory(examples) endif() - From 1fb672121c14e39ab4c86e8c74905f6515dc0041 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 24 Jun 2016 13:57:53 +0100 Subject: [PATCH 16/17] build fix for cygwin/mingw --- scripts/mk_util.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 509487e23..8fafd1caa 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -604,7 +604,7 @@ elif os.name == 'posix': IS_OPENBSD=True elif os.uname()[0][:6] == 'CYGWIN': IS_CYGWIN=True - if ("mingw" in CC): + if (CC != None and "mingw" in CC): IS_CYGWIN_MINGW=True def display_help(exit_code): From e9eb88e1b3cd993641f68add997061a831e5b315 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 24 Jun 2016 15:08:56 +0100 Subject: [PATCH 17/17] fixed java build issues. Relates to #648. --- examples/java/JavaExample.java | 2 +- src/api/java/Context.java | 5 +++++ 2 files changed, 6 insertions(+), 1 deletion(-) diff --git a/examples/java/JavaExample.java b/examples/java/JavaExample.java index 74e94617d..5c8a7508f 100644 --- a/examples/java/JavaExample.java +++ b/examples/java/JavaExample.java @@ -188,7 +188,7 @@ class JavaExample /* do something with the context */ /* be kind to dispose manually and not wait for the GC. */ - ctx.dispose(); + ctx.close(); } } diff --git a/src/api/java/Context.java b/src/api/java/Context.java index 39d35d9d3..da924026c 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -35,6 +35,11 @@ public class Context implements AutoCloseable { init(); } + protected Context (long m_ctx) { + this.m_ctx = m_ctx; + init(); + } + /** * Constructor.