Implement Z3_optimize_translate for context translation (#8072)

* Initial plan

* Implement Z3_optimize_translate functionality

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Fix compilation errors and add tests for optimize translate

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Revert changes to opt_solver.cpp as requested

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

src/api/api_opt.cpp

@@ -481,4 +481,22 @@ extern "C" {
         Z3_CATCH;        
     }
 
+    Z3_optimize Z3_API Z3_optimize_translate(Z3_context c, Z3_optimize o, Z3_context target) {
+        Z3_TRY;
+        LOG_Z3_optimize_translate(c, o, target);
+        RESET_ERROR_CODE();
+        
+        // Translate the opt::context to the target manager
+        opt::context* translated_ctx = to_optimize_ptr(o)->translate(mk_c(target)->m());
+        
+        // Create a new Z3_optimize_ref in the target context
+        Z3_optimize_ref* result_ref = alloc(Z3_optimize_ref, *mk_c(target));
+        result_ref->m_opt = translated_ctx;
+        mk_c(target)->save_object(result_ref);
+        
+        Z3_optimize result = of_optimize(result_ref);
+        RETURN_Z3(result);
+        Z3_CATCH_RETURN(nullptr);
+    }
+
 };

src/api/c++/z3++.h

@@ -3313,6 +3313,7 @@ namespace z3 {
         Z3_optimize m_opt;
 
     public:
+        struct translate {};
         class handle final {
             unsigned m_h;
         public:
@@ -3320,6 +3321,12 @@ namespace z3 {
             unsigned h() const { return m_h; }
         };
         optimize(context& c):object(c) { m_opt = Z3_mk_optimize(c); Z3_optimize_inc_ref(c, m_opt); }
+        optimize(context & c, optimize const& src, translate): object(c) { 
+            Z3_optimize o = Z3_optimize_translate(src.ctx(), src, c); 
+            check_error(); 
+            m_opt = o; 
+            Z3_optimize_inc_ref(c, m_opt); 
+        }
         optimize(optimize const & o):object(o), m_opt(o.m_opt) {
             Z3_optimize_inc_ref(o.ctx(), o.m_opt);
         }

src/api/z3_optimization.h

@@ -379,6 +379,23 @@ extern "C" {
         void*        ctx,
         Z3_model_eh  model_eh);
 
+    /**
+       \brief Copy an optimization context from a source to a target context.
+       
+       This function allows translating an optimization context from one Z3_context
+       to another. This is useful when working with multiple contexts and needing to
+       transfer optimization problems between them.
+       
+       \param c Source context containing the optimization context to translate
+       \param o The optimization context to translate from the source context
+       \param target Target context where the optimization context will be created
+       
+       \return A new optimization context in the target context with the same state
+       
+       def_API('Z3_optimize_translate', OPTIMIZE, (_in(CONTEXT), _in(OPTIMIZE), _in(CONTEXT)))
+     */
+    Z3_optimize Z3_API Z3_optimize_translate(Z3_context c, Z3_optimize o, Z3_context target);
+
 
     /**@}*/
     /**@}*/

src/opt/opt_context.cpp

@@ -20,6 +20,7 @@ Notes:
 #include "util/gparams.h"
 #include "ast/for_each_expr.h"
 #include "ast/ast_pp.h"
+#include "ast/ast_translation.h"
 #include "ast/bv_decl_plugin.h"
 #include "ast/pb_decl_plugin.h"
 #include "ast/ast_smt_pp.h"
@@ -155,6 +156,57 @@ namespace opt {
         reset_maxsmts();
     }
 
+    context* context::translate(ast_manager& target_m) {
+        // Create AST translator
+        ast_translation translator(m, target_m);
+        
+        // Create new context in target manager
+        context* result = alloc(context, target_m);
+        
+        // Copy parameters
+        result->updt_params(m_params);
+        
+        // Set logic
+        if (m_logic != symbol::null) {
+            result->set_logic(m_logic);
+        }
+        
+        // Translate hard constraints from scoped state
+        for (expr* e : m_scoped_state.m_hard) {
+            result->add_hard_constraint(translator(e));
+        }
+        
+        // Translate objectives
+        for (auto const& obj : m_scoped_state.m_objectives) {
+            if (obj.m_type == O_MAXIMIZE || obj.m_type == O_MINIMIZE) {
+                // Translate maximize/minimize objectives
+                app_ref translated_term(to_app(translator(obj.m_term.get())), target_m);
+                result->add_objective(translated_term, obj.m_type == O_MAXIMIZE);
+            }
+            else if (obj.m_type == O_MAXSMT) {
+                // Translate soft constraints for MaxSMT objectives
+                for (unsigned i = 0; i < obj.m_terms.size(); ++i) {
+                    result->add_soft_constraint(
+                        translator(obj.m_terms.get(i)),
+                        obj.m_weights[i],
+                        obj.m_id
+                    );
+                }
+            }
+        }
+        
+        // Copy configuration flags
+        result->m_enable_sat = m_enable_sat;
+        result->m_enable_sls = m_enable_sls;
+        result->m_is_clausal = m_is_clausal;
+        result->m_pp_neat = m_pp_neat;
+        result->m_pp_wcnf = m_pp_wcnf;
+        result->m_incremental = m_incremental;
+        result->m_maxsat_engine = m_maxsat_engine;
+        
+        return result;
+    }
+
     void context::reset_maxsmts() {
         for (auto& kv : m_maxsmts) {
             dealloc(kv.m_value);

src/opt/opt_context.h

@@ -209,6 +209,13 @@ namespace opt {
     public:
         context(ast_manager& m);
         ~context() override;
+        
+        /**
+         * \brief Create a clone of the optimization context in a different ast_manager.
+         * Translates all assertions, objectives, and solver state.
+         */
+        context* translate(ast_manager& target_m);
+        
         unsigned add_soft_constraint(expr* f, rational const& w, symbol const& id);
         unsigned add_objective(app* t, bool is_max);
         void add_hard_constraint(expr* f);

src/test/api.cpp

@@ -107,8 +107,62 @@ static void test_mk_distinct() {
     
 }
 
+void test_optimize_translate() {
+    Z3_config cfg1 = Z3_mk_config();
+    Z3_context ctx1 = Z3_mk_context(cfg1);
+    Z3_del_config(cfg1);
+    
+    // Create optimization context in first context
+    Z3_optimize opt1 = Z3_mk_optimize(ctx1);
+    Z3_optimize_inc_ref(ctx1, opt1);
+    
+    // Add some constraints
+    Z3_sort int_sort = Z3_mk_int_sort(ctx1);
+    Z3_symbol x_sym = Z3_mk_string_symbol(ctx1, "x");
+    Z3_ast x = Z3_mk_const(ctx1, x_sym, int_sort);
+    
+    Z3_ast zero = Z3_mk_int(ctx1, 0, int_sort);
+    Z3_ast constraint = Z3_mk_gt(ctx1, x, zero);  // x > 0
+    
+    Z3_optimize_assert(ctx1, opt1, constraint);
+    
+    // Add an objective to maximize x
+    Z3_optimize_maximize(ctx1, opt1, x);
+    
+    // Create second context
+    Z3_config cfg2 = Z3_mk_config();
+    Z3_context ctx2 = Z3_mk_context(cfg2);
+    Z3_del_config(cfg2);
+    
+    // Translate optimize context to second context
+    Z3_optimize opt2 = Z3_optimize_translate(ctx1, opt1, ctx2);
+    Z3_optimize_inc_ref(ctx2, opt2);
+    
+    // Check sat in the translated context
+    Z3_lbool result = Z3_optimize_check(ctx2, opt2, 0, nullptr);
+    
+    ENSURE(result == Z3_L_TRUE);
+    
+    // Verify we can get assertions from translated context
+    Z3_ast_vector assertions = Z3_optimize_get_assertions(ctx2, opt2);
+    unsigned num_assertions = Z3_ast_vector_size(ctx2, assertions);
+    ENSURE(num_assertions == 1);
+    
+    // Verify we can get objectives from translated context
+    Z3_ast_vector objectives = Z3_optimize_get_objectives(ctx2, opt2);
+    unsigned num_objectives = Z3_ast_vector_size(ctx2, objectives);
+    ENSURE(num_objectives == 1);
+    
+    // Clean up
+    Z3_optimize_dec_ref(ctx2, opt2);
+    Z3_optimize_dec_ref(ctx1, opt1);
+    Z3_del_context(ctx2);
+    Z3_del_context(ctx1);
+}
+
 void tst_api() {
     test_apps();
     test_bvneg();
     test_mk_distinct();
+    test_optimize_translate();
 }