mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-11 00:23:25 +00:00
Code Activity

fix build

Browse source 
reference types are not part of C
This commit is contained in:
Nikolaj Bjorner 2022-04-16 15:16:53 +02:00
parent 807121aa03
commit f4c500c519
5 changed files with 12 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/api/api_solver.cpp
View file

@ -978,7 +978,7 @@ extern "C" {
void Z3_API Z3_solver_propagate_decide(Z3_context c, Z3_solver s, Z3_decide_eh decide_eh) { void Z3_API Z3_solver_propagate_decide(Z3_context c, Z3_solver s, Z3_decide_eh decide_eh) {
Z3_TRY; Z3_TRY;
RESET_ERROR_CODE(); RESET_ERROR_CODE();
user_propagator::decide_eh_t c = (void(*)(void*, user_propagator::callback*, expr*&, unsigned&, lbool&))decide_eh; user_propagator::decide_eh_t c = (void(*)(void*, user_propagator::callback*, expr**, unsigned*, lbool*))decide_eh;
to_solver_ref(s)->user_propagate_register_decide(c); to_solver_ref(s)->user_propagate_register_decide(c);
Z3_CATCH; Z3_CATCH;
} }

2
src/api/z3_api.h
View file

@ -1444,7 +1444,7 @@ Z3_DECLARE_CLOSURE(Z3_fixed_eh, void, (void* ctx, Z3_solver_callback cb, Z3_as
Z3_DECLARE_CLOSURE(Z3_eq_eh, void, (void* ctx, Z3_solver_callback cb, Z3_ast s, Z3_ast t)); Z3_DECLARE_CLOSURE(Z3_eq_eh, void, (void* ctx, Z3_solver_callback cb, Z3_ast s, Z3_ast t));
Z3_DECLARE_CLOSURE(Z3_final_eh, void, (void* ctx, Z3_solver_callback cb)); Z3_DECLARE_CLOSURE(Z3_final_eh, void, (void* ctx, Z3_solver_callback cb));
Z3_DECLARE_CLOSURE(Z3_created_eh, void, (void* ctx, Z3_solver_callback cb, Z3_ast t)); Z3_DECLARE_CLOSURE(Z3_created_eh, void, (void* ctx, Z3_solver_callback cb, Z3_ast t));
Z3_DECLARE_CLOSURE(Z3_decide_eh, void, (void* ctx, Z3_solver_callback cb, Z3_ast&, unsigned&, Z3_lbool&)); Z3_DECLARE_CLOSURE(Z3_decide_eh, void, (void* ctx, Z3_solver_callback cb, Z3_ast*, unsigned*, Z3_lbool*));
/** /**

11
src/opt/maxres.cpp
View file

@ -700,7 +700,7 @@ public:
} }
} }
#if 0 #if 1
void bin_max_resolve(exprs const& _core, rational const& w) { void bin_max_resolve(exprs const& _core, rational const& w) {
expr_ref_vector core(m, _core.size(), _core.data()); expr_ref_vector core(m, _core.size(), _core.data());
@ -708,8 +708,8 @@ public:
for (unsigned i = 0; i + 1 < core.size(); ++i) { for (unsigned i = 0; i + 1 < core.size(); ++i) {
expr* a = core.get(i); expr* a = core.get(i);
expr* b = core.get(i + 1); expr* b = core.get(i + 1);
expr_ref u = mk_fresh_bool("u"); expr* u = mk_fresh_bool("u");
expr_ref v = mk_fresh_bool("v"); expr* v = mk_fresh_bool("v");
// u = a or b // u = a or b
// v = a and b // v = a and b
cls = m.mk_or(a, b); cls = m.mk_or(a, b);
@ -725,8 +725,13 @@ public:
new_assumption(u, w); new_assumption(u, w);
core.push_back(v); core.push_back(v);
} }
s().assert_expr(m.mk_not(core.back()));
} }
#endif
#if 0
struct unfold_record { struct unfold_record {
ptr_vector<expr> ws; ptr_vector<expr> ws;
rational weight; rational weight;

2
src/smt/theory_user_propagator.cpp
View file

@ -190,7 +190,7 @@ void theory_user_propagator::decide(bool_var& var, bool& is_pos) {
lbool phase = is_pos ? l_true : l_false; lbool phase = is_pos ? l_true : l_false;
expr* e = var2expr(original_enode->get_th_var(get_family_id())); expr* e = var2expr(original_enode->get_th_var(get_family_id()));
m_decide_eh(m_user_context, this, e, new_bit, phase); m_decide_eh(m_user_context, this, &e, &new_bit, &phase);
enode* new_enode = ctx.get_enode(e); enode* new_enode = ctx.get_enode(e);
// check if the callback changed something // check if the callback changed something

2
src/tactic/user_propagator_base.h
View file

@ -25,7 +25,7 @@ namespace user_propagator {
typedef std::function<void(void*, callback*)> push_eh_t; typedef std::function<void(void*, callback*)> push_eh_t;
typedef std::function<void(void*, callback*, unsigned)> pop_eh_t; typedef std::function<void(void*, callback*, unsigned)> pop_eh_t;
typedef std::function<void(void*, callback*, expr*)> created_eh_t; typedef std::function<void(void*, callback*, expr*)> created_eh_t;
typedef std::function<void(void*, callback*, expr*&, unsigned&, lbool&)> decide_eh_t; typedef std::function<void(void*, callback*, expr**, unsigned*, lbool*)> decide_eh_t;
class plugin : public decl_plugin { class plugin : public decl_plugin {
public: public: