mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-02 13:26:10 +00:00
Code Activity

Add solve_for and import_model_converter to C++ solver API (#8465)

Browse source 
* 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 <nbjorner@microsoft.com>
This commit is contained in:
Copilot 2026-02-02 09:01:23 -08:00 • committed by GitHub
parent f5a44cf0b9
commit 9007728ddb
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 20 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

20
src/api/c++/z3++.h
View file

@ -2997,6 +2997,26 @@ namespace z3 {
set_initial_value(var, ctx().bool_val(b)); 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); } 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); friend std::ostream & operator<<(std::ostream & out, solver const & s);