mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

Added overloaded versions of context::recfun in the c++ api that allow for the declaration of recursive functions where the domain is given by a z3::sort_vector instead of an arity and sort* (#6576)

Browse source 
Co-authored-by: Julian Parsert <julian.parsert@uibk.ac.at>
This commit is contained in:
Julian Parsert 2023-02-10 18:00:26 +00:00 • committed by GitHub
parent 02d48adae5
commit d52e893528
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 25 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -360,6 +360,8 @@ namespace z3 {
func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & d4, sort const & d5, sort const & range); func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & d4, sort const & d5, sort const & range);
func_decl recfun(symbol const & name, unsigned arity, sort const * domain, sort const & range); func_decl recfun(symbol const & name, unsigned arity, sort const * domain, sort const & range);
func_decl recfun(symbol const & name, const sort_vector& domain, sort const & range);
func_decl recfun(char const * name, sort_vector const& domain, sort const & range);
func_decl recfun(char const * name, unsigned arity, sort const * domain, sort const & range); func_decl recfun(char const * name, unsigned arity, sort const * domain, sort const & range);
func_decl recfun(char const * name, sort const & domain, sort const & range); func_decl recfun(char const * name, sort const & domain, sort const & range);
func_decl recfun(char const * name, sort const & d1, sort const & d2, sort const & range); func_decl recfun(char const * name, sort const & d1, sort const & d2, sort const & range);
@ -2712,6 +2714,16 @@ namespace z3 {
void set(char const * k, double v) { params p(ctx()); p.set(k, v); set(p); } void set(char const * k, double v) { params p(ctx()); p.set(k, v); set(p); }
void set(char const * k, symbol const & v) { params p(ctx()); p.set(k, v); set(p); } void set(char const * k, symbol const & v) { params p(ctx()); p.set(k, v); set(p); }
void set(char const * k, char const* v) { params p(ctx()); p.set(k, v); set(p); } void set(char const * k, char const* v) { params p(ctx()); p.set(k, v); set(p); }
/**
\brief Create a backtracking point.
The solver contains a stack of assertions.
\sa Z3_solver_get_num_scopes
\sa Z3_solver_pop
def_API('Z3_solver_push', VOID, (_in(CONTEXT), _in(SOLVER)))
*/
void push() { Z3_solver_push(ctx(), m_solver); check_error(); } void push() { Z3_solver_push(ctx(), m_solver); check_error(); }
void pop(unsigned n = 1) { Z3_solver_pop(ctx(), m_solver, n); check_error(); } void pop(unsigned n = 1) { Z3_solver_pop(ctx(), m_solver, n); check_error(); }
void reset() { Z3_solver_reset(ctx(), m_solver); check_error(); } void reset() { Z3_solver_reset(ctx(), m_solver); check_error(); }
@ -3604,6 +3616,19 @@ namespace z3 {
} }
inline func_decl context::recfun(symbol const & name, sort_vector const& domain, sort const & range) {
check_context(domain, range);
array<Z3_sort> domain1(domain);
Z3_func_decl f = Z3_mk_rec_func_decl(m_ctx, name, domain1.size(), domain1.ptr(), range);
check_error();
return func_decl(*this, f);
}
inline func_decl context::recfun(char const * name, sort_vector const& domain, sort const & range) {
return recfun(str_symbol(name), domain, range);
}
inline func_decl context::recfun(char const * name, unsigned arity, sort const * domain, sort const & range) { inline func_decl context::recfun(char const * name, unsigned arity, sort const * domain, sort const & range) {
return recfun(str_symbol(name), arity, domain, range); return recfun(str_symbol(name), arity, domain, range);
} }