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

Constructor & Destructor Documentation

◆ user_propagator_base() [1/2]

user_propagator_base ( context c)
inline

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

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

◆ user_propagator_base() [2/2]

user_propagator_base ( solver s)
inline

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

4209  : s(s), c(nullptr) {
4210  Z3_solver_propagate_init(ctx(), *s, this, push_eh, pop_eh, fresh_eh);
4211  }
context & ctx()
Definition: z3++.h:4223
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 ( )
inlinevirtual

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

4216  {
4217  for (auto& subcontext : subcontexts) {
4218  subcontext->detach(); // detach first; the subcontexts will be freed internally!
4219  delete subcontext;
4220  }
4221  }

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

4360  {
4361  if (cb)
4363  else if (s)
4365  else
4366  assert(false);
4367  }
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...

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

◆ conflict() [1/2]

void conflict ( expr_vector const &  fixed)
inline

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

4369  {
4370  assert(cb);
4371  expr conseq = ctx().bool_val(false);
4372  array<Z3_ast> _fixed(fixed);
4373  Z3_solver_propagate_consequence(ctx(), cb, fixed.size(), _fixed.ptr(), 0, nullptr, nullptr, conseq);
4374  }
expr bool_val(bool b)
Definition: z3++.h:3625
virtual void fixed(expr const &, expr const &)
Definition: z3++.h:4331
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...

◆ conflict() [2/2]

void conflict ( expr_vector const &  fixed,
expr_vector const &  lhs,
expr_vector const &  rhs 
)
inline

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

4376  {
4377  assert(cb);
4378  assert(lhs.size() == rhs.size());
4379  expr conseq = ctx().bool_val(false);
4380  array<Z3_ast> _fixed(fixed);
4381  array<Z3_ast> _lhs(lhs);
4382  array<Z3_ast> _rhs(rhs);
4383  Z3_solver_propagate_consequence(ctx(), cb, fixed.size(), _fixed.ptr(), lhs.size(), _lhs.ptr(), _rhs.ptr(), conseq);
4384  }

◆ created()

virtual void created ( expr const &  )
inlinevirtual

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

4337 {}

Referenced by UserPropagateBase::add_created(), and user_propagator_base::register_created().

◆ ctx()

context& ctx ( )
inline

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

4223  {
4224  return c ? *c : s->ctx();
4225  }
context & ctx() const
Definition: z3++.h:463

