Z3
Data Structures | Public Member Functions
user_propagator_base Class Referenceabstract

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 ()
 
contextctx ()
 
virtual user_propagator_basefresh (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 &, unsigned &, Z3_lbool &)
 
void 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)
 
void propagate (expr_vector const &fixed, expr const &conseq)
 
void propagate (expr_vector const &fixed, expr_vector const &lhs, expr_vector const &rhs, expr const &conseq)
 

Detailed Description

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

Constructor & Destructor Documentation

user_propagator_base ( context c)
inline

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

4322 : s(nullptr), c(&c) {}
user_propagator_base ( solver s)
inline

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

4324  : s(s), c(nullptr) {
4325  Z3_solver_propagate_init(ctx(), *s, this, push_eh, pop_eh, fresh_eh);
4326  }
context & ctx()
Definition: z3++.h:4338
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-properator with the solver.
virtual ~user_propagator_base ( )
inlinevirtual

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

4331  {
4332  for (auto& subcontext : subcontexts) {
4333  subcontext->detach(); // detach first; the subcontexts will be freed internally!
4334  delete subcontext;
4335  }
4336  }

Member Function Documentation

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

4475  {
4476  if (cb)
4478  else if (s)
4480  else
4481  assert(false);
4482  }
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...
context & ctx()
Definition: z3++.h:4338
void conflict ( expr_vector const &  fixed)
inline

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

4484  {
4485  assert(cb);
4486  expr conseq = ctx().bool_val(false);
4487  array<Z3_ast> _fixed(fixed);
4488  Z3_solver_propagate_consequence(ctx(), cb, fixed.size(), _fixed.ptr(), 0, nullptr, nullptr, conseq);
4489  }
void 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. This is a callback a client may invoke during the fixe...
context & ctx()
Definition: z3++.h:4338
expr bool_val(bool b)
Definition: z3++.h:3740
virtual void fixed(expr const &, expr const &)
Definition: z3++.h:4446
void conflict ( expr_vector const &  fixed,
expr_vector const &  lhs,
expr_vector const &  rhs 
)
inline

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

4491  {
4492  assert(cb);
4493  assert(lhs.size() == rhs.size());
4494  expr conseq = ctx().bool_val(false);
4495  array<Z3_ast> _fixed(fixed);
4496  array<Z3_ast> _lhs(lhs);
4497  array<Z3_ast> _rhs(rhs);
4498  Z3_solver_propagate_consequence(ctx(), cb, fixed.size(), _fixed.ptr(), lhs.size(), _lhs.ptr(), _rhs.ptr(), conseq);
4499  }
void 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. This is a callback a client may invoke during the fixe...
context & ctx()
Definition: z3++.h:4338
expr bool_val(bool b)
Definition: z3++.h:3740
virtual void fixed(expr const &, expr const &)
Definition: z3++.h:4446
virtual void created ( expr const &  )
inlinevirtual

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

Referenced by user_propagator_base::register_created().

4452 {}
context& ctx ( )
inline
virtual void decide ( expr ,
unsigned &  ,
Z3_lbool  
)
inlinevirtual

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

Referenced by user_propagator_base::register_decide().

4454 {}
virtual void eq ( expr const &  ,
expr const &   
)
inlinevirtual

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

Referenced by user_propagator_base::register_eq().

4448 { }
virtual void final ( )
inlinevirtual

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

4450 { }
virtual void fixed ( expr const &  ,
expr const &   
)
inlinevirtual

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

Referenced by user_propagator_base::register_fixed().

