mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-13 17:36:15 +00:00
Code Activity

Do not lock on context creation and deletion.

Browse source
This commit is contained in:
George Karpenkov 2016-06-13 12:09:34 +02:00
parent 22ffd65d1e
commit 27aa37946e
1 changed files with 7 additions and 17 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -31,12 +31,7 @@ public class Context implements AutoCloseable {
static final Object creation_lock = new Object(); static final Object creation_lock = new Object();
public static Context mkContext() { public static Context mkContext() {
long m_ctx; return new Context(Native.mkContextRc(0));
synchronized (creation_lock) {
m_ctx = Native.mkContextRc(0);
// TODO: then adding settings will not be under the lock.
}
return new Context(m_ctx);
} }
@ -59,14 +54,11 @@ public class Context implements AutoCloseable {
**/ **/
public static Context mkContext(Map<String, String> settings) public static Context mkContext(Map<String, String> settings)
{ {
long m_ctx; long cfg = Native.mkConfig();
synchronized (creation_lock) { for (Map.Entry<String, String> kv : settings.entrySet())
long cfg = Native.mkConfig(); Native.setParamValue(cfg, kv.getKey(), kv.getValue());
for (Map.Entry<String, String> kv : settings.entrySet()) long m_ctx = Native.mkContextRc(cfg);
Native.setParamValue(cfg, kv.getKey(), kv.getValue()); Native.delConfig(cfg);
m_ctx = Native.mkContextRc(cfg);
Native.delConfig(cfg);
}
return new Context(m_ctx); return new Context(m_ctx);
} }
@ -4047,8 +4039,6 @@ 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);
}
} }
} }