mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

coercions

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-02-06 10:35:28 -08:00
parent 16448104eb
commit e856cfc458
2 changed files with 5 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/api/api_opt.cpp
View file

@ -456,7 +456,7 @@ extern "C" {
ctx.c = c; ctx.c = c;
ctx.m = m; ctx.m = m;
ctx.user_context = user_context; 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); to_optimize_ptr(o)->register_on_model(ctx, _model_eh);
Z3_CATCH; Z3_CATCH;
} }

11
src/api/python/z3/z3.py
View file

@ -7408,8 +7408,8 @@ class OptimizeObjective:
_on_models = {} _on_models = {}
def _global_on_model(ctx): def _global_on_model(ctx):
(opt, mdl) = _on_models[ctx] (fn, mdl) = _on_models[ctx]
opt.on_model(mdl) fn(mdl)
_on_model_eh = on_model_eh_type(_global_on_model) _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) 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): def set_on_model(self, on_model):
self._on_model = on_model
id = len(_on_models) + 41 id = len(_on_models) + 41
mdl = Model(self.ctx) 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) Z3_optimize_register_model_eh(self.ctx.ref(), self.optimize, mdl.model, ctypes.c_void_p(id), _on_model_eh)