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

Use constructors instead of static methods for Context.java.

Browse source
This commit is contained in:
George Karpenkov 2016-06-16 18:21:55 +02:00
parent b65d83aacf
commit b086aac45f
1 changed files with 9 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -30,8 +30,9 @@ public class Context implements AutoCloseable {
private final long m_ctx; private final long m_ctx;
static final Object creation_lock = new Object(); static final Object creation_lock = new Object();
public static Context mkContext() { public Context () {
return new Context(Native.mkContextRc(0)); 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 * 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} * module parameters. For this purpose we should now use {@code Global.setParameter}
**/ **/
public static Context mkContext(Map<String, String> settings) public Context(Map<String, String> settings) {
{
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());
long m_ctx = Native.mkContextRc(cfg); }
m_ctx = Native.mkContextRc(cfg);
Native.delConfig(cfg); Native.delConfig(cfg);
return new Context(m_ctx); init();
} }
/** private void init() {
* 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); setPrintMode(Z3_ast_print_mode.Z3_PRINT_SMTLIB2_COMPLIANT);
Native.setInternalErrorHandler(m_ctx); Native.setInternalErrorHandler(m_ctx);
} }