From e856cfc458630f54980643d702deec2abb522273 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 6 Feb 2021 10:35:28 -0800
Subject: [PATCH] coercions
---
src/api/api_opt.cpp | 2 +-
src/api/python/z3/z3.py | 11 ++++-------
2 files changed, 5 insertions(+), 8 deletions(-)
diff --git a/src/api/api_opt.cpp b/src/api/api_opt.cpp
index b12cbe209..220e85241 100644
--- a/src/api/api_opt.cpp
+++ b/src/api/api_opt.cpp
@@ -456,7 +456,7 @@ extern "C" {
ctx.c = c;
ctx.m = m;
ctx.user_context = user_context;
- ctx.on_model = model_eh;
+ ctx.on_model = (void*)model_eh;
to_optimize_ptr(o)->register_on_model(ctx, _model_eh);
Z3_CATCH;
}
diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index 6f2dde684..0c298e42f 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -7408,8 +7408,8 @@ class OptimizeObjective:
_on_models = {}
def _global_on_model(ctx):
- (opt, mdl) = _on_models[ctx]
- opt.on_model(mdl)
+ (fn, mdl) = _on_models[ctx]
+ fn(mdl)
_on_model_eh = on_model_eh_type(_global_on_model)
@@ -7606,14 +7606,11 @@ class Optimize(Z3PPObject):
"""
return Statistics(Z3_optimize_get_statistics(self.ctx.ref(), self.optimize), self.ctx)
- def on_model(self, m):
- self._on_model(m)
-
def set_on_model(self, on_model):
- self._on_model = on_model
id = len(_on_models) + 41
mdl = Model(self.ctx)
- _on_models[id] = (self, mdl)
+ _on_models[id] = (on_model, mdl)
+ self._on_models_id = id
Z3_optimize_register_model_eh(self.ctx.ref(), self.optimize, mdl.model, ctypes.c_void_p(id), _on_model_eh)