mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 04:03:39 +00:00
Code Activity

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

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-10-19 12:24:41 -04:00
parent 86147d01ea 3557e0b0c5
commit 839a0852fe
1 changed files with 36 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1516,7 +1516,7 @@ namespace z3 {
expr substitute(expr_vector const& dst); expr substitute(expr_vector const& dst);
class iterator { class iterator {
expr& e; expr& e;
unsigned i; unsigned i;
public: public:
@ -1912,14 +1912,14 @@ namespace z3 {
Z3_ast r; Z3_ast r;
if (a.is_int()) { if (a.is_int()) {
expr zero = a.ctx().int_val(0); expr zero = a.ctx().int_val(0);
expr ge = a >= zero; expr ge = a >= zero;
expr na = -a; expr na = -a;
r = Z3_mk_ite(a.ctx(), ge, a, na); r = Z3_mk_ite(a.ctx(), ge, a, na);
} }
else if (a.is_real()) { else if (a.is_real()) {
expr zero = a.ctx().real_val(0); expr zero = a.ctx().real_val(0);
expr ge = a >= zero; expr ge = a >= zero;
expr na = -a; expr na = -a;
r = Z3_mk_ite(a.ctx(), ge, a, na); r = Z3_mk_ite(a.ctx(), ge, a, na);
} }
else { else {
@ -3954,12 +3954,28 @@ namespace z3 {
Z3_solver_propagate_fixed(ctx(), *s, fixed_eh); Z3_solver_propagate_fixed(ctx(), *s, fixed_eh);
} }
void register_fixed() {
assert(s);
m_fixed_eh = [this](unsigned id, expr const& e) {
fixed(id, e);
};
Z3_solver_propagate_fixed(ctx(), *s, fixed_eh);
}
void register_eq(eq_eh_t& f) { void register_eq(eq_eh_t& f) {
assert(s); assert(s);
m_eq_eh = f; m_eq_eh = f;
Z3_solver_propagate_eq(ctx(), *s, eq_eh); Z3_solver_propagate_eq(ctx(), *s, eq_eh);
} }
void register_eq() {
assert(s);
m_eq_eh = [this](unsigned x, unsigned y) {
eq(x, y);
};
Z3_solver_propagate_eq(ctx(), *s, eq_eh);
}
/** /**
\brief register a callback on final-check. \brief register a callback on final-check.
During the final check stage, all propagations have been processed. During the final check stage, all propagations have been processed.
@ -3973,6 +3989,21 @@ namespace z3 {
m_final_eh = f; m_final_eh = f;
Z3_solver_propagate_final(ctx(), *s, final_eh); Z3_solver_propagate_final(ctx(), *s, final_eh);
} }
void register_final() {
assert(s);
m_final_eh = [this]() {
final();
};
Z3_solver_propagate_final(ctx(), *s, final_eh);
}
virtual void fixed(unsigned id, expr const& e) { }
virtual void eq(unsigned x, unsigned y) { }
virtual void final() { }
/** /**
\brief tracks \c e by a unique identifier that is returned by the call. \brief tracks \c e by a unique identifier that is returned by the call.