mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

Merge branch 'master' of https://github.com/z3prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-04-11 17:06:03 +02:00
commit eb2dd92d37
6 changed files with 31 additions and 23 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/api/api_solver.cpp
View file

@ -883,8 +883,8 @@ extern "C" {
Z3_TRY;
RESET_ERROR_CODE();
init_solver(c, s);
user_propagator::push_eh_t _push = push_eh;
user_propagator::pop_eh_t _pop = pop_eh;
user_propagator::push_eh_t _push = (void(*)(void*,user_propagator::callback*)) push_eh;
user_propagator::pop_eh_t _pop = (void(*)(void*,user_propagator::callback*,unsigned)) pop_eh;
user_propagator::fresh_eh_t _fresh = [=](void * user_ctx, ast_manager& m, user_propagator::context_obj*& _ctx) {
ast_context_params params;
params.set_foreign_manager(&m);

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

@ -3964,18 +3964,23 @@ namespace z3 {
}
};
static void push_eh(void* p) {
static void push_eh(void* _p, Z3_solver_callback cb) {
user_propagator_base* p = static_cast<user_propagator_base*>(_p);
scoped_cb _cb(p, cb);
static_cast<user_propagator_base*>(p)->push();
}
static void pop_eh(void* p, unsigned num_scopes) {
static_cast<user_propagator_base*>(p)->pop(num_scopes);
static void pop_eh(void* _p, Z3_solver_callback cb, unsigned num_scopes) {
user_propagator_base* p = static_cast<user_propagator_base*>(_p);
scoped_cb _cb(p, cb);
static_cast<user_propagator_base*>(_p)->pop(num_scopes);
}
static void* fresh_eh(void* p, Z3_context ctx) {
static void* fresh_eh(void* _p, Z3_context ctx) {
user_propagator_base* p = static_cast<user_propagator_base*>(_p);
context* c = new context(ctx);
static_cast<user_propagator_base*>(p)->subcontexts.push_back(c);
return static_cast<user_propagator_base*>(p)->fresh(*c);
p->subcontexts.push_back(c);
return p->fresh(*c);
}
static void fixed_eh(void* _p, Z3_solver_callback cb, Z3_ast _var, Z3_ast _value) {

4
src/api/z3_api.h
View file

@ -1434,8 +1434,8 @@ Z3_DECLARE_CLOSURE(Z3_error_handler, void, (Z3_context c, Z3_error_code e));
/**
\brief callback functions for user propagator.
*/
Z3_DECLARE_CLOSURE(Z3_push_eh, void, (void* ctx));
Z3_DECLARE_CLOSURE(Z3_pop_eh, void, (void* ctx, unsigned num_scopes));
Z3_DECLARE_CLOSURE(Z3_push_eh, void, (void* ctx, Z3_solver_callback cb));
Z3_DECLARE_CLOSURE(Z3_pop_eh, void, (void* ctx, Z3_solver_callback cb, unsigned num_scopes));
Z3_DECLARE_CLOSURE(Z3_fresh_eh, void*, (void* ctx, Z3_context new_context));
Z3_DECLARE_CLOSURE(Z3_fixed_eh, void, (void* ctx, Z3_solver_callback cb, Z3_ast t, Z3_ast value));
Z3_DECLARE_CLOSURE(Z3_eq_eh, void, (void* ctx, Z3_solver_callback cb, Z3_ast s, Z3_ast t));