Referenced by ArithRef::__add__(), BitVecRef::__add__(), FPRef::__add__(), BitVecRef::__and__(), FuncDeclRef::__call__(), Probe::__call__(), AstMap::__contains__(), AstRef::__copy__(), Goal::__copy__(), AstVector::__copy__(), FuncInterp::__copy__(), ModelRef::__copy__(), Solver::__copy__(), AstRef::__deepcopy__(), Datatype::__deepcopy__(), ParamsRef::__deepcopy__(), ParamDescrsRef::__deepcopy__(), Goal::__deepcopy__(), AstVector::__deepcopy__(), AstMap::__deepcopy__(), FuncEntry::__deepcopy__(), FuncInterp::__deepcopy__(), ModelRef::__deepcopy__(), Statistics::__deepcopy__(), Solver::__deepcopy__(), Fixedpoint::__deepcopy__(), Optimize::__deepcopy__(), ApplyResult::__deepcopy__(), Tactic::__deepcopy__(), Probe::__deepcopy__(), Context::__del__(), AstRef::__del__(), ScopedConstructor::__del__(), ScopedConstructorList::__del__(), ParamsRef::__del__(), ParamDescrsRef::__del__(), Goal::__del__(), AstVector::__del__(), AstMap::__del__(), FuncEntry::__del__(), FuncInterp::__del__(), ModelRef::__del__(), Statistics::__del__(), Solver::__del__(), Fixedpoint::__del__(), Optimize::__del__(), ApplyResult::__del__(), Tactic::__del__(), Probe::__del__(), ParserContext::__del__(), ArithRef::__div__(), BitVecRef::__div__(), FPRef::__div__(), ExprRef::__eq__(), Probe::__eq__(), ArithRef::__ge__(), BitVecRef::__ge__(), Probe::__ge__(), FPRef::__ge__(), SeqRef::__ge__(), AstVector::__getitem__(), SeqRef::__getitem__(), ModelRef::__getitem__(), Statistics::__getitem__(), ApplyResult::__getitem__(), AstMap::__getitem__(), ArithRef::__gt__(), BitVecRef::__gt__(), Probe::__gt__(), FPRef::__gt__(), SeqRef::__gt__(), BitVecRef::__invert__(), ArithRef::__le__(), BitVecRef::__le__(), Probe::__le__(), FPRef::__le__(), SeqRef::__le__(), CharRef::__le__(), AstVector::__len__(), AstMap::__len__(), ModelRef::__len__(), Statistics::__len__(), ApplyResult::__len__(), BitVecRef::__lshift__(), ArithRef::__lt__(), BitVecRef::__lt__(), Probe::__lt__(), FPRef::__lt__(), SeqRef::__lt__(), ArithRef::__mod__(), BitVecRef::__mod__(), BoolRef::__mul__(), ArithRef::__mul__(), BitVecRef::__mul__(), FPRef::__mul__(), ExprRef::__ne__(), Probe::__ne__(), ArithRef::__neg__(), BitVecRef::__neg__(), BitVecRef::__or__(), ArithRef::__pow__(), ArithRef::__radd__(), BitVecRef::__radd__(), FPRef::__radd__(), BitVecRef::__rand__(), ArithRef::__rdiv__(), BitVecRef::__rdiv__(), FPRef::__rdiv__(), ParamsRef::__repr__(), ParamDescrsRef::__repr__(), AstMap::__repr__(), Statistics::__repr__(), BitVecRef::__rlshift__(), ArithRef::__rmod__(), BitVecRef::__rmod__(), ArithRef::__rmul__(), BitVecRef::__rmul__(), FPRef::__rmul__(), BitVecRef::__ror__(), ArithRef::__rpow__(), BitVecRef::__rrshift__(), BitVecRef::__rshift__(), ArithRef::__rsub__(), BitVecRef::__rsub__(), FPRef::__rsub__(), BitVecRef::__rxor__(), AstVector::__setitem__(), AstMap::__setitem__(), ArithRef::__sub__(), BitVecRef::__sub__(), FPRef::__sub__(), BitVecRef::__xor__(), DatatypeSortRef::accessor(), user_propagator_base::add(), Fixedpoint::add_cover(), ParserContext::add_decl(), Fixedpoint::add_rule(), Optimize::add_soft(), ParserContext::add_sort(), Tactic::apply(), AlgebraicNumRef::approx(), ExprRef::arg(), FuncEntry::arg_value(), FuncInterp::arity(), Goal::as_expr(), ApplyResult::as_expr(), FPNumRef::as_string(), Solver::assert_and_track(), Optimize::assert_and_track(), Goal::assert_exprs(), Solver::assert_exprs(), Fixedpoint::assert_exprs(), Optimize::assert_exprs(), Solver::assertions(), Optimize::assertions(), SeqRef::at(), SeqSortRef::basis(), ReSortRef::basis(), QuantifierRef::body(), BoolSortRef::cast(), Solver::check(), Optimize::check(), user_propagator_base::conflict(), UserPropagateBase::conflict(), Solver::consequences(), DatatypeSortRef::constructor(), Goal::convert_model(), AstRef::ctx_ref(), UserPropagateBase::ctx_ref(), ExprRef::decl(), ModelRef::decls(), ArrayRef::default(), RatNumRef::denominator(), Goal::depth(), Goal::dimacs(), Solver::dimacs(), ArraySortRef::domain(), FuncDeclRef::domain(), ArraySortRef::domain_n(), FuncInterp::else_value(), FuncInterp::entry(), AstMap::erase(), ModelRef::eval(), FPNumRef::exponent(), FPNumRef::exponent_as_bv(), FPNumRef::exponent_as_long(), Solver::from_file(), Optimize::from_file(), Solver::from_string(), Optimize::from_string(), ParserContext::from_string(), Goal::get(), Fixedpoint::get_answer(), Fixedpoint::get_assertions(), Fixedpoint::get_cover_delta(), ParamDescrsRef::get_documentation(), Fixedpoint::get_ground_sat_answer(), ModelRef::get_interp(), Statistics::get_key_value(), ParamDescrsRef::get_kind(), ParamDescrsRef::get_name(), Fixedpoint::get_num_levels(), Fixedpoint::get_rule_names_along_trace(), Fixedpoint::get_rules(), Fixedpoint::get_rules_along_trace(), ModelRef::get_sort(), ModelRef::get_universe(), Solver::help(), Fixedpoint::help(), Optimize::help(), Tactic::help(), Solver::import_model_converter(), Goal::inconsistent(), CharRef::is_digit(), FPNumRef::isInf(), FPNumRef::isNaN(), FPNumRef::isNegative(), FPNumRef::isNormal(), FPNumRef::isPositive(), FPNumRef::isSubnormal(), FPNumRef::isZero(), AstMap::keys(), Statistics::keys(), SortRef::kind(), Optimize::maximize(), Optimize::minimize(), Solver::model(), Optimize::model(), SortRef::name(), FuncDeclRef::name(), Solver::next(), user_propagator_base::next_split(), QuantifierRef::no_pattern(), Solver::non_units(), FuncEntry::num_args(), FuncInterp::num_entries(), Solver::num_scopes(), ModelRef::num_sorts(), RatNumRef::numerator(), Optimize::objectives(), Solver::param_descrs(), Fixedpoint::param_descrs(), Optimize::param_descrs(), Tactic::param_descrs(), FuncDeclRef::params(), Fixedpoint::parse_file(), Fixedpoint::parse_string(), QuantifierRef::pattern(), AlgebraicNumRef::poly(), Optimize::pop(), Solver::pop(), Goal::prec(), Solver::proof(), user_propagator_base::propagate(), Solver::push(), Optimize::push(), AstVector::push(), Fixedpoint::query(), Fixedpoint::query_from_lvl(), FuncDeclRef::range(), ArraySortRef::range(), Solver::reason_unknown(), Fixedpoint::reason_unknown(), Optimize::reason_unknown(), DatatypeSortRef::recognizer(), Context::ref(), user_propagator_base::register_created(), user_propagator_base::register_decide(), user_propagator_base::register_eq(), user_propagator_base::register_final(), user_propagator_base::register_fixed(), Fixedpoint::register_relation(), AstMap::reset(), Solver::reset(), AstVector::resize(), Solver::root(), Solver::set(), Fixedpoint::set(), Optimize::set(), ParamsRef::set(), Optimize::set_on_model(), Fixedpoint::set_predicate_representation(), Goal::sexpr(), AstVector::sexpr(), ModelRef::sexpr(), Solver::sexpr(), Fixedpoint::sexpr(), Optimize::sexpr(), ApplyResult::sexpr(), FPNumRef::sign(), FPNumRef::sign_as_bv(), FPNumRef::significand(), FPNumRef::significand_as_bv(), FPNumRef::significand_as_long(), ParamDescrsRef::size(), Goal::size(), Tactic::solver(), ExprRef::sort(), BoolRef::sort(), QuantifierRef::sort(), ArithRef::sort(), BitVecRef::sort(), ArrayRef::sort(), DatatypeRef::sort(), FiniteDomainRef::sort(), FPRef::sort(), SeqRef::sort(), Solver::statistics(), Fixedpoint::statistics(), Optimize::statistics(), CharRef::to_bv(), CharRef::to_int(), Solver::to_smt2(), Fixedpoint::to_string(), Solver::trail(), Solver::trail_levels(), AstVector::translate(), FuncInterp::translate(), AstRef::translate(), Goal::translate(), ModelRef::translate(), Solver::translate(), Solver::units(), Solver::unsat_core(), Optimize::unsat_core(), Fixedpoint::update_rule(), user_propagator_base::user_propagator_base(), ParamsRef::validate(), FuncEntry::value(), QuantifierRef::var_name(), and QuantifierRef::var_sort().

