From 9007728ddbdfc8bb7ce879a980392b7ee87a15fa Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Mon, 2 Feb 2026 09:01:23 -0800 Subject: [PATCH] Add solve_for and import_model_converter to C++ solver API (#8465) * Initial plan * Add solve_for and import_model_converter methods to C++ API (fixes issues 6 and 8) Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Address code review feedback and add comprehensive test Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Remove accidentally committed binary * Delete examples/c++/test_issues_6_7_8.cpp --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> Co-authored-by: Nikolaj Bjorner --- src/api/c++/z3++.h | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index b4c8ddbf8..a55918058 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -2997,6 +2997,26 @@ namespace z3 { set_initial_value(var, ctx().bool_val(b)); } + void solve_for(expr_vector const& vars, expr_vector& terms, expr_vector& guards) { + // Create a copy of vars since the C API modifies the variables vector + expr_vector variables(ctx()); + for (unsigned i = 0; i < vars.size(); ++i) { + check_context(*this, vars[i]); + variables.push_back(vars[i]); + } + // Clear output vectors before calling C API + terms = expr_vector(ctx()); + guards = expr_vector(ctx()); + Z3_solver_solve_for(ctx(), m_solver, variables, terms, guards); + check_error(); + } + + void import_model_converter(solver const& src) { + check_context(*this, src); + Z3_solver_import_model_converter(ctx(), src.m_solver, m_solver); + check_error(); + } + expr proof() const { Z3_ast r = Z3_solver_get_proof(ctx(), m_solver); check_error(); return expr(ctx(), r); } friend std::ostream & operator<<(std::ostream & out, solver const & s);