From dc2d2e2edf5e31ef83c338896cb3f702093eaec5 Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Thu, 8 Jan 2026 15:16:55 -0800 Subject: [PATCH] Add missing C++ API methods for congruence closure and model sort universe (#8124) * Initial plan * Add missing C++ API functions for congruence closure and model sort universe Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Add error checking and context validation to new API methods Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Add documentation for get_sort precondition Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Delete examples/c++/test_missing_apis.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 | 42 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 42 insertions(+) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 23d852000..dcc040e56 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -2702,6 +2702,29 @@ namespace z3 { check_error(); } + unsigned num_sorts() const { + unsigned r = Z3_model_get_num_sorts(ctx(), m_model); + check_error(); + return r; + } + + /** + \brief Return the uninterpreted sort at position \c i. + \pre i < num_sorts() + */ + sort get_sort(unsigned i) const { + Z3_sort s = Z3_model_get_sort(ctx(), m_model, i); + check_error(); + return sort(ctx(), s); + } + + expr_vector sort_universe(sort const& s) const { + check_context(*this, s); + Z3_ast_vector r = Z3_model_get_sort_universe(ctx(), m_model, s); + check_error(); + return expr_vector(ctx(), r); + } + friend std::ostream & operator<<(std::ostream & out, model const & m); std::string to_string() const { return m_model ? std::string(Z3_model_to_string(ctx(), m_model)) : "null"; } @@ -2890,6 +2913,25 @@ namespace z3 { check_error(); return result; } + expr congruence_root(expr const& t) const { + check_context(*this, t); + Z3_ast r = Z3_solver_congruence_root(ctx(), m_solver, t); + check_error(); + return expr(ctx(), r); + } + expr congruence_next(expr const& t) const { + check_context(*this, t); + Z3_ast r = Z3_solver_congruence_next(ctx(), m_solver, t); + check_error(); + return expr(ctx(), r); + } + expr congruence_explain(expr const& a, expr const& b) const { + check_context(*this, a); + check_context(*this, b); + Z3_ast r = Z3_solver_congruence_explain(ctx(), m_solver, a, b); + check_error(); + return expr(ctx(), r); + } void set_initial_value(expr const& var, expr const& value) { Z3_solver_set_initial_value(ctx(), m_solver, var, value); check_error();