mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-12 09:03:26 +00:00
Code Activity

Re-added context creation locks in the Java API. Relates to #819.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-12-01 23:16:15 +00:00
parent dedae29300
commit f1a704484b
1 changed files with 20 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/api/java/Context.java
View file

@ -31,14 +31,18 @@ public class Context implements AutoCloseable {
static final Object creation_lock = new Object(); static final Object creation_lock = new Object();
public Context () { public Context () {
synchronized (creation_lock) {
m_ctx = Native.mkContextRc(0); m_ctx = Native.mkContextRc(0);
init(); init();
} }
}
protected Context (long m_ctx) { protected Context (long m_ctx) {
synchronized (creation_lock) {
this.m_ctx = m_ctx; this.m_ctx = m_ctx;
init(); init();
} }
}
/** /**
@ -59,6 +63,7 @@ public class Context implements AutoCloseable {
* module parameters. For this purpose we should now use {@code Global.setParameter} * module parameters. For this purpose we should now use {@code Global.setParameter}
**/ **/
public Context(Map<String, String> settings) { public Context(Map<String, String> settings) {
synchronized (creation_lock) {
long cfg = Native.mkConfig(); long cfg = Native.mkConfig();
for (Map.Entry<String, String> kv : settings.entrySet()) { for (Map.Entry<String, String> kv : settings.entrySet()) {
Native.setParamValue(cfg, kv.getKey(), kv.getValue()); Native.setParamValue(cfg, kv.getKey(), kv.getValue());
@ -67,6 +72,7 @@ public class Context implements AutoCloseable {
Native.delConfig(cfg); Native.delConfig(cfg);
init(); init();
} }
}
private void init() { private void init() {
setPrintMode(Z3_ast_print_mode.Z3_PRINT_SMTLIB2_COMPLIANT); setPrintMode(Z3_ast_print_mode.Z3_PRINT_SMTLIB2_COMPLIANT);
@ -4038,6 +4044,8 @@ public class Context implements AutoCloseable {
m_realSort = null; m_realSort = null;
m_stringSort = null; m_stringSort = null;
synchronized (creation_lock) {
Native.delContext(m_ctx); Native.delContext(m_ctx);
} }
} }
}