4446 { }
virtual user_propagator_base* fresh ( 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.

void next_split ( expr const &  e,
unsigned  idx,
Z3_lbool  phase 
)
inline

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

4456  {
4457  assert(cb);
4458  Z3_solver_next_split(ctx(), cb, e, idx, phase);
4459  }
void Z3_API Z3_solver_next_split(Z3_context c, Z3_solver_callback cb, Z3_ast t, unsigned idx, Z3_lbool phase)
context & ctx()
Definition: z3++.h:4338
virtual void pop ( unsigned  num_scopes)
pure virtual
void propagate ( expr_vector const &  fixed,
expr const &  conseq 
)
inline

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

4501  {
4502  assert(cb);
4503  assert((Z3_context)conseq.ctx() == (Z3_context)ctx());
4504  array<Z3_ast> _fixed(fixed);
4505  Z3_solver_propagate_consequence(ctx(), cb, _fixed.size(), _fixed.ptr(), 0, nullptr, nullptr, conseq);
4506  }
void 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. This is a callback a client may invoke during the fixe...
context & ctx()
Definition: z3++.h:4338
virtual void fixed(expr const &, expr const &)
Definition: z3++.h:4446
void propagate ( expr_vector const &  fixed,
expr_vector const &  lhs,
expr_vector const &  rhs,
expr const &  conseq 
)
inline

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

4510  {
4511  assert(cb);
4512  assert((Z3_context)conseq.ctx() == (Z3_context)ctx());
4513  assert(lhs.size() == rhs.size());
4514  array<Z3_ast> _fixed(fixed);
4515  array<Z3_ast> _lhs(lhs);
4516  array<Z3_ast> _rhs(rhs);
4517 
4518  Z3_solver_propagate_consequence(ctx(), cb, _fixed.size(), _fixed.ptr(), lhs.size(), _lhs.ptr(), _rhs.ptr(), conseq);
4519  }
void 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. This is a callback a client may invoke during the fixe...
context & ctx()
Definition: z3++.h:4338
virtual void fixed(expr const &, expr const &)
Definition: z3++.h:4446
virtual void push ( )
pure virtual
void register_created ( created_eh_t &  c)
inline

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

4414  {
4415  m_created_eh = c;
4416  if (s) {
4417  Z3_solver_propagate_created(ctx(), *s, created_eh);
4418  }
4419  }
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...
context & ctx()
Definition: z3++.h:4338
void register_created ( )
inline

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

4421  {
4422  m_created_eh = [this](expr const& e) {
4423  created(e);
4424  };
4425  if (s) {
4426  Z3_solver_propagate_created(ctx(), *s, created_eh);
4427  }
4428  }
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...
virtual void created(expr const &)
Definition: z3++.h:4452
context & ctx()
Definition: z3++.h:4338
void register_decide ( decide_eh_t &  c)
inline

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

4430  {
4431  m_decide_eh = c;
4432  if (s) {
4433  Z3_solver_propagate_decide(ctx(), *s, decide_eh);
4434  }
4435  }
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 set...
context & ctx()
Definition: z3++.h:4338
void register_decide ( )
inline

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

4437  {
4438  m_decide_eh = [this](expr& val, unsigned& bit, Z3_lbool& is_pos) {
4439  decide(val, bit, is_pos);
4440  };
4441  if (s) {
4442  Z3_solver_propagate_decide(ctx(), *s, decide_eh);
4443  }
4444  }
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:60
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 set...
virtual void decide(expr &, unsigned &, Z3_lbool &)
Definition: z3++.h:4454
context & ctx()
Definition: z3++.h:4338
void register_eq ( eq_eh_t &  f)
inline

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

4374  {
4375  m_eq_eh = f;
4376  if (s) {
4377  Z3_solver_propagate_eq(ctx(), *s, eq_eh);
4378  }
4379  }
context & ctx()
Definition: z3++.h:4338
void Z3_API Z3_solver_propagate_eq(Z3_context c, Z3_solver s, Z3_eq_eh eq_eh)
register a callback on expression equalities.
void register_eq ( )
inline

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

4381  {
4382  m_eq_eh = [this](expr const& x, expr const& y) {
4383  eq(x, y);
4384  };
4385  if (s) {
4386  Z3_solver_propagate_eq(ctx(), *s, eq_eh);
4387  }
4388  }
virtual void eq(expr const &, expr const &)
Definition: z3++.h:4448
context & ctx()
Definition: z3++.h:4338
void Z3_API Z3_solver_propagate_eq(Z3_context c, Z3_solver s, Z3_eq_eh eq_eh)
register a callback on expression equalities.
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 4398 of file z3++.h.

4398  {
4399  m_final_eh = f;
4400  if (s) {
4401  Z3_solver_propagate_final(ctx(), *s, final_eh);
4402  }
4403  }
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...
context & ctx()
Definition: z3++.h:4338
void register_final ( )
inline

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

4405  {
4406  m_final_eh = [this]() {
4407  final();
4408  };
4409  if (s) {
4410  Z3_solver_propagate_final(ctx(), *s, final_eh);
4411  }
4412  }
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...
context & ctx()
Definition: z3++.h:4338
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 4358 of file z3++.h.

4358  {
4359  m_fixed_eh = f;
4360  if (s) {
4361  Z3_solver_propagate_fixed(ctx(), *s, fixed_eh);
4362  }
4363  }
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 ...
context & ctx()
Definition: z3++.h:4338
void register_fixed ( )
inline

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

4365  {
4366  m_fixed_eh = [this](expr const &id, expr const &e) {
4367  fixed(id, e);
4368  };
4369  if (s) {
4370  Z3_solver_propagate_fixed(ctx(), *s, fixed_eh);
4371  }
4372  }
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 ...
context & ctx()
Definition: z3++.h:4338
virtual void fixed(expr const &, expr const &)
Definition: z3++.h:4446