◆ decide()

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

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

4339 {}

Referenced by UserPropagateBase::add_decide(), and user_propagator_base::register_decide().

◆ eq()

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

◆ final()

virtual void final ( )
inlinevirtual

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

4335 { }

Referenced by UserPropagateBase::add_final().

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

4341  {
4342  assert(cb);
4343  Z3_solver_next_split(ctx(), cb, e, idx, phase);
4344  }
void Z3_API Z3_solver_next_split(Z3_context c, Z3_solver_callback cb, Z3_ast t, unsigned idx, Z3_lbool phase)

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

4386  {
4387  assert(cb);
4388  assert((Z3_context)conseq.ctx() == (Z3_context)ctx());
4389  array<Z3_ast> _fixed(fixed);
4390  Z3_solver_propagate_consequence(ctx(), cb, _fixed.size(), _fixed.ptr(), 0, nullptr, nullptr, conseq);
4391  }
System.IntPtr Z3_context
Definition: Context.cs:29

Referenced by UserPropagateBase::conflict().

◆ propagate() [2/2]

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

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

4395  {
4396  assert(cb);
4397  assert((Z3_context)conseq.ctx() == (Z3_context)ctx());
4398  assert(lhs.size() == rhs.size());
4399  array<Z3_ast> _fixed(fixed);
4400  array<Z3_ast> _lhs(lhs);
4401  array<Z3_ast> _rhs(rhs);
4402 
4403  Z3_solver_propagate_consequence(ctx(), cb, _fixed.size(), _fixed.ptr(), lhs.size(), _lhs.ptr(), _rhs.ptr(), conseq);
4404  }

