Public Member Functions | |
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. More... | |
void | register_fixed (fixed_eh_t &f) |
register callbacks. Callbacks can only be registered with user_propagators that were created using a solver. More... | |
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. More... | |
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. More... | |
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) |
|
inline |
|
inline |
|
inlinevirtual |
|
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 4476 of file z3++.h.
|
inline |
Definition at line 4485 of file z3++.h.
|
inline |
Definition at line 4492 of file z3++.h.
|
inlinevirtual |
Definition at line 4453 of file z3++.h.
Referenced by user_propagator_base::register_created().
|
inline |
Definition at line 4339 of file z3++.h.
Referenced by user_propagator_base::add(), user_propagator_base::conflict(), user_propagator_base::next_split(), user_propagator_base::propagate(), user_propagator_base::register_created(), user_propagator_base::register_decide(), user_propagator_base::register_eq(), user_propagator_base::register_final(), user_propagator_base::register_fixed(), and user_propagator_base::user_propagator_base().
|
inlinevirtual |
Definition at line 4455 of file z3++.h.
Referenced by user_propagator_base::register_decide().
Definition at line 4447 of file z3++.h.
Referenced by user_propagator_base::register_fixed().
|
pure virtual |
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.
|
pure virtual |
|
inline |
Definition at line 4502 of file z3++.h.
|
inline |
Definition at line 4509 of file z3++.h.
|
pure virtual |
|
inline |
|
inline |
|
inline |
|
inline |
Definition at line 4438 of file z3++.h.
|
inline |
|
inline |
|
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 4399 of file z3++.h.
|
inline |
|
inline |
register callbacks. Callbacks can only be registered with user_propagators that were created using a solver.
Definition at line 4359 of file z3++.h.
|
inline |
Definition at line 4366 of file z3++.h.