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

Update z3++.h

Browse source 
with bindings for user propagate functions
This commit is contained in:
Nikolaj Bjorner 2021-12-18 11:56:05 -08:00
parent f0740bdf60
commit 85e362277c
1 changed files with 36 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -334,6 +334,7 @@ namespace z3 {
func_decl recfun(char const * name, sort const & d1, sort const & d2, sort const & range);
void recdef(func_decl, expr_vector const& args, expr const& body);
func_decl user_propagate_function(symbol const& name, unsigned arity, sort const* domain, sort const& range);
expr constant(symbol const & name, sort const & s);
expr constant(char const * name, sort const & s);
@ -3424,6 +3425,17 @@ namespace z3 {
Z3_add_rec_def(f.ctx(), f, vars.size(), vars.ptr(), body);
}
inline func_decl context::user_propagate_function(symbol const& name, unsigned arity, sort const* domain, sort const& range) {
array<Z3_sort> args(arity);
for (unsigned i = 0; i < arity; i++) {
check_context(domain[i], range);
args[i] = domain[i];
}
Z3_func_decl f = Z3_user_propagate_declare(m_ctx, name, arity, args.ptr(), range);
check_error();
return func_decl(*this, f);
}
inline expr context::constant(symbol const & name, sort const & s) {
Z3_ast r = Z3_mk_const(m_ctx, name, s);
check_error();
@ -3877,10 +3889,12 @@ namespace z3 {
typedef std::function<void(unsigned, expr const&)> fixed_eh_t;
typedef std::function<void(void)> final_eh_t;
typedef std::function<void(unsigned, unsigned)> eq_eh_t;
typedef std::function<void(unsigned, expr const&)> created_eh_t;
final_eh_t m_final_eh;
eq_eh_t m_eq_eh;
fixed_eh_t m_fixed_eh;
created_eh_t m_created_eh;
solver* s;
Z3_context c;
Z3_solver_callback cb { nullptr };
@ -3929,6 +3943,14 @@ namespace z3 {
static_cast<user_propagator_base*>(p)->m_final_eh();
}
static void created_eh(void* p, Z3_solver_callback cb, unsigned id, Z3_ast _e) {
user_propagator_base* p = static_cast<user_propagator_base*>(_p);
scoped_cb _cb(p, cb);
scoped_context ctx(p->ctx());
expr e(ctx(), _e);
static_cast<user_propagator_base*>(p)->m_created_eh(id, e);
}
public:
user_propagator_base(Z3_context c) : s(nullptr), c(c) {}
@ -4008,6 +4030,18 @@ namespace z3 {
Z3_solver_propagate_final(ctx(), *s, final_eh);
}
void register_created(created_eh_t& c) {
assert(s);
m_created_eh = c;
Z3_solver_propagate_created(c, *s, created_eh);
}
void register_created() {
m_created_eh = [this](unsigned id, expr const& e) {
created(id, e);
};
Z3_solver_propagate_created(c, *s, created_eh);
}
virtual void fixed(unsigned /*id*/, expr const& /*e*/) { }
@ -4015,6 +4049,8 @@ namespace z3 {
virtual void final() { }
virtual void created(unsigned /*id*/, expr const& /*e*/) {}
/**
\brief tracks \c e by a unique identifier that is returned by the call.