diff --git a/scripts/update_api.py b/scripts/update_api.py index 8a808a5a5..c973ff200 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -357,6 +357,9 @@ def Z3_solver_propagate_diseq(ctx, s, diseq_eh, _elems = Elementaries(_lib.Z3_so _elems.f(ctx, s, diseq_eh) _elems.Check(ctx) +def Z3_optimize_register_model_eh(ctx, o, m, user_ctx, on_model_eh, _elems = Elementaries(_lib.Z3_optimize_register_model_eh)): + _elems.f(ctx, o, m, user_ctx, on_model_eh) + _elems.Check(ctx) """) @@ -1868,6 +1871,9 @@ _lib.Z3_solver_propagate_eq.argtypes = [ContextObj, SolverObj, eq_eh_type] _lib.Z3_solver_propagate_diseq.restype = None _lib.Z3_solver_propagate_diseq.argtypes = [ContextObj, SolverObj, eq_eh_type] +on_model_eh_type = ctypes.CFUNCTYPE(None, ctypes.c_void_p) +_lib.Z3_optimize_register_model_eh.restype = None +_lib.Z3_optimize_register_model_eh.argtypes = [ContextObj, OptimizeObj, ModelObj, ctypes.c_void_p, on_model_eh_type] """ ) diff --git a/src/api/api_opt.cpp b/src/api/api_opt.cpp index 697dd6e2f..b12cbe209 100644 --- a/src/api/api_opt.cpp +++ b/src/api/api_opt.cpp @@ -435,6 +435,32 @@ extern "C" { Z3_CATCH_RETURN(nullptr); } + static void optimize_on_model(opt::on_model_t& o, model_ref& m) { + Z3_context c = (Z3_context) o.c; + auto model_eh = (void(*)(void*)) o.on_model; + Z3_model_ref * m_ref = (Z3_model_ref*) o.m; + m_ref->m_model = m.get(); + model_eh(o.user_context); + } + + void Z3_API Z3_optimize_register_model_eh( + Z3_context c, + Z3_optimize o, + Z3_model m, + void* user_context, + Z3_model_eh model_eh) { + Z3_TRY; + + std::function _model_eh = optimize_on_model; + opt::on_model_t ctx; + ctx.c = c; + ctx.m = m; + ctx.user_context = user_context; + ctx.on_model = 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 8c91c5cdc..6f2dde684 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -6281,6 +6281,7 @@ class ModelRef(Z3PPObject): def __deepcopy__(self, memo={}): return self.translate(self.ctx) + def Model(ctx = None): ctx = _get_ctx(ctx) return ModelRef(Z3_mk_model(ctx.ref()), ctx) @@ -7403,12 +7404,22 @@ class OptimizeObjective: return "%s:%s" % (self._value, self._is_max) + +_on_models = {} + +def _global_on_model(ctx): + (opt, mdl) = _on_models[ctx] + opt.on_model(mdl) + +_on_model_eh = on_model_eh_type(_global_on_model) + class Optimize(Z3PPObject): """Optimize API provides methods for solving using objective functions and weighted soft constraints""" def __init__(self, ctx=None): self.ctx = _get_ctx(ctx) self.optimize = Z3_mk_optimize(self.ctx.ref()) + self._on_models_id = None Z3_optimize_inc_ref(self.ctx.ref(), self.optimize) def __deepcopy__(self, memo={}): @@ -7417,6 +7428,8 @@ class Optimize(Z3PPObject): def __del__(self): if self.optimize is not None and self.ctx.ref() is not None: Z3_optimize_dec_ref(self.ctx.ref(), self.optimize) + if self._on_models_id is not None: + del _on_models[self._on_models_id] def set(self, *args, **keys): """Set a configuration option. The method `help()` return a string containing all available options. @@ -7593,7 +7606,15 @@ 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) + Z3_optimize_register_model_eh(self.ctx.ref(), self.optimize, mdl.model, ctypes.c_void_p(id), _on_model_eh) ######################################### diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 5f8f02a9a..d16295418 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -1382,7 +1382,7 @@ typedef enum def_Type('SORT', 'Z3_sort', 'Sort') def_Type('FUNC_DECL', 'Z3_func_decl', 'FuncDecl') def_Type('PATTERN', 'Z3_pattern', 'Pattern') - def_Type('MODEL', 'Z3_model', 'Model') + def_Type('MODEL', 'Z3_model', 'ModelObj') def_Type('LITERALS', 'Z3_literals', 'Literals') def_Type('CONSTRUCTOR', 'Z3_constructor', 'Constructor') def_Type('CONSTRUCTOR_LIST', 'Z3_constructor_list', 'ConstructorList') @@ -1420,6 +1420,7 @@ typedef void Z3_fixed_eh(void* ctx, Z3_solver_callback cb, unsigned id, Z3_ast v typedef void Z3_eq_eh(void* ctx, Z3_solver_callback cb, unsigned x, unsigned y); typedef void Z3_final_eh(void* ctx, Z3_solver_callback cb); + /** \brief A Goal is essentially a set of formulas. Z3 provide APIs for building strategies/tactics for solving and transforming Goals. diff --git a/src/api/z3_optimization.h b/src/api/z3_optimization.h index 140d31846..51d8853e0 100644 --- a/src/api/z3_optimization.h +++ b/src/api/z3_optimization.h @@ -18,6 +18,11 @@ Notes: --*/ #pragma once +/** + \brief callback functions for models. + */ +typedef void Z3_model_eh(void* ctx); + #ifdef __cplusplus extern "C" { #endif // __cplusplus @@ -351,6 +356,18 @@ extern "C" { */ Z3_ast_vector Z3_API Z3_optimize_get_objectives(Z3_context c, Z3_optimize o); + + /** + \brief register a model event handler for new models. + */ + void Z3_API Z3_optimize_register_model_eh( + Z3_context c, + Z3_optimize o, + Z3_model m, + void* ctx, + Z3_model_eh model_eh); + + /*@}*/ /*@}*/ diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index fa38ee2a9..0789cb2a4 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -382,6 +382,13 @@ namespace opt { model_ref md = m->copy(); fix_model(md); } + if (m_on_model_eh && m) { + model_ref md = m->copy(); + if (!m_model_fixed.contains(md.get())) + fix_model(md); + m_on_model_eh(m_on_model_ctx, md); + m_model_fixed.pop_back(); + } } diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index c8e0ce92a..7bf7ce7e2 100644 --- a/src/opt/opt_context.h +++ b/src/opt/opt_context.h @@ -66,6 +66,14 @@ namespace opt { It handles combinations of objectives. */ + struct on_model_t { + void* c; + void* m; + void* user_context; + void* on_model; + }; + + class context : public opt_wrapper, public pareto_callback, @@ -143,6 +151,8 @@ namespace opt { }; ast_manager& m; + on_model_t m_on_model_ctx; + std::function m_on_model_eh; arith_util m_arith; bv_util m_bv; expr_ref_vector m_hard_constraints; @@ -245,6 +255,11 @@ namespace opt { void model_updated(model* mdl) override; + void register_on_model(on_model_t& ctx, std::function& on_model) { + m_on_model_ctx = ctx; + m_on_model_eh = on_model; + } + private: lbool execute(objective const& obj, bool committed, bool scoped); lbool execute_min_max(unsigned index, bool committed, bool scoped, bool is_max);