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

Constructor & Destructor Documentation

◆ user_propagator_base() [1/2]

user_propagator_base ( context c)
inline

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

4148 : s(nullptr), c(&c) {}

◆ user_propagator_base() [2/2]

user_propagator_base ( solver s)
inline

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

4150  : s(s), c(nullptr) {
4151  Z3_solver_propagate_init(ctx(), *s, this, push_eh, pop_eh, fresh_eh);
4152  }

◆ ~user_propagator_base()

virtual ~user_propagator_base ( )
inlinevirtual

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

4157  {
4158  for (auto& subcontext : subcontexts) {
4159  subcontext->detach(); // detach first; the subcontexts will be freed internally!
4160  delete subcontext;
4161  }
4162  }

Member Function Documentation

◆ add()

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

4301  {
4302  if (cb)
4304  else if (s)
4306  else
4307  assert(false);
4308  }

◆ conflict()

void conflict ( expr_vector const &  fixed)
inline

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

4310  {
4311  assert(cb);
4312  expr conseq = ctx().bool_val(false);
4313  array<Z3_ast> _fixed(fixed);
4314  Z3_solver_propagate_consequence(ctx(), cb, fixed.size(), _fixed.ptr(), 0, nullptr, nullptr, conseq);
4315  }

◆ created()

virtual void created ( expr const &  )
inlinevirtual

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

4278 {}

Referenced by user_propagator_base::register_created().

◆ ctx()

context& ctx ( )
inline

◆ decide()

virtual void decide ( expr ,
unsigned &  ,
Z3_lbool  
)
inlinevirtual

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

4280 {}

Referenced by user_propagator_base::register_decide().

◆ eq()

virtual void eq ( expr const &  ,
expr const &   
)
inlinevirtual

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

4274 { }

Referenced by user_propagator_base::register_eq().

◆ final()

virtual void final ( )
inlinevirtual

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

4276 { }

◆ fixed()

virtual void fixed ( expr const &  ,
expr const &   
)
inlinevirtual

◆ fresh()

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.

◆ next_split()

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

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

4282  {
4283  assert(cb);
4284  Z3_solver_next_split(ctx(), cb, e, idx, phase);
4285  }

◆ pop()

virtual void pop ( unsigned  num_scopes)
pure virtual

◆ propagate() [1/2]

void propagate ( expr_vector const &  fixed,
expr const &  conseq 
)
inline

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

4317  {
4318  assert(cb);
4319  assert((Z3_context)conseq.ctx() == (Z3_context)ctx());
4320  array<Z3_ast> _fixed(fixed);
4321  Z3_solver_propagate_consequence(ctx(), cb, _fixed.size(), _fixed.ptr(), 0, nullptr, nullptr, conseq);
4322  }

◆ propagate() [2/2]

void propagate ( expr_vector const &  fixed,
expr_vector const &  lhs,
expr_vector const &  rhs,
expr const &  conseq 
)
inline

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

4326  {
4327  assert(cb);
4328  assert((Z3_context)conseq.ctx() == (Z3_context)ctx());
4329  assert(lhs.size() == rhs.size());
4330  array<Z3_ast> _fixed(fixed);
4331  array<Z3_ast> _lhs(lhs);
4332  array<Z3_ast> _rhs(rhs);
4333 
4334  Z3_solver_propagate_consequence(ctx(), cb, _fixed.size(), _fixed.ptr(), lhs.size(), _lhs.ptr(), _rhs.ptr(), conseq);
4335  }

◆ push()

virtual void push ( )
pure virtual

◆ register_created() [1/2]

void register_created ( )
inline

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

4247  {
4248  m_created_eh = [this](expr const& e) {
4249  created(e);
4250  };
4251  if (s) {
4252  Z3_solver_propagate_created(ctx(), *s, created_eh);
4253  }
4254  }

◆ register_created() [2/2]

void register_created ( created_eh_t &  c)
inline

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

4240  {
4241  m_created_eh = c;
4242  if (s) {
4243  Z3_solver_propagate_created(ctx(), *s, created_eh);
4244  }
4245  }

◆ register_decide() [1/2]

void register_decide ( )
inline

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

4263  {
4264  m_decide_eh = [this](expr& val, unsigned& bit, Z3_lbool& is_pos) {
4265  decide(val, bit, is_pos);
4266  };
4267  if (s) {
4268  Z3_solver_propagate_decide(ctx(), *s, decide_eh);
4269  }
4270  }

◆ register_decide() [2/2]

void register_decide ( decide_eh_t &  c)
inline

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

4256  {
4257  m_decide_eh = c;
4258  if (s) {
4259  Z3_solver_propagate_decide(ctx(), *s, decide_eh);
4260  }
4261  }

◆ register_eq() [1/2]

void register_eq ( )
inline

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

4207  {
4208  m_eq_eh = [this](expr const& x, expr const& y) {
4209  eq(x, y);
4210  };
4211  if (s) {
4212  Z3_solver_propagate_eq(ctx(), *s, eq_eh);
4213  }
4214  }

◆ register_eq() [2/2]

void register_eq ( eq_eh_t &  f)
inline

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

4200  {
4201  m_eq_eh = f;
4202  if (s) {
4203  Z3_solver_propagate_eq(ctx(), *s, eq_eh);
4204  }
4205  }

◆ register_final() [1/2]

void register_final ( )
inline

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

4231  {
4232  m_final_eh = [this]() {
4233  final();
4234  };
4235  if (s) {
4236  Z3_solver_propagate_final(ctx(), *s, final_eh);
4237  }
4238  }

◆ register_final() [2/2]

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

4224  {
4225  m_final_eh = f;
4226  if (s) {
4227  Z3_solver_propagate_final(ctx(), *s, final_eh);
4228  }
4229  }

◆ register_fixed() [1/2]

void register_fixed ( )
inline

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

4191  {
4192  m_fixed_eh = [this](expr const &id, expr const &e) {
4193  fixed(id, e);
4194  };
4195  if (s) {
4196  Z3_solver_propagate_fixed(ctx(), *s, fixed_eh);
4197  }
4198  }

◆ register_fixed() [2/2]

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

4184  {
4185  m_fixed_eh = f;
4186  if (s) {
4187  Z3_solver_propagate_fixed(ctx(), *s, fixed_eh);
4188  }
4189  }
Z3_solver_propagate_created
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...
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::user_propagator_base::ctx
context & ctx()
Definition: z3++.h:4164
z3::user_propagator_base::eq
virtual void eq(expr const &, expr const &)
Definition: z3++.h:4274
Z3_solver_propagate_init
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.
Z3_solver_propagate_register_cb
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...
z3::context::bool_val
expr bool_val(bool b)
Definition: z3++.h:3601
Microsoft.Z3.Z3_context
System.IntPtr Z3_context
Definition: Context.cs:29
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_lbool
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:59
z3::user_propagator_base::fixed
virtual void fixed(expr const &, expr const &)
Definition: z3++.h:4272
Z3_solver_propagate_decide
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...
Z3_solver_propagate_register
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...
Z3_solver_propagate_consequence
void Z3_API Z3_solver_propagate_consequence(Z3_context c, Z3_solver_callback, 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...
z3::user_propagator_base::decide
virtual void decide(expr &, unsigned &, Z3_lbool &)
Definition: z3++.h:4280
z3::user_propagator_base::created
virtual void created(expr const &)
Definition: z3++.h:4278
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::object::ctx
context & ctx() const
Definition: z3++.h:451
Z3_solver_next_split
void Z3_API Z3_solver_next_split(Z3_context c, Z3_solver_callback cb, Z3_ast t, unsigned idx, Z3_lbool phase)