From 313be1ca1b40af566f9b02c802385e3a068d1af7 Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Sat, 13 Dec 2025 05:12:08 +0000 Subject: [PATCH] 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 | 18 +++++++++++++ src/api/c++/z3++.h | 7 +++++ src/api/z3_optimization.h | 17 ++++++++++++ src/opt/opt_context.cpp | 52 +++++++++++++++++++++++++++++++++++++ src/opt/opt_context.h | 7 +++++ src/test/api.cpp | 54 +++++++++++++++++++++++++++++++++++++++ 6 files changed, 155 insertions(+) diff --git a/src/api/api_opt.cpp b/src/api/api_opt.cpp index c3774dd85..7da23cd6e 100644 --- a/src/api/api_opt.cpp +++ b/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); + } + }; diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 2acb010cb..23d852000 100644 --- a/src/api/c++/z3++.h +++ b/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); } diff --git a/src/api/z3_optimization.h b/src/api/z3_optimization.h index 4e585efb2..739dc2307 100644 --- a/src/api/z3_optimization.h +++ b/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); + /**@}*/ /**@}*/ diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 388befe93..2892376be 100644 --- a/src/opt/opt_context.cpp +++ b/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); diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index ed2377bab..4b18dde51 100644 --- a/src/opt/opt_context.h +++ b/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); diff --git a/src/test/api.cpp b/src/test/api.cpp index 560dd1121..d047d2881 100644 --- a/src/test/api.cpp +++ b/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(); }