Z3 |

Data Structures | Public Member Functions
user_propagator_base Class Referenceabstract

`#include <z3++.h>`

## Public Member Functions
| user_propagator_base (solver *s)
| user_propagator_base (Z3_context c)
virtual void | push ()=0
virtual void | pop (unsigned num_scopes)=0
virtual user_propagator_base * | fresh (Z3_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 | fixed (fixed_eh_t &f)
| register callbacks. Callbacks can only be registered with user_propagators that were created using a solver. More...
void | eq (eq_eh_t &f)
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...
unsigned | add (expr const &e)
| tracks `e` by a unique identifier that is returned by the call. More...
void | conflict (unsigned num_fixed, unsigned const *fixed)
void | propagate (unsigned num_fixed, unsigned const *fixed, expr const &conseq)
void | propagate (unsigned num_fixed, unsigned const *fixed, unsigned num_eqs, unsigned const *lhs, unsigned const *rhs, expr const &conseq)

## Detailed Description

Definition at line 3806 of file z3++.h.

## Constructor & Destructor Documentation

## ◆ user_propagator_base() [1/2]

user_propagator_base | ( | solver * | s | ) |
| inline

Definition at line 3865 of file z3++.h.

3865: s(s), c(nullptr) {}

## ◆ user_propagator_base() [2/2]

user_propagator_base | ( | Z3_context | c | ) |
| inline

Definition at line 3866 of file z3++.h.

3866: s(nullptr), c(c) {}

## Member Function Documentation

## ◆ add()

unsigned 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 3927 of file z3++.h.

3927 {
3928 assert(s);
3929 return Z3_solver_propagate_register(ctx(), *s, e);
3930 }
Z3_solver_propagate_register
unsigned 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...

Referenced by Solver::__iadd__(), Fixedpoint::__iadd__(), and Optimize::__iadd__().

## ◆ conflict()

void conflict | ( | unsigned | num_fixed,
|  | unsigned const * | fixed
| ) |  |
| inline

Definition at line 3932 of file z3++.h.

3932 {
3933 assert(cb);
3934 scoped_context _ctx(ctx());
3935 expr conseq = _ctx().bool_val(false);
3936 Z3_solver_propagate_consequence(ctx(), cb, num_fixed, fixed, 0, nullptr, nullptr, conseq);
3937 }
z3::user_propagator_base::fixed
void fixed(fixed_eh_t &f)
register callbacks. Callbacks can only be registered with user_propagators that were created using a ...
Definition: z3++.h:3887
Z3_solver_propagate_consequence
void Z3_API Z3_solver_propagate_consequence(Z3_context c, Z3_solver_callback, unsigned num_fixed, unsigned const *fixed_ids, unsigned num_eqs, unsigned const *eq_lhs, unsigned const *eq_rhs, Z3_ast conseq)
propagate a consequence based on fixed values. This is a callback a client may invoke during the fixe...

## ◆ eq()

void eq | ( | eq_eh_t & | f | ) |
| inline

Definition at line 3893 of file z3++.h.

3893 {
3894 assert(s);
3895 m_eq_eh = f;
3896 Z3_solver_propagate_eq(ctx(), *s, eq_eh);
3897 }
Z3_solver_propagate_eq
void Z3_API Z3_solver_propagate_eq(Z3_context c, Z3_solver s, Z3_eq_eh eq_eh)
register a callback on expression equalities.

Referenced by AstRef::__eq__(), UserPropagateBase::add_eq(), SortRef::cast(), and BoolSortRef::cast().

## ◆ fixed()

void 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 3887 of file z3++.h.

3887 {
3888 assert(s);
3889 m_fixed_eh = f;
3890 Z3_solver_propagate_fixed(ctx(), *s, fixed_eh);
3891 }
Z3_solver_propagate_fixed
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 ...

Referenced by UserPropagateBase::add_fixed(), user_propagator_base::conflict(), and user_propagator_base::propagate().

## ◆ fresh()

virtual user_propagator_base * fresh | ( | Z3_context | ctx | ) |
| 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.

## ◆ pop()

virtual void pop | ( | unsigned | num_scopes | ) |
| pure virtual

## ◆ propagate() [1/2]

void propagate | ( | unsigned | num_fixed,
|  | unsigned const * | fixed,
|  | expr const & | conseq
| ) |  |
| inline

Definition at line 3939 of file z3++.h.

3939 {
3940 assert(cb);
3941 assert(conseq.ctx() == ctx());
3942 Z3_solver_propagate_consequence(ctx(), cb, num_fixed, fixed, 0, nullptr, nullptr, conseq);
3943 }

Referenced by UserPropagateBase::conflict().

## ◆ propagate() [2/2]

void propagate | ( | unsigned | num_fixed,
|  | unsigned const * | fixed,
|  | unsigned | num_eqs,
|  | unsigned const * | lhs,
|  | unsigned const * | rhs,
|  | expr const & | conseq
| ) |  |
| inline

Definition at line 3945 of file z3++.h.

3947 {
3948 assert(cb);
3949 assert(conseq.ctx() == ctx());
3950 Z3_solver_propagate_consequence(ctx(), cb, num_fixed, fixed, num_eqs, lhs, rhs, conseq);
3951 }

Referenced by UserPropagateBase::conflict().

## ◆ push()

virtual void push | ( |  | ) |
| pure virtual

## ◆ register_final()

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 3907 of file z3++.h.

3907 {
3908 assert(s);
3909 m_final_eh = f;
3910 Z3_solver_propagate_final(ctx(), *s, final_eh);
3911 }
Z3_solver_propagate_final
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...