#include <z3++.h>
|
| user_propagator_base (context &c) |
|
| user_propagator_base (solver *s) |
|
virtual void | push ()=0 |
|
virtual void | pop (unsigned num_scopes)=0 |
|
virtual | ~user_propagator_base () |
|
context & | ctx () |
|
virtual user_propagator_base * | fresh (context &ctx)=0 |
| user_propagators created using fresh() are created during search and their lifetimes are restricted to search time. They should be garbage collected by the propagator used to invoke fresh() . The life-time of the Z3_context object can only be assumed valid during callbacks, such as fixed() , which contains expressions based on the context.
|
|
void | register_fixed (fixed_eh_t &f) |
| register callbacks. Callbacks can only be registered with user_propagators that were created using a solver.
|
|
void | register_fixed () |
|
void | register_eq (eq_eh_t &f) |
|
void | register_eq () |
|
void | register_final (final_eh_t &f) |
| register a callback on final-check. During the final check stage, all propagations have been processed. This is an opportunity for the user-propagator to delay some analysis that could be expensive to perform incrementally. It is also an opportunity for the propagator to implement branch and bound optimization.
|
|
void | register_final () |
|
void | register_created (created_eh_t &c) |
|
void | register_created () |
|
void | register_decide (decide_eh_t &c) |
|
void | register_decide () |
|
virtual void | fixed (expr const &, expr const &) |
|
virtual void | eq (expr const &, expr const &) |
|
virtual void | final () |
|
virtual void | created (expr const &) |
|
virtual void | decide (expr const &, unsigned, bool) |
|
bool | next_split (expr const &e, unsigned idx, Z3_lbool phase) |
|
void | add (expr const &e) |
| tracks e by a unique identifier that is returned by the call.
|
|
void | conflict (expr_vector const &fixed) |
|
void | conflict (expr_vector const &fixed, expr_vector const &lhs, expr_vector const &rhs) |
|
bool | propagate (expr_vector const &fixed, expr const &conseq) |
|
bool | propagate (expr_vector const &fixed, expr_vector const &lhs, expr_vector const &rhs, expr const &conseq) |
|
Definition at line 4291 of file z3++.h.
◆ user_propagator_base() [1/2]
Definition at line 4374 of file z3++.h.
4374: s(nullptr), c(&c) {}
Referenced by fresh().
◆ user_propagator_base() [2/2]
Definition at line 4376 of file z3++.h.
4376 : s(s), c(nullptr) {
4378 }
void Z3_API Z3_solver_propagate_init(Z3_context c, Z3_solver s, void *user_context, Z3_push_eh push_eh, Z3_pop_eh pop_eh, Z3_fresh_eh fresh_eh)
register a user-propagator with the solver.
◆ ~user_propagator_base()
Definition at line 4383 of file z3++.h.
4383 {
4384 for (auto& subcontext : subcontexts) {
4385 subcontext->detach();
4386 delete subcontext;
4387 }
4388 }
◆ add()
void add |
( |
expr const & | e | ) |
|
|
inline |
tracks e
by a unique identifier that is returned by the call.
If the fixed()
callback is registered and if e
is a Boolean or Bit-vector, the fixed()
callback gets invoked when e
is bound to a value. If the eq()
callback is registered, then equalities between registered expressions are reported. A consumer can use the propagate
or conflict
functions to invoke propagations or conflicts as a consequence of these callbacks. These functions take a list of identifiers for registered expressions that have been fixed. The list of identifiers must correspond to already fixed values. Similarly, a list of propagated equalities can be supplied. These must correspond to equalities that have been registered during a callback.
Definition at line 4527 of file z3++.h.
4527 {
4528 if (cb)
4530 else if (s)
4532 else
4533 assert(false);
4534 }
void Z3_API Z3_solver_propagate_register_cb(Z3_context c, Z3_solver_callback cb, Z3_ast e)
register an expression to propagate on with the solver. Only expressions of type Bool and type Bit-Ve...
void Z3_API Z3_solver_propagate_register(Z3_context c, Z3_solver s, Z3_ast e)
register an expression to propagate on with the solver. Only expressions of type Bool and type Bit-Ve...
◆ conflict() [1/2]
Definition at line 4536 of file z3++.h.
4536 {
4537 assert(cb);
4538 expr conseq = ctx().bool_val(false);
4539 array<Z3_ast> _fixed(fixed);
4541 }
bool Z3_API Z3_solver_propagate_consequence(Z3_context c, Z3_solver_callback cb, unsigned num_fixed, Z3_ast const *fixed, unsigned num_eqs, Z3_ast const *eq_lhs, Z3_ast const *eq_rhs, Z3_ast conseq)
propagate a consequence based on fixed values and equalities. A client may invoke it during the pro...
◆ conflict() [2/2]
Definition at line 4543 of file z3++.h.
4543 {
4544 assert(cb);
4545 assert(lhs.size() == rhs.size());
4546 expr conseq = ctx().bool_val(false);
4547 array<Z3_ast> _fixed(fixed);
4548 array<Z3_ast> _lhs(lhs);
4549 array<Z3_ast> _rhs(rhs);
4551 }
◆ created()
virtual void created |
( |
expr const & | | ) |
|
|
inlinevirtual |
◆ ctx()
Definition at line 4390 of file z3++.h.
4390 {
4391 return c ? *c : s->ctx();
4392 }
Referenced by add(), conflict(), conflict(), fresh(), next_split(), propagate(), propagate(), register_created(), register_created(), register_decide(), register_decide(), register_eq(), register_eq(), register_final(), register_final(), register_fixed(), register_fixed(), and user_propagator_base().
◆ decide()
virtual void decide |
( |
expr const & | , |
|
|
unsigned | , |
|
|
bool | ) |
|
inlinevirtual |
◆ eq()
virtual void eq |
( |
expr const & | , |
|
|
expr const & | ) |
|
inlinevirtual |
◆ final()
◆ fixed()
virtual void fixed |
( |
expr const & | , |
|
|
expr const & | ) |
|
inlinevirtual |
◆ fresh()
user_propagators created using fresh()
are created during search and their lifetimes are restricted to search time. They should be garbage collected by the propagator used to invoke fresh()
. The life-time of the Z3_context object can only be assumed valid during callbacks, such as fixed()
, which contains expressions based on the context.
◆ next_split()
bool next_split |
( |
expr const & | e, |
|
|
unsigned | idx, |
|
|
Z3_lbool | phase ) |
|
inline |
Definition at line 4508 of file z3++.h.
4508 {
4509 assert(cb);
4511 }
bool Z3_API Z3_solver_next_split(Z3_context c, Z3_solver_callback cb, Z3_ast t, unsigned idx, Z3_lbool phase)
◆ pop()
virtual void pop |
( |
unsigned | num_scopes | ) |
|
|
pure virtual |
◆ propagate() [1/2]
Definition at line 4553 of file z3++.h.
4553 {
4554 assert(cb);
4555 assert((Z3_context)conseq.ctx() == (Z3_context)ctx());
4556 array<Z3_ast> _fixed(fixed);
4558 }
◆ propagate() [2/2]
Definition at line 4560 of file z3++.h.
4562 {
4563 assert(cb);
4564 assert((Z3_context)conseq.ctx() == (Z3_context)ctx());
4565 assert(lhs.size() == rhs.size());
4566 array<Z3_ast> _fixed(fixed);
4567 array<Z3_ast> _lhs(lhs);
4568 array<Z3_ast> _rhs(rhs);
4569
4571 }
◆ push()
◆ register_created() [1/2]
void register_created |
( |
| ) |
|
|
inline |
Definition at line 4473 of file z3++.h.
4473 {
4474 m_created_eh = [this](expr const& e) {
4475 created(e);
4476 };
4477 if (s) {
4479 }
4480 }
void Z3_API Z3_solver_propagate_created(Z3_context c, Z3_solver s, Z3_created_eh created_eh)
register a callback when a new expression with a registered function is used by the solver The regist...
◆ register_created() [2/2]
void register_created |
( |
created_eh_t & | c | ) |
|
|
inline |
Definition at line 4466 of file z3++.h.
4466 {
4467 m_created_eh = c;
4468 if (s) {
4470 }
4471 }
◆ register_decide() [1/2]
Definition at line 4489 of file z3++.h.
4489 {
4490 m_decide_eh = [this](expr val, unsigned bit, bool is_pos) {
4491 decide(val, bit, is_pos);
4492 };
4493 if (s) {
4495 }
4496 }
void Z3_API Z3_solver_propagate_decide(Z3_context c, Z3_solver s, Z3_decide_eh decide_eh)
register a callback when the solver decides to split on a registered expression. The callback may cha...
◆ register_decide() [2/2]
void register_decide |
( |
decide_eh_t & | c | ) |
|
|
inline |
Definition at line 4482 of file z3++.h.
4482 {
4483 m_decide_eh = c;
4484 if (s) {
4486 }
4487 }
◆ register_eq() [1/2]
Definition at line 4433 of file z3++.h.
4433 {
4434 m_eq_eh = [this](expr const& x, expr const& y) {
4436 };
4437 if (s) {
4439 }
4440 }
void Z3_API Z3_solver_propagate_eq(Z3_context c, Z3_solver s, Z3_eq_eh eq_eh)
register a callback on expression equalities.
◆ register_eq() [2/2]
void register_eq |
( |
eq_eh_t & | f | ) |
|
|
inline |
Definition at line 4426 of file z3++.h.
4426 {
4427 m_eq_eh = f;
4428 if (s) {
4430 }
4431 }
◆ register_final() [1/2]
Definition at line 4457 of file z3++.h.
4457 {
4458 m_final_eh = [this]() {
4459 final();
4460 };
4461 if (s) {
4463 }
4464 }
void Z3_API Z3_solver_propagate_final(Z3_context c, Z3_solver s, Z3_final_eh final_eh)
register a callback on final check. This provides freedom to the propagator to delay actions or imple...
◆ register_final() [2/2]
void register_final |
( |
final_eh_t & | f | ) |
|
|
inline |
register a callback on final-check. During the final check stage, all propagations have been processed. This is an opportunity for the user-propagator to delay some analysis that could be expensive to perform incrementally. It is also an opportunity for the propagator to implement branch and bound optimization.
Definition at line 4450 of file z3++.h.
4450 {
4451 m_final_eh = f;
4452 if (s) {
4454 }
4455 }
◆ register_fixed() [1/2]
Definition at line 4417 of file z3++.h.
4417 {
4418 m_fixed_eh = [this](expr const &id, expr const &e) {
4419 fixed(id, e);
4420 };
4421 if (s) {
4423 }
4424 }
void Z3_API Z3_solver_propagate_fixed(Z3_context c, Z3_solver s, Z3_fixed_eh fixed_eh)
register a callback for when an expression is bound to a fixed value. The supported expression types ...
◆ register_fixed() [2/2]
void register_fixed |
( |
fixed_eh_t & | f | ) |
|
|
inline |
register callbacks. Callbacks can only be registered with user_propagators that were created using a solver.
Definition at line 4410 of file z3++.h.
4410 {
4411 m_fixed_eh = f;
4412 if (s) {
4414 }
4415 }