Referenced by UserPropagateBase::conflict().

◆ push()

virtual void push ( )
pure virtual

◆ register_created() [1/2]

void register_created ( )
inline

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

4306  {
4307  m_created_eh = [this](expr const& e) {
4308  created(e);
4309  };
4310  if (s) {
4311  Z3_solver_propagate_created(ctx(), *s, created_eh);
4312  }
4313  }
virtual void created(expr const &)
Definition: z3++.h:4337
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 4299 of file z3++.h.

4299  {
4300  m_created_eh = c;
4301  if (s) {
4302  Z3_solver_propagate_created(ctx(), *s, created_eh);
4303  }
4304  }

◆ register_decide() [1/2]

void register_decide ( )
inline

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

4322  {
4323  m_decide_eh = [this](expr& val, unsigned& bit, Z3_lbool& is_pos) {
4324  decide(val, bit, is_pos);
4325  };
4326  if (s) {
4327  Z3_solver_propagate_decide(ctx(), *s, decide_eh);
4328  }
4329  }
virtual void decide(expr &, unsigned &, Z3_lbool &)
Definition: z3++.h:4339
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...

◆ register_decide() [2/2]

void register_decide ( decide_eh_t &  c)
inline

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

4315  {
4316  m_decide_eh = c;
4317  if (s) {
4318  Z3_solver_propagate_decide(ctx(), *s, decide_eh);
4319  }
4320  }

◆ register_eq() [1/2]

void register_eq ( )
inline

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

4266  {
4267  m_eq_eh = [this](expr const& x, expr const& y) {
4268  eq(x, y);
4269  };
4270  if (s) {
4271  Z3_solver_propagate_eq(ctx(), *s, eq_eh);
4272  }
4273  }
virtual void eq(expr const &, expr const &)
Definition: z3++.h:4333
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 4259 of file z3++.h.

4259  {
4260  m_eq_eh = f;
4261  if (s) {
4262  Z3_solver_propagate_eq(ctx(), *s, eq_eh);
4263  }
4264  }

◆ register_final() [1/2]

void register_final ( )
inline

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

4290  {
4291  m_final_eh = [this]() {
4292  final();
4293  };
4294  if (s) {
4295  Z3_solver_propagate_final(ctx(), *s, final_eh);
4296  }
4297  }
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 4283 of file z3++.h.

4283  {
4284  m_final_eh = f;
4285  if (s) {
4286  Z3_solver_propagate_final(ctx(), *s, final_eh);
4287  }
4288  }

◆ register_fixed() [1/2]

void register_fixed ( )
inline

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

4250  {
4251  m_fixed_eh = [this](expr const &id, expr const &e) {
4252  fixed(id, e);
4253  };
4254  if (s) {
4255  Z3_solver_propagate_fixed(ctx(), *s, fixed_eh);
4256  }
4257  }
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 4243 of file z3++.h.

4243  {
4244  m_fixed_eh = f;
4245  if (s) {
4246  Z3_solver_propagate_fixed(ctx(), *s, fixed_eh);
4247  }
4248  }