add new model event handler for incremental optimization

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]
 
 """
   )

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<void(opt::on_model_t&, model_ref&)> _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;
+    }
+
 
 
 };

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)
 
 
 #########################################

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.

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);
+
+
     /*@}*/
     /*@}*/
 

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();
+        }
     }
 
 

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<void(on_model_t&, model_ref&)> 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<void(on_model_t&, model_ref&)>& 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);