mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-27 06:13:35 +00:00
Code Activity

Add missing C++ API methods for congruence closure and model sort universe (#8124)

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

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

@ -2702,6 +2702,29 @@ namespace z3 {
check_error(); 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); 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"; } 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(); check_error();
return result; 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) { void set_initial_value(expr const& var, expr const& value) {
Z3_solver_set_initial_value(ctx(), m_solver, var, value); Z3_solver_set_initial_value(ctx(), m_solver, var, value);
check_error(); check_error();