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 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)
 

Detailed Description

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

Constructor & Destructor Documentation

user_propagator_base ( context c)
inline

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

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

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

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

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

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

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

4476  {
4477  if (cb)
4479  else if (s)
4481  else
4482  assert(false);
4483  }
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:4339
void conflict ( expr_vector const &  fixed)
inline

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

4485  {
4486  assert(cb);
4487  expr conseq = ctx().bool_val(false);
4488  array<Z3_ast> _fixed(fixed);
4489  Z3_solver_propagate_consequence(ctx(), cb, fixed.size(), _fixed.ptr(), 0, nullptr, nullptr, conseq);
4490  }
context & ctx()
Definition: z3++.h:4339
expr bool_val(bool b)
Definition: z3++.h:3740
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 propa...
virtual void fixed(expr const &, expr const &)
Definition: z3++.h:4447
void conflict ( expr_vector const &  fixed,
expr_vector const &  lhs,
expr_vector const &  rhs 
)
inline

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

4492  {
4493  assert(cb);
4494  assert(lhs.size() == rhs.size());
4495  expr conseq = ctx().bool_val(false);
4496  array<Z3_ast> _fixed(fixed);
4497  array<Z3_ast> _lhs(lhs);
4498  array<Z3_ast> _rhs(rhs);
4499  Z3_solver_propagate_consequence(ctx(), cb, fixed.size(), _fixed.ptr(), lhs.size(), _lhs.ptr(), _rhs.ptr(), conseq);
4500  }
context & ctx()
Definition: z3++.h:4339
expr bool_val(bool b)
Definition: z3++.h:3740
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 propa...
virtual void fixed(expr const &, expr const &)
Definition: z3++.h:4447
virtual void created ( expr const &  )
inlinevirtual

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

Referenced by user_propagator_base::register_created().

4453 {}
context& ctx ( )
inline
virtual void decide ( expr const &  ,
unsigned  ,
bool   
)
inlinevirtual

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

Referenced by user_propagator_base::register_decide().

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

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

Referenced by user_propagator_base::register_eq().

4449 { }
virtual void final ( )
inlinevirtual

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

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

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

Referenced by user_propagator_base::register_fixed().

4447 { }
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.

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

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

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

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

4502  {
4503  assert(cb);
4504  assert((Z3_context)conseq.ctx() == (Z3_context)ctx());
4505  array<Z3_ast> _fixed(fixed);
4506  return Z3_solver_propagate_consequence(ctx(), cb, _fixed.size(), _fixed.ptr(), 0, nullptr, nullptr, conseq);
4507  }
context & ctx()
Definition: z3++.h:4339
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 propa...
virtual void fixed(expr const &, expr const &)
Definition: z3++.h:4447
bool propagate ( expr_vector const &  fixed,
expr_vector const &  lhs,
expr_vector const &  rhs,
expr const &  conseq 
)
inline

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

4511  {
4512  assert(cb);
4513  assert((Z3_context)conseq.ctx() == (Z3_context)ctx());
4514  assert(lhs.size() == rhs.size());
4515  array<Z3_ast> _fixed(fixed);
4516  array<Z3_ast> _lhs(lhs);
4517  array<Z3_ast> _rhs(rhs);
4518 
4519  return Z3_solver_propagate_consequence(ctx(), cb, _fixed.size(), _fixed.ptr(), lhs.size(), _lhs.ptr(), _rhs.ptr(), conseq);
4520  }
context & ctx()
Definition: z3++.h:4339
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 propa...
virtual void fixed(expr const &, expr const &)
Definition: z3++.h:4447
virtual void push ( )
pure virtual
void register_created ( created_eh_t &  c)
inline

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

4415  {
4416  m_created_eh = c;
4417  if (s) {
4418  Z3_solver_propagate_created(ctx(), *s, created_eh);
4419  }
4420  }
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:4339
void register_created ( )
inline

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

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

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

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

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

4438  {
4439  m_decide_eh = [this](expr val, unsigned bit, bool is_pos) {
4440  decide(val, bit, is_pos);
4441  };
4442  if (s) {
4443  Z3_solver_propagate_decide(ctx(), *s, decide_eh);
4444  }
4445  }
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...
virtual void decide(expr const &, unsigned, bool)
Definition: z3++.h:4455
context & ctx()
Definition: z3++.h:4339
void register_eq ( eq_eh_t &  f)
inline

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

4375  {
4376  m_eq_eh = f;
4377  if (s) {
4378  Z3_solver_propagate_eq(ctx(), *s, eq_eh);
4379  }
4380  }
context & ctx()
Definition: z3++.h:4339
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 4382 of file z3++.h.

4382  {
4383  m_eq_eh = [this](expr const& x, expr const& y) {
4384  eq(x, y);
4385  };
4386  if (s) {
4387  Z3_solver_propagate_eq(ctx(), *s, eq_eh);
4388  }
4389  }
virtual void eq(expr const &, expr const &)
Definition: z3++.h:4449
context & ctx()
Definition: z3++.h:4339
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 4399 of file z3++.h.

4399  {
4400  m_final_eh = f;
4401  if (s) {
4402  Z3_solver_propagate_final(ctx(), *s, final_eh);
4403  }
4404  }
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:4339
void register_final ( )
inline

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

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

4359  {
4360  m_fixed_eh = f;
4361  if (s) {
4362  Z3_solver_propagate_fixed(ctx(), *s, fixed_eh);
4363  }
4364  }
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:4339
void register_fixed ( )
inline

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

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