Z3
Data Structures | Public Member Functions
user_propagator_base Class Referenceabstract

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_basefresh (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 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 3599 of file z3++.h.

Constructor & Destructor Documentation

◆ user_propagator_base() [1/2]

user_propagator_base ( solver s)
inline

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

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

◆ user_propagator_base() [2/2]

user_propagator_base ( Z3_context  c)
inline

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

3659 : 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 3720 of file z3++.h.

3720  {
3721  assert(s);
3722  return Z3_solver_propagate_register(ctx(), *s, e);
3723  }

◆ conflict()

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

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

3725  {
3726  assert(cb);
3727  scoped_context _ctx(ctx());
3728  expr conseq = _ctx().bool_val(false);
3729  Z3_solver_propagate_consequence(ctx(), cb, num_fixed, fixed, 0, nullptr, nullptr, conseq);
3730  }

◆ eq()

void eq ( eq_eh_t &  f)
inline

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

3686  {
3687  assert(s);
3688  m_eq_eh = f;
3689  Z3_solver_propagate_eq(ctx(), *s, eq_eh);
3690  }

◆ final()

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

3700  {
3701  assert(s);
3702  m_final_eh = f;
3703  Z3_solver_propagate_final(ctx(), *s, final_eh);
3704  }

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

3680  {
3681  assert(s);
3682  m_fixed_eh = f;
3683  Z3_solver_propagate_fixed(ctx(), *s, fixed_eh);
3684  }

Referenced by 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 3732 of file z3++.h.

3732  {
3733  assert(cb);
3734  assert(conseq.ctx() == ctx());
3735  Z3_solver_propagate_consequence(ctx(), cb, num_fixed, fixed, 0, nullptr, nullptr, conseq);
3736  }

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

3740  {
3741  assert(cb);
3742  assert(conseq.ctx() == ctx());
3743  Z3_solver_propagate_consequence(ctx(), cb, num_fixed, fixed, num_eqs, lhs, rhs, conseq);
3744  }

◆ push()

virtual void push ( )
pure virtual
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.
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...
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...
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...
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 ...
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:3680