Z3
Data Structures | Public Member Functions
user_propagator_base Class Referenceabstract

Public Member Functions

 user_propagator_base (Z3_context c)
 
 user_propagator_base (solver *s)
 
virtual void push ()=0
 
virtual void pop (unsigned num_scopes)=0
 
virtual ~user_propagator_base ()=default
 
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 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 ()
 
virtual void fixed (unsigned, expr const &)
 
virtual void eq (unsigned, unsigned)
 
virtual void final ()
 
virtual void created (unsigned, expr const &)
 
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 3891 of file z3++.h.

Constructor & Destructor Documentation

◆ user_propagator_base() [1/2]

user_propagator_base ( Z3_context  c)
inline

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

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

◆ user_propagator_base() [2/2]

user_propagator_base ( solver s)
inline

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

3962  : s(s), c(nullptr) {
3963  Z3_solver_propagate_init(ctx(), *s, this, push_eh, pop_eh, fresh_eh);
3964  }
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.

◆ ~user_propagator_base()

virtual ~user_propagator_base ( )
virtualdefault

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

4072  {
4073  if (cb)
4074  return Z3_solver_propagate_register_cb(ctx(), cb, e);
4075  if (s)
4076  return Z3_solver_propagate_register(ctx(), *s, e);
4077  assert(false);
4078  return 0;
4079  }
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...
unsigned 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...

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

◆ conflict()

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

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

4081  {
4082  assert(cb);
4083  scoped_context _ctx(ctx());
4084  expr conseq = _ctx().bool_val(false);
4085  Z3_solver_propagate_consequence(ctx(), cb, num_fixed, fixed, 0, nullptr, nullptr, conseq);
4086  }
virtual void fixed(unsigned, expr const &)
Definition: z3++.h:4050
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...

◆ created()

virtual void created ( unsigned  ,
expr const &   
)
inlinevirtual

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

4056 {}

Referenced by user_propagator_base::register_created().

◆ eq()

virtual void eq ( unsigned  ,
unsigned   
)
inlinevirtual

◆ final()

virtual void final ( )
inlinevirtual

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

4054 { }

Referenced by UserPropagateBase::add_final().

◆ fixed()

virtual void fixed ( unsigned  ,
expr const &   
)
inlinevirtual

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

4088  {
4089  assert(cb);
4090  assert(conseq.ctx() == ctx());
4091  Z3_solver_propagate_consequence(ctx(), cb, num_fixed, fixed, 0, nullptr, nullptr, conseq);
4092  }

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

4096  {
4097  assert(cb);
4098  assert(conseq.ctx() == ctx());
4099  Z3_solver_propagate_consequence(ctx(), cb, num_fixed, fixed, num_eqs, lhs, rhs, conseq);
4100  }

Referenced by UserPropagateBase::conflict().

◆ push()

virtual void push ( )
pure virtual

◆ register_created() [1/2]

void register_created ( )
inline

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

4043  {
4044  m_created_eh = [this](unsigned id, expr const& e) {
4045  created(id, e);
4046  };
4047  Z3_solver_propagate_created(ctx(), *s, created_eh);
4048  }
virtual void created(unsigned, expr const &)
Definition: z3++.h:4056
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...

◆ register_created() [2/2]

void register_created ( created_eh_t &  c)
inline

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

4037  {
4038  assert(s);
4039  m_created_eh = c;
4040  Z3_solver_propagate_created(ctx(), *s, created_eh);
4041  }

◆ register_eq() [1/2]

void register_eq ( )
inline

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

4007  {
4008  assert(s);
4009  m_eq_eh = [this](unsigned x, unsigned y) {
4010  eq(x, y);
4011  };
4012  Z3_solver_propagate_eq(ctx(), *s, eq_eh);
4013  }
virtual void eq(unsigned, unsigned)
Definition: z3++.h:4052
void Z3_API Z3_solver_propagate_eq(Z3_context c, Z3_solver s, Z3_eq_eh eq_eh)
register a callback on expression equalities.

◆ register_eq() [2/2]

void register_eq ( eq_eh_t &  f)
inline

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

4001  {
4002  assert(s);
4003  m_eq_eh = f;
4004  Z3_solver_propagate_eq(ctx(), *s, eq_eh);
4005  }

◆ register_final() [1/2]

void register_final ( )
inline

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

4029  {
4030  assert(s);
4031  m_final_eh = [this]() {
4032  final();
4033  };
4034  Z3_solver_propagate_final(ctx(), *s, final_eh);
4035  }
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...

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

4023  {
4024  assert(s);
4025  m_final_eh = f;
4026  Z3_solver_propagate_final(ctx(), *s, final_eh);
4027  }

◆ register_fixed() [1/2]

void register_fixed ( )
inline

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

3993  {
3994  assert(s);
3995  m_fixed_eh = [this](unsigned id, expr const& e) {
3996  fixed(id, e);
3997  };
3998  Z3_solver_propagate_fixed(ctx(), *s, fixed_eh);
3999  }
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 ...

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

3987  {
3988  assert(s);
3989  m_fixed_eh = f;
3990  Z3_solver_propagate_fixed(ctx(), *s, fixed_eh);
3991  }