Z3
 
Loading...
Searching...
No Matches
Public Member Functions
user_propagator_base Class Referenceabstract

#include <z3++.h>

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.
 
void register_fixed (fixed_eh_t &f)
 register callbacks. Callbacks can only be registered with user_propagators that were created using a solver.
 
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.
 
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.
 
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() [1/2]

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

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

◆ user_propagator_base() [2/2]

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

◆ ~user_propagator_base()

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

◆ 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 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...

Referenced by Solver::__iadd__().

◆ conflict() [1/2]

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 }
expr bool_val(bool b)
Definition z3++.h:3740
virtual void fixed(expr const &, expr const &)
Definition z3++.h:4447
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. 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 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 }

◆ created()

virtual void created ( expr const & )
inlinevirtual

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

4453{}

Referenced by user_propagator_base::register_created().

◆ ctx()

context & ctx ( )
inline

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

4339 {
4340 return c ? *c : s->ctx();
4341 }
context & ctx() const
Definition z3++.h:473

Referenced by ArithRef::__add__(), BitVecRef::__add__(), BitVecRef::__and__(), FuncDeclRef::__call__(), AstMap::__contains__(), AstRef::__copy__(), Goal::__copy__(), AstVector::__copy__(), FuncInterp::__copy__(), ModelRef::__copy__(), AstRef::__deepcopy__(), Datatype::__deepcopy__(), ParamsRef::__deepcopy__(), ParamDescrsRef::__deepcopy__(), Goal::__deepcopy__(), AstVector::__deepcopy__(), AstMap::__deepcopy__(), FuncEntry::__deepcopy__(), FuncInterp::__deepcopy__(), ModelRef::__deepcopy__(), Statistics::__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__(), ArithRef::__div__(), BitVecRef::__div__(), ExprRef::__eq__(), ArithRef::__ge__(), BitVecRef::__ge__(), AstVector::__getitem__(), ModelRef::__getitem__(), Statistics::__getitem__(), AstMap::__getitem__(), ArithRef::__gt__(), BitVecRef::__gt__(), BitVecRef::__invert__(), ArithRef::__le__(), BitVecRef::__le__(), AstVector::__len__(), AstMap::__len__(), ModelRef::__len__(), Statistics::__len__(), BitVecRef::__lshift__(), ArithRef::__lt__(), BitVecRef::__lt__(), ArithRef::__mod__(), BitVecRef::__mod__(), BoolRef::__mul__(), ArithRef::__mul__(), BitVecRef::__mul__(), ExprRef::__ne__(), ArithRef::__neg__(), BitVecRef::__neg__(), BitVecRef::__or__(), ArithRef::__pow__(), ArithRef::__radd__(), BitVecRef::__radd__(), BitVecRef::__rand__(), ArithRef::__rdiv__(), BitVecRef::__rdiv__(), ParamsRef::__repr__(), ParamDescrsRef::__repr__(), AstMap::__repr__(), Statistics::__repr__(), BitVecRef::__rlshift__(), ArithRef::__rmod__(), BitVecRef::__rmod__(), ArithRef::__rmul__(), BitVecRef::__rmul__(), BitVecRef::__ror__(), ArithRef::__rpow__(), BitVecRef::__rrshift__(), BitVecRef::__rshift__(), ArithRef::__rsub__(), BitVecRef::__rsub__(), BitVecRef::__rxor__(), AstVector::__setitem__(), AstMap::__setitem__(), ArithRef::__sub__(), BitVecRef::__sub__(), BitVecRef::__xor__(), DatatypeSortRef::accessor(), user_propagator_base::add(), ExprRef::arg(), FuncEntry::arg_value(), FuncInterp::arity(), Goal::as_expr(), Solver::assert_and_track(), Goal::assert_exprs(), Solver::assert_exprs(), QuantifierRef::body(), Solver::check(), user_propagator_base::conflict(), user_propagator_base::conflict(), Goal::convert_model(), AstRef::ctx_ref(), ExprRef::decl(), ModelRef::decls(), ArrayRef::default(), RatNumRef::denominator(), Goal::depth(), Goal::dimacs(), FuncDeclRef::domain(), ArraySortRef::domain_n(), FuncInterp::else_value(), FuncInterp::entry(), AstMap::erase(), ModelRef::eval(), Goal::get(), ParamDescrsRef::get_documentation(), ModelRef::get_interp(), Statistics::get_key_value(), ParamDescrsRef::get_kind(), ParamDescrsRef::get_name(), ModelRef::get_sort(), ModelRef::get_universe(), Goal::inconsistent(), AstMap::keys(), Statistics::keys(), Solver::model(), SortRef::name(), user_propagator_base::next_split(), QuantifierRef::no_pattern(), FuncEntry::num_args(), FuncInterp::num_entries(), Solver::num_scopes(), ModelRef::num_sorts(), FuncDeclRef::params(), QuantifierRef::pattern(), AlgebraicNumRef::poly(), Solver::pop(), Goal::prec(), user_propagator_base::propagate(), user_propagator_base::propagate(), Solver::push(), AstVector::push(), QuantifierRef::qid(), FuncDeclRef::range(), ArraySortRef::range(), DatatypeSortRef::recognizer(), Context::ref(), user_propagator_base::register_created(), user_propagator_base::register_created(), user_propagator_base::register_decide(), user_propagator_base::register_decide(), user_propagator_base::register_eq(), user_propagator_base::register_eq(), user_propagator_base::register_final(), user_propagator_base::register_final(), user_propagator_base::register_fixed(), user_propagator_base::register_fixed(), AstMap::reset(), Solver::reset(), AstVector::resize(), Solver::set(), ParamsRef::set(), Goal::sexpr(), AstVector::sexpr(), ModelRef::sexpr(), ParamDescrsRef::size(), Goal::size(), QuantifierRef::skolem_id(), AstVector::translate(), AstRef::translate(), Goal::translate(), ModelRef::translate(), user_propagator_base::user_propagator_base(), ParamsRef::validate(), FuncEntry::value(), QuantifierRef::var_name(), and QuantifierRef::var_sort().

◆ decide()

virtual void decide ( expr const & ,
unsigned ,
bool  )
inlinevirtual

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

4455{}

Referenced by user_propagator_base::register_decide().

◆ eq()

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

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

4449{ }

Referenced by AstRef::__eq__(), SortRef::cast(), and user_propagator_base::register_eq().

◆ final()

virtual void final ( )
inlinevirtual

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

4451{ }

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

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 }
bool 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

Referenced by Solver::__exit__().

◆ propagate() [1/2]

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 }

◆ propagate() [2/2]

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 }

◆ push()

virtual void push ( )
pure virtual

Referenced by Solver::__enter__().

◆ register_created() [1/2]

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 }
virtual void created(expr const &)
Definition z3++.h:4453
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 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 }

◆ register_decide() [1/2]

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 }
virtual void decide(expr const &, unsigned, bool)
Definition z3++.h:4455
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...

◆ register_decide() [2/2]

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 }

◆ register_eq() [1/2]

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

◆ register_final() [1/2]

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

◆ 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 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 }

◆ register_fixed() [1/2]

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

◆ 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 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 }